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

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



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


Sara Van Langenhove

Ghent University
Department of Pure Mathematics and Computer Algebra
Galglaan 2 - S25 - 0/181
B 9000 Gent

sara.vanlangenhove@rug.ac.be
svlangen@cage.rug.ac.be
http://cage.rug.ac.be/~svlangen

%% PVS Version 3.0
%% 6.2 [Linux (x86)] (Dec 19, 2002 3:09)
$$$even.pvs
even:theory
   begin

     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

%     next1(s0,s1): bool =
%           PC(s0) = dec and
%           B(s1) = B(s0) - 2 and
%           PC(s1) = inc

     next(s0,s1): bool = next0(s0,s1) %or next1(s0,s1)
     
     inv1(s): bool = B(s) >= 0

     prop: theorem init(s) implies AX(next,inv1)(s)
     prop1: theorem init(s) implies AG(next, inv1)(s)
     prop2: theorem init(s) implies AF(next, inv1)(s)
     prop3: theorem init(s) implies EF(next, inv1)(s)

     prop4: theorem init(s) implies EG(next, inv1)(s)
     prop5: theorem init(s) implies EX(next, inv1)(s)

   end even

$$$even.prf
(even
 (prop 0
  (prop-1 nil 3226561185 3226561593
   (""
    (abstract-and-mc "State" "abs_State"
     (("abs_B" "lambda (s:State): B(s) >= 0")))
    nil nil)
   unchecked
   ((init const-decl "bool" even nil)
    (AG const-decl "pred[state]" ctlops nil)
    (EF const-decl "pred[state]" ctlops nil)
    (EU const-decl "pred[state]" ctlops nil)
    (EX const-decl "bool" ctlops nil)
    (K_conversion const-decl "T1" K_conversion nil)
    (inv1 const-decl "bool" even nil)
    (next0 const-decl "bool" even nil)
    (next const-decl "bool" even nil))
   4412 320 t shostak))
 (prop1 0
  (prop1-1 nil 3226561783 3226561794
   (""
    (abstract-and-mc "State" "abs_State"
     (("abs_B" "lambda (s:State): B(s) >= 0")))
    nil nil)
   unchecked
   ((next const-decl "bool" even nil)
    (next0 const-decl "bool" even nil)
    (inv1 const-decl "bool" even nil)
    (K_conversion const-decl "T1" K_conversion nil)
    (EX const-decl "bool" ctlops nil)
    (EU const-decl "pred[state]" ctlops nil)
    (EF const-decl "pred[state]" ctlops nil)
    (AG const-decl "pred[state]" ctlops nil)
    (init const-decl "bool" even nil))
   11828 580 t shostak))
 (prop2 0
  (prop2-1 nil 3226561824 3226561829
   (""
    (abstract-and-mc "State" "abs_State"
     (("abs_B" "lambda (s:State): B(s) >= 0")))
    nil nil)
   unchecked
   ((next const-decl "bool" even nil)
    (next0 const-decl "bool" even nil)
    (inv1 const-decl "bool" even nil) (EX const-decl "bool" ctlops nil)
    (EG const-decl "pred[state]" ctlops nil)
    (AF const-decl "pred[state]" ctlops nil)
    (init const-decl "bool" even nil))
   4675 490 t shostak))
 (prop3 0
  (prop3-1 nil 3226561916 3226561926
   (""
    (abstract-and-mc "State" "abs_State"
     (("abs_B" "lambda (s:State): B(s) >= 0")))
    (("" (grind) nil nil)) nil)
   unchecked
   ((<= const-decl "bool" mucalculus nil)
    (lfp const-decl "pred[T]" mucalculus nil)
    (mu const-decl "pred[T]" mucalculus nil)
    (member const-decl "bool" sets nil)
    (glb const-decl "pred[T]" mucalculus nil)
    (State type-eq-decl nil even nil) (PCtype type-decl nil even nil)
    (int nonempty-type-eq-decl nil integers nil)
    (next const-decl "bool" even nil)
    (next0 const-decl "bool" even nil)
    (inv1 const-decl "bool" even nil)
    (K_conversion const-decl "T1" K_conversion nil)
    (EX const-decl "bool" ctlops nil)
    (EU const-decl "pred[state]" ctlops nil)
    (EF const-decl "pred[state]" ctlops nil)
    (init const-decl "bool" even nil))
   9462 1140 t shostak))
 (prop4 0
  (prop4-1 nil 3226561950 3226561966
   (""
    (abstract-and-mc "State" "abs_State"
     (("abs_B" "lambda (s:State): B(s) >= 0")))
    (("1" (postpone) nil nil)
     ("2" (grind) (("1" (postpone) nil nil) ("2" (postpone) nil nil))
      nil))
    nil)
   unfinished nil 15707 1610 t shostak))
 (prop5 0
  (prop5-1 nil 3226561984 3226561995
   (""
    (abstract-and-mc "State" "abs_State"
     (("abs_B" "lambda (s:State): B(s) >= 0")))
    (("1" (postpone) nil nil) ("2" (postpone) nil nil)) nil)
   unfinished nil 10797 760 t shostak)))