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

*To*: Sara Van Langenhove <Sara.VanLangenhove@rug.ac.be>*Subject*: Re: intersection, implication, predicate problem, specific example problem*From*: Sam Owre <owre@csl.sri.com>*Date*: Tue, 11 Feb 2003 12:27:10 -0800*cc*: support PVS <pvs-help@csl.sri.com>, owre@csl.sri.com*In-Reply-To*: Your message of "Tue, 11 Feb 2003 08:01:01 +0100." <Pine.GSO.4.31.0302110739130.23520-100000@allserv.rug.ac.be>*Sender*: pvs-help-owner@csl.sri.com

Hi Sara, Could you send me a dump of your specs? M-x dump-pvs-files can be used for this, or you can send a tar file, as long as all the imported theories are included. I want to check if this is a bug, and if not, see if I can find the explanation. Thanks, Sam Owre <Owre@csl.sri.com> Computer Science Lab, SRI International Tel: (650) 859-5114 333 Ravenswood Avenue FAX: (650) 859-2844 Menlo Park, CA 94025 USA WWW: http://www.csl.sri.com/~owre > 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,

**References**:**intersection, implication, predicate problem, specific exampleproblem***From:*Sara Van Langenhove <Sara.VanLangenhove@rug.ac.be>

- Prev by Date:
**intersection, implication, predicate problem, specific exampleproblem** - Next by Date:
**"<" on a subset of nat is well_founded** - Prev by thread:
**intersection, implication, predicate problem, specific exampleproblem** - Next by thread:
**the "the" operator** - Index(es):