[More Detail] [Collapse All]
Feature: Verify possibilities

Correctness criteria often use universal quantification, which is
vacuously true, if the set being quantified over is empty. This
raises concerns, whether passing correctness criteria has actually
verified what was intended.

Confidence would be increased, if it we check that is is possible
reach a state, where correctness criterion should hold
non-trivially. To Especially, the state should defined using an
operator.

TLA+ does not natively support expressing possibilities. However, a
possibility check can be simulated using an operator representing
the possibility, and demonstrating that the negation of this
operator does not hold always.

In Sbuilder, a possibility check is enabled by giving the name of a
operator for the possibility in `possibilities` array in a setup.

Sbuilder generates separate set of specification modules for each
possibility in the `possibilites`. This allows each possibility to
be checked in a separate run. Separate runs are needed, because TLA+
model checker stops after finding the first (possibility) property
violation, leaving it uncertain whether correctness criteria would
hold also in states left unexplored.
features/048-possibility/010-verify-possibilities.feature
- Background: Create specification model
link

Create a specification model
- interface operation '/customer(post)'
- definition 'Customer'
- resolver to find domains for interface operation parameters
- specification snippets
   -- state variable 'customers'
   -- service entry point 'customer_post'
   -- transaction 'customer_db_entry' to put entries into state variable 'customers'
features/048-possibility/010-verify-possibilities.feature:30
Given I run `sbuilder.rb init`
And I successfully run `sbuilder.rb init`
And I successfully run `sbuilder.rb extend`
And a file named "cnf/sbuilder.yaml" with:
#
# Define interfaces

interfaces:
    -  className: Sbuilder::ParamSetLoaderSwagger
       file: customer-interface.yaml
And a file named "cnf/customer-interface.yaml" with:
swagger: "2.0"
info:
  version: 1.0.0
  title: Sbuilder.rb customer customer example
  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/customer-interface.yaml` in path `paths`

# Interface operation /customer(post) in swagger configuration

  /customer:
    post: 
      operationId: postCustomer
      parameters:
        - name: customer
          in: body
          description: Customers to enter
          required: true
          schema:
              $ref: '#/definitions/Customer'
      responses:
         200:
            description: OK
And YAML configuration file `cnf/customer-interface.yaml` in path `definitions`

# Defition 'Customer' in swagger YAML


 Customer:
         properties:
           id:
            type: string
           type:
            type: string
           name:
            type: string
And YAML configuration file `cnf/sbuilder.yaml`
#
# Define domain resolvers in 'cnf/sbuilder.yaml'
#
resolvers:
      - url: cnf/customer-resolver.yaml
Given a file named "cnf/customer-resolver.yaml" with:
# resolver which catch-all matcher to match all 
# parameter sets, espcially operation /customer(post).
#
# Resolver rules match domain for parameters 'id', and 'name', and
# catch-all rule matching parameter 'type' in operation
# '/customer(post)'.

   -    Name: default-relsover
        Matcher: !ruby/regexp /.*/
        Rules: 
          - Matcher: id
            Domain: id_domain
          - Matcher: name
            Domain: name_domain
          - Matcher: !ruby/regexp /.*/
            Domain: default_domain
And a file named "cnf/extend-implementation.yaml" with:
#
# interface-extension: define implemehtation for interface
# operation '/customer(post)'

- interface-extension:
   - matcher: /customer(post)
     implementation: customer_post
And a file named "cnf/step-customer_post.yaml" with:

# Define steps, which environment will take. In this case,
# environment call interface '/customer(post)', and because no
# input constaint is defined, environment uses all input
# combination for 'id', 'name', and 'type' parameters in the
# operation.
#
- step-extension:
       - interface: /customer(post)
# ------------------------------------------------------------------
# Speication code snippets in specification code repository 'src'
And I append to "src/state" with:
(* Initialize state variable 'customer' to empty set *)

customers = {}; 
And I append to "src/interface" with:
{{>customer_db_enter.code}} {{! include implementation for 'customer_db_entry' }}
{{>customer_post.code}}     {{! include implementation for 'customer_post' }}
And a file named "src/customer_post.code" with:
  (* This macro is called for interface /customer(post)  *)
   macro customer_post( input ) {
       customer_db_entry( input.customer );
   }
And a file named "src/customer_db_enter.code" with:
  (* This macro is called for interface /customer(post)  *)
   macro customer_db_entry( input ) {
       customers :=  customers \union {input};
   }
- Scenario: Verify invariants and possibility
link


Define correctness criterion 'Customers_ValidDomain', and activate it
using INVARIANT -directive.


Define possibility criterion 'Customers_not_empty', and define it in
'possibilities' property for 'example' -setup.

Generating setup 'example' creates possibility configuration
'possible_Customers_not_empty'.

Possibility configuration 'possible_Customers_not_empty' can
demonstrate that a state where possibility 'Customers_ValidDomain'
is true can, indeed, be reached in the setup. 


In a setup, which makes a call to customer post.
features/048-possibility/010-verify-possibilities.feature:200
Given YAML configuration file `cnf/sbuilder.yaml`
#
# setup extensions:
# - for interface implementation
# - check possibility 'Customers_not_empty'
# - steps to execute
#
setups:
  - setupDirectory: example
    possibilities:
        - Customers_not_empty
    extensions:
      -  url: cnf/step-customer_post.yaml
      -  url: cnf/extend-implementation.yaml
And I append to "src/correctness" with:
(* 
   Define correctness operator to verify that all entries in state
   variable 'customers' have a correct type. In this case require the
   type to be 't_Customer'.

 *)
Customers_ValidDomain == \A entry \in customers: entry  \in t_Customer
And a file named "src/extend/extend_invariant_cfg.mustache" with:

\* Activate correctness invariant 'Customers_ValidDomain' defined above

INVARIANT Customers_ValidDomain
And I append to "src/possibility" with:
(* 
   Define a possibility operator to check that variable 'customers' get populated. 

*)
Customers_not_empty == customers # {}
When I successfully run `sbuilder.rb generate example`
Then the following files should exist:
Configuration files to verify possiblility
gen/example/tla/possible_Customers_not_empty.cfg
gen/example/tla/possible_Customers_not_empty.tla
When I cd to "gen/example/tla"
And I successfully run command `java -cp $TLATOOLS pcal.trans model`
And the stdout should contain "Translation completed."
And I run command `java -cp $TLATOOLS tlc2.TLC setup`
Then the stdout should contain "Model checking completed. No error has been found."
When I run command `java -cp $TLATOOLS tlc2.TLC possible_Customers_not_empty`
Then the stdout should contain "Error: Invariant possible_Customers_not_empty is violated."