[More Detail] [Collapse All]
Feature: Example walk trough


An example configration with success and failure scenarios.

Configuration include

- swager 2.0 definition
   - operation '/customer(post)'
   - definition 'Customer'
- resolver
   - id_domain, name_domain, default_domain
- extension:
  - interface-implementation: customer(post) --> customer_post (macro)
  - step-extension: env. calls /customer(post) with all input combinations
- implementation
   - state-variable: customers
   - correctness invariant: Customers_ValidDomain
   - macro: customer_db_entry ( to update state variable 'customer')

Two scenarios:
- correct implementation (Customers_ValidDomain not violated)
- incorrect implementation (Customers_ValidDomain violated)
features/003-example/010-example-walktrough.feature
- Background: Create configuration
link

- Create sbuilder directories 'cnf', 'src', 'gen', 'cache'
- Create application extension points 'src/interfaces', 'src/interface' etc.
- Define sewagger interface with '/customer(post)' and definition 'Customer'
- Define resolver to map domains for '/customer(post)' and definition 'Customer'
- Define setup 'example'
  -- implement interface '/customer(post)' --> customer_post
  -- steps to call '/customer(post)'
- Implementation
  -- state variable 'customers'      
  -- correctness: Customers_ValidDomain
  -- interface: {{>customer_post.code }} --> see scenarios
  -- transaction: {{>customer_db_enter.code }}--> macro customer_db_entry

  - Use `sbuilder document setups` to output 'INVARIANT' and 'SETUP'
    configuration
features/003-example/010-example-walktrough.feature:27
When I successfully run `sbuilder.rb init`
And I successfully run `sbuilder.rb extend`
Then the following files should exist:
Application extension templates
src/assumption
src/correctness
src/possibility
src/infrastructure
src/interface
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: Sbuilder.rb example walk-trough
 description: A example walk-trough using swagger-2.0 specification
host: localhost
basePath: /api
schemes:
 - http
consumes:
 - application/json
produces:
 - application/json
paths: {}
definitions: {}
And YAML configuration file `cnf/example_interface.yaml` in path `paths`

# Interface operation /customer(post) in swagger configuration

  /customer:
    post: 
      operationId: postCustomer
      parameters:
        - name: customer
          in: body
          description: Customers to enter
          required: true
          schema:
              $ref: '#/definitions/Customer'
      responses:
         200:
            description: OK
And YAML configuration file `cnf/example_interface.yaml` in path `definitions`

# Defition 'Customer' in swagger YAML


 Customer:
         properties:
           id:
            type: string
           type:
            type: string
           name:
            type: string
And YAML configuration file `cnf/sbuilder.yaml`
#
# Define domain resolvers in 'cnf/sbuilder.yaml'
#
resolvers:
      - url: cnf/resolver_customer.yaml
Given a file named "cnf/resolver_customer.yaml" with:
# resolver which catch-all matcher to match all 
# parameter sets, espcially operation /customer(post).
#
# Resolver rules match domain for parameters 'id', and 'name', and
# catch-all rule matching parameter 'type' in operation
# '/customer(post)'.

   -    Name: default-relsover
        Matcher: !ruby/regexp /.*/
        Rules: 
          - Matcher: id
            Domain: id_domain
          - Matcher: name
            Domain: name_domain
          - Matcher: !ruby/regexp /.*/
            Domain: default_domain
And YAML configuration file `cnf/sbuilder.yaml`
#
# setup extensions:
# - for interface implementation
# - steps to execute
#
setups:
  - setupDirectory: example
    desc: Example setup
    extensions:
      -  url: cnf/extend-steps.yaml
      -  url: cnf/extend-implementation.yaml
And a file named "cnf/extend-implementation.yaml" with:
#
# interface-extension: define implemehtation for interface
# operation '/customer(post)'

- interface-extension:
   - matcher: /customer(post)
     implementation: customer_post
And a file named "cnf/extend-steps.yaml" with:

# Define steps, which environment will take. In this case,
# environment call interface '/customer(post)', and because no
# input constaint is defined, environment uses all input
# combination for 'id', 'name', and 'type' parameters in the
# operation.
#
- step-extension:
       - interface: /customer(post)
# ------------------------------------------------------------------
# Speication code snippets in specification code repository 'src'
And I append to "src/state" with:
       (* Initialize state variable 'customer' to empty set *)

       customers = {}; 
And I append to "src/correctness" with:
(* Define correctness operator to verify that all entries in state
   variable 'customers' have a correct type. In this case require the
   type to be 't_Customer'.

 *)
Customers_ValidDomain == \A entry \in customers: entry  \in t_Customer
And YAML configuration file `cnf/sbuilder.yaml`
#
# Define resolver in file example_resolver.yaml

invariants:
      - Customers_ValidDomain: Customer entries have correct type
And I append to "src/interface" with:
  {{>customer_post.code }}
And I append to "src/transaction" with:
  {{>customer_db_enter.code }}
And a file named "src/customer_db_enter.code" with:
  (* This macro is called for interface /customer(post)  *)
   macro customer_db_entry( input ) {
       customers :=  customers \union {input};
   }
When I successfully run `sbuilder.rb document setups`
Then the stdout should contain:
INVARIANTS:
- Customers_ValidDomain: Customer entries have correct type
And the stdout should contain:
SETUPS:
- example: Example setup
    - possibilities: 
    - assumptions: 
    - interfaces: /customer(post)
- Scenario: Correct implementation, correctness invariant not violated
link

Correct implementation  extracts customer field from input.

Step 'I can observe operation ...' looks for output message
"<<"Default process p__customer_post_ for operation
'/customer(post)',tick=", 0>>" standard output.
features/003-example/010-example-walktrough.feature:261
And a file named "src/customer_post.code" with:
  (* This macro is called for interface /customer(post)  *)
   macro customer_post( input ) {
       print << "/customer(post) called!!!" >>;
       customer_db_entry( input.customer );
   }
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 run command `java -cp $TLATOOLS tlc2.TLC setup`
And the stdout should contain "Model checking completed. No error has been found."
And I can observe operation `/customer(post)` called on time tick `0`
Then the stdout should contain "/customer(post) called!!!"
- Scenario: Incorrect implementation, correctness violation detected
link

An error in implementation does correctly access customer field in
input causing incorrect value to entered into 'customer' state
variable, and a violation of invariant 'Customers_ValidDomain'
features/003-example/010-example-walktrough.feature:287
And a file named "src/customer_post.code" with:
  (* This macro is called for interface /customer(post)  *)
   macro customer_post( input ) {
       print << "/customer(post) called!!!" >>;
       \* customer_db_entry( input.customer );
       \* ERROR fail to extract customer value from input
       customer_db_entry( input );
   }
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 run command `java -cp $TLATOOLS tlc2.TLC setup`
Then the stdout should contain "Invariant Customers_ValidDomain is violated."