From: Chao Wang (Wangc_at_colorado.edu)
Date: Mon Jul 19 2004 - 14:45:07 MDT
Hi Tom,
VIS normally does not remember the results of previous calls to
check_invariant. However, if the reachable states of the system's default
FSM is available, the check_invariant command will use it; this is true
no mater how these reachable states have been computed. For example, if
you run check_invariant once and the FSM cannot be simplified by COI
reduction, the reachable states MAY be computed (and if so, will be stored
for later use).
Chao
> I have a question on the check_invariant command.
>
> Assume we have an FSM read in (including all the things for building
> BDDs and so on). Further, we have several invariants to be checked, not
> all in one file, but one file for each invariant. Then, we are calling
> check_invariant iteratively for each of the invariants.
>
> Question: Does vis somehow remember results (including, for instance,
> reached states / BDDs for the last runs(s)) when calling check_invariant
> repeatedly and does vis somehow exploit that knowledge for other
> check_invariant runs? I think it will be at least restricted as for each
> ci-command a COI-computation should take place, but may be there are
> rules which allow to remember data even for different ci-runs on the
> same FSM.
>
> Looking forward to your anwer(s)!
>
> Tom
>
This archive was generated by hypermail 2.1.7 : Mon Jul 19 2004 - 17:36:46 MDT