[More Detail] [Collapse All]
Feature: Model operator `InTransaction`


Sbuilder operator `InTransaction` yields TRUE when application
service is running.

This operator is useful, when an application services uses
intermediate steps, which are not-consistent, and system state
should be verified only after the application service has finished.

INVARIANT transaction

transaction == ~InTransaction => SystemStateValid
features/003-example/100-model-operator-in-transaction.feature
- Background:
link
features/003-example/100-model-operator-in-transaction.feature:17
Given I successfully run `sbuilder.rb init`
And I successfully run `sbuilder.rb extend`
And a file named "cnf/sbuilder.yaml" with:
# Setup1:
#
#
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
paths: 
 /transaction:
   post: 
       responses:
           default:
             description: default

definitions: {}
And YAML configuration file `cnf/sbuilder.yaml`
#
# Define only setup 'example' - no extensions.

setups:
  - setupDirectory: example
    desc: Example setup
    extensions: 
        - file: example-extension.yaml
And YAML configuration file `cnf/sbuilder.yaml`
#
# Define domain resolvers in 'cnf/sbuilder.yaml'
#
resolvers:
      - file: resolver-default.yaml
Given a file named "cnf/resolver-default.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: !ruby/regexp /.*/
            Domain: default_domain
And YAML configuration file `cnf/sbuilder.yaml`
#
# Map service implementation 

snippets:

  - className: Sbuilder::SnippetLoaderSimple 
    snippets:

        # interface /transaction(post) calls 'interface_transaction'
      - metatype: service_implementation
        appName: /transaction(post)
        name: interface_transaction
And a file named "cnf/example-extension.yaml" with:
# - interface-extension:
#    - matcher: /transaction(post)
#      implementation: interface_transaction
- step-extension:
       - interface: /transaction(post)
 
And I append to "src/interface" with:
  {{>interface_transaction.code }}
And a file named "src/interface_transaction.code" with:
  (* Procedure being called different in scenarios  *)
   macro interface_transaction( input ) {
       call transaction();
   }
And I append to "src/service" with:
  {{>service_transaction.code }}
And I append to "src/state" with:
  v_State1={};
  v_State2={};
And YAML configuration file `cnf/sbuilder.yaml`
#
# Activate INVARIANT directive in setup.tla

invariants:
      - transaction_consistent: Verify that all entries in customers -state variable are valid
- Scenario: System state modified in a single step - transaction_consistent validated
link

Procedure defines just starting label, and the two variable
assignments are executed in one step. Correctness criteria
'transaction_consistent' is verified.
features/003-example/100-model-operator-in-transaction.feature:138
Given a file named "src/service_transaction.code" with:
procedure transaction() {
   transaction_start:
       v_State1 := { 1 };
       v_State2 := { 1 };
       return;
}
And I append to "src/correctness" with:
transaction_consistent == v_State1 = v_State2
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."
- Scenario: System state modified in a two steps - transaction_consistent violated
link

Procedure defines starting label `transaction_start`, and a label
for an intermediate step `transaction_intermadiate_step`. This
split state assignment to to states, and results to correctness
criteria 'transaction_consistent' violated.
features/003-example/100-model-operator-in-transaction.feature:164
Given a file named "src/service_transaction.code" with:
procedure transaction() {
   transaction_start:
       v_State1 := { 1 };

   transaction_intermadiate_step:
       v_State2 := { 1 };
       return;
}
And I append to "src/correctness" with:
transaction_consistent == v_State1 = v_State2
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 "transaction_consistent is violated."
- Scenario: System state modified in a two steps - transaction_consistent passed when using premise ~InTransaction
link

Procedure defines just starting label, and the two variable
assignments are executed in one step. Correctness criteria
'transaction_consistent' is modified to use premise
`InTransaction`.
features/003-example/100-model-operator-in-transaction.feature:194
Given a file named "src/service_transaction.code" with:
procedure transaction() {
   transaction_start:
       v_State1 := { 1 };

   transaction_intermadiate_step:
       v_State2 := { 1 };
       return;
}
And I append to "src/correctness" with:
transaction_consistent == ~InTransaction => v_State1 = v_State2
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."
- Scenario: System state modified in a two steps, application errro - transaction_consistent faile when using premise ~InTransaction
link

Procedure defines just starting label, and the two variable
assignments are executed in one step. Correctness criteria
'transaction_consistent' is modified to use premise
`InTransaction`.
features/003-example/100-model-operator-in-transaction.feature:223
Given a file named "src/service_transaction.code" with:
procedure transaction() {
   transaction_start:
       v_State1 := { 1 };

   transaction_intermadiate_step:
       v_State2 := { 2 };
       return;
}
And I append to "src/correctness" with:
transaction_consistent == ~InTransaction => v_State1 = v_State2
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 "transaction_consistent is violated."