[More Detail] [Collapse All]
Feature: Calling infrastructure service

Infrastructure services allow aggregation of (application) services
from smaller units.

In SBuilder, infrastructure services are modeled as PlusCal
procedures. Infrastructure service interfaces use the same Swagger
2.0 specification language as application services.

To add support for an service to return responses, Sbuilder uses
property `infrastructureServices: true` in sbuilder.yaml.
features/003-example/050-calling-infrastructure-service.feature
- Background:
link

Define interfaces

- (public) application interface: /customer(post)
- (private) infrastructure interface: /id/customer(get)

Define domain resolver

- default-resolver to map parameter 'id' to domain 'id_domain'

Define setup:

- interface-implementation: /customer(post)-> macro customer_post
- extend domains: set cardinality for 'id_domain' to 6
- environment steps: call interface '/customer(post)' with all possible input combinations

Create specification snippets:

- macro 'post_customer', which calls application service implementation 's_post_customer'
  procedure

Procedure 's_post_customer' is implemented in various scnenarios, which present:
- successful calling to infrastrcture service  
- error when calling an unknown infrastrcture service
- error when accessing return value from an unknown infrastrcture service
- error when infrastructure service returns invalid data value
features/003-example/050-calling-infrastructure-service.feature:16
Given I successfully run `sbuilder.rb init`
And I successfully run `sbuilder.rb extend`
And a file named "cnf/sbuilder.yaml" with:
#
# Define public application interface and 
# private infrastrctureu interface

# In this example, we set 'interfaceServices' for interfaces
# loaded from file 'infrastructure_interface.yaml', which
# instructure sbuilder NOT to generate interface processes for
# these services. Default true is used for interfaces in file
# 'public_interface.yaml', which generates interface processes,
# and allows these interfacess to be called externally.


interfaces:
    -  className: Sbuilder::ParamSetLoaderSwagger
       file: public_interface.yaml
    -  className: Sbuilder::ParamSetLoaderSwagger
       infrastructureServices: true
       interfaceServices: false
       file: infrastructure_interface.yaml
And a file named "cnf/public_interface.yaml" with:
swagger: "2.0"
info:
   version: 1.0.0
   title: TLA-sbuilder demo application public interface
host: localhost
basePath: /api
schemes:
    - http
consumes:
    - application/json
produces:
   - application/json
paths:
 /customer:
   post: 
     operationId: postCustomer
     parameters:
       - name: customer
         in: body
         description: Customers to enter
         required: true
         schema:
             $ref: '#/definitions/Customer'
     responses:
        200:
           description: OK
definitions: 
   Customer:
        properties:
          id:
           type: string
          name:
           type: string
And a file named "cnf/infrastructure_interface.yaml" with:
swagger: "2.0"
info:
   version: 1.0.0
   title: TLA-sbuilder demo application infrastructure interface
host: localhost
basePath: /api
schemes:
    - http
consumes:
    - application/json
produces:
   - application/json
paths:
  /id/customer:
     get:
          operationId: findCustomers by id
          responses:
             200:
               description: OK
               schema:
                  $ref: '#/definitions/Id'
definitions:
    Id:
       required:
          - id
       properties:
          id:
             type: string
And YAML configuration file `cnf/sbuilder.yaml`
resolvers:
     - url: cnf/example_resolver.yaml
Given a file named "cnf/example_resolver.yaml" with:
# catch all resolver
-    Name: default-relsover
     Matcher: !ruby/regexp /.*/
     Rules: 
      - Matcher: id
        Domain: id_domain
      - Matcher: !ruby/regexp /.*/
        Domain: default_domain
And YAML configuration file `cnf/sbuilder.yaml`
#
# Setup defined in extension file 
#
setups:
  - setupDirectory: example
    extensions:
      -  url: cnf/setup-extension.yaml
And YAML configuration file `cnf/sbuilder.yaml`
#
# Map service implementation 

snippets:

  - className: Sbuilder::SnippetLoaderSimple 
    snippets:

        # interface /customer(post) calls customer_post
      - metatype: service_implementation
        appName: /customer(post)
        name: customer_post
Given a file named "cnf/setup-extension.yaml" with:
# Define interface implementation

# - interface-extension:
#    - matcher: /customer(post)
#      implementation: customer_post


# Extend domain and set cardinality for id_domain

- domain-extension:
    - domain: id_domain
      cardinality: 6

# Environment defines one step, in which 
# interface '/customer(post)' is called 
# using all possible input combinations

- step-extension:
     - interface: /customer(post)
Given a file named "src/interface" should exist
And I append to "src/interface" with:
macro customer_post( input ) {
    call s_post_customer( input );
}
- Scenario: Example of successfully generating id in infratructure service
link

This scenario

- state variable 'ids', and initialize it with valid id-elements
- operators
   -- to create new-customer record,
   -- to extract new id from free id-values
