[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification RGI-Conds
enrich
   IOfun, 
   cstate, 
   nat

with
   

   
   
   
   predicates  Init : cstate;
               Idle : nat × cstate;
               Rely : nat × cstate × cstate;
               Guar : nat × cstate × cstate;
               Inv : cstate;
   procedures COP nat × (nat → input) : cstate × (nat → output) nonfunctional nondeterministic;
   variables  CS : cstate flexible;
              m0 : nat;
              cs1 : cstate;
              cs2 : cstate;
              cs3 : cstate;
   
   

   

   axioms COP-sat-rely-guar
          : Idle(n, CS), Inv(CS)
            ⊦ [: CS, Outp
              | (Rely(n, CS', CS'') ∧ (Idle(n, CS') ↔ Idle(n, CS'')))
              , (Guar(n, CS, CS') ∧ (∀ m. m ≠ n → (Idle(m, CS) ↔ Idle(m, CS'))))
              , Inv(CS)
              , COP(n, Inp; CS, Outp)
              ] (Idle(n, CS) ∧ Inv(CS));
          used for: tl;
          init-ex :  ⊦ ∃ cs. Init(cs);
          init-idle :  ⊦ Init(cs) → (∀ n. Idle(n, cs));
          init-inv :  ⊦ Init(cs) → (¬ Inv(cs) ↔ false);
          used for: s, ls;
          g-r :  ⊦ m ≠ n ∧ Guar(m, cs1, cs2) ∧ Inv(cs1) ∧ Inv(cs2) → (¬ Rely(n, cs1, cs2) ↔ false);
          g-refl :  ⊦ Inv(cs) → (¬ Guar(m, cs, cs) ↔ false);
          used for: s, ls;
          r-trans :  ⊦ Rely(m, cs1, cs2) ∧ Rely(m, cs2, cs3) ∧ Inv(cs1) → Rely(m, cs1, cs3);
          used for: f, lf;

   

   
end enrich