[More Detail] [Collapse All]
Feature: Initialize example applications

Sbuilder includes example applications 'Pet store' using
OpenAPI-specification
[Pet store Api](https://github.com/OAI/OpenAPI-Specification/blob/master/examples/v2.0/yaml/petstore-expanded.yaml).

To use the example

- run 'sbuilder.rb init' to create directory structure under current
  working directory

- run 'sbuilder.rb example pet'
features/001-example-app/example-generate.feature
- Background: Initialize directory strucutre and create pet example
link

Run `sbuilder.rb init` to create directory structure for sbuilder,
and `sbuidler.rb example pet` to create configuration files for
pet store example.

Specification source files for 'pet' example are found under
directory 'src/pet', and template extenstion, which include source
files to the generated model are in directory 'src/pet/extend'.
features/001-example-app/example-generate.feature:15
When I successfully run `sbuilder.rb init`
And the following directories should exist:
Tla-sbuilder default directories
cnf
src
gen
When I successfully run `sbuilder.rb example pet`
Then the following files should exist:
Configuration files created
cnf/sbuilder.yaml
cnf/resolver_petstore.yaml
cnf/extend_petstore_doms.yaml
cnf/extend_petstore_run2.yaml
cnf/extend_petstore_run1.yaml
And the following directories should exist:
TLA-sbuilder code repository
src/pet
And the following files should exist:
Application extension templates
src/pet/assumption
src/pet/correctness
src/pet/infrastructure
src/pet/operator
src/pet/service
src/pet/state
src/pet/transaction
And the following files should exist:
Some of specification code modules
src/pet/service_pet_post.tla
src/pet/operator_new_pet.tla
src/pet/transaction_enter_pet.tla
And the following directories should exist:
TLA extension direcrory
src/pet/extend
And the following files should exist:
TLA extension templates
src/pet/extend/extend_assumptions.mustache
src/pet/extend/extend_implementation.mustache
src/pet/extend/extend_invariant_cfg.mustache
src/pet/extend/extend_invariant.mustache
src/pet/extend/extend_macros.mustache
src/pet/extend/extend_operations.mustache
src/pet/extend/extend_state.mustache
- Scenario: Get on-line instructions on using example applications
link

Command `sbuilder.rb example help pet` output help
features/001-example-app/example-generate.feature:75
When I successfully run `sbuilder.rb example help pet`
And the stdout should contain "Create 'Pet Store' TLA+ model"
- Scenario: Generate example setup 'pet1'
link

Specification code for the example is stored in directory
'src/pet', which is NOT the default source repository directory
`src`.

To access the code, we need to pass the directory directory using
'--templates' option.
features/001-example-app/example-generate.feature:84
When I successfully run `sbuilder.rb generate pet1 --templates src/pet/`
And the following directories should exist:
Setup directories created
gen/pet1/tla
gen/pet1/doc
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
- Scenario: Error message if TLA-sbuilder code repository incorrectly specified
link

Pet example cannot find specification snippets from default
location, and error 'No such template' is raised.
features/001-example-app/example-generate.feature:107
When I run `sbuilder.rb generate pet1`
Then the exit status should not be 0
Then the stderr should contain "No such template"