[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
# ------------------------------------------------------------------
# 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:193
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:208
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:221
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: option '--filter-list' not set --> exiting"
- Scenario: Parse error when pruning model - processing continues
link

Using option '--filter-list' allows generation to continue, even
in if parser encounters error in option '--filter-src'.
features/050-prune-model/010-filter-snippets.feature:242
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;
}
And a file named "manual-include.dat" with:
When I successfully run `sbuilder.rb generate setup1 --filter-src --filter-list manual-include.dat`
Then the exit status should be 0
And stderr should contain "Parser error: option '--filter-list' set --> continue"
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"
Then the file "gen/setup1/tla/model.tla" should not contain "macro syntax_error"
And I do PLC transformation for setup `setup1`
And I run TLC for setup `setup1`
- Scenario: Parse error when pruning model - processing continues & load any file into model
link

Using option '--filter-list' allows including partial modules into
specification code, which '--filter-src' would otherwise prune out.

In this scenario, we include module 'syntax_error' causing the
parser error into specification code. The example also names
another module, 'file-not-referenced.code', which, however, is NOT
includes into specification code, because the module is not
includes as partial in 'src/extend/extend_macros.mustache'.
features/050-prune-model/010-filter-snippets.feature:272
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; 
}
And a file named "manual-include.dat" with:
parse_error.code
file-not-referenced.code
When I successfully run `sbuilder.rb generate setup1 --filter-src --filter-list manual-include.dat`
Then the exit status should be 0
And stderr should contain "Parser error: option '--filter-list' set --> continue"
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"
Then the file "gen/setup1/tla/model.tla" should contain "macro syntax_error"
- 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:310
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\"/