From: Chao Wang (chaowang_at_nec-labs.com)
Date: Tue May 08 2007 - 12:01:04 MDT
Hi Yang,
The initial state(s) of a circuit is part of the definition of the model
in VIS; it cannot be "given" by the user.
However, you can define your own "final states" (e.g., with a
propositional formula 'p'), and then model_check the CTL formula "EF
p".
The model_check command in VIS will compute "all the states from which
the circuit can reach" p.
Chao
This archive was generated by hypermail 2.1.7 : Tue May 08 2007 - 12:06:59 MDT