From: Fabio Somenzi (Fabio_at_colorado.edu)
Date: Wed Mar 21 2007 - 17:59:16 MDT
>>>>> "HL" == Huy Lam <lamhuy_at_vt.edu> writes:
HL> To whom this may concern:
HL> My name is Jason. I am currently a graduate student at Virginia Tech. I have
HL> been trying to use VIS model_checking commands to verify a few properties
HL> such as reachablity: EF(p). If I like to specify an initial state S0:
HL> S0 |= EF(p)
I forgot to add that the other option is to change the model so that
it has only S0 as initial state. It may be more efficient, in fact,
to do so for a complex model.
Fabio
This archive was generated by hypermail 2.1.7 : Wed Mar 21 2007 - 18:00:17 MDT