[SAL] Adding constraints

Ashish Tiwari tiwari at csl.sri.com
Wed Apr 13 11:15:15 PDT 2011


An alternative is to add a constraint in the guard with prime variables.

For example, Lee suggested:

X > 10 --> X' IN { y: NATURAL | y < 50 }

Alternatively, you can also use

X > 10 AND X' < 50 --> X' IN {y: NATURAL}

Ashish


On Tue, 12 Apr 2011, Lee Pike wrote:

> If I understand your question, then yes, what you'd like to do is possible. 
> You can nondeterministically assign a next-state value to a variable using 
> set-builder notation.  Supposing your variable v is of type NATURAL, then you 
> can nondeterministically update its value using a transition rule of the 
> form:
>
> ... --> v' IN {x : NATURAL | x >= 3 AND x <= 10};
>
> or whatever constraints you'd like.
>
> Regards,
> Lee
>
>
> On 04/12/2011 02:34 PM, Jhonatan Serna wrote:
>> Greetings,
>> 
>> I want to specify a system into SAL that work with variables in a
>> constraint system, that is, the variables don't have always any value,
>> only a information ( for example X > 10). I need add constraints over
>> the variables during the process system, i. e. that the modules can add
>> information during the transitions. For example, in the beginning X > 10
>> and then a module says that X < 50. Is that possible in SAL?
>> 
>> I'll really appreciate your help.
>> 
>> Thank you.
>> 
>> Jhonatan Serna.
>> 
>> 
>> --
>> ...
>



More information about the SAL mailing list