[SAL] Re: Some questions for using SAL

[David Friggens]

Hi Harry

> I have some questions regarding the SAL.

Hopefully I can answer some of your questions. First, I'll point out 
that SAL is not a procedural language - you define the transitions by 
writing the changes that happen to the variables. If you want to model 
some code from a procedural language you'll need to define a program 
counter variable. Then you can define transitions from location1 to 
location2, from location2 to location3, etc.

The msclock example (in SAL 2.4) is a good example of this.

> 1. Can I write the assertion in the module ? For instance, I want to
> express "assert(a==b)", how to write it in module as I see the
> example that the assertion written in the Theorem.

You can put a=b in the guard of the transition, and have another one 
that goes to an error state. For example

pc = locX AND a = b --> pc' = locY

and

pc = locX AND a /= b --> pc' = locError

Then you could test that the module doesn't ever enter the error state:
THEOREM system |- G(pc /= locError)


> 2. Is there way to express the wait condition ? For instance, I want
> to express the java expression "while ( a != 0) wait();" in SAL .

You could use a transition like:

pc = locX AND a = 0 --> pc' = locY

This transition is only enabled if the module is at location locX and a 
is zero, so if it's at locX and a isn't zero, then it has to wait until 
a transition becomes enabled (i.e. when a becomes zero).

> Anway, I saw example that has "sleeping, trying, critical ". Are
> those keywords SAL reserved keywords or user defined ?

These are user defined.

> 3. How to expression the invariant in SAL ?

If you want to prove that a property "p" is an invariant you can use the 
LTL formula G(p). For example
THEOREM system |- G(a <= 5 AND b >= 10).

> 4. Is there "for" loop in SAL ?

Not explicitly, but you can express it easily.


Cheers
David