13.4 Confidence condition verification13.4 Confidence condition verification
13 SAL Translator 13 SAL Translator
13.5 Using the tool

13.5 Using the tool

The RSL-SAL translator works on different operative systems. In particular, it is possible to use Linux and Windows platforms.

For using the tool on Windows platform it is necessary to:

For using the tool on Linux platform it is necessary to:

13.5.1 Activating the SAL translator

The translator's activation is through the Emacs editor, so for using the RSL-SAL translator

When the "Translate to SAL" option is executed, the tool generate some files (they are in the same folder where .rsl file is). Some of these files are:

Once the "Translate to SAL" option has been executed, it is possible to check if the specification resulting from the translation is well formed. This one is activated in the Emacs editor, selecting the "RSL" option and the "Run SAL well-formed checker" option. This step also generates some .sal files from some .m4 files and so is essential.

After executing the "Run SAL well-formed checker" option, other utilities provided for the tool are enabled. Also they are activated using the Emacs editor. In this case, it is necessary to select the "RSL" option and some one of the following, 

  Run SAL deadlock checker 
    Base 
    CC 
    Simple CC
  Run SAL model checker  
    Base 
    CC 
    Simple CC

In the next subsection an example is used to show how the tool works in more detail.

13.5.2 An example

The following code is in a file named "TOKENS.rsl",

                                     
 scheme TOKENS =
 class
 type
 Token == a | b | c | d | e | f,
 State ::
 S1 : Token-set ↔ re_S1
 S2 : Token-set ↔ re_S2
 
 value
 init : State =
 mk_State({a, b, c}, {d, e, f}),
 
 give21 : Token × State → State
 give21(t, s) ≡
 re_S1({t} ∪ S1(s), re_S2(S2(s) \ {t}, s))
 
 give12 : Token × State → State
 give12(t, s) ≡
 re_S2({t} ∪ S2(s), re_S1(S1(s) \ {t}, s)),
 
 transition_system
 [sys]
 local state : State := init
 in
 ([] tok : Token •
  [give21]
  tok ∈ S2(state) ⇒
  state′ = give21(tok, state))
 []
 ([] tok : Token •
  [give12]
  tok ∈ S1(state) ⇒
  state′ = give12(tok, state))
 end
 
 ltl_assertion
 [consistent] sys   G(S1(state) ∩ S2(state) = {}),
 [no_loss]
 sys  
 G(S1(state) ∪ S2(state) = {a, b, c, d, e, f}),
 [empty_S1_reachable] sys   G(S1(state) ≠ {}),
 [empty_S2_reachable] sys   G(S2(state) ≠ {})
 end

- Translating to SAL

If the "TOKENS.rsl" file is opened using the Emacs editor and the "Translate to SAL" option is executed, the tool will generate these files, 

Bool__cc_OPS.m4
Bool__cc_OPS_simple.m4
BT_AN.sal
Int__cc_OPS.m4
Int__cc_OPS_simple.m4
Int__OPS.m4
IT_AN.sal
L_BUILTIN.sal
L_BUILTIN_simple.sal
NT_AN.sal
SAL_GLOBAL.sal
SAL_TYPES.sal
SAL_TYPES_cc.sal
SAL_TYPES_cc_simple.sal
State_cc_OPS.m4
State_cc_OPS_simple.m4
Token_cc_OPS.m4
Token_cc_OPS_simple.m4
Token_set_cc_OPS.m4
Token_set_cc_OPS_simple.m4
Token_set_OPS.m4
TOKENS.sal
TOKENS_cc.sal
TOKENS_cc_simple.sal

- Running SAL well-formed checker

Now, it is possible to check if "TOKENS.sal", "TOKENS_cc.sal" and "TOKENS_cc_simple.sal" are well formed. For that, the tool first copies prelude files, and later it generates .sal files from .m4 files.

The well formed checking is enabled selecting the "Run SAL well-formed checker" option. So, the compilation buffer shows,

sal_wfc_check TOKENS

sal-wfc TOKENS
Ok.
sal-wfc TOKENS_cc
Ok.
sal-wfc TOKENS_cc_simple
Ok.

Compilation finished at ...

And the following files are generated: 

Bool__cc_OPS.sal
Bool__cc_OPS_simple.sal
Bool_cc_prelude
cc_type_prelude
Int__cc_OPS.sal
Int__cc_OPS_simple.sal
Int__OPS.sal
int_cc_prelude
int_prelude
map_cc_prelude
map_prelude
set_cc_prelude
set_prelude
State_cc_OPS.sal
State_cc_OPS_simple.sal
Token_cc_OPS.sal
Token_cc_OPS_simple.sal
Token_set_cc_OPS.sal
Token_set_cc_OPS_simple.sal
Token_set_OPS.sal