- infrastructure service 'generateId'
- application service implementation 's_post_customer', which
  -- calls infrastructure service 'generateId'
  -- retrieves generated id returned from infrastructure service 
  --retrieves status from infrastructure service call
features/003-example/050-calling-infrastructure-service.feature:220
Given a file named "src/state" should exist
And I append to "src/state" with:
     (* 
        State variable 'ids' intialized with all elements in 
        set 'd_id_domain', expect Nil -value.

     *)
     ids = d_id_domain \ {Nil}
Given a file named "src/operator" should exist
And I append to "src/operator" with:
(* Define operator to create customer record *)

New_Customer( input, id ) == [ id |-> id, name |-> input.name ]

(* Define operator to return id from state variable 'ids' *)

Next_Customer_Id == CHOOSE x \in ids: TRUE
Given a file named "src/infrastructure" should exist
And I append to "src/infrastructure" with:
procedure generateId() {

  generateId_start:

   \* remove the consume id from the set of ids
   ids :=  ids \ { Next_Customer_Id };

   \* return the generated identifier
   InfrastructureServiceReturn( "/id/customer(get)", "status-200", [ id |-> Next_Customer_Id ] );

   return;
}
Given a file named "src/service" should exist
And I append to "src/service" with:
  procedure s_post_customer( post_pet_input ) {
    post_customer_entry:
        \* synchrnous call to infracstureu service
        call generateId();
    post_customer_generated:
        \* access the generated id
        print << "Generated id:", InfrastructureServiceGetResponse( "/id/customer(get)" ) >>;
        print << "Generate status:", InfrastructureServiceGetStatus( "/id/customer(get)" ) >>;
    return;
  }
When I successfully run `sbuilder.rb generate example`
And I cd to "gen/example/tla"
And I successfully run command `java -cp $TLATOOLS pcal.trans model`
And I successfully run command `java -cp $TLATOOLS tlc2.TLC setup`
Then the stdout should contain "Model checking completed. No error has been found."
Then the stdout should contain "Generated id:"
And the output should match %r<Generate status:[,"\s]*status-200">
- Scenario: Failure when accessing unknow infrastructure service
link

This scenario:

- defines application service implementation 's_post_customer', which
  tries to access return value from a non-existing infrastructure service
features/003-example/050-calling-infrastructure-service.feature:302
Given a file named "src/service" should exist
And I append to "src/service" with:
  procedure s_post_customer( post_pet_input ) {
    post_customer_entry:
        \* access the generated id
        print << "Generated id:", InfrastructureServiceGetResponse( "/id/unkwon_service(get)" ) >>;
        return;
  }
When I generate TLA+ model setup `example`
And I do PLC transformation for setup `example`
And I fail to run TLC for setup `example`
Then the stdout should contain "Unknown infrastructure service"
- Scenario: Failure if setting return value to an unknow reinfrastructure service
link

This scenario:

- infrastructure service sets return value for an unknown infrastructure service
features/003-example/050-calling-infrastructure-service.feature:326
Given a file named "src/infrastructure" should exist
And I append to "src/infrastructure" with:
procedure generateId() {

  generateId_start:

   \* set return generated identifier
   InfrastructureServiceReturn( "/id/wrong_service_name", "status-200", 1 );

   return;
}
Given a file named "src/service" should exist
And I append to "src/service" with:
  procedure s_post_customer( post_pet_input ) {

    post_customer_entry:

        \* access infrastructure service
        call generateId() ;

    post_customer_generateId_return:
        print << "should not get here" >>;
        return;
  }
When I successfully run `sbuilder.rb generate example`
And I cd to "gen/example/tla"
And I successfully run command `java -cp $TLATOOLS pcal.trans model`
And I successfully run command `java -cp $TLATOOLS tlc2.TLC setup`
Then the stdout should contain "Unknown infrastructure service"
And the stdout should not contain "should not get here"
- Scenario: Error when infrastructure service returns invalid data value
link

In this scenario, infrastructure service return a out-of-domain value.
features/003-example/050-calling-infrastructure-service.feature:373
Given a file named "src/infrastructure" should exist
And I append to "src/infrastructure" with:
procedure generateId() {

  generateId_start:

   \* set return generated identifier
   InfrastructureServiceReturn( "/id/customer(get)", "status-200", "invalida-data-value" );

   return;
}
Given a file named "src/service" should exist
And I append to "src/service" with:
  procedure s_post_customer( post_pet_input ) {

    post_customer_entry:

        \* access infrastructure service
        call generateId() ;

    post_customer_generateId_return:
        print << "should not get here" >>;
        return;
  }
When I successfully run `sbuilder.rb generate example`
And I cd to "gen/example/tla"
And I successfully run command `java -cp $TLATOOLS pcal.trans model`
And I successfully run command `java -cp $TLATOOLS tlc2.TLC setup`
Then the stdout should contain "Evaluating invariant InfrastructureService_TypeInvariant failed"
And the stdout should not contain "should not get here"