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

[PVS-Help] A question about abstraction in PVS




Dear PVS  expert,

While working on a simple example about abstraction, I encountered the
following problem:

The original model is a Kripke structure with one variable B:int. In the
initial state B is -10, and in the next state B is incremented by 1.


     State: type = [# B: int #]

     s, s0, s1: var State

     init(s): bool = B(s) = -10

     next(s0,s1): bool =  s1 = s0 WITH [B := B(s0) + 1]

     inv(s): bool = B(s) >= 0

     prop1: theorem init(s) implies AG(next, inv)(s)
     prop2: theorem init(s) implies AF(next, inv)(s)

If we abstract this model with predicates "B1 = lambda(s): B(s) >= 0" and
"B2 = lambda(s): B(s) < 0", the transition relation of the resulting
abstract model is expected to be:

B2 --> (B2 \/ B1)
B1 --> B1

Thus, prop2 should hold in the abstract model. However, when I tried
(abstract-and-mc ("lambda(s): B(s) >= 0" "lambda(s): B(s) < 0") ),
PVS couldn't prove prop2. Moreover, when I reviewed the result of
boolean abstraction, I noticed that the abstract transition relation
generated by PVS is different from the one that I expected:

B2 --> B2
B1 --> B1

This is strange to me because the abstraction of the above model should
satisfy prop2.

I have also included the .pvs and .prf files.

Thank you so much,
Shiva.
(|inc|
 (|prop1| ""
  (ABSTRACT-AND-MC ("lambda(s): B(s) >= 0" "lambda(s): B(s) < 0"))
  (("" (POSTPONE) NIL NIL)) NIL)
 (|prop2| ""
  (ABSTRACT-AND-MC ("lambda(s): B(s) >= 0" "lambda(s): B(s) < 0"))
  (("" (POSTPONE) NIL NIL)) NIL))

inc:theory
   begin


     State: type = [# B: int #]
 
     s, s0, s1: var State
 
     init(s): bool = B(s) = -10

     next(s0,s1): bool =  s1 = s0 WITH [B := B(s0) + 1]
     
     inv(s): bool = B(s) >= 0

     prop1: theorem init(s) implies AG(next, inv)(s)
     prop2: theorem init(s) implies AF(next, inv)(s)
    

   end inc