From: Chao Wang (Wangc_at_colorado.edu)
Date: Sat Nov 08 2003 - 10:41:14 MST
Nikalas,
There is no existing VIS command that does this. But you can easily modify
the code to output the BDDs into a file.
You can start with fsm/fsmCmd.c and fsm/fsmReach.c. Right after
compute_reach, call the existing CUDD function to output the BDDs into a
file.
Chao
On Sat, 8 Nov 2003, Niklas Een wrote:
> I wish to use VIS' reachability analysis to create invariants for
> other (SAT-based) model checkers. Is there a way to make VIS output the
> conjunction of BDDs representing the reachable state space as computed by
> 'compute_reach'?
>
> // Niklas
>
--
This archive was generated by hypermail 2.1.7 : Sat Nov 08 2003 - 10:43:52 MST