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

*To*: support PVS <pvs-help@csl.sri.com>*Subject*: Re: strange problem with EG operator (fwd)*From*: Sara Van Langenhove <svlangen@cage.rug.ac.be>*Date*: Thu, 8 May 2003 11:15:10 +0200 (CEST)*Sender*: pvs-help-owner@csl.sri.com

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

- Prev by Date:
**Re: strange problem with EG operator** - Next by Date:
**[Repost] Instantiating multiple theories simultaneously** - Prev by thread:
**Re: [Reposting again] Re: [Repost] Instantiating multiple theories simultaneously** - Next by thread:
**strange problem with EG operator** - Index(es):