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

Re: strange problem with EG operator



Hi,

the things does not yet work like I expect but the problem with the EG is
solved. The problem with the AF operator still remains.

To make it clear I made a little more complex example

I have 5 states namely C1, C2, C3, C4, C5 with the following relation

C1 -> C2
C2 -> C3 or C2 -> C4 (disjunct transitions, otherwise they cannot be taken)
C4 -> C5
C5 -> C4
C3 -> C3

The transitions that leave state C2 has to be disjunct and in my
transition relation I check that with the following predicate:

uniquetransition(some arguments): exists1! (...): pred1 & pred2 & pred3

This predicate checks threee things that may not occur. So if there are
two transitions which states the three predicates it returns false and
that is what I need the make some states unreachable.

The total transitionrelation consists of this predicate and some other
conditions. Let us suppose that the transitions from C2 to C3 and C4 are
not disjunct so they can be enabled at the same time.
Because of the uniquetransitionpredicate C3 and C4 are unreachable for the
model-checker or at least they have to be.

Now if I write a theorem which checks if C3 (or C4) is reachable PVS
returns a correct counterexample. (one path so EF)
If i write a theorem which checks if C3 (or C4) is reachable on every path
(AF) PVS returns falsly a QED.
If I remove the uniquetrans. predicate from the entire transitionrelation
it works perfect ... Now you can say that I made a mistake in the
uniquepredicate but I made a little theorem and that theorem returns
false and gives a counterexample.
How can I solve this to get the right result?

Thanks a lot for the help,

