[SAL-HELP] sal-bmc

[silky.arora at gm.com]

Thanks Gasso,

I think I have a different question. Let me explain.

When I invoke sal-bmc as in the following:

        sal-bmc <module-name> <property>

the initial state is taken as given in the "INITIALIZATION" portion of 
<module-name>

However, my intention is to call sal-bmc with a parametrized initial state 
as:

        sal-bmc <module-name> <property> <init-state>

such that sal-bmc will take the <init-state> as initial and will override 
the "INITIALIZATION" portion.

Is it possible to do it using some SAL API's? I am quite a novice to SAL 
and hence would appreciate
if you can give some specific instructions.

Thanks a lot in anticipation,

Silky



"Gasso Wilson Mwaluseke" <gm015d5056 at blueyonder.co.uk> 
11/13/2007 09:52 PM

To
<silky.arora at gm.com>
cc

Subject
Re: [SAL-HELP] sal-bmc






Dear Silky,
Theoretically, that should pause no problems at all.  However, it may be a 
big problem if you don't provide the bounds properly.
I hope you have installed sal-3.0 in your computer with Linux or UNIX 
version as an operating system.  You should try it first by simulation and 
when satisfied, run your bounded model checker.
 
Good Luck!.
 
 
Gasso
----- Original Message ----- 
From: silky.arora at gm.com 
To: sal-help at csl.sri.com 
Sent: Tuesday, November 13, 2007 10:54 AM
Subject: [SAL-HELP] sal-bmc


Hi, 

I have a SAL module and want to call sal-bmc  on it  from some state other 
than the initial state. 
Is that possible? 

Please help. 

Thanks, 
Silky.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.csl.sri.com/pipermail/sal-help/attachments/20071114/4863c1f8/attachment.html