[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 state
enrich datafuns with
   predicates 
      init : (name × Agent → Data);
      maxOneNotNull : (name × Agent → Data);
      comment: true if at most one state or Mailbox is NOT null.;
       
      allNull : (name × Agent → Data);
      comment: true if every state and Mailbox is null.;
       
      stateNotNull : (name × Agent → Data);
      comment: true if at most one state is not null.;
       
      mailboxNotNull : (name × Agent → Data);
      comment: true if at most one Mailbox is not null.;
       
   variables 
      s, s0, s1, s2, s3 : name × Agent → Data; 
      nam2, nam3, nam4, nam5 : name; 
      ag2, ag3, ag4, ag5 : Agent; 
      d4, d5 : Data; 
   
   axioms 
      allNull-def :  ⊦ allNull(s) ↔ (∀ str, ag. s(state(str), ag) = null) ∧ (∀ cmd, ag. s(Mailbox(cmd), ag) = null);
      stateNotNull-def
      : ⊦ 
          stateNotNull(s)
        ↔ (∀ str, ag. 
            s(state(str), ag) ≠ null → (∀ str0, ag0. ag ≠ ag0 ∨ str0 ≠ str → s(state(str0), ag0) = null) ∧ (∀ cmd0, ag0. s(Mailbox(cmd0), ag0) = null));
      mailboxNotNull-def
      : ⊦ 
          mailboxNotNull(s)
        ↔ (∀ cmd, ag. 
              s(Mailbox(cmd), ag) ≠ null
            → (∀ str0, ag0. s(state(str0), ag0) = null) ∧ (∀ cmd0, ag0. ag ≠ ag0 ∨ cmd0 ≠ cmd → s(Mailbox(cmd0), ag0) = null));
      maxOneNotNull-def
      : ⊦ 
          maxOneNotNull(s)
        ↔   (∀ str, ag. 
                s(state(str), ag) ≠ null
              → (∀ str0, ag0. ag ≠ ag0 ∨ str0 ≠ str → s(state(str0), ag0) = null) ∧ (∀ cmd0, ag0. s(Mailbox(cmd0), ag0) = null))
          ∧ (∀ cmd, ag. 
                s(Mailbox(cmd), ag) ≠ null
              → (∀ str0, ag0. s(state(str0), ag0) = null) ∧ (∀ cmd0, ag0. ag ≠ ag0 ∨ cmd0 ≠ cmd → s(Mailbox(cmd0), ag0) = null));
      maxOneNotNull-other-def :  ⊦ maxOneNotNull(s) ↔ stateNotNull(s) ∧ mailboxNotNull(s);
      used for : generated;
       
      allNull-maxOneNotNull :  ⊦ allNull(s) → maxOneNotNull(s);
      used for : generated;
       
      maxOneNotNull-locvar :  ⊦ maxOneNotNull(s(locVar(str), ag ; d)) ↔ maxOneNotNull(s);
      used for : s, ls, generated;
       
      maxOneNotNull-locvar-01 :  ⊦ maxOneNotNull(s(locVar(str), ag ; d)(nam, ag0 ; d0)) ↔ maxOneNotNull(s(nam, ag0 ; d0));
      used for : s, ls, generated;
       
      maxOneNotNull-misc-02 :  ⊦ maxOneNotNull(s(declassify-count(str), ag ; d)(nam, ag0 ; d0)) ↔ maxOneNotNull(s(nam, ag0 ; d0));
      used for : s, ls, generated;
       
      maxOneNotNull-misc-04 :  ⊦ maxOneNotNull(s(User-GetInput-count(str), ag ; d)(nam, ag0 ; d0)) ↔ maxOneNotNull(s(nam, ag0 ; d0));
      used for : s, ls, generated;
       
      maxOneNotNull-misc-05 :  ⊦ maxOneNotNull(s(User-GetInput(str), ag ; d)(nam, ag0 ; d0)) ↔ maxOneNotNull(s(nam, ag0 ; d0));
      used for : s, ls, generated;
       
      maxOneNotNull-misc-06 :  ⊦ maxOneNotNull(s(User-GetSingleSelection-count(str), ag ; d)(nam, ag0 ; d0)) ↔ maxOneNotNull(s(nam, ag0 ; d0));
      used for : s, ls, generated;
       
      maxOneNotNull-misc-07 :  ⊦ maxOneNotNull(s(User-GetSingleSelection(str), ag ; d)(nam, ag0 ; d0)) ↔ maxOneNotNull(s(nam, ag0 ; d0));
      used for : s, ls, generated;
       
      maxOneNotNull-misc-08 :  ⊦ maxOneNotNull(s(User-ConfirmRelease-count(str), ag ; d)) ↔ maxOneNotNull(s);
      used for : s, ls, generated;
       
      maxOneNotNull-misc-09 :  ⊦ maxOneNotNull(s(User-ConfirmedRelease-count(str), ag ; d)(nam, ag0 ; d0)) ↔ maxOneNotNull(s(nam, ag0 ; d0));
      used for : s, ls, generated;
       
      maxOneNotNull-misc-10 :  ⊦ maxOneNotNull(s(User-ConfirmRelease-count(str), ag ; d)(nam, ag0 ; d0)) ↔ maxOneNotNull(s(nam, ag0 ; d0));
      used for : s, ls, generated;
       
      maxOneNotNull-next
      : ⊦ 
          s(Mailbox(cmd), ag) = wrapMessage2Data(msg) ∧ maxOneNotNull(s)
        → maxOneNotNull(s(Mailbox(cmd), ag ; null)(state(str0), ag0 ; wrapBoolean2Data(mkBoolean(true))));
      used for : s, ls, generated;
       
      maxOneNotNull-next-01 :  ⊦ maxOneNotNull(s) ∧ s(state(str0), ag0) ≠ null → maxOneNotNull(s(state(str0), ag0 ; null)(Mailbox(cmd), ag ; d));
      used for : s, ls, generated;
       
      maxOneNotNull-next-02 :  ⊦ maxOneNotNull(s) ∧ s(state(str0), ag0) ≠ null → maxOneNotNull(s(state(str0), ag0 ; null)(state(str), ag ; d));
      used for : s, ls, generated;
       
      maxOneNotNull-next-03
      :  ⊦ s(Mailbox(cmd), ag) = wrapMessage2Data(msg) ∧ maxOneNotNull(s) → maxOneNotNull(s(Mailbox(cmd), ag ; null)(Mailbox(cmd0), ag0 ; d));
      used for : s, ls, generated;
       
      maxOneNotNull-null :  ⊦ maxOneNotNull(s) → maxOneNotNull(s(Mailbox(cmd), ag ; null));
      used for : s, ls, generated;
       
end enrich