- Running SAL deadlock checker

SAL model checking is only valid if there are no deadlock states. The tool allows one to check for no deadlock states, selecting the "Run SAL deadlock checker" option. Next, it is necessary to choose between "base", "CC", or "simple_CC" options. In all these cases, the Emacs minibuffer shows,

Transition system identifier:

Then it is necessary to specify a transition system identifier (in the TOKEN example its name is "sys"),

Transition system identifier: sys

So, if previously the "base" option was selected, the compilation buffer will show,

sal-deadlock-checker TOKENS sys

ok (module does NOT contain deadlock states).

- Running SAL model checker

The tool allows one to run the SAL model checker, selecting the "Run SAL model checker" option. Next, it is necessary to choose between "base", "CC", or "simple_CC" options. In all these cases, the Emacs minibuffer shows,

Assertion identifier (default all assertions):

If an assertion identifier is specified (for example, "consistent"), and previously the "base" option was selected, the compilation buffer will show,

sal-smc TOKENS consistent

proved.

But if no particular assertion identifier is specified, by default all assertions are checked. In this case, the result is 

sal-smc TOKEN2 

Counterexample for 'empty_S1_reachable' located at [Context: TOKEN2, line(49), column(0)]:
========================
Path
========================
Step 0:
--- System Variables (assignments) ---
state =
mk_State((LAMBDA (arg!9 : Token):
           (arg!9 /= f) and (arg!9 /= e) and (arg!9 /= d)),
         (LAMBDA (arg!10 : Token):
           (arg!10 = f) or (arg!10 = e) or (arg!10 = d)))
------------------------
Transition Information: 
(module instance at [Context: TOKEN2, line(47), column(21)]
  (with tok = a at [Context: TOKEN2, line(40), column(0)]
    (label give12
      transition at [Context: TOKEN2, line(42), column(4)])))
------------------------
Step 1:
--- System Variables (assignments) ---
state =
mk_State((LAMBDA (arg!11 : Token):
           (arg!11 /= f) and
           (arg!11 /= e) and
           (arg!11 /= d) and
           ((arg!11 = c) or (arg!11 = b))),
         (LAMBDA (arg!12 : Token):
           (arg!12 = f) or
           (arg!12 = e) or
           (arg!12 = d) or
           (arg!12 /= c) and (arg!12 /= b)))
------------------------
Transition Information: 
(module instance at [Context: TOKEN2, line(47), column(21)]
  (with tok = c at [Context: TOKEN2, line(40), column(0)]
    (label give12
      transition at [Context: TOKEN2, line(42), column(4)])))
------------------------
Step 2:
--- System Variables (assignments) ---
state =
mk_State((LAMBDA (arg!13 : Token):
           (arg!13 /= f) and
           (arg!13 /= e) and
           (arg!13 /= d) and
           (arg!13 /= c) and
           (arg!13 = b)),
         (LAMBDA (arg!14 : Token):
           (arg!14 = f) or
           (arg!14 = e) or
           (arg!14 = d) or
           (arg!14 = c) or
           (arg!14 /= b)))
------------------------
Transition Information: 
(module instance at [Context: TOKEN2, line(47), column(21)]
  (with tok = b at [Context: TOKEN2, line(40), column(0)]
    (label give12
      transition at [Context: TOKEN2, line(42), column(4)])))
------------------------
Step 3:
--- System Variables (assignments) ---
state =
mk_State((LAMBDA (arg!15 : Token): false),
         (LAMBDA (arg!16 : Token): true))

Counterexample for 'empty_S2_reachable' located at [Context: TOKEN2, line(50), column(0)]:
========================
Path
========================
Step 0:
--- System Variables (assignments) ---
state =
mk_State((LAMBDA (arg!17 : Token):
           (arg!17 /= f) and (arg!17 /= e) and (arg!17 /= d)),
         (LAMBDA (arg!18 : Token):
           (arg!18 = f) or (arg!18 = e) or (arg!18 = d)))
------------------------
Transition Information: 
(module instance at [Context: TOKEN2, line(47), column(21)]
  (with tok = d at [Context: TOKEN2, line(34), column(0)]
    (label give21
      transition at [Context: TOKEN2, line(36), column(4)])))
------------------------
Step 1:
--- System Variables (assignments) ---
state =
mk_State((LAMBDA (arg!19 : Token):
           (arg!19 /= f) and (arg!19 /= e)),
         (LAMBDA (arg!20 : Token): (arg!20 = f) or (arg!20 = e)))
