[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 Hashset-refines-Set
automaton refinement 
   export Set-proofs
   
   import Hashset-proofs
   
   using abs
   abstraction absset(gs.ar, ags.set);
   
   local abstraction 
       idle : apc = idle;
      
       I1 -> I4, I6, I10 -> I12, I16 -> I18, I20 : apc = invInsert;
      
       I5 : apc = (b ⊃ retInsert;invInsert);
      
       I7, I13 : apc = (e = e0 ⊃ retInsert;invInsert);
      
       I8 : apc = retInsert;
      
       I9, I14, I15, I19, I21 : apc = retInsert;
      
       I7, I8, I13, I14 : e = e0 → lb;
      
       I9, I15, I19 : lb ↔ b;
      
       I5 : b → ¬ lb;
      
       I21 : ¬ lb;
      
       M1 -> M6, M17 : apc = invMember;
      
       M7 : apc = (e0 ≠ e ∧ e0 ≠ ⊥ ∧ (n + 1) % # ar ≠ n0 ⊃ invMember;retMember);
      
       M10 : apc = (e0 ≠ ⊥ ∧ (n + 1) % # ar ≠ n0 ⊃ invMember;retMember);
      
       M13 : apc = ((n + 1) % # ar ≠ n0 ⊃ invMember;retMember);
      
       M14 : apc = (n ≠ n0 ⊃ invMember;retMember);
      
       M8, M9, M11, M12, M15, M16 : apc = retMember;
      
       M7 : e0 = e ∨ e0 = ⊥ ∨ (n + 1) % # ar = n0 → (e = e0 ↔ lb);
      
       M10 : e0 = ⊥ ∨ (n + 1) % # ar = n0 → ¬ lb;
      
       M13 : (n + 1) % # ar = n0 → ¬ lb;
      
       M14 : n = n0 → ¬ lb;
      
       M9, M12, M16 : lb ↔ b;
      
       M11, M15 : ¬ lb;
      
       M8 : lb;
      
        : apc = invMember ∨ apc = invInsert → e = le;
   
   by action mapping invINSERT(tid, e); -> AInvInsert(tid, e); doINSERT(tid, b); -> ADoInsert(tid, b); retINSERT(tid, b); -> ARetInsert(tid, b); 
                     invMEMBER(tid, e); -> AInvMember(tid, e); doMEMBER(tid); -> ADoMember(tid); retMEMBER(tid, b); -> ARetMember(tid, b);
   
end automaton refinement