# something I`m missing to let it work

```Hi,

My problem concerns rewrite rules combined with a transition relation.

(dumpfile included)

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

I have three list, each containing one different state.

Voor each state with an undefined type I defined a predicate as a rewrite
rule. I thought it was useful to work with rewrite rule...
For each configuration I also defined a predicate but in this case a
rewrite rule isn`t necessary.

pred(v:Vertex): pred[V]
pred(c:configuration, v:V): bool = forall(x:Vertex): member(x,c) and pred(x)(v)

pred_StateS1: axiom pred(StateS1) = lambda (v:V): a(v) = true and b(v) = true
pred_StateS2: axiom pred(StateS2) = lambda (v:V): a(v) = false and b(v) = true
pred_StateS3: axiom pred(StateS3) = lambda (v:V): a(v) = false and b(v) = true
pred_StateRoot: axiom pred(StateRoot) = lambda (v:V): true

Now consider the following transition relation with a very simple and
trivial theorem.

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

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

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

Conf2: Type = [# conf: Conf, v: V #]
s2, s02, s12: var Conf2
relation6(s02, s12): bool = (exists(tr:Trans): member(source(PT(tr)), P(conf(s02))) &
member(target(PT(tr)), P(conf(s12)))) &
pred(P(conf(s02)), v(s02)) &
pred(P(conf(s12)), v(s12))

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

theorem61: theorem init6(s2) => EF(relation6, voorwaarde6)(s2)

When model-checking the theorem it seems that the model-checker has
problems with the predicates which are however installed as rewrite rules.
The modelchecker returns a goal in mucalculusformat.
I`ve tried the three options in the defs argument but without any success.

Does anyone know how I can get this work? Or am i doing something wrong?

Thanks,

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)

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

rewriting: theory
begin

importing AbstractSyntax

V: Type = [# a: bool, b:bool  #]

abs_V: Type

StateS1: Vertex
StateS2: Vertex
StateS3: Vertex
StateRoot: Vertex

configuration: type = finite_set[Vertex]

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

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

pred(v:Vertex): pred[V]
pred(c:configuration, v:V): bool = forall(x:Vertex): member(x,c) and pred(x)(v)

pred_StateS1: axiom pred(StateS1) = lambda (v:V): a(v) = true and b(v) = true
pred_StateS2: axiom pred(StateS2) = lambda (v:V): a(v) = false and b(v) = true
pred_StateS3: axiom pred(StateS3) = lambda (v:V): a(v) = false and b(v) = true
pred_StateRoot: axiom pred(StateRoot) = lambda (v:V): true

auto_rewrite+ pred_StateS1
auto_rewrite+ pred_StateS2
auto_rewrite+ pred_StateS3
auto_rewrite+ pred_StateRoot

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

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

Conf2: Type = [# conf: Conf, v: V #]
s2, s02, s12: var Conf2
relation6(s02, s12): bool = (exists(tr:Trans): member(source(PT(tr)), P(conf(s02))) &
member(target(PT(tr)), P(conf(s12)))) &
pred(P(conf(s02)), v(s02)) &
pred(P(conf(s12)), v(s12))

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

theorem61: theorem init6(s2) => EF(relation6, voorwaarde6)(s2)

end rewriting

\$\$\$rewrite.prf
(rewriting
(P_TCC1 0
(P_TCC1-1 nil 3228540637 3228541359 ("" (cond-disjoint-tcc) nil nil)
proved nil 78 30 nil shostak))
(P_TCC2 0
(P_TCC2-1 nil 3228540637 3228541359 ("" (cond-coverage-tcc) nil nil)
proved nil 64 50 nil shostak))
(PT_TCC1 0
(PT_TCC1-1 nil 3228540637 3228541359 ("" (cond-disjoint-tcc) nil nil)
proved nil 14 10 nil shostak))
(PT_TCC2 0
(PT_TCC2-1 nil 3228540637 3228541359
("" (cond-coverage-tcc) (("" (postpone) nil nil)) nil) unfinished
nil 82 60 nil shostak))
(theorem61 0
(theorem61-1 nil 3228541365 3228541375
("" (model-check)
(("" (grind)
(("1" (postpone) nil nil) ("2" (postpone) nil nil)
("3" (postpone) nil nil))
nil))
nil)
unfinished nil 10290 1510 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

```