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

*To*: support PVS <pvs-help@csl.sri.com>*Subject*: existskwantor problem*From*: Sara Van Langenhove <Sara.VanLangenhove@rug.ac.be>*Date*: Fri, 21 Feb 2003 10:29:37 +0100 (MET)*Sender*: pvs-help-owner@csl.sri.com

Hello, I'm working on a problem which acts on subsets of some specific sets. Here is an simplified example of my problem: First of all I have defined my own types and some specific constants of that type: State: Type+ StateS1: State StateS2: State StateS3: State StateRoot: State After that, I need a set that contains all defined stateconstants. StateSet: type+ = finite_set[State] I also need a record which contains two elements: - the first member: is the set of all stateconstants - the second member: defines a special state among those stateconstants StateRecord : type+ = [# States : StateSet, Root : State #] Define a specific record with the above constants sm : StateRecord = (# States := add(StateS1, add(StateS2, add(StateS3, add(StateRoot, emptyset)))), Root := StateRoot #) Now I define another set of states, which contains or must contain a subset of the set of all stateconstants, but the Root always has to be a member of this set. AState : type+ = finite_set[State] C1 : AState = add(StateS1, add(StateRoot, emptyset)) Because my problem has to search for such sets and it is not very good to define such sets (like C1) by myself because there can be to many (and it must be used with model-checking) And now the problem arises: The first theorem ("existstheorem") returns a QED. So there exists a correctly formed subset which is C1. If I reject the second argument (c=C1) I expect also a QED because we know there exists a correctly formed subset. (C1 or another subset that contains the RootState). However this QED is not generated. existstheorem: theorem exists(c:AState | subset?(c, States(sm))): member(Root(sm), c) and c=C1 existstheorem2: theorem exists(c:AState | subset?(c, States(sm))): member(Root(sm), c) What am I missing? How can I force PVS to return a QED. I also included the dumpfile. Thx for the help, Sara

%% PVS Version 3.0 %% 6.2 [Linux (x86)] (Dec 19, 2002 3:09) $$$problem.pvs problem : theory begin % Define some specific types and elements of that type State: Type+ StateS1: State StateS2: State StateS3: State StateRoot: State % Define a set that contains State-elements StateSet: type+ = finite_set[State] % Define the following record StateRecord : type+ = [# States : StateSet, Root : State #] % Define a specific record sm : StateRecord = (# States := add(StateS1, add(StateS2, add(StateS3, add(StateRoot, emptyset)))), Root := StateRoot #) % Define another sets of states AState : type+ = finite_set[State] C1 : AState = add(StateS1, add(StateRoot, emptyset)) % Now I want to check the following theorem % Does there exists a set, subset of States, which contains the RootState? % (it must be automatically be found...) % The first theorem returns QED ... doest such a set can be found % The second theorem doesn`t return that. However we know that such a set exists, so % I expect also a QED. What am I missing here? existstheorem: theorem exists(c:AState | subset?(c, States(sm))): member(Root(sm), c) and c=C1 existstheorem2: theorem exists(c:AState | subset?(c, States(sm))): member(Root(sm), c) end problem $$$problem.prf (problem (existstheorem 0 (existstheorem-1 nil 3223270809 3223270893 ("" (grind) nil nil) unchecked ((C1 const-decl "AState" problem nil) (member const-decl "bool" sets nil) (sm const-decl "StateRecord" problem nil) (emptyset const-decl "set" sets nil) (add const-decl "(nonempty?)" sets nil) (subset? const-decl "bool" sets nil)) 7765 170 t shostak)) (existstheorem2 0 (existstheorem2-1 nil 3223270991 3223270995 ("" (grind) nil nil) proved ((sm const-decl "StateRecord" problem nil) (member const-decl "bool" sets nil) (emptyset const-decl "set" sets nil) (add const-decl "(nonempty?)" sets nil) (subset? const-decl "bool" sets nil) (C1 const-decl "AState" problem nil)) 3234 350 t shostak)))

- Prev by Date:
**Re: Proof of override expressions** - Next by Date:
**Induction derivation tree** - Prev by thread:
**Induction derivation tree** - Next by thread:
**Proof of override expressions** - Index(es):