in entities.mod .
-- =====================
-- =====================
--  Transition Patterns
-- =====================
-- =====================

mod PATTERNS {
  pr ( DIVISIONSET + EQBOOL + EVIDENCEHISTORY +
       DOCUMENTTYPE + DOCUMENTIDSET + SESSIONID +
       DOCUMENTIDLIST )
  *[ State ]*

-- **************
--  observations
-- **************
  -- observations for document's attributes
   -- visible information
    -- observation for created document types
  bop DocumentType :
     State DocumentID -> DocumentType
    -- observation for evidence history
  bop Evidences : State DocumentID -> EvidenceHistory
    -- observation for place where a document is
  bop Place : State DocumentID -> Division
    -- observation for session ID
  bop SessionID : State DocumentID -> SessionID
   -- meta information
    -- observation for information about forge
  bop Legal? : State DocumentID -> Bool
   -- observation for original document
  bop OriginalID : State DocumentID -> SessionID
  --
  -- observation for created document IDs
  bop DocumentIDList :
      State SessionID DocumentType -> DocumentIDList
  -- observation for the untrusted set
  bop UntrustedSet : State -> DivisionSet
--
  var S : State
  vars T T1 T2 : DocumentType
  vars D D1 D2 D3 : DocumentID
  vars I I1 I2 : SessionID
  var DL : DocumentIDList
  eq Place(S, noDocumentID) = noDivision .
  eq DocumentIDList(S, noSessionID, T) = nillDID .
  eq DocumentIDList(S, I, noDocumentType) = nillDID .
--
-- *************
--  transitions
-- *************
 -- ================
 --  regular events
 -- ================
 -- creating a document
  -- creating a document without referring
  op Create-1 :
      State SessionID Division DocumentID DocumentType
      -> State
  -- creating a document from another one
  op Create-2 :
      State Division DocumentID DocumentType DocumentID
      -> State
  -- creating a document without referring
  -- with a carbon copy
  op Create-cc-1 :
      State SessionID Division DocumentID DocumentType
      -> State
  -- creating a document from another one
  -- with a carbon copy
  op Create-cc-2 :
      State Division DocumentID DocumentType DocumentID
      -> State
 -- sending a document
  op Send : State Division DocumentID Division
             -> State
 -- =================
 --  Irregular event
 -- =================
 -- forging a document
  op Forge : State DocumentID -> State
 -- changing session
  op ChangeSession : State DocumentID SessionID
                      -> State
 -- ================
 --  control events
 -- ================
 -- checking a document
  -- checking a document with another one
  op Check-1 : State Division DocumentID DocumentID
                -> State
  -- checking a document which has an evidence 
  -- with another one
  op Check-2 :
      State Division DocumentID Evidence DocumentID
      -> State
  -- checking a docuement with another one
  -- which has an evidence
  op Check-3 :
      State Division DocumentID DocumentID Evidence 
      -> State
  -- checking a document which has an evidence with 
  -- another one which has an evidence
  op Check-4 :
      State Division DocumentID Evidence DocumentID Evidence
      -> State
 -- approving a document
  -- approving a document without checking an evidence
  op Approve-1 : State Division DocumentID -> State
  -- approving a document with checking an evidence
  op Approve-2 : State Division DocumentID Evidence
                  -> State
--
-- variables
  vars T T1 T2 T3 : DocumentType
  vars V V1 V2 : Division
  vars E E1 E2 : Evidence
--
--
-- ******************
--  transition rules
-- ******************
-- in this module, 
-- transitions do not have effective conditions.
-- when we specify actual transitions
-- which are defined for specific business processes
-- by using transitions in this module,
-- we define only flamework of effective conditions.
-- =========================
--  Create-1(S, I, V, D, T)
-- =========================
-- ----------------------------------
--  flamework of effective condition
-- ----------------------------------
  op c-Create-1 :
     State SessionID Division DocumentID DocumentType
     -> Bool
  -- the effective condition is that
  -- document type T has not been created yet.
  eq c-Create-1(S, I, V, D, T)
     = (Place(S, D) = noDivision) .
-- ------------------------------------------
--
-- ------------------------------------------
-- DoucmentType
  eq DocumentType(Create-1(S, I, V, D1, T), D2)
     = if (D1 = D2) then T
       else DocumentType(S, D2) fi .
-- ------------------------------------------
-- Evidences
  eq Evidences(Create-1(S, I, V, D1, T), D2)
     = if (D1 = D2) then emptyE
       else Evidences(S, D2) fi .
-- ------------------------------------------
-- Place
  -- a new document is put in division V.
  eq Place(Create-1(S, I, V, D1, T), D2)
     = if (D1 = D2) then V
       else Place(S, D2) fi .
-- ------------------------------------------
-- SessionID
  eq SessionID(Create-1(S, I, V, D1, T), D2)
     = if (D1 = D2) then I
       else SessionID(S, D2) fi .
-- ------------------------------------------
-- Legal?
  -- Create-1 is a regular event.
  eq Legal?(Create-1(S, I, V, D1, T), D2)
     = if (D1 = D2) then true
       else Legal?(S, D2) fi .
-- ------------------------------------------
-- OriginalID
  eq OriginalID(Create-1(S, I, V, D1, T), D2)
     = if (D1 = D2) then I
       else OriginalID(S, D2) fi .
-- ------------------------------------------
-- DocumentIDList
  eq DocumentIDList(Create-1(S, I1, V, D1, T1), I2, T2)
     = if (I1 = I2) and (T1 = T2) then
          (D1 ; DocumentIDList(S, I1, T1))
       else DocumentIDList(S, I2, T2) fi .
-- ------------------------------------------
-- UntrustedSet
  eq UntrustedSet(Create-1(S, I, V, D, T))
      = UntrustedSet(S) .
-- ------------------------------------------
--
-- ===========================
--  Create-2(S, V, D1, T, D2)
-- ===========================
-- ----------------------------------
--  flamework of effective condition
-- ----------------------------------
  op c-Create-2 :
     State Division DocumentID DocumentType DocumentID
     -> Bool
  -- the effective condition is that
  -- document D1 is not created,
  -- document D2 has been created, and
  -- D2 is in division V.
  eq c-Create-2(S, V, D1, T, D2)
     = (Place(S, D1) = noDivision) and
       (Place(S, D2) = V) .
-- ------------------------------------------
--
-- ------------------------------------------
-- DocumentType
  eq DocumentType(Create-2(S, V, D1, T, D2), D3)
     = if (D1 = D3) then T
       else DocumentType(S, D3) fi .
-- ------------------------------------------
-- Evidences
  eq Evidences(Create-2(S, V, D1, T, D2), D3)
     = if (D1 = D3) then emptyE
       else Evidences(S, D3) fi .
-- ------------------------------------------
-- Place
  -- a new document is put in division V.
  eq Place(Create-2(S, V, D1, T, D2), D3)
     = if (D1 = D3) then V
       else Place(S, D3) fi .
-- ------------------------------------------
-- SessionID
  eq SessionID(Create-2(S, V, D1, T, D2), D3)
     = if (D1 = D3) then SessionID(S, D2)
       else SessionID(S, D3) fi .
-- ------------------------------------------
-- Legal?
  -- Create-2 is a regular event.
  eq Legal?(Create-2(S, V, D1, T, D2), D3)
     = if (D1 = D3) then Legal?(S, D2)
       else Legal?(S, D3) fi .
-- ------------------------------------------
-- OriginalID
  eq OriginalID(Create-2(S, V, D1, T, D2), D3)
     = if (D1 = D3) then SessionID(S, D2)
       else OriginalID(S, D3) fi .
-- ------------------------------------------
-- DocumentIDList
  eq DocumentIDList(Create-2(S, V, D1, T1, D2), I, T2)
     = if ((I = SessionID(S, D2)) and (T1 = T2)) then
          (D1 ; DocumentIDList(S, I, T1))
       else DocumentIDList(S, I, T2) fi .
-- ------------------------------------------
-- UntrustedSet
  eq UntrustedSet(Create-cc-1(S, I, V, D1, T))
      = UntrustedSet(S) .
-- ------------------------------------------
--
-- ============================
--  Create-cc-1(S, I, V, D, T)
-- ============================
-- ----------------------------------
--  flamework of effective condition
-- ----------------------------------
  op c-Create-cc-1 :
     State SessionID Division DocumentID DocumentType
     -> Bool
  -- the effective condition is that
  -- document type T has not been created yet.
  eq c-Create-cc-1(S, I, V, D, T)
     = (Place(S, D) = noDivision) .
-- ------------------------------------------
--
-- ------------------------------------------
-- DocumentType
  eq DocumentType(Create-cc-1(S, I, V, D1, T), D2)
     = if (D1 = D2) then T
       else
         if (cc(D1) = D2) then cc(T)
         else DocumentType(S, D2) fi fi .
-- ------------------------------------------
-- Evidences
  eq Evidences(Create-cc-1(S, I, V, D1, T), D2)
     = if ((D1 = D2) or (cc(D1) = D2)) then emptyE
       else Evidences(S, D2) fi .
-- ------------------------------------------
-- Place
  -- a new document is put in division V.
  eq Place(Create-cc-1(S, I, V, D1, T), D2)
     = if ((D1 = D2) or (cc(D1) = D2)) then V
       else Place(S, D2) fi .
-- ------------------------------------------
-- SessionID
  eq SessionID(Create-cc-1(S, I, V, D1, T), D2)
     = if ((D1 = D2) or (cc(D1) = D2)) then I
       else SessionID(S, D2) fi .
-- ------------------------------------------
-- Legal?
  -- Create-1 is a regular event.
  eq Legal?(Create-cc-1(S, I, V, D1, T), D2)
     = if ((D1 = D2) or (cc(D1) = D2)) then true
       else Legal?(S, D2) fi .
-- ------------------------------------------
-- OriginalID
  eq OriginalID(Create-cc-1(S, I, V, D1, T), D2)
     = if ((D1 = D2) or (cc(D1) = D2)) then I
       else OriginalID(S, D2) fi .
-- ------------------------------------------
-- DocumentIDList
  eq DocumentIDList(Create-cc-1(S, I1, V, D1, T1), I2, T2)
     = if (I1 = I2) then
         if (T1 = T2) then
            (D1 ; DocumentIDList(S, I1, T1))
         else
           if (cc(T1) = T2) then
              (cc(D1) ; DocumentIDList(S, I1, cc(T1)))
           else DocumentIDList(S, I1, T2) fi fi
       else DocumentIDList(S, I2, T2) fi .
-- ------------------------------------------
-- UntrustedSet
  eq UntrustedSet(Create-cc-1(S, I, V, D, T))
      = UntrustedSet(S) .
-- ------------------------------------------
--
-- ==============================
--  Create-cc-2(S, V, D1, T, D2)
-- ==============================
-- ----------------------------------
--  flamework of effective condition
-- ----------------------------------
  op c-Create-cc-2 :
     State Division DocumentID DocumentType DocumentID
     -> Bool
  -- the effective condition is that
  -- document D1 has not been created yet,
  -- document D2 has been created, and
  -- D2 is in division V.
  eq c-Create-cc-2(S, V, D1, T, D2)
     = (Place(S, D1) = noDivision) and
       (Place(S, D2) = V) .
-- ------------------------------------------
--
-- ------------------------------------------
-- DocumentType
  eq DocumentType(Create-cc-2(S, V, D1, T, D2), D3)
     = if (D1 = D3) then T
       else
          if (cc(D1) = D3) then cc(T)
          else DocumentType(S, D3) fi fi .
-- ------------------------------------------
-- Evidences
  eq Evidences(Create-cc-2(S, V, D1, T, D2), D3)
     = if ((D1 = D3) or (cc(D1) = D3))
          then emptyE
       else Evidences(S, D3) fi .
-- ------------------------------------------
-- Place
  -- a new document is put in division V.
  eq Place(Create-cc-2(S, V, D1, T, D2), D3)
     = if ((D1 = D3) or (cc(D1) = D3))
          then V
       else Place(S, D3) fi .
-- ------------------------------------------
-- SessionID
  eq SessionID(Create-cc-2(S, V, D1, T, D2), D3)
     = if ((D1 = D3) or (cc(D1) = D3)) then
          SessionID(S, D2)
       else SessionID(S, D3) fi .
-- ------------------------------------------
-- Legal?
  -- Create-cc-2 is a regular event.
  eq Legal?(Create-cc-2(S, V, D1, T, D2), D3)
     = if ((D1 = D3) or (cc(D1) = D3))
          then Legal?(S, D2)
       else Legal?(S, D3) fi .
-- ------------------------------------------
-- OriginalID
  eq OriginalID(Create-cc-2(S, V, D1, T, D2), D3)
     = if ((D1 = D3) or (cc(D1) = D3)) then
          SessionID(S, D2)
       else OriginalID(S, D3) fi .
-- ------------------------------------------
-- DocumentIDList
  eq DocumentIDList(Create-cc-2(S, V, D1, T1, D2), I, T2)
     = if (SessionID(S, D2) = I) then
         if (T1 = T2) then
            (D1 ; DocumentIDList(S, I, T1))
         else
           if (cc(T1) = T2) then
              (cc(D1) ; DocumentIDList(S, I, cc(T1)))
           else DocumentIDList(S, I, T2) fi fi
       else DocumentIDList(S, I, T2) fi .
-- ------------------------------------------
-- UntrustedSet
  eq UntrustedSet(Create-cc-2(S, V, D1, T, D2))
      = UntrustedSet(S) .
-- ------------------------------------------
--
-- ====================
--  Send(S, V1, D, V2)
-- ====================
-- ----------------------------------
--  flamework of effective condition
-- ----------------------------------
  op c-Send : State Division DocumentID Division
              -> Bool
  -- the effective condition is that
  -- document D had been created, and
  -- is in division V1.
  eq c-Send(S, V1, D, V2)
     = (Place(S, D) = V1) .
-- ------------------------------------------
--
-- ------------------------------------------
-- DocumentType
  eq DocumentType(Send(S, V1, D1, V2), D2)
     = DocumentType(S, D2) .
-- ------------------------------------------
-- Evidences
  eq Evidences(Send(S, V1, D1, V2), D2)
     = Evidences(S, D2) .
-- ------------------------------------------
-- Place
  -- a document is sent to division V.
  eq Place(Send(S, V1, D1, V2), D2)
     = if (D1 = D2) then V2
       else Place(S, D2) fi .
-- ------------------------------------------
-- SessionID
  eq SessionID(Send(S, V1, D1, V2), D2)
     = SessionID(S, D2) .
-- ------------------------------------------
-- Legal?
  eq Legal?(Send(S, V1, D1, V2), D2)
     = Legal?(S, D2) .
-- ------------------------------------------
-- OriginalID
  eq OriginalID(Send(S, V1, D1, V2), D2)
     = OriginalID(S, D2) .
-- ------------------------------------------
-- DocumentIDList
  eq DocumentIDList(Send(S, V1, D1, V2), I, T)
     = DocumentIDList(S, I, T) .
-- ------------------------------------------
-- UntrustedSet
  eq UntrustedSet(Send(S, V1, D1, V2))
      = UntrustedSet(S) .
-- ------------------------------------------
--
-- =============
--  Forge(S, D)
-- =============
-- ----------------------------------
--  flamework of effective condition
-- ----------------------------------
  op c-Forge : State DocumentID -> Bool
  -- the effective condition is that
  -- document D has been created and
  -- is in an untrusted division.
  eq c-Forge(S, D)
     = in?(Place(S, D), UntrustedSet(S)) .
-- ------------------------------------------
--
-- ------------------------------------------
-- DocumentType
  eq DocumentType(Forge(S, D1), D2)
     = DocumentType(S, D2) .
-- ------------------------------------------
-- Evidences
  eq Evidences(Forge(S, D1), D2)
     = if (D1 = D2) then emptyE
       else Evidences(S, D2) fi .
-- ------------------------------------------
-- Place
  eq Place(Forge(S, D1), D2) = Place(S, D2) .
-- ------------------------------------------
-- SessionID
  eq SessionID(Forge(S, D1), D2)
     = SessionID(S, D2) .
-- ------------------------------------------
-- Legal?
  eq Legal?(Forge(S, D1), D2)
     = if (D1 = D2) then
          if is-cc?(D1) then Legal?(S, D1)
             else false fi
       else Legal?(S, D2) fi .
-- ------------------------------------------
-- OriginalID
  eq OriginalID(Forge(S, D1), D2)
     = OriginalID(S, D2) .
-- ------------------------------------------
-- DocumentIDList
  eq DocumentIDList(Forge(S, D), I, T)
     = DocumentIDList(S, I, T) .
-- ------------------------------------------
-- UntrustedSet
  eq UntrustedSet(Forge(S, D))
      = UntrustedSet(S) .
-- ------------------------------------------
--
-- =====================
--  ChangeSession(S, D)
-- =====================
-- ----------------------------------
--  flamework of effective condition
-- ----------------------------------
  op c-ChangeSession : State DocumentID SessionID
                       -> Bool
  -- the effective condition is that
  -- document D has been created and
  -- is in an untrusted division.
  eq c-ChangeSession(S, D, I)
      = in?(Place(S,D), UntrustedSet(S)) and
        (D = top(DocumentIDList(S,
                                I,
                                DocumentType(S, D)))) .
-- ------------------------------------------
--
-- ------------------------------------------
-- DocumentType
  eq DocumentType(ChangeSession(S, D1, I), D2)
     = DocumentType(S, D2) .
-- ------------------------------------------
-- Evidences
  eq Evidences(ChangeSession(S, D1, I), D2)
     = Evidences(S, D2) .
-- ------------------------------------------
-- Place
  eq Place(ChangeSession(S, D1, I), D2) = Place(S, D2) .
-- ------------------------------------------
-- SessionID
  eq SessionID(ChangeSession(S, D1, I), D2)
     = if (D1 = D2) then I
       else SessionID(S, D2) fi .
-- ------------------------------------------
-- Legal?
  eq Legal?(ChangeSession(S, D1, I), D2)
     = if (D1 = D2) then false 
       else Legal?(S, D2) fi .
-- ------------------------------------------
-- OriginalID
  eq OriginalID(ChangeSession(S, D1, I), D2)
     = OriginalID(S, D2) .
-- ------------------------------------------
-- DocumentIDList
  eq DocumentIDList(ChangeSession(S, D, I1), I2, T)
     = if ((I1 = I2) and (DocumentType(S, D) = T)) then
          (D ; DocumentIDList(S, I1, T))
       else
         if ((SessionID(S, D) = I2) and
             (DocumentType(S, D) = T)) then
            delete(D, DocumentIDList(S, I2, T))
         else DocumentIDList(S, I2, T) fi fi .
-- ------------------------------------------
-- UntrustedSet
  eq UntrustedSet(Forge(S, D))
      = UntrustedSet(S) .
-- ------------------------------------------
--
-- =======================
--  Check-1(S, V, D1, D2)
-- =======================
-- ----------------------------------
--  flamework of effective condition
-- ----------------------------------
  op c-Check-1 : State Division DocumentID DocumentID
                 -> Bool
  -- the effective condition is that
  -- the document D1 and D2 have been created, 
  -- in division V, and
  -- in the same session. 
  eq c-Check-1(S, V, D1, D2)
      = (Place(S, D1) = V) and
        (Place(S, D2) = V) and
        (SessionID(S, D1) = SessionID(S, D2)) .
-- ------------------------------------------
--
-- ------------------------------------------
-- DocumentType
  eq DocumentType(Check-1(S, V, D1, D2), D3)
     = DocumentType(S, D3) .
-- ------------------------------------------
-- Evidences
  -- the check for D1 is passed when 
  -- the boolean value in D1 is the same as D2,
  -- o.w. the check for D1 is not passed.
  -- when the check is passed, 
  -- an evidence is put in D1.
  eq Evidences(Check-1(S, V, D1, D2), D3)
     = if (D1 = D3) then
          if (Legal?(S, D1) = Legal?(S, D2)) then
             (ch(DocumentType(S, D2)) Evidences(S, D1))
          else Evidences(S, D1) fi
       else Evidences(S, D3) fi .
-- ------------------------------------------
-- Place
  eq Place(Check-1(S, V, D1, D2), D3)
     = Place(S, D3) .
-- ------------------------------------------
-- SessionID
  eq SessionID(Check-1(S, V, D1, D2), D3)
     = SessionID(S, D3) .
-- ------------------------------------------
-- Legal?
  eq Legal?(Check-1(S, V, D1, D2), D3)
     = Legal?(S, D3) .
-- ------------------------------------------
-- OriginalID
  eq OriginalID(Check-1(S, V, D1, D2), D3)
     = OriginalID(S, D3) .
-- ------------------------------------------
-- DocumentIDList
  eq DocumentIDList(Check-1(S, V, D1, D2), I, T)
     = DocumentIDList(S, I, T) .
-- ------------------------------------------
-- UntrustedSet
  eq UntrustedSet(Check-1(S, V, D1, D2))
      = UntrustedSet(S) .
-- ------------------------------------------
--
-- =============================
--  Check-2(S, V, D1, E, D2)
-- =============================
-- ----------------------------------
--  flamework of effective condition
-- ----------------------------------
  op c-Check-2 :
     State Division DocumentID Evidence DocumentID
     -> Bool
  -- the effective condition is that
  -- document D1 and D2 have been created, 
  -- they are in division V, and
  -- are in the same session.
  eq c-Check-2(S, V, D1, E, D2)
     = (Place(S, D1) = V) and
       (Place(S, D2) = V) and
       (SessionID(S, D1) = SessionID(S, D2)) .
-- ------------------------------------------
--
-- ------------------------------------------
-- DocumentType
  eq DocumentType(Check-2(S, V, D1, E, D2), D3)
     = DocumentType(S, D3) .
-- ------------------------------------------
-- Evidences
  -- if document D1 has an evidence E, 
  -- document D1 is checked with D2.
     -- the check for D1 is passed, 
     -- if the boolean value in D1 is the same as D2,
     -- o.w. the check for D1 is not passed.
  -- when the check is passed, 
  -- an evidence is put in D1.
  eq Evidences(Check-2(S, V, D1, E, D2), D3)
     = if (D1 = D3) then
          if (in?(E, Evidences(S, D1)) and
              (Legal?(S, D1) = Legal?(S, D2))) then
             (ch(DocumentType(S, D2)) Evidences(S, D1))
          else Evidences(S, D1) fi
       else Evidences(S, D3) fi .
-- ------------------------------------------
-- Place
  eq Place(Check-2(S, V, D1, E, D2), D3)
     = Place(S, D3) .
-- ------------------------------------------
-- SessionID
  eq SessionID(Check-2(S, V, D1, E, D2), D3)
     = SessionID(S, D3) .
-- ------------------------------------------
-- Legal?
  eq Legal?(Check-2(S, V, D1, E, D2), D3)
     = Legal?(S, D3) .
-- ------------------------------------------
-- OriginalID
  eq OriginalID(Check-2(S, V, D1, E, D2), D3)
     = OriginalID(S, D3) .
-- ------------------------------------------
-- DocumentIDList
  eq DocumentIDList(Check-2(S, V, D1, E, D2), I, T)
     = DocumentIDList(S, I, T) .
-- ------------------------------------------
-- UntrustedSet
  eq UntrustedSet(Check-2(S, V, D1, E, D2))
      = UntrustedSet(S) .
-- ------------------------------------------
--
-- ==========================
--  Check-3(S, V, D1, D2, E)
-- ==========================
-- ----------------------------------
--  flamework of effective condition
-- ----------------------------------
  op c-Check-3 :
     State Division DocumentID DocumentID Evidence
     -> Bool
  -- the effective condition is that
  -- the document D1 and D2 have been created,
  -- they are in division V, and
  -- are in the same session.
  eq c-Check-3(S, V, D1, D2, E)
      = (Place(S, D1) = V) and
        (Place(S, D2) = V) and
        (SessionID(S, D1) = SessionID(S, D2)) .
-- ------------------------------------------
--
-- ------------------------------------------
-- DocumentType
  eq DocumentType(Check-3(S, V, D1, D2, E), D3)
     = DocumentType(S, D3) .
-- ------------------------------------------
-- Evidences
  -- if document D2 has an evidence E, 
  -- document D1 is checked with D2.
     -- the check for D1 is passed, 
     -- if the boolean value in D1 is the same as D2,
     -- o.w. the check for D1 is not passed.
  -- when the check is passed, 
  -- an evidence is put in D1.
  eq Evidences(Check-3(S, V, D1, D2, E), D3)
     = if (D1 = D3) then
          if (in?(E, Evidences(S, D2)) and
              (Legal?(S, D1) = Legal?(S, D2))) then
             (ch(DocumentType(S, D2)) Evidences(S, D1))
          else Evidences(S, D1) fi
       else Evidences(S, D3) fi .
-- ------------------------------------------
-- Place
  eq Place(Check-3(S, V, D1, D2, E), D3)
     = Place(S, D3) .
-- ------------------------------------------
-- SessionID
  eq SessionID(Check-3(S, V, D1, D2, E), D3)
     = SessionID(S, D3) .
-- ------------------------------------------
-- Legal?
  eq Legal?(Check-3(S, V, D1, D2, E), D3)
     = Legal?(S, D3) .
-- ------------------------------------------
-- OriginalID
  eq OriginalID(Check-3(S, V, D1, D2, E), D3)
     = OriginalID(S, D3) .
-- ------------------------------------------
-- DocumentIDList
  eq DocumentIDList(Check-3(S, V, D1, D2, E), I, T)
     = DocumentIDList(S, I, T) .
-- ------------------------------------------
-- UntrustedSet
  eq UntrustedSet(Check-3(S, V, D1, D2, E))
      = UntrustedSet(S) .
-- ------------------------------------------
--
-- ===============================
--  Check-4(S, V, D1, E1, D2, E2)
-- ===============================
-- ----------------------------------
--  flamework of effective condition
-- ----------------------------------
  op c-Check-4 :
     State Division DocumentID Evidence DocumentID Evidence 
     -> Bool
  -- the effective condition is that
  -- the document D1 and D2 have been created and
  -- they are in division V.
  eq c-Check-4(S, V, D1, E1, D2, E2) 
     = (Place(S, D1) = V) and
       (Place(S, D2) = V) and
       (SessionID(S, D1) = SessionID(S, D2)) .
-- ------------------------------------------
--
-- ------------------------------------------
-- DocumentType
  eq DocumentType(Check-4(S, V, D1, E1, D2, E2), D3)
     = DocumentType(S, D3) .
-- ------------------------------------------
-- Evidences
  -- if document D1 and D2 are in division V and
  --    D1 and D2 have an evidence E1 and
  --    E2 respectively, 
  -- document D1 is checked with D2.
     -- the check for D1 is passed, 
     -- if the boolean value in D1 is the same as D2,
     -- o.w. the check for D1 is not passed.
  -- when the check is passed, 
  -- an evidence is put in D1.
  eq Evidences(Check-4(S, V, D1, E1, D2, E2), D3)
     = if (D1 = D3) then
          if (in?(E1, Evidences(S, D1)) and
              in?(E2, Evidences(S, D2)) and
              (Legal?(S, D1) = Legal?(S, D2))) then
             (ch(DocumentType(S, D2)) Evidences(S, D1))
          else Evidences(S, D1) fi
       else Evidences(S, D3) fi .
-- ------------------------------------------
-- Place
  eq Place(Check-4(S, V, D1, E1, D2, E2), D3)
     = Place(S, D3) .
-- ------------------------------------------
-- SessionID
  eq SessionID(Check-4(S, V, D1, E1, D2, E2), D3)
     = SessionID(S, D3) .
-- ------------------------------------------
-- Legal?
  eq Legal?(Check-4(S, V, D1, E1, D2, E2), D3)
     = Legal?(S, D3) .
-- ------------------------------------------
-- OriginalID
  eq OriginalID(Check-4(S, V, D1, E1, D2, E2), D3)
     = OriginalID(S, D3) .
-- ------------------------------------------
-- DocumentIDList
  eq DocumentIDList(Check-4(S, V, D1, E1, D2, E2), I, T)
     = DocumentIDList(S, I, T) .
-- ------------------------------------------
-- UntrustedSet
  eq UntrustedSet(Check-4(S, V, D1, E1, D2, E2))
      = UntrustedSet(S) .
-- ------------------------------------------
--
-- ====================
--  Approve-1(S, V, D)
-- ====================
-- ----------------------------------
--  flamework of effective condition
-- ----------------------------------
  op c-Approve-1 :
     State Division DocumentID -> Bool
  -- the effective condition is that
  -- the document D has been created and
  -- is in division V.
  eq c-Approve-1(S, V, D)
     = (Place(S, D) = V) .
-- ------------------------------------------
--
-- ------------------------------------------
-- DocumentType
  eq DocumentType(Approve-1(S, V, D1), D2)
     = DocumentType(S, D2) .
-- ------------------------------------------
-- Evidences
  eq Evidences(Approve-1(S, V, D1), D2)
     = if (D1 = D2) then
          (apv(V) Evidences(S, D1))
       else Evidences(S, D2) fi .
-- ------------------------------------------
-- Place
  eq Place(Approve-1(S, V, D1), D2)
     = Place(S, D2) .
-- ------------------------------------------
-- SessionID
  eq SessionID(Approve-1(S, V, D1), D2)
     = SessionID(S, D2) .
-- ------------------------------------------
-- Legal?
  eq Legal?(Approve-1(S, V, D1), D2)
     = Legal?(S, D2) .
-- ------------------------------------------
-- OriginalID
  eq OriginalID(Approve-1(S, V, D1), D2)
     = OriginalID(S, D2) .
-- ------------------------------------------
-- DocumentIDList
  eq DocumentIDList(Approve-1(S, V, D), I, T)
     = DocumentIDList(S, I, T) .
-- ------------------------------------------
-- UntrustedSet
  eq UntrustedSet(Approve-1(S, V, D))
      = UntrustedSet(S) .
-- ------------------------------------------
--
-- =======================
--  Approve-2(S, V, D, E)
-- =======================
-- ----------------------------------
--  flamework of effective condition
-- ----------------------------------
  op c-Approve-2 :
     State Division DocumentID Evidence -> Bool
  -- the effective condition is that
  -- the document D has been created and
  -- is in division V.
  eq c-Approve-2(S, V, D, E) 
     = (Place(S, D) = V) .
-- ------------------------------------------
--
-- ------------------------------------------
-- DocumentType
  eq DocumentType(Approve-2(S, V, D1, E), D2)
     = DocumentType(S, D2) .
-- ------------------------------------------
-- Evidences
  -- if D1 has an evidence E, 
  -- document D1 is approved.
  eq Evidences(Approve-2(S, V, D1, E), D2)
     = if (D1 = D2) then
          if in?(E, Evidences(S, D1)) then
             (apv(V) Evidences(S, D1))
          else Evidences(S, D1) fi 
       else Evidences(S, D2) fi .
-- ------------------------------------------
-- Place
  eq Place(Approve-2(S, V, D1, E), D2)
     = Place(S, D2) .
-- ------------------------------------------
-- SessionID
  eq SessionID(Approve-2(S, V, D1, E), D2)
     = SessionID(S, D2) .
-- ------------------------------------------
-- Legal?
  eq Legal?(Approve-2(S, V, D1, E), D2)
     = Legal?(S, D2) .
-- ------------------------------------------
-- OriginalID
  eq OriginalID(Approve-2(S, V, D1, E), D2)
     = OriginalID(S, D2) .
-- ------------------------------------------
-- DocumentIDList
  eq DocumentIDList(Approve-2(S, V, D, E), I, T)
     = DocumentIDList(S, I, T) .
-- ------------------------------------------
-- UntrustedSet
  eq UntrustedSet(Approve-2(S, V, D, E))
      = UntrustedSet(S) .
-- ------------------------------------------
--
} eof