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

problem with transition relation (model-checking)



Hi,

To demonstrate the problem I`ve created a little example. (see dumpfile
for a complete specification)
Suppose we have three configurations each containing two states.
There is one state the same for alle the configurations but that is not
important here.

C1 = {StateRoot, StateS1}
C2 = {StateRoot, StateS2}
C3 = {StateRoot, StateS3}

With these three configurations I`ve created a finite type (so i can use
the model-checker and not the abstracted version). Therefore I used tabled
and enumerated types.

Conf: type = {C1, C2, C3}
conf : var Conf
confoutput : type = configuration
P(conf): confoutput = table
   |[ conf = C1 | conf = C2 | conf = C3 ]|
   | C1         | C2        | C3        ||
   endtable
Conf2: Type = [# conf: Conf, v: V #]

In the specification there are also transitions from one state to another
and thus also from a configuration to another.

t1: Transition = (# source := StateS1, trigger := EmptyE, guard := Cond1,
                        effect := EmptyA,  target  := StateS2 #)

t2: Transition = (# source := StateS1, trigger := EmptyE, guard := EmptyC,
                        effect := EmptyA,  target  := StateS3 #)

If you look closely you can see that C1 -> C2 with transition t1 and C1 ->
C3 with transition t2.

With these elements I want to check some simple properties in CTL.
Therefore I`ve written down two necessary predicates namely:

% The initial predicate states that each initial configuration contains StateS1
init2(s2)      : bool = member(StateS1, P(conf(s2)))
% The check predicate states that each other configuration contains StateS2 or StateS3
check(s2): bool = (member(StateS2, P(conf(s2))) or member(StateS3, P(conf(s2))))

the first transition relation gives no problems for proving four
different CTL properties (EF, AF, EX, AX). You can see it quite easily
from our specification

% Relation3 is a transitionrelation between two configurations
% More detailed: C1 -> C2, C1 -> C3 but no other relations between two configurations
     relation3(s02, s12): bool = (member(source(t1), P(conf(s02))) &
                                  member(target(t1), P(conf(s12)))) or
                                 (member(source(t2), P(conf(s02))) &
                                  member(target(t2), P(conf(s12))))

     theorem31: theorem init2(s2) implies EF(relation3, check)(s2) %true as expected
     theorem32: theorem init2(s2) implies EX(relation3, check)(s2) %true as expected
     theorem33: theorem init2(s2) implies AF(relation3, check)(s2) %true as expected
     theorem34: theorem init2(s2) implies AX(relation3, check)(s2) %true as expected

If there are however a lot of configurations and transitions, writing down
all possible transitions in the relation is not quite usefull. Therefore
I`ve created a new relation which says the same a the first one but
captures all possible cases. Thus this is a more compact version. For the
same properties I expect the same results but this is not the the case

     relation4(s02, s12): bool = exists(tr:(Transition(sm))): member(source(tr), P(conf(s02))) &
                            member(target(tr), P(conf(s12)))

     theorem41: theorem init2(s2) => EF(relation4, check)(s2) % not true as not expected
     theorem42: theorem init2(s2) => AF(relation4, check)(s2) % not true as not expected
     theorem43: theorem init2(s2) => AX(relation4, check)(s2) % true ... but
     theorem44: theorem init2(s2) => EX(relation4, check)(s2) % not true as not expected

I have the following questions concerning this example...

I do not understand why the model-checker is not capable to prove the
theorems4x. Does anyone know the reason of this failure?
How can I force the model-checker to prove this theorems?
how is the existskwantor implemented in PVS? (as a choice function, as a
backtrackingfunction until an element is found which satisfy the property
or as ... ?)

Thanks a lot for the explanation. It would help me a lot.

Sara


%% PVS Version 3.1
%% 6.2 [Linux (x86)] (Feb 14, 2003 18:46)
$$$pvs-strategies
(defstep lemmas ()
                 (then (lemma "prop_StateS1")
                       (lemma "prop_StateS2")
                       (lemma "prop_StateS3")
                       (lemma "prop_StateRoot")
                       (lemma "pred_StateS1")
                       (lemma "pred_StateS2")
                       (lemma "pred_StateS3")
                       (lemma "pred_StateRoot") 
                       (lemma "pred_Cond1")                    
                       (flatten)                       
                  )
          ""
          ""
)

(defmethod mu-atom? ((expr t) cstate) t)

$$$general.pvs
% -----------------------------------------------------------------
% Voorbeeld die de door ons gedefinieerde statechart semantiek test
% -----------------------------------------------------------------

general: theory
  begin
   
    importing AbstractSyntax
 
    V: Type = [# var1: bool  #] 

    StateS1: Vertex 
    StateS2: Vertex 
    StateS3: Vertex 
    StateRoot: Vertex 

    Cond1: Condition

    SmRoot: Vertex = StateRoot 
    SmState: State = add(StateS1, add(StateS2, add(SmRoot, emptyset)))

    t1: Transition = (# source := StateS1, trigger := EmptyE, guard := Cond1, 
                        effect := EmptyA,  target  := StateS2 #)

    t2: Transition = (# source := StateS1, trigger := EmptyE, guard := EmptyC, 
                        effect := EmptyA,  target  := StateS3 #)
    
    SmTransition: Transitions = add(t2, add(t1, emptyset))

    sm: StateMachine = (# State := SmState,
           		  StubState := emptyset, 
                          SynchState := emptyset, 
                          Initial := emptyset,
                          Choice := emptyset,
                          DeepH := emptyset,
                          Join := emptyset,
                          Fork := emptyset,
                          Junction := emptyset,
                          FinalState := emptyset,
                          SubmachineState := emptyset,
                          PseudoState := emptyset,
                          Vertex := SmState,
           		  CallEvent := emptyset,
		          TimeEvent := emptyset,
		          ChangeEvent := emptyset,
		          SignalEvent := emptyset,
		          Event := emptyset, 
		          Action := emptyset,
		          Condition := emptyset,
		          Transition := SmTransition,
		          Root := SmRoot,
		          Context := behavioral         
		        #)

    importing semantiek[sm, V]    

    C1: configuration = add(Root(sm), add(StateS1, emptyset))
    C2: configuration = add(Root(sm), add(StateS2, emptyset))
    C3: configuration = add(Root(sm), add(StateS3, emptyset))

     Conf: type = {C1, C2, C3} 
     conf : var Conf

     confoutput : type = configuration

     P(conf): confoutput = table 
       |[ conf = C1 | conf = C2 | conf = C3 ]|
       | C1         | C2        | C3        ||
     endtable

     Conf2: Type = [# conf: Conf, v: V #]

     s2, s02, s12: var Conf2
     
     % The initial predicate states that each initial configuration contains StateS1
     init2(s2)      : bool = member(StateS1, P(conf(s2))) 
     % The check predicate states that each other configuration contains StateS2 or StateS3     
     check(s2): bool = (member(StateS2, P(conf(s2))) or member(StateS3, P(conf(s2))))

     % Relation3 is a transitionrelation between two configurations 
     % More detailed: C1 -> C2, C1 -> C3 but no other relations between two configurations
     relation3(s02, s12): bool = (member(source(t1), P(conf(s02))) &
                                  member(target(t1), P(conf(s12)))) or 
                                 (member(source(t2), P(conf(s02))) &
                                  member(target(t2), P(conf(s12))))
                                 
     theorem31: theorem init2(s2) implies EF(relation3, check)(s2) %true as expected
     theorem32: theorem init2(s2) implies EX(relation3, check)(s2) %true as expected 
     theorem33: theorem init2(s2) implies AF(relation3, check)(s2) %true as expected
     theorem34: theorem init2(s2) implies AX(relation3, check)(s2) %true as expected
 
     % Relation4 generalizes relation3.
     % There exists a relation between two configurations if there is a transition (tr) from the first
     % one two the second one. 
     % In this way we don`t have to write down all possibilities. 
     % The properties to be checked must also be true for this relation.
     relation4(s02, s12): bool = exists(tr:(Transition(sm))):  member(source(tr), P(conf(s02))) &
                                                               member(target(tr), P(conf(s12))) 
      
     theorem41: theorem init2(s2) => EF(relation4, check)(s2) % not true as not expected
     theorem42: theorem init2(s2) => AF(relation4, check)(s2) % not true as not expected
     theorem43: theorem init2(s2) => AX(relation4, check)(s2) % true ... but 
     theorem44: theorem init2(s2) => EX(relation4, check)(s2) % not true as not expected      

  end general

$$$general.prf
(general
 (P_TCC1 0
  (P_TCC1-1 nil 3228038167 3228038167 ("" (cond-disjoint-tcc) nil nil)
   proved nil 88 60 nil shostak))
 (P_TCC2 0
  (P_TCC2-1 nil 3228038167 3228038167 ("" (cond-coverage-tcc) nil nil)
   proved nil 72 50 nil shostak))
 (theorem41 0
  (theorem41-1 nil 3228038515 3228038577
   ("" (model-check)
    (("" (grind) (("1" (postpone) nil nil) ("2" (postpone) nil nil))
      nil))
    nil)
   unfinished nil 62240 2510 t shostak))
 (theorem42 0
  (theorem42-1 nil 3228038582 3228038609
   ("" (model-check)
    (("" (grind)
      (("1" (postpone) nil nil) ("2" (postpone) nil nil)
       ("3" (postpone) nil nil) ("4" (postpone) nil nil)
       ("5" (postpone) nil nil) ("6" (postpone) nil nil)
       ("7" (postpone) nil nil) ("8" (postpone) nil nil)
       ("9" (postpone) nil nil) ("10" (postpone) nil nil)
       ("11" (postpone) nil nil) ("12" (postpone) nil nil))
      nil))
    nil)
   unfinished nil 27001 3370 t shostak))
 (theorem43 0
  (theorem43-1 nil 3228038620 3228038630
   ("" (model-check) (("" (grind) nil nil)) nil) proved
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (Actions type-eq-decl nil AbstractSyntax nil)
    (CallEvent type-eq-decl nil AbstractSyntax nil)
    (ChangeEvent type-eq-decl nil AbstractSyntax nil)
    (Choice type-eq-decl nil AbstractSyntax nil)
    (Conditions type-eq-decl nil AbstractSyntax nil)
    (Context type-decl nil AbstractSyntax nil)
    (DeepH type-eq-decl nil AbstractSyntax nil)
    (Events type-eq-decl nil AbstractSyntax nil)
    (FinalState type-eq-decl nil AbstractSyntax nil)
    (Fork type-eq-decl nil AbstractSyntax nil)
    (Initial type-eq-decl nil AbstractSyntax nil)
    (Join type-eq-decl nil AbstractSyntax nil)
    (Junction type-eq-decl nil AbstractSyntax nil)
    (PseudoState type-eq-decl nil AbstractSyntax nil)
    (Vertex nonempty-type-decl nil AbstractSyntax nil)
    (SignalEvent type-eq-decl nil AbstractSyntax nil)
    (State type-eq-decl nil AbstractSyntax nil)
    (StubState type-eq-decl nil AbstractSyntax nil)
    (SubmachineState type-eq-decl nil AbstractSyntax nil)
    (SynchState type-eq-decl nil AbstractSyntax nil)
    (TimeEvent type-eq-decl nil AbstractSyntax nil)
    (Transitions type-eq-decl nil AbstractSyntax nil)
    (Vertexen type-eq-decl nil AbstractSyntax nil)
    (StateMachine nonempty-type-eq-decl nil AbstractSyntax nil)
    (Action nonempty-type-decl nil AbstractSyntax nil)
    (Condition nonempty-type-decl nil AbstractSyntax nil)
    (Event nonempty-type-decl nil AbstractSyntax nil)
    (Transition nonempty-type-eq-decl nil AbstractSyntax nil)
    (add const-decl "(nonempty?)" sets nil)
    (member const-decl "bool" sets nil)
    (emptyset const-decl "set" sets nil)
    (relation4 const-decl "bool" general nil)
    (check const-decl "bool" general nil)
    (EX const-decl "bool" ctlops nil)
    (AX const-decl "pred[state]" ctlops nil)
    (init2 const-decl "bool" general nil)
    (P const-decl "confoutput" general nil)
    (C3 const-decl "configuration" general nil)
    (C2 const-decl "configuration" general nil)
    (C1 const-decl "configuration" general nil)
    (sm const-decl "StateMachine" general nil)
    (SmTransition const-decl "Transitions" general nil)
    (t1 const-decl "Transition" general nil)
    (t2 const-decl "Transition" general nil)
    (SmState const-decl "State" general nil)
    (SmRoot const-decl "Vertex" general nil))
   9261 1790 t shostak))
 (theorem44 0
  (theorem44-1 nil 3228038643 3228038656
   ("" (model-check)
    (("" (grind)
      (("1" (postpone) nil nil) ("2" (postpone) nil nil)
       ("3" (postpone) nil nil) ("4" (postpone) nil nil)
       ("5" (postpone) nil nil) ("6" (postpone) nil nil)
       ("7" (postpone) nil nil) ("8" (postpone) nil nil))
      nil))
    nil)
   unfinished nil 12774 1580 t shostak)))