[More Detail] [Collapse All]
Feature: Init example model

Removing '.example' suffix from configuration files in 'cnf'
-directory enables an example' model, and defines three setups
('default', 'customer1', 'customer2'), which all pass TLA+ model
checking.
features/002-init/use-init-configuration.feature
- Background: Run 'sbuilder.rb init' and rename 'cnf/*.example'
link
features/002-init/use-init-configuration.feature:10
When I successfully run `sbuilder.rb init`
Then the following files should exist:
cnf/extend_customer_run1.yaml.example
cnf/extend_customer_run2.yaml.example
cnf/extend_customer_if.yaml.example
cnf/interface_customer.yaml.example
cnf/resolver_customer.yaml.example
cnf/sbuilder.yaml.example
When I move a file named "cnf/sbuilder.yaml.example" to "cnf/sbuilder.yaml"
And I move a file named "cnf/extend_customer_doms.yaml.example" to "cnf/extend_customer_doms.yaml"
And I move a file named "cnf/extend_customer_if.yaml.example" to "cnf/extend_customer_if.yaml"
And I move a file named "cnf/interface_customer.yaml.example" to "cnf/interface_customer.yaml"
And I move a file named "cnf/extend_customer_run1.yaml.example" to "cnf/extend_customer_run1.yaml"
And I move a file named "cnf/extend_customer_run2.yaml.example" to "cnf/extend_customer_run2.yaml"
And I move a file named "cnf/resolver_customer.yaml.example" to "cnf/resolver_customer.yaml"
- Scenario: List setups in init example
link
features/002-init/use-init-configuration.feature:28
When I successfully run `sbuilder.rb list setups`
Then the stdout should contain "default"
Then the stdout should contain "customer1"
Then the stdout should contain "customer2"
- Scenario: Run 'default' setup in init example configuration
link

Running command `sbuilder.rb generate default` results to an
executable setup.
features/002-init/use-init-configuration.feature:36
When I successfully run `sbuilder.rb generate default`
Given a directory named "gen/default/tla" should exist
And I cd to "gen/default/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 'customer1' setup in init example configuration
link

Running command `sbuilder.rb generate customer1` results to an
executable setup.
features/002-init/use-init-configuration.feature:50
When I successfully run `sbuilder.rb generate customer1`
Given a directory named "gen/customer1/tla" should exist
And I cd to "gen/customer1/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 'customer2' setup in init example configuration
link

Running command `sbuilder.rb generate customer2` results to an
executable setup.
features/002-init/use-init-configuration.feature:65
When I successfully run `sbuilder.rb generate customer2`
Given a directory named "gen/customer2/tla" should exist
And I cd to "gen/customer2/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."