[SAL-HELP] Re: question

[Bruno Dutertre]

Dulce María Hernández Rojas wrote:
> $ sal-inf-bmc --preserve-tmp-files --disable-traceability --disable-cse
> --show-var-mapping -d 1 horno.sal  prop1
> 
> 

The integer variable comes from the property:

prop1: THEOREM main |- G(d => F(h));

SAL constructs a Buchi automaton for this and it encodes
the state of that automaton as an integer variable.

The simplest way to avoid this is to make sure
the property is of the from G(p) with no temporal
operators in p. You may need to construct a monitor
to express more complex properties. There are
examples of this technique in the sal-atg report,
see  http://sal.csl.sri.com/documentation.shtml

Regards,

Bruno