[SAL-HELP] question

[suman kasam]

Hi all,
   
         I have doubt.Can any one compare SAL with PVS or in other words mention advantages of one over the other( if a problem can be modeled in both) in terms of simulation time, memory  etc. I know the basic thing that SAL is for LTL and PVS is for CTL.
   
         I am presently facing problems with my SAL model. For large size problems my model is consuming more than 1.5 GB of memory. I just want to know if I can get rid of the problem using PVS in place of SAL. I can mention my constraints in both the languages.
   
   
  Thanking you ,
   
  Regards,
  Suman Kasam

Bruno Dutertre <bruno at csl.sri.com> wrote:
  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



 
---------------------------------
TV dinner still cooling?
Check out "Tonight's Picks" on Yahoo! TV.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.csl.sri.com/pipermail/sal-help/attachments/20070403/8274ae91/attachment.html