# 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]

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

```