[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