[More Detail] [Collapse All]
Feature: Verify OK for setup without any extensions

Environment steps are defined as setups, which can be listed using
command 'sbuilder.rb list setups'. Fixture configuration can be
verifiied without specifying any extensions.
          

Create a minimal example configuration includes defining

- empty swager 2.0 interface configuration file
- empty setup

and successfully
- generate model
- run TLA+ pcal translation
- run TLA+ tlc model checking
features/010-setups/020-verify-setup-without-extensions.feature
- Background: Initialize directory structure
link
features/010-setups/020-verify-setup-without-extensions.feature:20
When I successfully run `sbuilder.rb init`
# ------------------------------------------------------------------
# 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
    # extensions:
    #    -  type: default-yaml
    #       url: cnf/extend_example.yaml
- Scenario: Run successfully empty model
link

First list the example setup.

Generate model for setup 'example', run PlusCal transformation,
and TLC model checking in setup directory `gen/example/tla`.
features/010-setups/020-verify-setup-without-extensions.feature:66
When I successfully run `sbuilder.rb list setups`
Then the stdout should contain "example"
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
And I cd to "gen/example/tla"
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."