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

Re: intersection, implication, predicate problem, specific example problem

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.


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,