[More Detail] [Collapse All]
Feature: Throw excpetion - and interrupt execution

Process execution may be aborted using throw.

Throw modifies stack of currently executing process to
containg two elements:

- top of the stack return from current procedure to abort location
- bottom of the stack return from currently executing process

After modifying the stack, simple return sufficies to end the process.

Notice: process implementation should take care that transaction
should be commited only if not exiting via abort label.
features/300-scheduler/200-throw.feature
- Background: Create application
link

Define interfaces '/set1(post)', which accepts an integer range 2..8.

Enviroment calls this inferface with values 2,3,4,5.

Service implementation accepts all other values expect 3 in which
case it thrown an exception, and exist to via abort label,
and prints out abort message.

We use invariant 'neverThree' to verify that value 3 is rejected.
features/300-scheduler/200-throw.feature:20
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 a file named "cnf/example_interface.yaml" with:
swagger: "2.0"
info:
 version: 1.0.0
 title: Sbuilder.rb example walk-trough
 description: A scheduler example
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 /max2(post) and /set1(post)

  /set1:
    post: 
      operationId: set1
      parameters:
        - name: input
          in: query
          required: false
          type: integer
          format: int32
      responses:
         200:
            description: OK
And YAML configuration file `cnf/sbuilder.yaml`
#
# Define domain resolvers in 'cnf/sbuilder.yaml'
#
resolvers:
      - url: cnf/resolver_default.yaml
Given a file named "cnf/resolver_default.yaml" with:
# resolver which catch-all matcher 

   -    Name: default-relsover
        Matcher: !ruby/regexp /.*/
        Rules: 
          - Matcher: input
            Domain: integer
          - Matcher: !ruby/regexp /.*/
            Domain: default_domain
And YAML configuration file `cnf/sbuilder.yaml`
#
# setup extensions:
# - for interface implementation
# - steps to execute
#
setups:
  - setupDirectory: example
    desc: Example setup
    extensions:
      -  url: cnf/extend-steps.yaml
      # -  url: cnf/extend-implementation.yaml
And YAML configuration file `cnf/sbuilder.yaml`
#
# Map service implementation 

snippets:

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

    snippets:

      - metatype: service_implementation
        appName: /set1(post)
        file: set1_post.tla

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

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

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

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

      - metatype: framework-svc
        appName: neverThree
        file: neverThree.tla
And a file named "cnf/extend-steps.yaml" with:
#
# Integer domain
#
- domain-extension:
        - domain: integer
          range: [2,8]

# Define steps
#

- step-extension:
       - interface: /set1(post)
         input:
            input: 2

       - interface: /set1(post)
         input:
            input: 3

       - interface: /set1(post)
         input:
            input: 4

       - interface: /set1(post)
         input:
            input: 5
# ------------------------------------------------------------------
#
# Specification code
#
And a file named "src/mem.tla" with:
     {{#SPEC_NAME}}code.mem{{/SPEC_NAME}} = 0; 
And a file named "src/set1_post.tla" with:
\* set1_post:
macro {{#SPEC_NAME}}service_implementation./set1(post){{/SPEC_NAME}}( input ) {
   call {{#SPEC_NAME}}code.set1{{/SPEC_NAME}}( input.input );
}
Given a file named "src/set1.tla" with:
\* set1:
procedure  {{#SPEC_NAME}}code.set1{{/SPEC_NAME}}( input ) {

   {{#SPEC_NAME}}code.set1{{/SPEC_NAME}}_start:
        call {{#SPEC_NAME}}code.call1{{/SPEC_NAME}}( input );
   {{#SPEC_NAME}}code.set1{{/SPEC_NAME}}_return:
        skip;
        goto {{#SPEC_NAME}}code.set1{{/SPEC_NAME}}_end;
   {{#SPEC_NAME}}code.set1{{/SPEC_NAME}}_abort:
       print <<"Aborting", input >>;
   {{#SPEC_NAME}}code.set1{{/SPEC_NAME}}_end:
       return;
}
And a file named "src/call1.tla" with:
\* call1:
procedure  {{#SPEC_NAME}}code.call1{{/SPEC_NAME}}( input ) {

   {{#SPEC_NAME}}code.call1{{/SPEC_NAME}}_start:

              call {{#SPEC_NAME}}code.call2{{/SPEC_NAME}}( input );
  {{#SPEC_NAME}}code.call1{{/SPEC_NAME}}_end:

       return;
}
And a file named "src/call2.tla" with:
\* call2: finally accepts input

procedure  {{#SPEC_NAME}}code.call2{{/SPEC_NAME}}( input ) {

   {{#SPEC_NAME}}code.call2{{/SPEC_NAME}}_start:
       if ( input = 3 ) {
          schedule_throw( "{{#SPEC_NAME}}code.set1{{/SPEC_NAME}}_abort" );
   {{#SPEC_NAME}}code.call2{{/SPEC_NAME}}_throw:
          return;
       };
   {{#SPEC_NAME}}code.call2{{/SPEC_NAME}}_threw:
        
        {{#SPEC_NAME}}code.mem{{/SPEC_NAME}} := input;
        print << "mem set=", {{#SPEC_NAME}}code.mem{{/SPEC_NAME}}>>;

   {{#SPEC_NAME}}code.call2{{/SPEC_NAME}}_end:
       return;
}
And a file named "src/neverThree.tla" with:
\* 
neverThree == {{#SPEC_NAME}}code.mem{{/SPEC_NAME}} # 3
And YAML configuration file `cnf/sbuilder.yaml`
#
# mem variable must remain always less than 2
# - set1 : sets it to 1
# - max2 : checks that it is before incrementing it
#
invariants:
       - neverThree: number three is rejected
- Scenario: Exception thrown for input 3
link

We may observe that

- input 2 - valid
- input 3 - rejected && abort message
- input 4 - valid
- input 5 - valid
features/300-scheduler/200-throw.feature:279
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 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 /mem set=", 2/
And the output should match /Aborting", 3/
And the output should not match /mem set=", 3/
And the output should match /mem set=", 4/
And the output should match /mem set=", 5/