------------------------
Transition Information: 
(module instance at [Context: TOKEN2, line(47), column(21)]
  (with tok = f at [Context: TOKEN2, line(34), column(0)]
    (label give21
      transition at [Context: TOKEN2, line(36), column(4)])))
------------------------
Step 2:
--- System Variables (assignments) ---
state =
mk_State((LAMBDA (arg!21 : Token):
           (arg!21 = f) or (arg!21 /= e)),
         (LAMBDA (arg!22 : Token): (arg!22 /= f) and (arg!22 = e)))
------------------------
Transition Information: 
(module instance at [Context: TOKEN2, line(47), column(21)]
  (with tok = e at [Context: TOKEN2, line(34), column(0)]
    (label give21
      transition at [Context: TOKEN2, line(36), column(4)])))
------------------------
Step 3:
--- System Variables (assignments) ---
state =
mk_State((LAMBDA (arg!23 : Token): true),
         (LAMBDA (arg!24 : Token): false))

Summary:
The assertion 'consistent' located at [Context: TOKEN2, line(47), column(0)] is valid.
The assertion 'no_loss' located at [Context: TOKEN2, line(48), column(0)] is valid.
The assertion 'empty_S1_reachable' located at [Context: TOKEN2, line(49), column(0)] is invalid.
The assertion 'empty_S2_reachable' located at [Context: TOKEN2, line(50), column(0)] is invalid.

Compilation finished ...

13.5.3 Confidence conditions

SAL is only sound when there are no deadlocks. So you have to check for deadlocks in the CC version as well as the basic one.

To illustrate this, and show how to get information from the CC version, we use the lift example from section 13.3.4. Suppose we change, in the BUTTONS module, the definition of "required_beyond" to

                                     
 -- wrong version
 required_beyond : T.Direction × T.Floor × Buttons → Bool
 required_beyond(d, f, bs) ≡
 let f′ = T.next_floor(d, f) in
 required_here(d, f′, bs) \/
  T.is_next_floor(d, f′) /\
  let f′′ = T.next_floor(d, f′) in
 required_here(d, f′′, bs)
 end
 end /\ T.is_next_floor(d, f)

Note that we gave moved the conjunct T.is_next_floor(d, f) from the beginning to the end. This looks logically equivalent to the original, because /\ is normally commutative. But we have to remember RSL's left-to-right evaluation rule, and also recall that T.is_next_floor(d, f) is a precondition of T.next_floor(d, f). In the original version, if T.is_next_floor(d, f) is false, then T.next_floor(d, f) is not evaluated. In the new version, this is not so and we can get a precondition violation.

If we make this change to required_beyond, recompile to SAL, check well-formedness, and model check the CC version it reports all is well. But if we remember to also run the deadlock checker on the CC version it reports a deadlock: 

Total number of deadlock states: 1.0
Deadlock states:
State 1
--- System Variables (assignments) ---
lift =
Lift_cc(mk_Lift_(mk_Cage_(up, halted, 0),
                 mk_Doors_(open, shut, shut),
                 mk_Buttons_(lit, lit, lit, lit, lit, lit, lit)))

This tells us that the "no errors" report from the CC model check cannot be trusted, but otherwise is not very helpful, because no Nav value is reported. We might notice that the buttons have all become lit, which means that the press transition is not enabled. The other transition must also not be enabled (since we have a deadlock), which means that can_next(lift) must not be true. In fact can_next contains a Nav. We can investigate what is happening by adding a variable to the system so that we can see the value of can_next:

Now we get the result that the check on the variables is invalid: cn contains a Nav: 

Step 1:
--- System Variables (assignments) ---
lift =
Lift_cc(mk_Lift_(mk_Cage_(up, halted, 0),
                 mk_Doors_(open, shut, shut),
                 mk_Buttons_(clear, lit, clear, clear, clear, clear, clear)))
cn =
Bool__nav(Precondition_of_function_T_next_floor_not_satisfied)

Summary:
The assertion 'LIFT_max_floor_cc_check' located at [Context: LIFT_cc, line(180), column(0)] is valid.

The assertion 'LIFT_min_floor_cc_check' located at [Context: LIFT_cc, line(181), column(0)] is valid.

The assertion 'LIFT_L_cc_check' located at [Context: LIFT_cc, line(209), column(0)] is invalid.

and we see that T.next_floor is the function whose precondition is violated. We can proceed in the same way if necessary, adding more variables to show how the values of particular expressions change in this run, until we find the error.

Chris George, April 17, 2008

13.5 Using the tool
13.4 Confidence condition verification13.4 Confidence condition verification
13 SAL Translator 13 SAL Translator