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

strange problem with EG operator



Hi,

I have the following simple state space:

(details are in the attachement)

C1 with a = true, b = 1
C2 with a = true, b = 2
C3 with a = true, b = 3

and from C1 I can go to C2 and from C2 I can go to C3

It is very trivial that there exists a path for which a is true in each
node. However for PVS this is not the case but I do not see where I make a
mistake. Can anyone explain to me why this is the case?

(the AG operator works fine, the AF not because it is implemented in
function of the EG operator)

Thanks a lot for the help,

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)

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

eindig: theory
  begin
   
    importing AbstractSyntax

    som: type = {1,2,3,4,5,6,7,8}
 
    V: Type = [# a: bool, b:som  #] 

    Vertex2: type = {StateS1, StateS2, StateS3, StateS4, StateS5, StateRoot}    
    Events: type = {EmptyE, Event1}

    Transition2: TYPE+ = [# source : Vertex2, 
                           trigger: Events, 
                           guard  : Condition, 
                           effect : Action, 
                           target : Vertex2 
                         #]

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

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

    t3: Transition2 = (# source := StateS1, trigger := Event1, guard := EmptyC, 
                         effect := EmptyA,  target  := StateS4 #)

    t4: Transition2 = (# source := StateS4, trigger := Event1, guard := EmptyC, 
                         effect := EmptyA,  target  := StateS5 #)

    configuration: type = finite_set[Vertex2]

    C1: configuration = add(StateRoot, add(StateS1, emptyset))
    C2: configuration = add(StateRoot, add(StateS2, emptyset))
    C3: configuration = add(StateRoot, add(StateS3, emptyset))
    C4: configuration = add(StateRoot, add(StateS4, emptyset))
    C5: configuration = add(StateRoot, add(StateS5, emptyset))   

    v: var V

     Conf: type = {C1, C2, C3, C4, C5} 
     conf : var Conf
     confoutput : type = configuration
     P(conf): configuration = table 
       |[ conf = C1 | conf = C2 | conf = C3 | conf = C4 | conf = C5 ]|
       | C1         | C2        | C3        | C4        |   C5 ||
     endtable

% Tabel voor de transities, zelfde werkwijze als voor configuraties, we moeten rekening houden
% met de uitvoerbare kracht van pvs

     Trans: type = {T1, T2, T3, T4}
     trans: var Trans
     Transoutput: type = Transition2
     PT(trans): Transoutput = table 
       |[ trans = T1 | trans = T2 | trans = T3 | trans = T4 ]|
       |  t1         | t2         | t3         |   t4       ||
     endtable

     % Een tweede transitierelatie
     Conf2: Type = [# %conf: Conf, 
                      v: V #]

     s2, s02, s12: var Conf2
%     init2(s2)      : bool = member(StateS1, P(conf(s2))) 
%     voorwaarde2(s2): bool = (member(StateS2, P(conf(s2)))) %or member(StateS3, P(conf(s2)))) 

     predStateS1(v:V): bool = a(v) = true and b(v) = 1
     predStateS2(v:V): bool = a(v) = true and b(v) = 2
     predStateS3(v:V): bool = a(v) = true and b(v) = 3

     predStateS4(v:V): bool = a(v) = false and b(v) = 4
     predStateS5(v:V): bool = a(v) = false and b(v) = 5

     predC1(v:V): bool = predStateS1(v)
     predC2(v:V): bool = predStateS2(v)
     predC3(v:V): bool = predStateS3(v)
     predC4(v:V): bool = predStateS4(v)
     predC5(v:V): bool = predStateS5(v)

     importing ctlops[Conf2]

     % tabel om met de juiste boolean terug te geven
     v_state: var V
     Q(conf, v_state): bool = table 
                    |[ conf = C1  | conf = C2 | conf = C3  | conf = C4 | conf = C5]|
                    |  predC1(v_state)   | predC2(v_state) | predC3(v_state) | 
                       predC4(v_state) | predC5(v_state)||
                           endtable

     relation6(s02, s12): bool = (exists(c:Conf,c2:Conf): Q(c,v(s02)) & Q(c2,v(s12)) &
                                      (exists(tr:Trans): trigger(PT(tr)) = EmptyE &
                                                         member(source(PT(tr)), P(c)) &
       			 	                         member(target(PT(tr)), P(c2))))
                                
     init6(s2):       bool = a(v(s2)) = true and b(v(s2)) = 1  
     voorwaarde6(s2): bool = a(v(s2)) = true

     theorem61: theorem init6(s2) => AG(relation6, voorwaarde6)(s2)
     theorem62: theorem init6(s2) => EG(relation6, voorwaarde6)(s2)     
     theorem63: theorem init6(s2) => AF(relation6, voorwaarde6)(s2)    
%     theorem64: theorem init6(s2) => EF(relation6, voorwaarde6)(s2)   

  end eindig

$$$eindig.prf
(eindig
 (P_TCC1 0
  (P_TCC1-1 nil 3228626355 3228972667 ("" (cond-disjoint-tcc) nil nil)
   proved nil 158 130 nil shostak))
 (P_TCC2 0
  (P_TCC2-1 nil 3228626355 3228972667 ("" (cond-coverage-tcc) nil nil)
   proved nil 136 60 nil shostak))
 (PT_TCC1 0
  (PT_TCC1-1 nil 3228626355 3228972667 ("" (cond-disjoint-tcc) nil nil)
   proved nil 102 80 nil shostak))
 (PT_TCC2 0
  (PT_TCC2-1 nil 3228626355 3228972667
   ("" (cond-coverage-tcc) (("" (postpone) nil nil)) nil) proved nil 71
   50 nil shostak))
 (theorem61 0
  (theorem61-1 nil 3228626374 3228973165
   ("" (model-check :defs !!!) (("" (grind) nil nil)) nil) proved
   ((relation6 const-decl "bool" eindig nil)
    (emptyset const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (add const-decl "(nonempty?)" sets nil)
    (P const-decl "configuration" eindig nil)
    (C5 const-decl "configuration" eindig nil)
    (C4 const-decl "configuration" eindig nil)
    (C3 const-decl "configuration" eindig nil)
    (C2 const-decl "configuration" eindig nil)
    (C1 const-decl "configuration" eindig nil)
    (PT const-decl "Transoutput" eindig nil)
    (t4 const-decl "Transition2" eindig nil)
    (t3 const-decl "Transition2" eindig nil)
    (t2 const-decl "Transition2" eindig nil)
    (t1 const-decl "Transition2" eindig nil)
    (Q const-decl "bool" eindig nil)
    (predC5 const-decl "bool" eindig nil)
    (predStateS5 const-decl "bool" eindig nil)
    (predC4 const-decl "bool" eindig nil)
    (predStateS4 const-decl "bool" eindig nil)
    (predC3 const-decl "bool" eindig nil)
    (predStateS3 const-decl "bool" eindig nil)
    (predC2 const-decl "bool" eindig nil)
    (predStateS2 const-decl "bool" eindig nil)
    (predC1 const-decl "bool" eindig nil)
    (predStateS1 const-decl "bool" eindig nil)
    (EX const-decl "bool" ctlops nil)
    (voorwaarde6 const-decl "bool" eindig nil)
    (EG const-decl "pred[state]" ctlops nil)
    (V type-eq-decl nil eindig nil) (Conf2 type-eq-decl nil eindig nil)
    (init6 const-decl "bool" eindig nil))
   490919 2770 t shostak))
 (theorem62 0
  (theorem62-1 nil 3228626387 3228968905
   ("" (model-check :defs !!!) (("" (grind) nil nil)) nil) unchecked
   ((relation6 const-decl "bool" eindig nil)
    (emptyset const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (add const-decl "(nonempty?)" sets nil)
    (P const-decl "configuration" eindig nil)
    (C5 const-decl "configuration" eindig nil)
    (C4 const-decl "configuration" eindig nil)
    (C3 const-decl "configuration" eindig nil)
    (C2 const-decl "configuration" eindig nil)
    (C1 const-decl "configuration" eindig nil)
    (PT const-decl "Transoutput" eindig nil)
    (t4 const-decl "Transition2" eindig nil)
    (t3 const-decl "Transition2" eindig nil)
    (t2 const-decl "Transition2" eindig nil)
    (t1 const-decl "Transition2" eindig nil)
    (Q const-decl "bool" eindig nil)
    (predC5 const-decl "bool" eindig nil)
    (predStateS5 const-decl "bool" eindig nil)
    (predC4 const-decl "bool" eindig nil)
    (predStateS4 const-decl "bool" eindig nil)
    (predC3 const-decl "bool" eindig nil)
    (predStateS3 const-decl "bool" eindig nil)
    (predC2 const-decl "bool" eindig nil)
    (predStateS2 const-decl "bool" eindig nil)
    (predC1 const-decl "bool" eindig nil)
    (predStateS1 const-decl "bool" eindig nil)
    (voorwaarde6 const-decl "bool" eindig nil)
    (EX const-decl "bool" ctlops nil)
    (AX const-decl "pred[state]" ctlops nil)
    (V type-eq-decl nil eindig nil) (Conf2 type-eq-decl nil eindig nil)
    (init6 const-decl "bool" eindig nil))
   16345 1600 t shostak))
 (theorem63 0
  (theorem63-1 nil 3228640628 3228646353
   ("" (model-check :defs !) nil nil) unchecked
   ((relation6 const-decl "bool" eindig nil)
    (emptyset const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (add const-decl "(nonempty?)" sets nil)
    (P const-decl "configuration" eindig nil)
    (C5 const-decl "configuration" eindig nil)
    (C4 const-decl "configuration" eindig nil)
    (C3 const-decl "configuration" eindig nil)
    (C2 const-decl "configuration" eindig nil)
    (C1 const-decl "configuration" eindig nil)
    (PT const-decl "Transoutput" eindig nil)
    (t4 const-decl "Transition2" eindig nil)
    (t3 const-decl "Transition2" eindig nil)
    (t2 const-decl "Transition2" eindig nil)
    (t1 const-decl "Transition2" eindig nil)
    (Q const-decl "bool" eindig nil)
    (predC5 const-decl "bool" eindig nil)
    (predStateS5 const-decl "bool" eindig nil)
    (predC4 const-decl "bool" eindig nil)
    (predStateS4 const-decl "bool" eindig nil)
    (predC3 const-decl "bool" eindig nil)
    (predStateS3 const-decl "bool" eindig nil)
    (predC2 const-decl "bool" eindig nil)
    (predStateS2 const-decl "bool" eindig nil)
    (predC1 const-decl "bool" eindig nil)
    (predStateS1 const-decl "bool" eindig nil)
    (voorwaarde6 const-decl "bool" eindig nil)
    (EX const-decl "bool" ctlops nil)
    (EG const-decl "pred[state]" ctlops nil)
    (AF const-decl "pred[state]" ctlops nil)
    (Conf type-decl nil eindig nil) (V type-eq-decl nil eindig nil)
    (Conf2 type-eq-decl nil eindig nil)
    (init6 const-decl "bool" eindig nil))
   17158 1330 t shostak))
 (theorem64 0
  (theorem64-1 nil 3228626361 3228969120
   ("" (model-check :defs !!!) nil nil) unchecked
   ((Conf type-decl nil eindig nil)
    (init6 const-decl "bool" eindig nil)
    (Conf2 type-eq-decl nil eindig nil) (V type-eq-decl nil eindig nil)
    (EF const-decl "pred[state]" ctlops nil)
    (EU const-decl "pred[state]" ctlops nil)
    (voorwaarde6 const-decl "bool" eindig nil)
    (K_conversion const-decl "T1" K_conversion nil)
    (EX const-decl "bool" ctlops nil)
    (predStateS1 const-decl "bool" eindig nil)
    (predC1 const-decl "bool" eindig nil)
    (predStateS2 const-decl "bool" eindig nil)
    (predC2 const-decl "bool" eindig nil)
    (predStateS3 const-decl "bool" eindig nil)
    (predC3 const-decl "bool" eindig nil)
    (predStateS4 const-decl "bool" eindig nil)
    (predC4 const-decl "bool" eindig nil)
    (predStateS5 const-decl "bool" eindig nil)
    (predC5 const-decl "bool" eindig nil)
    (Q const-decl "bool" eindig nil)
    (t1 const-decl "Transition2" eindig nil)
    (t2 const-decl "Transition2" eindig nil)
    (t3 const-decl "Transition2" eindig nil)
    (t4 const-decl "Transition2" eindig nil)
    (PT const-decl "Transoutput" eindig nil)
    (C1 const-decl "configuration" eindig nil)
    (C2 const-decl "configuration" eindig nil)
    (C3 const-decl "configuration" eindig nil)
    (C4 const-decl "configuration" eindig nil)
    (C5 const-decl "configuration" eindig nil)
    (P const-decl "configuration" eindig nil)
    (add const-decl "(nonempty?)" sets nil)
    (member const-decl "bool" sets nil)
    (emptyset const-decl "set" sets nil)
    (relation6 const-decl "bool" eindig nil))
   8884 890 t shostak)))


$$$AbstractSyntax.pvs
% Met behulp van deze theory kunnen we alle mogelijke gegevens
% van een UML statechart opnemen in een PVS file.
% Werkwijze: UML mappen naar XML en XML mappen naar PVS
% Doel: zo generiek mogelijk werken.

% Gevraagd: is het mogelijk om te werken met niet-gedefinieerde types 
% Problemen: ontstaan bij die niet gedefinieerde types.

AbstractSyntax: THEORY
  BEGIN 
    
    % Een top komt overeen met een bepaalde toestand uit het toestandsdiagramma
    % Deze top wordt gedefinieerd als een niet ledig type. 
    
    Vertex: TYPE+ 
    EmptyV: Vertex 
    Vertexen: type = finite_set[Vertex]
    
    % Guard conditions
    Condition: TYPE+ 
    EmptyC: Condition 
    Conditions: type = finite_set[Condition]
    
    % Events
    % XML model duidt de verschillende elementen samen met hun type aan
    % We maken er wel types zdd dat we die voor ieder statechart kunnen gebruiken

    Event: TYPE+ 
    SignalEvent: type = finite_set[Event]
    CallEvent  : type = finite_set[Event]
    TimeEvent  : type = finite_set[Event]
    ChangeEvent: type = finite_set[Event]
    EmptyE: Event 
    Events: type = finite_set[Event]

    % Actions
    Action: TYPE+ 
    EmptyA: Action 
    Actions: type = finite_set[Action]
 
    % States 
    % Er wordt een onderscheid gemaakt tussen de pseudo en de niet-pseudostates.
    State: type = finite_set[Vertex]
    
    % Pseudo states
    PseudoState: type = finite_set[Vertex]
        % een verzameling bestaande uit de volgende pseudo-states
    Initial    : type = finite_set[Vertex]
    FinalState : type = finite_set[Vertex]
    DeepH      : type = finite_set[Vertex]
    Join       : type = finite_set[Vertex]
    Fork       : type = finite_set[Vertex]
    Junction   : type = finite_set[Vertex]
    Choice     : type = finite_set[Vertex]

    % Synch states
    SynchState: type = finite_set[Vertex]

    % Bound attribute associated to a synch state
    sync: VAR SynchState
    bound(sync): nat

    StubState: type = finite_set[Vertex]

    SubmachineState: type = finite_set[Vertex]

    % Stereotype are used for transition out of the initial state

    Stereotype: TYPE = {create, no_stereo}
    stereotype(e: Event): Stereotype

    % Context of a state machine
    Context: TYPE+ = {behavioral, classifier}

    % Transitions
    Transition: TYPE+ = [# source : Vertex, 
                           trigger: Event, 
                           guard  : Condition, 
                           effect : Action, 
                           target : Vertex 
                         #]

    EmptyTr: Transition = (# source := EmptyV,
                             trigger:= EmptyE,
                             guard  := EmptyC,
                             effect := EmptyA,
                             target := EmptyV 
                           #)
    Transitions: type = finite_set[Transition] 
                                  
    % Bijkomende definities/functies die we gebruiken om de mapping van het statechart
    % te kunnen voltooien. Er zijn twee mogelijkheden om dit te realiseren: ofwel maken 
    % we gebruik van functies, ofwel definieren we toestanden aan de hand van een record

    x : var Vertex  % variabele, want voor iedere top moet dit gedefinieerd worden
    
% 1. De verzameling van kinderen van een top op het eerste niveau. Deze informatie
%    kunnen we rechtstreeks uit de XML file halen.   

    dsubvertex(x): finite_set[Vertex]

% 2. De verzameling van alle kinderen van een top (op meerdere niveaus). Ook deze informatie
%    kan rechtstreeks uit de XML file gehaald worden
   
    subvertex(x) : finite_set[Vertex]
    subvertexInc(x) : finite_set[Vertex]

% 3. De defaulttoestanden voor iedere toestand aanduiden. 
%    Merk op dat we de default toestand enkel definieren voor hierarchische sequentiele toestanden
%    Het definieren van de defaultstate kan door de parser gebeuren.
     defaultstate(x) : Vertex

% 4. Voor hierarchische toestanden aanduiden of al dan niet concurrent
     statekind: type = {andstate, orstate, simplestate}
     typefunction(x) : statekind

% 5. Voor sequentiele toestanden bijhouden of de toestand al dan niet een historyconnector bevat
%    want dit zorgt voor een verschil in opbouw van configuraties. Een booleaanse waarde is hiervoor
%    meer dan voldoende.
     history: type = {shallow, deep, none}
     cHistory(x): history 

    % Representation of a statechart or state machine
    % We maken hiervoor gebruik van de vooraf gedefinieerde types.
    StateMachine: TYPE+ = 
        [# State: State,
           StubState: StubState, 
           SynchState: SynchState, 
           Initial: Initial,
           Choice: Choice,
           DeepH: DeepH,
           Join: Join,
           Fork: Fork,
           Junction: Junction,
           FinalState: FinalState,
           SubmachineState: SubmachineState,
           PseudoState: PseudoState,
           Vertex: Vertexen,
           CallEvent: CallEvent,
           TimeEvent: TimeEvent,
           ChangeEvent: ChangeEvent,
           SignalEvent: SignalEvent,
           Event: Events, 
           Action: Actions,
           Condition: Conditions,
           Transition: Transitions,
           Root: Vertex,
           Context: Context         
          #]

      EmptySm: StateMachine = (# State:= singleton(EmptyV),
                                 StubState:= emptyset,
                                 SynchState:= emptyset,
                                 Initial:= emptyset,
                                 Choice:= emptyset,
                                 DeepH:= emptyset,
                                 Join:= emptyset,
                                 Fork:= emptyset,
                                 Junction:= emptyset,
                                 FinalState:= emptyset,
                                 SubmachineState:= emptyset,
                                 PseudoState:= emptyset,
                                 Vertex:= singleton(EmptyV),
                                 CallEvent:= emptyset,
                                 TimeEvent:= emptyset,
                                 ChangeEvent:= emptyset,
                                 SignalEvent:= emptyset,
                                 Event:= singleton(EmptyE), 
                                 Action:= singleton(EmptyA),
                                 Condition:= singleton(EmptyC),
                                 Transition:= singleton(EmptyTr), 
                                 Root:= EmptyV,
                                 Context:= classifier         
                              #) 
                  
  END AbstractSyntax