From: Tom Bienmueller (bienmueller_at_osc-es.de)
Date: Fri Jul 16 2004 - 09:26:39 MDT
Hi all,
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 : Fri Jul 16 2004 - 09:41:15 MDT