[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: strange problem with EG operator (fwd)
same message but with the correct attachement (the previous contained an
error)
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)), e) &
member(source(PT(tr)), P(bronC)) &
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