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

intersection, implication, predicate problem, specific exampleproblem



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