From: Zhao, Yang (zhaoyang_at_ict.ac.cn)
Date: Tue May 08 2007 - 18:48:13 MDT
Hi, Chao
Thank you for your reply, and some more details I want to know:
1. Whether the initial state given in blif_mv file is treated as the objective state in VIS when excerting "compute_reach" to do backward reachable computation?
2. If EF property is checking in VIS using "model_check", will the backward preimage iteration stop when the initial state is included in states that have been reached? -- because at this time, the property has been proved true.
Thank you very much!
Zhao, Yang
2007-05-09
This archive was generated by hypermail 2.1.7 : Tue May 08 2007 - 18:56:27 MDT