[More Detail] [Collapse All]
Feature: Avoid state space explosion in interface input

Large domains ranges explode the number possible input combinations.
To avoid the need to iterate through an overly large domain range,
Sbuilder step-extension may define exact binding to interface
operation parameters.

To define exact binding, a step definition must set 'bindExact' to
true. In order to avoid the need to set value separately to every
parameter in interface operation, the binding definition may uses
'_default' pseudo parameter, which gives domain range index to use
for all parameters, which are not specifically listed in the binding
definition.
features/040-extend-steps/004-bindexact-input.feature
- Background: Configure setup extensions
link
features/040-extend-steps/004-bindexact-input.feature:18
Given I use a fixture named "fixture-resolver"
And YAML configuration file `cnf/sbuilder.yaml`
#
# 'setups' section defines a setup 'demo' 

setups:
- setupDirectory: setup
  extensions:
      -  url: cnf/setup-domains.yaml
      -  url: cnf/setup-steps.yaml
And a file named "cnf/resolver_customer.yaml" with:
# Common domain resolver
#
-    Name: default-relsover
     Matcher: !ruby/regexp /.*/
     Rules: 
          - Matcher: id
            Domain: id_domain
          - Matcher: name
            Domain: name_domain
          - Matcher: !ruby/regexp /.*/
            Domain: default_domain
And a file named "cnf/setup-domains.yaml" with:
# Common domain mapper

#
- domain-extension:
       - domain: id_domain
         cardinality: 1000
       - domain: name_domain
         cardinality: 1000
- Scenario: setup1: observe default value for all domains
link

Large domains ranges, in this scenario cardinality of 'id_domain'
is 1000, and cardinality of 'name'_domain is 1000, explode number
possible input combinations. Without 'bindExact' property running
'setup1' would take a very looong time.

However, using bind exact option allows TLA+ limit possible inputs
to 1, and faster model checking time.
features/040-extend-steps/004-bindexact-input.feature:63
Given a file named "cnf/setup-steps.yaml" with:
# Setup1:

# bindExact attribute instructs environment model
# set environment input exactly.
#
- step-extension:
       - interface: /customer(post)
         bindExact: true
         input:
           customer:
               _default: 1
               id: 500
               name: 501
When I generate TLA+ model setup `setup`
And I do PLC transformation for setup `setup`
And I run TLC for setup `setup`
Then the stdout should contain "Model checking completed. No error has been found."
And I can observe operation `/customer(post)` called on time tick `0`
And I can observe domain assignement:
Field Domain
id "d_id_domain_500"
name "d_name_domain_501"
street "d_default_domain_1"
- Scenario: setup2: one step, two 'bindExact' choices
link

Using 'bindExact' set interfaces parameter to fixed values. To allow
non-determinism interface operations, Sbuilder allows giving an array
of 'input' bindings.
features/040-extend-steps/004-bindexact-input.feature:106
Given a file named "cnf/setup-steps.yaml" with:
# Setup2:

# bindExact attribute instructs environment model
# set environment input exactly.
#
- step-extension:
       - interface: /customer(post)
         bindExact: true
         inputs:
           - input:
               customer:
                 _default: 1
                 id: 500
                 name: 501

           - input:
               customer:
                 _default: 1
                 id: 498
                 name: 499
When I generate TLA+ model setup `setup`
And I do PLC transformation for setup `setup`
And I run TLC for setup `setup`
Then the stdout should contain "Model checking completed. No error has been found."
And I can observe operation `/customer(post)` called on time tick `0`
And I can observe domain assignement:
Field Domain
id "d_id_domain_500"
name "d_name_domain_501"
id "d_id_domain_498"
name "d_name_domain_499"
street "d_default_domain_1"