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

*To*: support PVS <pvs-help@csl.sri.com>*Subject*: intersection, implication, predicate problem, specific exampleproblem*From*: Sara Van Langenhove <Sara.VanLangenhove@rug.ac.be>*Date*: Tue, 11 Feb 2003 08:01:01 +0100 (MET)*Sender*: pvs-help-owner@csl.sri.com

Hi, I would like to prove the following easy theorem to know if the predicate isInitConf? is correctly defined. test: thereom isInitConf?(C1) C1 : is a finite_set of elements (vertexen) and is defined as C1 : finite_set[Vertex] = add(Root(sm), add(StateS1, emptyset)) The predicate isInitConf? checks if the finite_set is a legal initial configuration and is defined as follows: isInitConf?(C): bool = member(Root(sm), C) and forall(x:(C)): (not isSimple?(x) => (isConcurrent?(x) => subset?(dsubstate(x), InitConf)) and (isSequential?(x) => intersection(InitConf,dsubstate(x)) = singleton(defaultstate(x))))) As you can see, this predicate uses some other predicates to check if some state (from a statechart) is concurrent, sequential, or simple). Defaultstate(x) returns the defaultstate of sequential state, dsubstate(x) returns the set of states a composite (concurrent, sequential) state contains. The problem arises when I want to check this predicate against a specific set and this problem is quite anoying because I have to use it quite a lot. Example: ------- C1 : finite_set[Vertex] = add(Root(sm), add(StateS1, emptyset)) Root(sm): sequential state defaultstate(Root(sm)) = StateS1 dsubstate(x) : finite_set[Vertex] = add(Root(sm), add(StateS1, add(StateS2,emptyset))) (these definitions are defined als rewrite rules) As you can see: C1 is a legal initial configuration and PVS states that to. To know if this "QED" is not just luck I define a new set of states C2 : finite_set[Vertex] = add(Root(sm), add(StateS1, add(StateS2,emptyset))) C2 cannot be an initial configuration because StateS2 is a member of the set. And the consequents of the two implications in the predicate isInitConf have to return false. (the whole predicate must then also be false). The strange is that PVS returns here also a QED and thus says that C2 is also an initial configuration which is not correct. (the intersection is not a singleton ...) I do not see where this problem comes from. Why does PVS returns a QED for the C2 set if one can easily see this is not correct? Could anyone help me? Thanks a lot, Sara

- Prev by Date:
**Re: the "the" operator** - Next by Date:
**Re: intersection, implication, predicate problem, specific example problem** - Prev by thread:
**Re: intersection, implication, predicate problem, specific example problem** - Next by thread:
**the "the" operator** - Index(es):