[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: AG/EG - AX/EX in abstract-and-mc




Sara:

In the PVS model AXp does not imply EXp, since there can be deadlocked
states, i.e., ones with no outgoing transitions, that satisfy the former
but not the latter.  For universal properties, the abstraction produces an
overapproximation of the concrete transition relation, whereas for
existential properties, it produces an underapproximation.  In this case,
the underapproximation comes out empty which is why EXp and EGp are
unprovable.  It turns out that EFp is actually provable for the trivial
reason that p is true in the initial state.  The EFp case generates a
feasibility proof obligation (each abstract state has at least one
concrete counterpart) that has to be discharged by a couple of manual
interactions.

-Shankar

> Hi,
> 
> While working with an easy and very little example about even numbers I
> found the following strange thing in the model-checker.
> 
>    PCtype: type = {inc, dec}
> 
>    State: type = [# PC : PCtype, B: int #]
> 
>    abs_State: type = [# PC : PCtype, abs_B: boolean #]
> 
>    s, s0, s1: var State
> 
>    init(s): bool = PC(s) = inc and B(s) = 0
> 
>    next0(s0,s1): bool = PC(s0) = inc and B(s1) = B(s0) + 2 and PC(s1) = dec
> 
> As you can see quite easily B(s) is always greater than zero.
> 
>    next(s0,s1): bool = next0(s0,s1)
> 
>    inv1(s): bool = B(s) >= 0
> 
> Now the model-checker (with abstraction lambda s: b(s) >= 0) is capable to
> proof the following theorem
> 
>    prop: theorem init(s) implies AX(next,inv1)(s)
> 
> but is not capable to proof
> 
>    prop5: theorem init(s) implies EX(next, inv1)(s)
> 
> which I think is very strange. If a property is correct for all next state
> then it must also be true for one state (EX).
> Can anyone explain to me why the invariant is true voor AX but not voor
> EX?  (I also included the dump file)
> (The same thing happens with AG and EG ...)
> 
> Thanks a lot
> 
> Sara