[More Detail] [Collapse All]
Feature: Filter snippets source from source

Increase in specification code volume in number of 

- state variables
- PlusCal macro definitions
- invariant operator definitions (and INVARIANT configurations)
- PlusCal procedure definitions
- PlusCal process definitions

leads to increases in TLC model checking time, i.e. it reduces the
number of states processed per second. Increase in processing time
becomes more severe, as the volume of the specification code
increases.

To mitigate this problem, Sbuilder adds a 'filter-src' option to do
call flow analysis of specification snippets in TLA sbuilder code
repository, and to include to TLA+ specification code only for those
snippet, which are reachable for the steps in a setup being
generated.
features/050-prune-model/010-filter-snippets.feature
- Background: Create TLA+ model
link

Create Sbuilder configuration with two service implementations:
/tag(post), and /pet(post). Create a setup, which calls only
interface operation '/tag(post)'.
features/050-prune-model/010-filter-snippets.feature:24
When I successfully run `sbuilder.rb init`
And a file named "cnf/sbuilder.yaml" with:
#
# Define interfaces

interfaces:
    -  className: Sbuilder::ParamSetLoaderSwagger
       file: example_interface.yaml
And YAML configuration file `cnf/sbuilder.yaml`
#
# Map service implementation 

snippets:

  - className: Sbuilder::SnippetLoaderSimple 
    snippets:

        # interface /customer(post) calls customer_post
      - metatype: service_implementation
        appName: /pet(post)
        name: pet_post

      - metatype: service_implementation
        appName: /tag(post)
        name: tag_post
# ------------------------------------------------------------------
# Swagger define input
And a file named "cnf/example_interface.yaml" with:
swagger: "2.0"
info:
 version: 1.0.0
 title: Sbuilder.rb example walk-trough
 description: A example walk-trough using swagger-2.0 specification
host: localhost
basePath: /api
schemes:
 - http
consumes:
 - application/json
produces:
 - application/json
paths: {}
definitions: {}
And YAML configuration file `cnf/example_interface.yaml` in path `paths`
#
# Interface operation '/pet(post)' 
#
  /pet:
    post: 
      operationId: postPet
      parameters:
        - name: pet_name
          in: query
          description: Name of pet to create
          required: false
          type: string
      responses:
         200:
            description: OK
And YAML configuration file `cnf/example_interface.yaml` in path `paths`
#
# Interface operation '/tag(post)' 
#
  /tag:
    post: 
      operationId: postTag
      parameters:
        - name: tag_id
          in: query
          description: Name of pet to create
          required: false
          type: string
      responses:
         200:
            description: OK
# ------------------------------------------------------------------
# Define setup:  steps & implementation
And YAML configuration file `cnf/sbuilder.yaml`
#
# 'setups' section defines setup extension for steps

setups:
  - setupDirectory: setup1
    extensions:
      -  url: cnf/setup-steps.yaml
      -  file: setup-implementation.yaml
And a file named "cnf/setup-steps.yaml" with:
# - setup setp calls only interface operation '/tag(post)'
#
- step-extension:
       - interface: /tag(post)
# ------------------------------------------------------------------
# Resolver
And YAML configuration file `cnf/sbuilder.yaml`
#
# 'resolvers' section loads resolvers from file
# 'cnf/resolver_customer.yaml'

resolvers:
     - url: cnf/resolver.yaml
And a file named "cnf/resolver.yaml" with:
# default resolver with one regexp rule
-    Name: default-relsolver
     Matcher: !ruby/regexp /.*/
     Rules: 
      - Matcher: pet_name
        Domain: pet_dom
      - Matcher: tag_id
        Domain: tag_dom
      
# ------------------------------------------------------------------
# interfaface implementations
And a file named "cnf/setup-implementation.yaml" with:
#
# implement interfaces

# - interface-extension:
#    - matcher: /pet(post)
#      implementation: pet_post
#    - matcher: /tag(post)
#      implementation: tag_post
And a file named "src/extend/extend_macros.mustache" with:
  {{! Extension template includes 'partials modules' }}
  {{>pet_post.code }}
  {{>tag_post.code }}
And a file named "src/pet_post.code" with:
  (* This macro is called for interface /pet(post)  *)
   macro pet_post( input ) {
       print << "Pet-post", input>>;
   }
And a file named "src/tag_post.code" with:
  (* This macro is called for interface /tag(post)  *)
   macro tag_post( input ) {
       print << "Tag-post", input>>;
   }
- Scenario: Full model - no filter-src option used
link

Default generate renders all mustache partial module into
specification code. Especially, macro pet_post is included, even
tough it is not used in the setup.
features/050-prune-model/010-filter-snippets.feature:213
When I successfully run `sbuilder.rb generate setup1`
Then the file "gen/setup1/tla/model.tla" should contain "macro tag_post"
Then the file "gen/setup1/tla/model.tla" should contain "macro pet_post"
And I do PLC transformation for setup `setup1`
And I run TLC for setup `setup1`
- Scenario: Prune model using '--filter-src' option
link

Using '--filter-src' option prunes unreachable code from
specification code. Especially, macro pet_post is NOT included,
because tough it is not used in the setup steps.
features/050-prune-model/010-filter-snippets.feature:227
When I successfully run `sbuilder.rb generate setup1 -f`
Then the file "gen/setup1/tla/model.tla" should contain "macro tag_post"
Then the file "gen/setup1/tla/model.tla" should not contain "macro pet_post"
And I do PLC transformation for setup `setup1`
And I run TLC for setup `setup1`
- Scenario: Parse error when pruning model - processing stops
link

Parser error stop generation with an error, when using option
'--filter-src'.
features/050-prune-model/010-filter-snippets.feature:240
Given I append to "src/extend/extend_macros.mustache" with:
  {{>parse_error.code }}
And a file named "src/parse_error.code" with:
macro syntax_error( input ) {
    a := := input;
}
When I run `sbuilder.rb generate setup1 --filter-src`
Then the exit status should not be 0
And stderr should contain " Parser error: --> exiting"
- Scenario: Unsatisified operator gets reported
link

A macro 'tag_post', which implements inteface operation '/tag(post)'
being called in 'setup1' makes a refence to an 'unknow operator'.

Specification code is generated including 'tag_post', but not with
unreferenced pet_post.

Especially, stdout reports 1 unresolved symbol, and lists
'unknown_operator'
features/050-prune-model/010-filter-snippets.feature:261
Given a file named "src/tag_post.code" with:
  (* This macro is called for interface /tag(post)  *)
   macro tag_post( input ) {
       print << "Tag-post", input, unknown_operator >>;
   }
When I successfully run `sbuilder.rb generate setup1 --filter-src`
Then the exit status should be 0
Then the file "gen/setup1/tla/model.tla" should contain "macro tag_post"
Then the file "gen/setup1/tla/model.tla" should not contain "macro pet_post"
And the stdout should contain "unresolved : count 1"
And the output should match /:symbol=>\"unknown_operator\"/