[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 FLITPSCweak-refines-PLIB
automaton refinement 
   export PLIB-proofs
   
   import FLITPSCweak-proofs
   
   using abs-FLITPSCweak-PLIB
   abstraction ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p);
   
   local abstraction 
       idle : apc = idle;
      
       ready : apc = ready;
      
       crashed : apc = crashed;
      
       R1 : apc = invRead;
      
       R2 -> R4 : apc = resRead;
      
       W1 -> W3 : apc = invWrite;
      
       W4 -> W7 : apc = resWrite;
      
       R1 : l = il;
      
       R2 -> R4 : v = ov;
      
       W1 -> W7 : l = il ∧ v = iv;
      
       idle, ready, R1, R4, W1, W5 : ∀ l. ¬ FO(t) ∈ p(l) → ((h | l) | t) | false = [];
      
       W2, W3, W6 -> W7 : ∀ l. ((h | l) | t) | false = [];
      
       R2, R3 : ∀ l0. l0 ≠ l ∧ ¬ FO(t) ∈ p(l0) → ((h | l0) | t) | false = [];
      
       R2 : ctr(l) = 0 → ((h | l) | t) | false = [];
      
       W4 : ((h | l) | t) | false = (W(t, l, v), false) ' ∨ ((h | l) | t) | false = [];
   
   by action mapping callPSCRUN(t); -> callARun(t); globalPSCCRASH; -> globalACrash; globalPSCPERSIST_W(l); -> globalAPersist(l); 
                     invFLITPSCREAD(t, l); -> AInvRead(t, l); invFLITPSCWRITE(t, l, v); -> AInvWrite(t, l, v); retFLITPSCREAD(t, v); -> ARetRead(t, v); 
                     retFLITPSCWRITE(t); -> ARetWrite(t); doWritePSC(t, l, v); -> ADoWrite(t); doReadPSC(t, l, v); -> ADoRead(t); 
                     callPSCCOMPLETE(t); -> callTSync(t);
   
end automaton refinement