[More Detail] [Collapse All]
Feature: Specification snippets in extension points are sorted

Sbuilder sorts specification snippets in a linear order, where
snippets, which are referered to come before to snippets, which make
the reference. Sorting is implemented on all module, i.e. modules
configured statically in extension points, and on modules loaded
dynamically using snippet extension plugins.

Implementation uses Ruby modoule Tsort.
features/100-plugin-extension/100-snippet-sorted.feature
- Background: Create a simple specification model
link

Initialize sbuilder directory structures

Configure Sbuilder model

- empty swager 2.0 interface configuration file
- empty setup
- create state variable 'customer', and initialize with empty set
features/100-plugin-extension/100-snippet-sorted.feature:12
When I successfully run `sbuilder.rb init`
And I successfully run `sbuilder.rb extend`
Then the following files should exist:
Application extension templates
src/assumption
src/correctness
src/possibility
src/infrastructure
src/interface
src/operator
src/service
src/state
src/transaction
# ------------------------------------------------------------------
# Configure  interface
And a file named "cnf/sbuilder.yaml" with:
# Setup1:
#
# Setup1:
# - set cardinality for domain 'dommi'
# - lauch /customer(get)
#
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: {}
definitions: {}
# ------------------------------------------------------------------
# Configure  step
And YAML configuration file `cnf/sbuilder.yaml`
#
# Define only setup 'example' - no extensions.

setups:
  - setupDirectory: example
Given a file named "src/state_customers.tla" with:
\* state variable for customer entries
customers = {}; 
And a file named "src/state" with:
{{>state_customers.tla}}
- Scenario: Define two operator in 'correct' order
link

Use extension point 'src/operator' to include operators
Customer_Valid, and Valid_Customers in 'correct' order.

Ensure that tla/model.tla -file contains operators
Customer_Valid, and Valid_Customers in correct order.

The resulting model can be successfully processed using TLA+
tools.
features/100-plugin-extension/100-snippet-sorted.feature:87
Given a file named "src/operator_customer_valid.tla" with:
\* Check validity of 'customer'
Customer_Valid( customer ) == TRUE
Given a file named "src/operator_customers_valid.tla" with:
\* Return set of valid customers 
Valid_Customers == { c \in customers: Customer_Valid( c ) }
And I append to "src/operator" with:
\* 
{{>operator_customer_valid.tla}}
{{>operator_customers_valid.tla}}
When I successfully run `sbuilder.rb generate example`
And the following files should exist:
TLA+ model files for setup 'example'
gen/example/tla/model.tla
gen/example/tla/setup.cfg
gen/example/tla/setup.tla
When I cd to "gen/example/tla"
Then I run command `sed -n -e '/Customer_Valid/' model.tla | grep Valid_Customers`
And I successfully run command `java -cp $TLATOOLS pcal.trans model`
And the stdout should contain "Translation completed.\nNew file model.tla written."
And I run command `java -cp $TLATOOLS tlc2.TLC setup`
And the stdout should contain "Model checking completed. No error has been found."
- Scenario: Define two operator in 'wrong' order
link

Use extension point 'src/operator' to include operators
Valid_Customers, Customer_Valid, in 'wrong' order.

Ensure that tla/model.tla -file contains operators
Customer_Valid, and Valid_Customers in correct order.

The resulting model can be successfully processed using TLA+
tools.
features/100-plugin-extension/100-snippet-sorted.feature:135
Given a file named "src/operator_customer_valid.tla" with:
\* Check validity of 'customer'
Customer_Valid( customer ) == TRUE
Given a file named "src/operator_customers_valid.tla" with:
\* Return set of valid customers 
Valid_Customers == { c \in customers: Customer_Valid( c ) }
And I append to "src/operator" with:
\* 
{{>operator_customers_valid.tla}}
{{>operator_customer_valid.tla}}
When I successfully run `sbuilder.rb generate example`
And the following files should exist:
TLA+ model files for setup 'example'
gen/example/tla/model.tla
gen/example/tla/setup.cfg
gen/example/tla/setup.tla
When I cd to "gen/example/tla"
Then I run command `sed -n -e '/Customer_Valid/' model.tla | grep Valid_Customers`
And I successfully run command `java -cp $TLATOOLS pcal.trans model`
And the stdout should contain "Translation completed.\nNew file model.tla written."
And I run command `java -cp $TLATOOLS tlc2.TLC setup`
And the stdout should contain "Model checking completed. No error has been found."