[More Detail] [Collapse All]
Feature: Create minimal (empty) model


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/003-example/001-example-minimal.feature
- Background: Initialize directory structure
link
features/003-example/001-example-minimal.feature:16
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

Generate model for setup 'example', run PlusCal transformation,
and TLC model checking in setup directory `gen/example/tla`.
features/003-example/001-example-minimal.feature:62
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."