Hi all,
I am working on a SAL model where I am using the command
sal-inf-bmc -v 3 -d 10 context spec
The depth here is 10 and for my problem I have to verify the specification up to a depth of atleast 300. But for depth of 100 itself my SAL process is just using 5% of CPU and thus it is taking days to complete the process.Can any one tell me what might be the problem with my model.My model has recursive function calls which I couldn't get rid of.Can there be any reason other than that.
The model is a absolute real time model and my specification are those that has to be verified in all the states and these specs are not inter related.
to be clear it is not like this : pc=1 => X(pc=2).
It does not involve either of F,X,U,W amd R.
It is just G(Forall (i:[1 .. N],j:[1 .. T]): pc(i) = funct(i,j));
Also it is a deterministic algorithm where i know what happends at a time 't'.I can know the state variables at time 't'.So instead of verifying up to a depth of 300 where my time changes say from 0 to 30000. Iam planning to go in steps of 1000.Like at first I want to verify from t=0 to t=1000 then initialize my model to the state at t=1000 and then repeat the procesdure for every 1000secs. Can I do this in SAL?
Can I output a state (at t=100) and all its variables to a output file from which I can develop new input context(file) to the model.In this way I can solve my above problem.
Please help in this .
Thanking you,
Suman Kasam
---------------------------------
Finding fabulous fares is fun.
Let Yahoo! FareChase search your favorite travel sites to find flight and hotel bargains.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.csl.sri.com/pipermail/sal-help/attachments/20070326/67061932/attachment.html