Specification IOrefine-def

[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,

enrich
   IOtrace
with
   predicates 
       C_≤*T_A : IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e);
       C_≤ωT_A : IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e);
       C_≤T_A : IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e);
       C_≡*T_A : IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e);
       C_≡ωT_A : IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e);
       C_≡T_A : IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e);
   
   variables 
       cal : List('ca);
       aal : List('aa);
       el : List('e);
       csf : Nat → 'cs;
       asf : Nat → 'as;
       csl : List('cs);
       asl : List('as);
       as : 'as;
       cs : 'cs;
       ca : 'ca;
       aa : 'aa;
       cα : Stream('aa);
       aα : Stream('aa);
       β : Stream('e);
       cσ : Stream('cs);
       aσ : Stream('as);
       cstart : 'cs → Bool;
       astart : 'as → Bool;
       cstep : 'cs × 'ca × 'cs → Bool;
       astep : 'as × 'aa × 'as → Bool;
       cext : 'ca → Option('e);
       aext : 'aa → Option('e);
       cioaut : IOAutomaton('cs, 'ca, 'e);
       aioaut : IOAutomaton('as, 'aa, 'e);
   
   
   axioms 
      leqstar-def: C_≤*T_A(cioaut, aioaut) ↔ (∀ el. trace*(cioaut)(el) → trace*(aioaut)(el));
      used for: ls;
      
      leq-def: C_≤T_A(cioaut, aioaut) ↔ (∀ β. trace(cioaut)(β) → trace(aioaut)(β));
      used for: ls;
      
      leqomega-def: C_≤ωT_A(cioaut, aioaut) ↔ (∀ ef. traceω(cioaut)(ef) → traceω(aioaut)(ef));
      used for: ls;
      
      equivstar-def: C_≡*T_A(cioaut, aioaut) ↔ (∀ el. trace*(cioaut)(el) ↔ trace*(aioaut)(el));
      used for: ls;
      
      equiv-def: C_≡T_A(cioaut, aioaut) ↔ (∀ β. trace(cioaut)(β) ↔ trace(aioaut)(β));
      used for: ls;
      
      equivomega-def: C_≡ωT_A(cioaut, aioaut) ↔ (∀ ef. traceω(cioaut)(ef) ↔ traceω(aioaut)(ef));
      used for: ls;
   
   
end enrich