[More Detail] [Collapse All]
Feature: Allow TLA+ tool assign input values


TLA+ model checker binds input parameters non-deterministic in
interface operations. Binding may be limited by setting some of the
parameter values to a fixed value.

Following scenarios are demonstated:

- setup1: no parameter bind --> TLA+ exercises three operations, all binding exercised
- setup2: no parameter bind --> TLA+ exercises two operations, all  combinations
- setup3: bind parameter using domain value index
- setup4: bind parameter using domain value (string)
features/040-extend-steps/003-bind-partially-input.feature
- Background: Configure setups
link
features/040-extend-steps/003-bind-partially-input.feature:17
Given I use a fixture named "fixture-resolver"
And YAML configuration file `cnf/sbuilder.yaml`
#
# 'extend-domain' configured below
# 'setup-steps' configures in scenarios 1,2,3,4

setups:
- setupDirectory: setup
  extensions:
      -  url: cnf/extend-domains.yaml
      -  url: cnf/setup-steps.yaml
And a file named "cnf/resolver_customer.yaml" with:
# Common domain resolver: maps interface parameter values
# to domain names
#
-    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/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
- Scenario: setup1: run default implementation for 'setup1' operations
link

Execute three interface operations in three step. Parameter values
not bound, and TLA+ is uses all input combinations in all steps.
features/040-extend-steps/003-bind-partially-input.feature:72
Given a file named "cnf/setup-steps.yaml" with:
# Setup1:
#
- step-extension:
       - interface: /customer(post)
       - interface: /customer(get)
       - interface: /customer(delete)
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 execution trace:
Operation Tick
/customer(post) 0
/customer(get) 1
/customer(delete) 2
And I can observe domain assignement:
Field Domain
id "d_id_domain_1"
id "d_id_domain_2"
id Nil
name "name1"
name "name2"
name Nil
- Scenario: setup2: does not call operations not in 'setup2'
link

Execute two interface operations in two step. Parameter values not
bound, and TLA+ is uses all input combinations in all steps.
features/040-extend-steps/003-bind-partially-input.feature:108
Given a file named "cnf/setup-steps.yaml" with:
# Setup2:
#
- step-extension:
       - interface: /customer(post)
       - interface: /customer(get)
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 execution trace:
Operation Tick
/customer(post) 0
/customer(get) 1
And I can observe domain assignement:
Field Domain
id "d_id_domain_1"
id "d_id_domain_2"
id Nil
name "name1"
name "name2"
name Nil
- Scenario: setup3: bind operation input with domain index
link

Execute two interface operations in two step. In these operations
'customer.id' is set to fixed domain index '2'.
features/040-extend-steps/003-bind-partially-input.feature:141
Given a file named "cnf/setup-steps.yaml" with:
# Setup3:
#
- step-extension:
       - interface: /customer(post)
         input:
            customer: 
                 id: 2
       - interface: /customer(get)
         input:
            id: 2
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 execution trace:
Operation Tick
/customer(post) 0
/customer(get) 1
And the stdout should not contain "d_id_domain_1"
And I can observe domain assignement:
Field Domain
id "d_id_domain_2"
name "name1"
name "name2"
name Nil
- Scenario: setup4: bind operation input with domain value
link

Execute two interface operations in two step. In these operations
'customer.name' is set to fixed domain value 'name1'.
features/040-extend-steps/003-bind-partially-input.feature:180
Given a file named "cnf/setup-steps.yaml" with:
# Setup4:
#
- step-extension:
       - interface: /customer(post)
         input:
            customer: 
                 name: name1
       - interface: /customer(get)
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 execution trace:
Operation Tick
/customer(post) 0
/customer(get) 1
And the stdout should not contain "name2"
And I can observe domain assignement:
Field Domain
id "d_id_domain_1"
id "d_id_domain_2"
id Nil
name "name1"