[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 MeydenIntransWithState
enrich AccessControlWithState
 , 
       gen-command-list
 , 
       gen-secdomain-set
 with
comment: tries to add a state that is ignored by the NIF spec. 
         However, it is no good because RMA-2 does not hold for a real system.;
   functions 
      run : systemstate × commandlist → systemstate;
      run : commandlist → systemstate;
      ipurge : commandlist × secdomain → commandlist;
      sources : commandlist × secdomain → secdomainset;
   predicates 
      eqds : systemstate × secdomainset × systemstate;
      comment: needed for the intransive case.;
       
   
   axioms 
      eqds-def :  ⊦ eqds(sys, ds, sys0) ↔ (∀ d. d ∈ ds → eqd(sys, d, sys0));
      run-base :  ⊦ run(sys, []) = sys;
      used for : s, ls;
       
      run-rec :  ⊦ run(sys, co ' + cl) = run(step(sys, co), cl);
      used for : s, ls;
       
      run-initial :  ⊦ run(cl) = run(initialstate, cl);
      sources-base :  ⊦ sources([], d) = ∅ ++ d;
      used for : s, ls;
       
      sources-rec :  ⊦ sources(co ' + cl, d) = (((∃ d0. d0 ∈ sources(cl, d) ∧ cdom(co) ⇒ d0) ⊃ sources(cl, d) ++ cdom(co); sources(cl, d)));
      used for : s, ls;
       
      ipurge-base :  ⊦ ipurge([], d) = [];
      used for : s, ls;
       
      ipurge-rec :  ⊦ ipurge(co ' + cl, d) = ((cdom(co) ∈ sources(co + cl, d) ⊃ co + ipurge(cl, d); ipurged(co) + ipurge(cl, d)));
      used for : s, ls;
       
end enrich