# strange problem with EG operator

```Hi,

I have the following simple state space:

(details are in the attachement)

C1 with a = true, b = 1
C2 with a = true, b = 2
C3 with a = true, b = 3

and from C1 I can go to C2 and from C2 I can go to C3

It is very trivial that there exists a path for which a is true in each
node. However for PVS this is not the case but I do not see where I make a
mistake. Can anyone explain to me why this is the case?

(the AG operator works fine, the AF not because it is implemented in
function of the EG operator)

Thanks a lot for the help,

Sara
```
```
%% PVS Version 3.1
%% 6.2 [Linux (x86)] (Feb 14, 2003 18:46)
\$\$\$pvs-strategies
(defstep lemmas ()
(then (lemma "prop_StateS1")
(lemma "prop_StateS2")
(lemma "prop_StateS3")
(lemma "prop_StateRoot")
(lemma "pred_StateS1")
(lemma "pred_StateS2")
(lemma "pred_StateS3")
(lemma "pred_StateRoot")
(lemma "pred_Cond1")
(flatten)
)
""
""
)

(defmethod mu-atom? ((expr t) cstate) t)

\$\$\$eindig.pvs
% -----------------------------------------------------------------
% Voorbeeld die de door ons gedefinieerde statechart semantiek test
% -----------------------------------------------------------------

eindig: theory
begin

importing AbstractSyntax

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}

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

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

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

t3: Transition2 = (# source := StateS1, trigger := Event1, guard := EmptyC,
effect := EmptyA,  target  := StateS4 #)

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

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

% Tabel voor de transities, zelfde werkwijze als voor configuraties, we moeten rekening houden
% met de uitvoerbare kracht van pvs

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

% Een tweede transitierelatie
Conf2: Type = [# %conf: Conf,
v: V #]

s2, s02, s12: var Conf2
%     init2(s2)      : bool = member(StateS1, P(conf(s2)))
%     voorwaarde2(s2): bool = (member(StateS2, P(conf(s2)))) %or member(StateS3, P(conf(s2))))

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) = true and b(v) = 3

predStateS4(v:V): bool = a(v) = false 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)

importing ctlops[Conf2]

% tabel om met de juiste boolean terug te geven
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

relation6(s02, s12): bool = (exists(c:Conf,c2:Conf): Q(c,v(s02)) & Q(c2,v(s12)) &
(exists(tr:Trans): trigger(PT(tr)) = EmptyE &
member(source(PT(tr)), P(c)) &
member(target(PT(tr)), P(c2))))

init6(s2):       bool = a(v(s2)) = true and b(v(s2)) = 1
voorwaarde6(s2): bool = a(v(s2)) = true

theorem61: theorem init6(s2) => AG(relation6, voorwaarde6)(s2)
theorem62: theorem init6(s2) => EG(relation6, voorwaarde6)(s2)
theorem63: theorem init6(s2) => AF(relation6, voorwaarde6)(s2)
%     theorem64: theorem init6(s2) => EF(relation6, voorwaarde6)(s2)

end eindig

\$\$\$eindig.prf
(eindig
(P_TCC1 0
(P_TCC1-1 nil 3228626355 3228972667 ("" (cond-disjoint-tcc) nil nil)
proved nil 158 130 nil shostak))
(P_TCC2 0
(P_TCC2-1 nil 3228626355 3228972667 ("" (cond-coverage-tcc) nil nil)
proved nil 136 60 nil shostak))
(PT_TCC1 0
(PT_TCC1-1 nil 3228626355 3228972667 ("" (cond-disjoint-tcc) nil nil)
proved nil 102 80 nil shostak))
(PT_TCC2 0
(PT_TCC2-1 nil 3228626355 3228972667
("" (cond-coverage-tcc) (("" (postpone) nil nil)) nil) proved nil 71
50 nil shostak))
(theorem61 0
(theorem61-1 nil 3228626374 3228973165
("" (model-check :defs !!!) (("" (grind) nil nil)) nil) proved
((relation6 const-decl "bool" eindig nil)
(emptyset const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(P const-decl "configuration" eindig nil)
(C5 const-decl "configuration" eindig nil)
(C4 const-decl "configuration" eindig nil)
(C3 const-decl "configuration" eindig nil)
(C2 const-decl "configuration" eindig nil)
(C1 const-decl "configuration" eindig nil)
(PT const-decl "Transoutput" eindig nil)
(t4 const-decl "Transition2" eindig nil)
(t3 const-decl "Transition2" eindig nil)
(t2 const-decl "Transition2" eindig nil)
(t1 const-decl "Transition2" eindig nil)
(Q const-decl "bool" eindig nil)
(predC5 const-decl "bool" eindig nil)
(predStateS5 const-decl "bool" eindig nil)
(predC4 const-decl "bool" eindig nil)
(predStateS4 const-decl "bool" eindig nil)
(predC3 const-decl "bool" eindig nil)
(predStateS3 const-decl "bool" eindig nil)
(predC2 const-decl "bool" eindig nil)
(predStateS2 const-decl "bool" eindig nil)
(predC1 const-decl "bool" eindig nil)
(predStateS1 const-decl "bool" eindig nil)
(EX const-decl "bool" ctlops nil)
(voorwaarde6 const-decl "bool" eindig nil)
(EG const-decl "pred[state]" ctlops nil)
(V type-eq-decl nil eindig nil) (Conf2 type-eq-decl nil eindig nil)
(init6 const-decl "bool" eindig nil))
490919 2770 t shostak))
(theorem62 0
(theorem62-1 nil 3228626387 3228968905
("" (model-check :defs !!!) (("" (grind) nil nil)) nil) unchecked
((relation6 const-decl "bool" eindig nil)
(emptyset const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(P const-decl "configuration" eindig nil)
(C5 const-decl "configuration" eindig nil)
(C4 const-decl "configuration" eindig nil)
(C3 const-decl "configuration" eindig nil)
(C2 const-decl "configuration" eindig nil)
(C1 const-decl "configuration" eindig nil)
(PT const-decl "Transoutput" eindig nil)
(t4 const-decl "Transition2" eindig nil)
(t3 const-decl "Transition2" eindig nil)
(t2 const-decl "Transition2" eindig nil)
(t1 const-decl "Transition2" eindig nil)
(Q const-decl "bool" eindig nil)
(predC5 const-decl "bool" eindig nil)
(predStateS5 const-decl "bool" eindig nil)
(predC4 const-decl "bool" eindig nil)
(predStateS4 const-decl "bool" eindig nil)
(predC3 const-decl "bool" eindig nil)
(predStateS3 const-decl "bool" eindig nil)
(predC2 const-decl "bool" eindig nil)
(predStateS2 const-decl "bool" eindig nil)
(predC1 const-decl "bool" eindig nil)
(predStateS1 const-decl "bool" eindig nil)
(voorwaarde6 const-decl "bool" eindig nil)
(EX const-decl "bool" ctlops nil)
(AX const-decl "pred[state]" ctlops nil)
(V type-eq-decl nil eindig nil) (Conf2 type-eq-decl nil eindig nil)
(init6 const-decl "bool" eindig nil))
16345 1600 t shostak))
(theorem63 0
(theorem63-1 nil 3228640628 3228646353
("" (model-check :defs !) nil nil) unchecked
((relation6 const-decl "bool" eindig nil)
(emptyset const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(P const-decl "configuration" eindig nil)
(C5 const-decl "configuration" eindig nil)
(C4 const-decl "configuration" eindig nil)
(C3 const-decl "configuration" eindig nil)
(C2 const-decl "configuration" eindig nil)
(C1 const-decl "configuration" eindig nil)
(PT const-decl "Transoutput" eindig nil)
(t4 const-decl "Transition2" eindig nil)
(t3 const-decl "Transition2" eindig nil)
(t2 const-decl "Transition2" eindig nil)
(t1 const-decl "Transition2" eindig nil)
(Q const-decl "bool" eindig nil)
(predC5 const-decl "bool" eindig nil)
(predStateS5 const-decl "bool" eindig nil)
(predC4 const-decl "bool" eindig nil)
(predStateS4 const-decl "bool" eindig nil)
(predC3 const-decl "bool" eindig nil)
(predStateS3 const-decl "bool" eindig nil)
(predC2 const-decl "bool" eindig nil)
(predStateS2 const-decl "bool" eindig nil)
(predC1 const-decl "bool" eindig nil)
(predStateS1 const-decl "bool" eindig nil)
(voorwaarde6 const-decl "bool" eindig nil)
(EX const-decl "bool" ctlops nil)
(EG const-decl "pred[state]" ctlops nil)
(AF const-decl "pred[state]" ctlops nil)
(Conf type-decl nil eindig nil) (V type-eq-decl nil eindig nil)
(Conf2 type-eq-decl nil eindig nil)
(init6 const-decl "bool" eindig nil))
17158 1330 t shostak))
(theorem64 0
(theorem64-1 nil 3228626361 3228969120
("" (model-check :defs !!!) nil nil) unchecked
((Conf type-decl nil eindig nil)
(init6 const-decl "bool" eindig nil)
(Conf2 type-eq-decl nil eindig nil) (V type-eq-decl nil eindig nil)
(EF const-decl "pred[state]" ctlops nil)
(EU const-decl "pred[state]" ctlops nil)
(voorwaarde6 const-decl "bool" eindig nil)
(K_conversion const-decl "T1" K_conversion nil)
(EX const-decl "bool" ctlops nil)
(predStateS1 const-decl "bool" eindig nil)
(predC1 const-decl "bool" eindig nil)
(predStateS2 const-decl "bool" eindig nil)
(predC2 const-decl "bool" eindig nil)
(predStateS3 const-decl "bool" eindig nil)
(predC3 const-decl "bool" eindig nil)
(predStateS4 const-decl "bool" eindig nil)
(predC4 const-decl "bool" eindig nil)
(predStateS5 const-decl "bool" eindig nil)
(predC5 const-decl "bool" eindig nil)
(Q const-decl "bool" eindig nil)
(t1 const-decl "Transition2" eindig nil)
(t2 const-decl "Transition2" eindig nil)
(t3 const-decl "Transition2" eindig nil)
(t4 const-decl "Transition2" eindig nil)
(PT const-decl "Transoutput" eindig nil)
(C1 const-decl "configuration" eindig nil)
(C2 const-decl "configuration" eindig nil)
(C3 const-decl "configuration" eindig nil)
(C4 const-decl "configuration" eindig nil)
(C5 const-decl "configuration" eindig nil)
(P const-decl "configuration" eindig nil)
(member const-decl "bool" sets nil)
(emptyset const-decl "set" sets nil)
(relation6 const-decl "bool" eindig nil))
8884 890 t shostak)))

\$\$\$AbstractSyntax.pvs
% Met behulp van deze theory kunnen we alle mogelijke gegevens
% van een UML statechart opnemen in een PVS file.
% Werkwijze: UML mappen naar XML en XML mappen naar PVS
% Doel: zo generiek mogelijk werken.

% Gevraagd: is het mogelijk om te werken met niet-gedefinieerde types
% Problemen: ontstaan bij die niet gedefinieerde types.

AbstractSyntax: THEORY
BEGIN

% Een top komt overeen met een bepaalde toestand uit het toestandsdiagramma
% Deze top wordt gedefinieerd als een niet ledig type.

Vertex: TYPE+
EmptyV: Vertex
Vertexen: type = finite_set[Vertex]

% Guard conditions
Condition: TYPE+
EmptyC: Condition
Conditions: type = finite_set[Condition]

% Events
% XML model duidt de verschillende elementen samen met hun type aan
% We maken er wel types zdd dat we die voor ieder statechart kunnen gebruiken

Event: TYPE+
SignalEvent: type = finite_set[Event]
CallEvent  : type = finite_set[Event]
TimeEvent  : type = finite_set[Event]
ChangeEvent: type = finite_set[Event]
EmptyE: Event
Events: type = finite_set[Event]

% Actions
Action: TYPE+
EmptyA: Action
Actions: type = finite_set[Action]

% States
% Er wordt een onderscheid gemaakt tussen de pseudo en de niet-pseudostates.
State: type = finite_set[Vertex]

% Pseudo states
PseudoState: type = finite_set[Vertex]
% een verzameling bestaande uit de volgende pseudo-states
Initial    : type = finite_set[Vertex]
FinalState : type = finite_set[Vertex]
DeepH      : type = finite_set[Vertex]
Join       : type = finite_set[Vertex]
Fork       : type = finite_set[Vertex]
Junction   : type = finite_set[Vertex]
Choice     : type = finite_set[Vertex]

% Synch states
SynchState: type = finite_set[Vertex]

% Bound attribute associated to a synch state
sync: VAR SynchState
bound(sync): nat

StubState: type = finite_set[Vertex]

SubmachineState: type = finite_set[Vertex]

% Stereotype are used for transition out of the initial state

Stereotype: TYPE = {create, no_stereo}
stereotype(e: Event): Stereotype

% Context of a state machine
Context: TYPE+ = {behavioral, classifier}

% Transitions
Transition: TYPE+ = [# source : Vertex,
trigger: Event,
guard  : Condition,
effect : Action,
target : Vertex
#]

EmptyTr: Transition = (# source := EmptyV,
trigger:= EmptyE,
guard  := EmptyC,
effect := EmptyA,
target := EmptyV
#)
Transitions: type = finite_set[Transition]

% Bijkomende definities/functies die we gebruiken om de mapping van het statechart
% te kunnen voltooien. Er zijn twee mogelijkheden om dit te realiseren: ofwel maken
% we gebruik van functies, ofwel definieren we toestanden aan de hand van een record

x : var Vertex  % variabele, want voor iedere top moet dit gedefinieerd worden

% 1. De verzameling van kinderen van een top op het eerste niveau. Deze informatie
%    kunnen we rechtstreeks uit de XML file halen.

dsubvertex(x): finite_set[Vertex]

% 2. De verzameling van alle kinderen van een top (op meerdere niveaus). Ook deze informatie
%    kan rechtstreeks uit de XML file gehaald worden

subvertex(x) : finite_set[Vertex]
subvertexInc(x) : finite_set[Vertex]

% 3. De defaulttoestanden voor iedere toestand aanduiden.
%    Merk op dat we de default toestand enkel definieren voor hierarchische sequentiele toestanden
%    Het definieren van de defaultstate kan door de parser gebeuren.
defaultstate(x) : Vertex

% 4. Voor hierarchische toestanden aanduiden of al dan niet concurrent
statekind: type = {andstate, orstate, simplestate}
typefunction(x) : statekind

% 5. Voor sequentiele toestanden bijhouden of de toestand al dan niet een historyconnector bevat
%    want dit zorgt voor een verschil in opbouw van configuraties. Een booleaanse waarde is hiervoor
%    meer dan voldoende.
history: type = {shallow, deep, none}
cHistory(x): history

% Representation of a statechart or state machine
% We maken hiervoor gebruik van de vooraf gedefinieerde types.
StateMachine: TYPE+ =
[# State: State,
StubState: StubState,
SynchState: SynchState,
Initial: Initial,
Choice: Choice,
DeepH: DeepH,
Join: Join,
Fork: Fork,
Junction: Junction,
FinalState: FinalState,
SubmachineState: SubmachineState,
PseudoState: PseudoState,
Vertex: Vertexen,
CallEvent: CallEvent,
TimeEvent: TimeEvent,
ChangeEvent: ChangeEvent,
SignalEvent: SignalEvent,
Event: Events,
Action: Actions,
Condition: Conditions,
Transition: Transitions,
Root: Vertex,
Context: Context
#]

EmptySm: StateMachine = (# State:= singleton(EmptyV),
StubState:= emptyset,
SynchState:= emptyset,
Initial:= emptyset,
Choice:= emptyset,
DeepH:= emptyset,
Join:= emptyset,
Fork:= emptyset,
Junction:= emptyset,
FinalState:= emptyset,
SubmachineState:= emptyset,
PseudoState:= emptyset,
Vertex:= singleton(EmptyV),
CallEvent:= emptyset,
TimeEvent:= emptyset,
ChangeEvent:= emptyset,
SignalEvent:= emptyset,
Event:= singleton(EmptyE),
Action:= singleton(EmptyA),
Condition:= singleton(EmptyC),
Transition:= singleton(EmptyTr),
Root:= EmptyV,
Context:= classifier
#)

END AbstractSyntax

```