[More Detail] [Collapse All]
Feature: Define service implementation to interface

Implementing a service for an interface requires 1) a mapping of the
interface to a service name , 2) and loading code for the service
implementation into sbuilder.

Mapping of a service name to an interface is done with
'service_implementation' -metatype entry in 'snippets' section in
'sbuilder.yaml'.

Service implementation may be defined together on the
'service_implementation' entry, loaded sepaterly, e.g. using
mustache template extension point.
features/020-extend-interface/020-application-extensions.feature
- Background:
link

- Configure interface operation '/customer(post)'

- Define a 'default-resolver', which finds domain for parameters
  in '/customer(post)'

- Define a setup, which
    
   -- maps interface operation '/customer(post)' to macro 'customer_post'

   -- environment model, which makes a call to '/customer(post)', and passes
      all parameter combination to the interface
features/020-extend-interface/020-application-extensions.feature:16
Given I successfully run `sbuilder.rb init`
And I successfully run `sbuilder.rb extend`
And the following files should exist:
Application extension templates created
src/assumption
src/correctness
src/infrastructure
src/operator
src/service
src/state
src/transaction
And a file named "cnf/sbuilder.yaml" with:
#
# Define interfaces

interfaces:
    -  className: Sbuilder::ParamSetLoaderSwagger
       file: example_interface.yaml
And a file named "cnf/example_interface.yaml" with:
swagger: "2.0"
info:
   version: 1.0.0
   title: TLA-sbuilder application extension-template demo
host: localhost
basePath: /api
schemes:
    - http
consumes:
    - application/json
produces:
   - application/json
#
# Interface operation /customer(post) 
#

paths:
 /customer:
   post: 
     operationId: postCustomer
     parameters:
       - name: customer
         in: body
         description: Customers to enter
         required: true
         schema:
             $ref: '#/definitions/Customer'
     responses:
        200:
           description: OK
#
# Definition 'Customer'
#

definitions: 
   Customer:
        properties:
          id:
           type: string
          name:
           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: !ruby/regexp /.*/
        Domain: default_domain
And YAML configuration file `cnf/sbuilder.yaml`
setups:
  - setupDirectory: example
    extensions:
      -  url: cnf/example_extension.yaml
Given a file named "cnf/example_extension.yaml" with:
# extend interface '/customer(post)'
# make one call to  '/customer(post)'
# - interface-extension:
#    - matcher: /customer(post)
#      implementation: customer_post
- step-extension:
     - interface: /customer(post)
- Scenario: Load interface implementation together with snippet loader inteface
link

Map interface '/customer(post)' to a name 'customer_post2', and
make sbuilder to load a macro with this name via snippet interface
by giving url pointing to the macro imlementation.

Implementation

- configure 'sbuilder.yaml' section 'snippets'
    -- define 'service_implementation' w. 'url' property
    -- define 'service_completion' w. 'url' property
- implemement macros
    -- 'src/interface_customer_post.tla' correspoding
       'url' in 'service_implementation'
    -- 'src/interface_customer_done.tla' correspoding
       'url' in 'service_completion'
features/020-extend-interface/020-application-extensions.feature:138
Given YAML configuration file `cnf/sbuilder.yaml`
#
# Map service implementation 

snippets:

  - className: Sbuilder::SnippetLoaderSimple 
    snippets:

        # interface /customer(post) calls customer_post2 
        # and load a macro in file 'src/interface_customer_post.tla'
        # implementing 'customer_post2'
      - metatype: service_implementation
        appName: /customer(post)
        name: customer_post2
        url: src/interface_customer_post.tla

      - metatype: service_completion
        appName: /customer(post)
        name: service_completed
        url: src/service_completed.tla
     
And a file named "src/interface_customer_post.tla" with:
   macro customer_post2( input ) {
       print << "Greets from Customer Post!!!" >>;
   }
And a file named "src/service_completed.tla" with:
   macro service_completed( interfaceName ) {
       print << "Finished with service completion",  interfaceName >>;
   }
When I generate TLA+ model setup `example`
And I do PLC transformation for setup `example`
And I run TLC for setup `example`
Then the stdout should contain "Model checking completed. No error has been found."
Then the stdout should contain "Greets from Customer Post!!!"
Then the stdout should contain "Finished with service completion"
- Scenario: Implemetation loaded sepatetely using template extension point
link

Map interface '/customer(post)' to a name 'customer_post', and
load a macroa using sbuilder template extension poinsts
'interface' and 'service'.

Implementation

- configure 'sbuilder.yaml' section 'snippets'
- add a mustache partial call into 'src/interface' 
- implemement macro in 'interface_customer_post.tla'
- add a mustache partial call into 'src/service' 
- implemement procedure in 'service_customer_post.tla'
features/020-extend-interface/020-application-extensions.feature:208
Given 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
And I append to "src/interface" with:
{{>interface_customer_post.tla}}
And a file named "src/interface_customer_post.tla" with:
   macro customer_post( input ) {
       call s_post_customer( input );
   }
And I append to "src/service" with:
{{>service_customer_post.tla}}
And a file named "src/service_customer_post.tla" with:
  procedure s_post_customer( post_pet_input ) {
    post_pet_entry:
       print << "Cheers from Customer Post Service!!!" >>;
    return;
  }
When I generate TLA+ model setup `example`
And I do PLC transformation for setup `example`
And I run TLC for setup `example`
Then the stdout should contain "Model checking completed. No error has been found."
Then the stdout should contain "Cheers from Customer Post Service!!!"