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

something I`m missing to let it work



Hi,

My problem concerns rewrite rules combined with a transition relation.

(dumpfile included)

C1: configuration = add(StateRoot, add(StateS1, emptyset))
C2: configuration = add(StateRoot, add(StateS2, emptyset))
C3: configuration = add(StateRoot, 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


I have three list, each containing one different state.

Voor each state with an undefined type I defined a predicate as a rewrite
rule. I thought it was useful to work with rewrite rule...
For each configuration I also defined a predicate but in this case a
rewrite rule isn`t necessary.


pred(v:Vertex): pred[V]
pred(c:configuration, v:V): bool = forall(x:Vertex): member(x,c) and pred(x)(v)

pred_StateS1: axiom pred(StateS1) = lambda (v:V): a(v) = true and b(v) = true
pred_StateS2: axiom pred(StateS2) = lambda (v:V): a(v) = false and b(v) = true
pred_StateS3: axiom pred(StateS3) = lambda (v:V): a(v) = false and b(v) = true
pred_StateRoot: axiom pred(StateRoot) = lambda (v:V): true

Now consider the following transition relation with a very simple and
trivial theorem.

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

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

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

 Conf2: Type = [# conf: Conf, v: V #]
 s2, s02, s12: var Conf2
 relation6(s02, s12): bool = (exists(tr:Trans): member(source(PT(tr)), P(conf(s02))) &
      				                member(target(PT(tr)), P(conf(s12)))) &
                                 pred(P(conf(s02)), v(s02)) &
                                 pred(P(conf(s12)), v(s12))

 init6(s2):       bool = a(v(s2)) = true  and b(v(s2)) = true
 voorwaarde6(s2): bool = a(v(s2)) = false and b(v(s2)) = true

 theorem61: theorem init6(s2) => EF(relation6, voorwaarde6)(s2)

When model-checking the theorem it seems that the model-checker has
problems with the predicates which are however installed as rewrite rules.
The modelchecker returns a goal in mucalculusformat.
I`ve tried the three options in the defs argument but without any success.

Does anyone know how I can get this work? Or am i doing something wrong?

Thanks,

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)

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

rewriting: theory
  begin
   
    importing AbstractSyntax
 
    V: Type = [# a: bool, b:bool  #] 

    abs_V: Type

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

    configuration: type = finite_set[Vertex]

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

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

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

    pred(v:Vertex): pred[V]
    pred(c:configuration, v:V): bool = forall(x:Vertex): member(x,c) and pred(x)(v)

    pred_StateS1: axiom pred(StateS1) = lambda (v:V): a(v) = true and b(v) = true
    pred_StateS2: axiom pred(StateS2) = lambda (v:V): a(v) = false and b(v) = true
    pred_StateS3: axiom pred(StateS3) = lambda (v:V): a(v) = false and b(v) = true
    pred_StateRoot: axiom pred(StateRoot) = lambda (v:V): true

    auto_rewrite+ pred_StateS1
    auto_rewrite+ pred_StateS2
    auto_rewrite+ pred_StateS3
    auto_rewrite+ pred_StateRoot

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

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

     Conf2: Type = [# conf: Conf, v: V #]
     s2, s02, s12: var Conf2
     relation6(s02, s12): bool = (exists(tr:Trans): member(source(PT(tr)), P(conf(s02))) &
         				            member(target(PT(tr)), P(conf(s12)))) &
                                 pred(P(conf(s02)), v(s02)) &
                                 pred(P(conf(s12)), v(s12))
                                 
     init6(s2):       bool = a(v(s2)) = true  and b(v(s2)) = true 
     voorwaarde6(s2): bool = a(v(s2)) = false and b(v(s2)) = true 

     theorem61: theorem init6(s2) => EF(relation6, voorwaarde6)(s2)
     
  end rewriting

$$$rewrite.prf
(rewriting
 (P_TCC1 0
  (P_TCC1-1 nil 3228540637 3228541359 ("" (cond-disjoint-tcc) nil nil)
   proved nil 78 30 nil shostak))
 (P_TCC2 0
  (P_TCC2-1 nil 3228540637 3228541359 ("" (cond-coverage-tcc) nil nil)
   proved nil 64 50 nil shostak))
 (PT_TCC1 0
  (PT_TCC1-1 nil 3228540637 3228541359 ("" (cond-disjoint-tcc) nil nil)
   proved nil 14 10 nil shostak))
 (PT_TCC2 0
  (PT_TCC2-1 nil 3228540637 3228541359
   ("" (cond-coverage-tcc) (("" (postpone) nil nil)) nil) unfinished
   nil 82 60 nil shostak))
 (theorem61 0
  (theorem61-1 nil 3228541365 3228541375
   ("" (model-check)
    (("" (grind)
      (("1" (postpone) nil nil) ("2" (postpone) nil nil)
       ("3" (postpone) nil nil))
      nil))
    nil)
   unfinished nil 10290 1510 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