-- invariant properties

mod INV {
  pr ( SALE-AND-SHIP )

  op inv1 : SaleAndShip DocumentID -> Bool
  op inv2 : SaleAndShip DocumentID -> Bool
  op inv3 : SaleAndShip DocumentID -> Bool
  op inv4 : SaleAndShip DocumentID DocumentID -> Bool
  op inv5 : SaleAndShip SessionID DocumentID -> Bool
  op inv6 : SaleAndShip DocumentID DocumentID DocumentID
            -> Bool
  op inv7 : SaleAndShip SessionID DocumentID DocumentID
            -> Bool
  op inv8 : SaleAndShip DocumentID DocumentID -> Bool
  op inv9 : SaleAndShip DocumentID -> Bool
  op inv10 : SaleAndShip DocumentID DocumentID -> Bool
  op inv11 : SaleAndShip DocumentID -> Bool
--
  op doc-inv1 :
     SaleAndShip SessionID DocumentID DocumentType
     -> Bool
  op doc-inv2 : SaleAndShip DocumentID
                -> Bool
  op doc-inv3 : SaleAndShip DocumentID DocumentType
                -> Bool
--
  var S : SaleAndShip
  vars D D1 D2 D3 : DocumentID
  var I : SessionID
  var T : DocumentType
-- 
  eq inv1(S, D)
     = ((DocumentType(S, D) = report) and
        (Place(S, D) = sales) and
        in?(ch(order), Evidences(S, D)))
       implies
       (Legal?(S, D) = true) .
--
  eq inv2(S, D)
     = ((DocumentType(S, D) = order) and
        in?(apv(sales), Evidences(S, D)) and
        (Legal?(S, D) = false))
       implies
       (DocumentIDList(S, SessionID(S, D), receipt) =
        nillDID) .
--
  eq inv3(S, D)
     = ((DocumentType(S, D) = report) and
        (Place(S, D) = shipping))
       implies
       (Evidences(S, D) = emptyE) .
--
 eq inv4(S, D1, D2)
    = ((DocumentType(S, D1) = order) and
       (DocumentType(S, D2) = invoice) and
       (Legal?(S, D1) = false) and
       in?(apv(sales), Evidences(S, D1)))
      implies
      (Evidences(S, D2) = emptyE) .
--
  eq inv5(S, I, D)
     = ((D = top(DocumentIDList(S, I, ack))) and
        (Place(S, D) = sales))
       implies
       (DocumentIDList(S, I, receipt) =
        nillDID) .
--
  eq inv6(S, D1, D2, D3)
    = ((DocumentType(S, D1) = order) and
       (DocumentType(S, D2) = cc(order)) and
       (DocumentType(S, D3) = invoice) and
       (Legal?(S, D1) = false) and
       in?(apv(sales), Evidences(S, D1)))
      implies
      not(Legal?(S, D2) = Legal?(S, D3)) .
--
  eq inv7(S, I, D1, D2)
     = ((D1 = top(DocumentIDList(S, I, ack))) and
        (Place(S, D1) = sales) and
        (SessionID(S, D2) = I))
       implies
       not(DocumentType(S, D2) = invoice) .
--
  eq inv8(S, D1, D2)
     = ((DocumentType(S, D1) = invoice) and
        (DocumentType(S, D2) = ack) and
        (SessionID(S, D1) = SessionID(S, D2)))
       implies
       (Place(S, D2) = client) .
--
  eq inv9(S, D)
     = (DocumentIDList(S, SessionID(S, D), ack)
        = nillDID)
       implies
       (DocumentIDList(S, SessionID(S, D), receipt) =
        nillDID) .
--
  eq inv10(S, D1, D2)
     = ((DocumentIDList(S, SessionID(S, D1), ack)
         = nillDID) and
        (SessionID(S, D1) = SessionID(S, D2)))
       implies
       not(DocumentType(S, D2) = invoice) .
--
  eq inv11(S, D)
     = (DocumentType(S, D) = invoice)
       implies
       not(DocumentIDList(S, SessionID(S, D), ack)
           = nillDID) .
--
  eq doc-inv1(S, I, D, T)
     = (D = top(DocumentIDList(S, I, T)))
       iff
       (DocumentType(S, D) = T) .
--
  eq doc-inv2(S, D)
     = (Place(S, D) = noDivision)
       implies
       (DocumentType(S, D) = noDocumentType) .
--
  eq doc-inv3(S, D, T)
     = (DocumentIDList(S, SessionID(S, D), T)
        = nillDID)
       implies
       not(DocumentType(S, D) = T) .

}

eof