Specification IO-Automaton

[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
   IO-Aut-data
with
   predicates 
       IOAut? : IOAutomaton('s, 'a, 'e);
   
   variables 
       ioa : IOAutomaton('s, 'a, 'e);
       start : 's → Bool;
       step : 's × 'a × 's → Bool;
       ext : 'a → Option('e);
       s : 's;
       a : 'a;
       e : 'e;
       oe : Option('e);
   
   
   axioms 
      isIOAut-def: IOAut?(IOAut(start, step, ext)) ↔ (∃ s. start(s) ∧ oinj(ext));
   
   
end enrich