[SAL-HELP] RE: [SAL] asking for help with SAL

Bruno Dutertre bruno at csl.sri.com
Mon Apr 2 10:13:55 PDT 2007


Bruno Dutertre wrote:
> Dulce María Hernández Rojas wrote:
> 
>> Thank you very much. Your help is being useful to me. I have another
>> question:
>> What is the meaning of these lines:
>>
>> map: pc1_ at _0!1 -> x_0
>> map: pc1_ at _0!2 -> x_1
>>
>> And what does the ! operator mean?
>>
>> Thank you again for your answer. :)
>>
>>
> 
> Hi,
> 
> You probably have two modules with a state variable called pc.
> SAL encodes one of them as pc..!1 and the other as pc...!2.
> 
> Bruno
> 
> 

Another possibility is that variable pc has a finite type and
gets encoded as two boolean variable pc..!1 and pc..!2

Bruno



More information about the SAL-HELP mailing list