Specification PurgeIntrans

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