Specification PurgeTransNoInitialstate

[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 gen-CongTrans-wf
 , 
       gen-command-list
 with
   functions 
      run : systemstate × commandlist → systemstate;
      step : systemstate × command → systemstate;
      outputt : systemstate × command → output;
      test : systemstate × commandlist × command → output;
      purge : commandlist × secdomain → commandlist;
   predicates 
      eqds : systemstate × secdomainset × systemstate;
      wf : commandlist;
   
   axioms 
      eqds-def :  ⊦ eqds(sys, ds, sys0) ↔ (∀ d. d ∈ ds → eqd(sys, d, sys0));
      wf-def :  ⊦ wf(cl) ↔ (∀ co. co ∈ cl → wf(co));
      test :  ⊦ test(sys, cl, co) = exec(run(sys, cl), co) .2;
      step :  ⊦ step(sys, co) = exec(sys, co) .1;
      output :  ⊦ outputt(sys, co) = exec(sys, co) .2;
      run-base :  ⊦ run(sys, []) = sys;
      used for : s, ls;
       
      run-rec :  ⊦ run(sys, co ' + cl) = run(exec(sys, co) .1, cl);
      used for : s, ls;
       
      purge-base :  ⊦ purge([], d) = [];
      used for : s, ls;
       
      purge-rec :  ⊦ purge(co ' + cl, d) = ((cdom(co) ⇒ d ⊃ co + purge(cl, d); purge(cl, d)));
end enrich