[More Detail] [Collapse All]
Feature: Application templates for interface extension

Running 'sbuilder.rb extend' creates empty application extension
templates in 'src' directory. 

Add partial calls to specification extension into application
extension templates to include own code into the specification code.
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:12
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: Implement interface extension as a macro in 'src/interface'
link

Service implementation in macro 'customer_post' print hello-word
message.

Implementation

- add a mustache partial call into 'src/interface' 
- implemement macro in 'interface_customer_post.tla'
features/020-extend-interface/020-application-extensions.feature:137
Given a file named "src/interface" should exist
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 ) {
       print << "Greets from Customer Post!!!" >>;
   }
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!!!"
- Scenario: Implement interface extension as procedure in 'src/service'
link


Service implementation in macro 'customer_post' calls procedure
's_customer_post', which output debug message.

Implementation

- 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:169
Given a file named "src/interface" should exist
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 );
   }
Given a file named "src/service" should exist
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!!!"