[More Detail] [Collapse All]
Feature: Example app init, generate, TLA+ processing

Pet store example defines setups 'pet1' and 'pet2'

The example uses environment variable '$TLATOOLS' to point to
tla2tools.jar for TLA+.
features/001-example-app/example-run.feature
- Background: Initialize directory strucutre and create pet example
link

Initialize sbuilder directories using command `sbuilder.rb init`,
and create pet store example with command `sbuilder.rb example pet`.

Generate TLA+ model setups 'pet1' and 'pet2'

    `sbuilder.rb generate --templates src/pet/`

Notice: the last backslash in 'src/pet/'
features/001-example-app/example-run.feature:9
When I successfully run `sbuilder.rb init`
When I successfully run `sbuilder.rb example pet`
When I successfully run `sbuilder.rb generate --templates src/pet/`
Then the stderr should not contain anything
Then the directory named "gen/pet1/tla" should exist
And the following files should exist:
TLA+ model files for setup 'pet1'
gen/pet1/tla/model.tla
gen/pet1/tla/setup.cfg
gen/pet1/tla/setup.tla
gen/pet1/doc/data-model.md
Then the directory named "gen/pet2/tla" should exist
And the following files should exist:
TLA+ model files for setup 'pet2'
gen/pet2/tla/model.tla
gen/pet2/tla/setup.cfg
gen/pet2/tla/setup.tla
gen/pet2/doc/data-model.md
- Scenario: List setup in pet example
link

Pet example defines setups 'pet1' and 'pet2'
features/001-example-app/example-run.feature:40
When I successfully run `sbuilder.rb list setups`
And the stdout should contain "pet1 pet2"
- Scenario: Run TLA+ for pet1 setup
link

  Assuming setup directory 'gen/pet1/tla' pet store example setup
  'pet1' exists. I can successfully run TLA+ 

  - PCAL translation 
  - TLC model checking

  for the model.
features/001-example-app/example-run.feature:48
Given a directory named "gen/pet1/tla" should exist
And I cd to "gen/pet1/tla"
And I successfully run command `java -cp $TLATOOLS pcal.trans model`
And the stdout should contain "New file model.tla written."
And I successfully run command `java -cp $TLATOOLS tlc2.TLC setup`
And the stdout should contain "Model checking completed. No error has been found."
- Scenario: Run TLA+ for pet2 setup
link

  Assuming setup directory 'gen/pet2/tla' pet store example setup
  'pet2' exists. I can successfully run TLA+ 

  - PCAL translation 
  - TLC model checking

  for the model.
features/001-example-app/example-run.feature:65
Given a directory named "gen/pet2/tla" should exist
And I cd to "gen/pet2/tla"
And I successfully run command `java -cp $TLATOOLS pcal.trans model`
And the stdout should contain "New file model.tla written."
And I successfully run command `java -cp $TLATOOLS tlc2.TLC setup`
And the stdout should contain "Model checking completed. No error has been found."
- Scenario: Run TLA+ with a failure 'error-duplicate-tag'
link

Example application includes setup 'error-duplicate-tag', which demonstrates
violating invariant definition 'UniqueTag'.

Failure is caused code snippet 'transaction_enter_tag.tla'
contains erronous code hidden behind mustache condition
{{#PREFERENCES.error-duplicate-tag}}


This erroneous code is enabled for setup 'error-duplicate-tag' with
the following preference setting

    - setupDirectory: error-duplicate-tag
      desc: Duplicate tag violation found
      preferences:
           error-duplicate-tag: true

The error is detected by invariant 'UniqueTag' defined in
'setup.cfg'.
features/001-example-app/example-run.feature:83
Given a directory named "gen/error-duplicate-tag/tla" should exist
And the file named "cnf/sbuilder.yaml" should match /error-duplicate-tag:\s*true/
And the file named "gen/error-duplicate-tag/tla/setup.cfg" should match /INVARIANT\s*UniqueTag/
And the file named "src/pet/transaction_enter_tag.tla" should match /\{\{#PREFERENCES.error-duplicate-tag\}\}/
And I cd to "gen/error-duplicate-tag/tla"
And I successfully run command `java -cp $TLATOOLS pcal.trans model`
And the stdout should contain "New file model.tla written."
And I run command `java -cp $TLATOOLS tlc2.TLC setup`
Then the stdout should contain "Invariant UniqueTag is violated."