[More Detail] [Collapse All]
Feature: Extend environment steps

Enviroment actions in sbuilder are given in setup extension
'extend-environment' as a sequence of steps. A step defines an
interface operation and its input parameters.

Parameter bindings (=domain values) of interface operation input
parameters are determined by 

* sbuilder when using 'bindExact=true' in setup step

* TLC model checker when using 'bindExact=false' in setup step
features/040-extend-steps/110-extend-environment-array-input.feature
- Background: Configure setups
link

This configuration defines:

- interface operation /customer(post)

- input parameters id,type,name for interface operation /customer(post)

- resolver in 'resolver-example.yaml' to identify domains for the input paramters

- a setup with the name 'setup1' pointing to files 
   -- 'extend-domains.yaml' to configure domain ranges
   -- 'extend-steps.yaml' to define interface operations
       with input parameter binding
features/040-extend-steps/110-extend-environment-array-input.feature:16
Given I successfully run `sbuilder.rb init`
# Configure interfaces
And a file named "cnf/sbuilder.yaml" with:
#
#  
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: Sbuild demo customer
And YAML configuration file `cnf/example_interface.yaml`

# Interface operation /customer(post) in swagger configuration

paths:
  /customers:
    post: 
      operationId: postCustomer
      parameters:
        - name: customer
          in: body
          description: Customers to enter
          required: true
          schema:
              $ref: '#/definitions/Customers'
      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

 Customers:
      type: array
      allOf: 
             - $ref: '#/definitions/Customer'
      # items:
      #    $ref: '#/definitions/Customer'
# ------------------------------------------------------------------
# resolver
Given YAML configuration file `cnf/sbuilder.yaml`
#
# Define domain resolvers in 'cnf/sbuilder.yaml'
#
resolvers:
      - url: cnf/resolver-example.yaml
And a file named "cnf/resolver-example.yaml" with:
# Common domain resolver: maps interface parameter values
# to domain names
#
-    Name: default-resolver
     Matcher: !ruby/regexp /.*/
     Rules: 
          - Matcher: id
            Domain: id_domain
          - Matcher: name
            Domain: name_domain
          - Matcher: type
            Domain: type_domain
          - Matcher: !ruby/regexp /.*/
            Domain: default_domain
And a file named "cnf/extend-domains.yaml" with:
# Extend domains: sets domain cardinality for 'id_domain', 
# set fixed domain values for 'name_domain'
#
- domain-extension:
       - domain: id_domain
         cardinality: 2
       - domain: name_domain
         values:
             - name1
             - name2
# ------------------------------------------------------------------
# Setup
When YAML configuration file `cnf/sbuilder.yaml`
#
# 'extend-domain' configured below
# 'setup-steps' configures in scenarios 1,2,3,4

setups:
- setupDirectory: setup1
  extensions:
      -  url: cnf/extend-domains.yaml
      -  url: cnf/extend-steps.yaml
- Scenario: Sbuilder reports 'Set cardinality too large' for powerset
link

Use 'bindExact: true' to allow sbuilder to generate binding input
set. No domain contraint on any of the customer fields
(rule:refault, domain: all).


In this scenario, /customers(post) -operation receives array of
customer objects. The powerset over all possible customer entries
grows so large that sbuilder reports 'set cardinality too large'
-error.
features/040-extend-steps/110-extend-environment-array-input.feature:164
And a file named "cnf/extend-steps.yaml" with:
# Setup1:
#
- extend-environment:
       - interface: /customers(post)
         bindExact: true
         validators:
            - rule: default
              action: all
When I run `sbuilder.rb generate setup1`
Then it should fail with regex:
Set cardinality '\d+' too large
- Scenario: Sbuilder generates values bind to array input
link

Use 'bindExact: true' to allow sbuilder to generate binding input
set. No domain contraint on any of the customer fields
(rule:refault, domain: all).


In this scenario, /customers(post) -operation receives array of
customer objects. The powerset over all possible customer entries
is limited by constaining some of the input fiel domain.
# When I successfully run `sbuilder.rb generate setup1`
# And I cd to "gen/setup1/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."
features/040-extend-steps/110-extend-environment-array-input.feature:203
And a file named "cnf/extend-steps.yaml" with:
# Setup1:
#
- extend-environment:
       - interface: /customers(post)
         bindExact: true
         validators:
            - rule: path
              rule_value: [customer, id]
              action: domain
              action_value: 1
            - rule: path
              rule_value: [customer, type]
              action: domain
              action_value: 0
            - rule: path
              rule_value: [customer, name]
              action: domain
              action_value: 2
            # - rule: default
            #   action: domain
            #   action_value: 1
            - rule: default
              action: all
# When I run `sbuilder.rb generate setup1`
# Then it should fail with regex:
# """
# Set cardinality '\d+' too large
# """
When I successfully run `sbuilder.rb generate setup1`
And I cd to "gen/setup1/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."