[More Detail] [Collapse All]
Feature: Integer range domain

Domain extensions may define integer ranges such as:

     - domain-extension:
       - domain: integer
         range: [1, 4]
features/030-extend-domain/100-range-domain.feature
- Background: Create specification model for demonstrate range domain
link
features/030-extend-domain/100-range-domain.feature:12
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: interface.yaml
And a file named "cnf/interface.yaml" with:
swagger: "2.0"
info:
  version: 1.0.0
  title: Sbuild demo customer
definitions: {}
And YAML configuration file `cnf/interface.yaml` in path `paths`

# Interface operation /customer(post) in swagger configuration

  /inc:
    post: 
      operationId: inc
      parameters:
        - name: id
          in: query
          required: false
          type: integer
          format: int32
      responses:
         200:
            description: OK
  /set:
    post: 
      operationId: set
      parameters:
        - name: id
          in: query
          required: false
          type: integer
          format: int32
      responses:
         200:
            description: OK
#
# Configure resolver
#
And YAML configuration file `cnf/sbuilder.yaml`
#
# Define domain resolvers in 'cnf/sbuilder.yaml'
#
resolvers:
      - url: cnf/resolver.yaml
Given a file named "cnf/resolver.yaml" with:

# Resolve all parameters to integer

   -    Name: default-relsover
        Matcher: !ruby/regexp /.*/
        Rules: 
          - Matcher: !ruby/regexp /.*/
            Domain: integer
# ---
# Specification code 
#
And YAML configuration file `cnf/sbuilder.yaml`
#
# Map service implementation 

snippets:

  - className: Sbuilder::SnippetLoaderSimple 
    configuration:
        metatypes:
           code: Example code

    snippets:

      - metatype: service_implementation
        appName: /inc(post)
        file: inc_post.tla

      - metatype: code
        appName: inc
        file: inc.tla

      - metatype: code
        appName: set
        file: set.tla

      - metatype: code
        appName: mem
        file: mem.tla

      # - metatype: framework-svc
      #   appName: alwaysLessThan2
      #   file: alwaysLessThan2.tla
And a file named "src/mem.tla" with:
     {{#SPEC_NAME}}code.mem{{/SPEC_NAME}} = 0; 
And a file named "src/inc_post.tla" with:
\* inc_post
macro {{#SPEC_NAME}}service_implementation./inc(post){{/SPEC_NAME}}( input ) {

   print << "Input", input >>;
   call {{#SPEC_NAME}}code.inc{{/SPEC_NAME}}( input.id );
}
Given a file named "src/set.tla" with:
\* set:
procedure  {{#SPEC_NAME}}code.set{{/SPEC_NAME}}( input ) {

   {{#SPEC_NAME}}code.set{{/SPEC_NAME}}_start:
   
        {{#SPEC_NAME}}code.mem{{/SPEC_NAME}} := input;

   {{#SPEC_NAME}}code.set{{/SPEC_NAME}}_end:
       return;
}
Given a file named "src/inc.tla" with:
\* inc:
procedure  {{#SPEC_NAME}}code.inc{{/SPEC_NAME}}( input ) {

   {{#SPEC_NAME}}code.inc{{/SPEC_NAME}}_start:
               
        print << "before inc=", {{#SPEC_NAME}}code.mem{{/SPEC_NAME}} >>;
        {{#SPEC_NAME}}code.mem{{/SPEC_NAME}} := {{#SPEC_NAME}}code.mem{{/SPEC_NAME}} + input;
        print << "after inc=", {{#SPEC_NAME}}code.mem{{/SPEC_NAME}} >>;

   {{#SPEC_NAME}}code.inc{{/SPEC_NAME}}_end:
       return;
}
- Scenario: Default setup - no increment operation
link


Defult domain defines a set with Nil element and one fixed string
element. Setup calls set-operation, which does not use
arithmetics. Model checking passed.
features/030-extend-domain/100-range-domain.feature:181
Given YAML configuration file `cnf/sbuilder.yaml`
#
# Define setup 'example' - no extensions.

setups:
  - setupDirectory: example
    extensions:
      -  url: cnf/run.yaml
    # extensions:
    #    -  type: default-yaml
    #       url: cnf/extend_example.yaml
And a file named "cnf/run.yaml" with:
#
# Call service without increment 
#
- step-extension:
       - interface: /set(post)
When I successfully run `sbuilder.rb generate example`
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."
- Scenario: Extend range domain - arithmetic operation
link

Setup defines integer range 1..4, and calls `/inc(post)` service
using arithcmetics sevaral times.

Max value after all setup steps have been executed is 17. We
expect to find messages "before inc=16", and "after inc=17" in the
output.

Notice: range is defined 1..4, but the definition does not enforce
that some variable is restricted only to include values in this
set. Thi scenario does check correcness using invariants, and
increment operation set variable 'id' value to 17.
features/030-extend-domain/100-range-domain.feature:220
Given YAML configuration file `cnf/sbuilder.yaml`
#
# Define setup 'example' - no extensions.

setups:
  - setupDirectory: example
    extensions:
      -  url: cnf/run.yaml
    # extensions:
    #    -  type: default-yaml
    #       url: cnf/extend_example.yaml
And a file named "cnf/run.yaml" with:
#
# Call service without increment 
#
- domain-extension:
    - domain: integer
      range: [1, 4]

- step-extension:
         # value 1-4
       - interface: /inc(post)

         # value 2-5
       - interface: /inc(post)
         input:
            id: 1

         # value 5-8
       - interface: /inc(post)
         bindExact: true
         input:
            id: 3

         # value 9-12
       - interface: /inc(post)
         bindExact: true
         validators:
           - rule: path
             rule_value: [id]
             action: all

         # value 13-16
       - interface: /inc(post)
         bindExact: true
         validators:
           - rule: path
             rule_value: [id]
             action: all

         # value 14-17
       - interface: /inc(post)
         validators:
           - rule: path
             rule_value: [id]
             action: domain
             action_value: 1
When I successfully run `sbuilder.rb generate example`
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."
And the output should match /before inc=", 16/
And the output should match /after inc=", 17/