From: Chao Wang (chaowang_at_nec-labs.com)
Date: Tue May 08 2007 - 19:36:25 MDT
Yang,
1. "compute_reach" does FORWARD reachable computation -- the initial
state I is the starting point of this computation. It computes the set
'R' of reachable states as follows,
R = {I}
R = R + image( R ) till convergence
Here image(R) is the set of states reachable from R in one step (i.e.,
if the current state belongs to R, the next state belongs to image(R)).
Yes, In VIS the initial state is retrieved from the corresponding
statements in the blif-mv file.
2. "model_check" normally does backward computation for properties like
"EF p". For a BAD state 'p', it computes the set 'Z' of states (which
can lead to the BAD state in one or more steps) as follows,
Z = {p}
Z = Z + preimage( Z )
Here preimage(R) is the set of states that can reach R in one step.
If "EF p" is the property, then "model_check" will stop as soon as the
set Z contains I (only when that never happens will the computation
complete with a fixpoint).
However, it should be easy to modify the source code (check
src/mc/mcMc.c) if you want to always complete the backward fixpoint. For
this purpose, you might want to check how the current code in VIS handle
properties like "EX (EF p)" or "EG (EF p)" --- in both cases, it needs
to first compute the set Z of states for "EF p", and then compute either
"EX Z" or "EG Z".
Chao
--- "Zhao, Yang" wrote:
>
> 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 - 19:43:55 MDT