Sara
confeindig: theory
  begin
   
    som: type = {1,2,3,4,5,6,7,8}
 
    V: Type = [# a: bool, b:som  #] 

    Vertex2:    type = {StateS1, StateS2, StateS3, StateS4, StateS5, StateRoot}    
    Events:     type = {EmptyE, Event1}
    Actions:    type = {EmptyA, A1}
    Conditions: type = {Cond1, Cond2, Cond3}

    Transition2: TYPE+ = [# source : Vertex2, 
                           trigger: Events, 
                           guard  : Conditions, 
                           effect : Actions, 
                           target : Vertex2 
                         #]

    t1: Transition2 = (# source := StateS1, trigger := EmptyE, guard := Cond1, 
                         effect := A1,  target  := StateS2 #)

    t2: Transition2 = (# source := StateS2, trigger := EmptyE, guard := Cond1, 
                         effect := EmptyA,  target  := StateS3 #)

    t3: Transition2 = (# source := StateS2, trigger := EmptyE, guard := Cond1, 
                         effect := EmptyA,  target  := StateS4 #)
  
    % self-loop

    t4: Transition2 = (# source := StateS3, trigger := Event1, guard := Cond2, 
                         effect := EmptyA,  target  := StateS3 #)
 
    % loop between StateS4 and StateS5

    t5 : Transition2 = (# source := StateS4 , trigger := Event1, guard := Cond1, 
                          effect := EmptyA, target  := StateS5 #)

    t6 : Transition2 = (# source := StateS5, trigger := EmptyE, guard := Cond2, 
                          effect := EmptyA,  target  := StateS4 #)

    configuration: type = finite_set[Vertex2]

    C1: configuration = add(StateRoot, add(StateS1, emptyset))
    C2: configuration = add(StateRoot, add(StateS2, emptyset))
    C3: configuration = add(StateRoot, add(StateS3, emptyset))
    C4: configuration = add(StateRoot, add(StateS4, emptyset))
    C5: configuration = add(StateRoot, add(StateS5, emptyset))   

    v: var V

     Conf: type = {C1, C2, C3, C4, C5} 
     conf : var Conf
     confoutput : type = configuration
     P(conf): configuration = table 
       |[ conf = C1 | conf = C2 | conf = C3 | conf = C4 | conf = C5 ]|
       | C1         | C2        | C3        | C4        |   C5 ||
     endtable

     Trans: type = {T1, T2, T3, T4, T5, T6}
     trans: var Trans
     Transoutput: type = Transition2
     PT(trans): Transoutput = table 
       |[ trans = T1 | trans = T2 | trans = T3 | trans = T4 | trans = T5 | trans = T6 ]|
       |  t1         | t2         | t3         |   t4       | t5         | t6      ||
     endtable

     Conf2: Type = [# v: V #]  

     s2, s02, s12: var Conf2

     predStateS1(v:V): bool = a(v) = true  and b(v) = 1 
     predStateS2(v:V): bool = a(v) = true  and b(v) = 2 
     predStateS3(v:V): bool = a(v) = false and b(v) = 3

     predStateS4(v:V): bool = a(v) = true  and b(v) = 4
     predStateS5(v:V): bool = a(v) = false and b(v) = 5

     predC1(v:V): bool = predStateS1(v)
     predC2(v:V): bool = predStateS2(v)
     predC3(v:V): bool = predStateS3(v)
     predC4(v:V): bool = predStateS4(v)
     predC5(v:V): bool = predStateS5(v)

     predCond1(v:V): bool = a(v) = true %and b(v) = 1
     predCond2(v:V): bool = a(v) = false
     predCond3(v:V): bool = b(v) = 2

     VC: type = [# pre: V, post: V #]
     vc: var VC

     predEmptyA(vc:VC): bool = true
     predA1(vc:VC)    : bool = b(pre(vc)) = 1 and b(post(vc)) = 2
 
    evalC(c:Conditions,v:V): bool = table 
       |[ c = Cond1     | c = Cond2    | c = Cond3    ]|
       |  predCond1(v)  | predCond2(v) | predCond3(v) ||
     endtable    

    evalA(a:Actions, vc:VC): bool = table
       |[ a = EmptyA      | a = A1     ]|
       |  predEmptyA(vc)  | predA1(vc) ||
     endtable    
      
     v_state: var V
     Q(conf, v_state): bool = table 
                    |[ conf = C1  | conf = C2 | conf = C3  | conf = C4 | conf = C5]|
                    |  predC1(v_state)   | predC2(v_state) | predC3(v_state) | 
                       predC4(v_state) | predC5(v_state)||
                           endtable
                                     
     init6(s2):       bool = b(v(s2)) = 1 and a(v(s2)) = true
     voorwaarde6(s2): bool = a(v(s2)) = false and b(v(s2)) = 3   

    requestedevent?(gEvent: Events, rEvent: Events): bool = (gEvent = rEvent)
    trueguard?(gTrans: Conditions, prev: V):         bool = evalC(gTrans,prev)
    truesource?(bronS: Vertex2, bronC: Conf):        bool = member(bronS, P(bronC))
    truetarget?(targetS: Vertex2, targetC: Conf):    bool = member(targetS, P(targetC))
    trueaction?(action:Actions, prev:V, post:V):     bool = evalA(action,vc) where
                                                            vc = (# pre:= prev, post:= post #)

   % A predicate which ensures that there can be never two transitions enabled at the same time
   % 
    uniquetransition?(e:Events, prev:V, bronC: Conf): bool = 
                        exists1! (tr: Trans): requestedevent?(trigger(PT(tr)), EmptyE) &
                                              member(source(PT(tr)), C2) &
                                              trueguard?(guard(PT(tr)), prev)  
                                                      
    SeqRelation(s02, s12): bool = 
                                 exists(c:Conf,c2:Conf): Q(c,v(s02)) & Q(c2,v(s12)) & 
                                   exists(e:Events): uniquetransition?(e, v(s02), c) & 
                                      exists(tr:Trans): 
                                              requestedevent?(trigger(PT(tr)), e) &
                                              truesource?(source(PT(tr)), c) &
      			 	              truetarget?(target(PT(tr)), c2) &              
                                              trueguard?(guard(PT(tr)), v(s02)) &
                                              trueaction?(effect(PT(tr)), v(s02), v(s12)) 
  
   theorem1: theorem init6(s2) => AF(SeqRelation, voorwaarde6)(s2)  
        % returns a QED while EF returns a counterexample ... strange 

  end confeindig