[More Detail] [Collapse All]
Feature: Check assumptions

TLA+ uses ASSUME statements, which instructs the TLA-tool to check
that operators references in the ASSUME statement is satisfied by
constant parameters in the model.

An example of using assumption is to define correctness on domain
model e.g. to check that types defined as sets are correct.

Define a generaric operator `Assume_CorrectDomain`

Assume_CorrectDomain( set, field, domain ) == { p[field] : p \in  set }  = domain

and use it in to check domains in application types. In the example below,
that field 'streed' in record t_Address has domain 'd_street'

assumption_address ==
                    Assume_CorrectDomain( t_Address, "street", d_street )
                /\  Assume_CorrectDomain( t_Address, "city", d_city )        


In sbuilder, assumptions are activated in configuration file
'sbuilder.yaml' in ''setup property 'assumptions',
               
  setups:
      - setupDirectory: default
        desc: Validate domain model
        assumptions:
          - assumption_address
          - ....
features/003-example/080-check-assumptions.feature
- Background:
link
features/003-example/080-check-assumptions.feature:34
Given I successfully run `sbuilder.rb init`
And I successfully run `sbuilder.rb extend`
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:
#
#  Define application interface /customer(post)
#
swagger: "2.0"
info:
   version: 1.0.0
   title: TLA-sbuilder demo application public interface
host: localhost
basePath: /api
schemes:
    - http
consumes:
     - application/json
produces:
    - application/json
paths:
 /customer:
    post: 
      operationId: postCustomer
      parameters:
        - name: customer
          in: body
          description: Customers to enter
          required: true
          schema:
              $ref: '#/definitions/Address'
      responses:
         200:
            description: OK
definitions: 
    Address:
         properties:
           street:
            type: string
           city:
            type: string
           country:
            type: string
    Very_big_definition:
         properties:
           fld000:
            type: string
           fld001:
            type: string
           fld001:
            type: string
           fld002:
            type: string
           fld003:
            type: string
           fld004:
            type: string
           fld005:
            type: string
           fld006:
            type: string
           fld007:
            type: string
           fld008:
            type: string
           fld009:
            type: string
           fld010:
            type: string
           fld011:
            type: string
           fld011:
            type: string
           fld012:
            type: string
           fld013:
            type: string
           fld014:
            type: string
           fld015:
            type: string
           fld016:
            type: string
           fld017:
            type: string
           fld018:
            type: string
           fld019:
            type: string
And YAML configuration file `cnf/sbuilder.yaml`
#
# Define resolver in file example_resolver.yaml

resolvers:
      - file: example_resolver.yaml
Given a file named "cnf/example_resolver.yaml" with:
#
#
-    Name: default-relsolver
     Matcher: !ruby/regexp /.*/
     Rules: 
        - Matcher: street
          Domain: street
        - Matcher: city
          Domain: city
        - Matcher: !ruby/regexp /.*/
          Domain: default_domain
And I append to "src/assumption" with:
{{! 
 
   Include mustache partial to define operator 'assume_address_domains'
}}
{{>assume_address_domains.tla}}
- Scenario: Correct domain model - assumptions passed
link
features/003-example/080-check-assumptions.feature:167
Given YAML configuration file `cnf/sbuilder.yaml`
setups:
  - setupDirectory: example
    assumptions:
        - assume_address_domains
And a file named "src/assume_address_domains.tla" with:
Assume_CorrectDomain( set, field, domain ) == { p[field] : p \in  set }  = domain

assume_address_domains == 
             Assume_CorrectDomain( t_Address, "street", d_street )
         /\  Assume_CorrectDomain( t_Address, "city", d_city )        
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 successfully run command `java -cp $TLATOOLS tlc2.TLC setup`
Then the stdout should contain "Model checking completed. No error has been found."
- Scenario: Invalid domain model - assumptions failed
link
features/003-example/080-check-assumptions.feature:193
Given YAML configuration file `cnf/sbuilder.yaml`
setups:
  - setupDirectory: example
    assumptions:
        - assume_address_domains
And a file named "src/assume_address_domains.tla" with:
Assume_CorrectDomain( set, field, domain ) == { p[field] : p \in  set }  = domain

assume_address_domains == 
             Assume_CorrectDomain( t_Address, "street", d_street )
         /\  Assume_CorrectDomain( t_Address, "city", d_street )        
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 successfully run command `java -cp $TLATOOLS tlc2.TLC setup`
Then the output should match /Error: Assumption line .* of module setup is false/
- Scenario: Enumerate too large set - TLA-error 'Attempted to construct a set with too many elements'
link

Trying to enumerate too large set in assumptions results to TLA-
tool error 'Attempted to construct a set with too many elements'.

In our exmple, the definition 'Very_big_definition' contains 20
fields, with each field resolved to domain 'd_default_domain'
defined as a set { "d_default_domain_1", Nil }. Size of
t_Very_big_definition is 2^20, and TLA issues a warning.
features/003-example/080-check-assumptions.feature:219
Given YAML configuration file `cnf/sbuilder.yaml`
setups:
  - setupDirectory: example
    assumptions:
        - assume_too_big
And a file named "src/assume_address_domains.tla" with:
Assume_CorrectDomain( set, field, domain ) == { p[field] : p \in  set }  = domain

assume_too_big == 
             Assume_CorrectDomain( t_Very_big_definition, "fld000", d_default_domain )
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 successfully run command `java -cp $TLATOOLS tlc2.TLC setup`
Then the output should contain "Error: Evaluating assumption line"
And the output should contain "Attempted to construct a set with too many elements"
- Scenario: Enumerate too large set - TLA-error 'Attempted to construct a set with too many elements' - fixed
link


To fix 'Attempted to construct a set with too many elements'
error, we remove Nil element from set domain using setup
-configuration

        configuration:
         allow_domain_nil_values: false

In our exmple, the definition 'Very_big_definition' contains 20
fields, with each field resolved to domain 'd_default_domain'
defined as a set { "d_default_domain_1" } with cardinality 1.
This allows us to t_Very_big_definition.  is 1 and TLA issues no.

Notice that domain set encode domain name, and it checking model
assumption is reliable.
features/003-example/080-check-assumptions.feature:254
Given YAML configuration file `cnf/sbuilder.yaml`
setups:
  - setupDirectory: example
    configuration:
         allow_domain_nil_values: false
    assumptions:
        - assume_too_big
And a file named "src/assume_address_domains.tla" with:
Assume_CorrectDomain( set, field, domain ) == { p[field] : p \in  set }  = domain

assume_too_big == 
             Assume_CorrectDomain( t_Very_big_definition, "fld000", d_default_domain )
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 successfully run command `java -cp $TLATOOLS tlc2.TLC setup`
Then the output should not contain "Error"
And the output should not contain "Attempted to construct a set with too many elements"
And the stdout should contain "Model checking completed. No error has been found."