-- ========================================================================
--                  QLOCK property specification
-- ========================================================================

-- ========================================================================
-- a comment starts with '-- ' or '** ' and ends at the end of line
--
-- a convention for commenting:
--   '-- ' is used before the commented CafeOBJ text
--   '** ' is used after the commented CafeOBJ text
-- ========================================================================

-- ========================================================================
-- this file requires the modules defined in the files qlock-sys.cafe 
-- and predCj.cafe if the features qlock-sys/predCi are not provided yet
require qlock-sys
require genCheck

-- ========================================================================
-- elementary functions on states 
mod! STATEfuns {ex(STATE + PNAT)
** 'ex' (shorthand for extending) indicates importation of module
** whithout changing equalities among existing elements
** but may introduce new elements into existing sorts
-- the queue in a state
op qu : State -> Qu .
eq qu(Q:Qu $ AS:Aobs) = Q .
-- the agent observations in a state
op aos : State -> Aobs .
eq aos(Q:Qu $ AS:Aobs) = AS .
-- length of an Aobs
op #laos : Aobs -> Nat.PNAT .
eq #laos(empty) = 0 .
eq #laos(A:Aob AS:Aobs) = (s 0) + #laos(AS) .
-- the number of a label in an Aobs
op #lss : Aobs Label -> Nat.PNAT .
eq #lss(empty,L:Label) = 0 .
eq #lss(((lb[A:Aid]: L1:Label) AS:Aobs),L2:Label) = 
   if (L1 = L2) then (s 0) + #lss((AS),L2) 
   else #lss(AS,L2) fi .
-- the number of a label in a state
op #ls : State Label -> Nat.PNAT .
eq #ls(S:State,L:Label) = #lss(aos(S),L) .
-- the number of an Aid in an Aobs
op #ass : Aobs Aid -> Nat.PNAT .
eq #ass(empty,A:Aid) = 0 .
eq #ass(((lb[A1:Aid]: L:Label) AS:Aobs),A2:Aid) =
   if (A1 = A2) then (s 0) + #ass((AS),A2) else #ass(AS,A2) fi .
-- the number of an Aid in a state
op #as : State Aid -> Nat.PNAT .
eq #as(S:State,A:Aid) = #ass(aos(S),A) .
-- the number of an Aid in a queue
op #aq : Qu Aid -> Nat.PNAT .
eq #aq(empQ,A:Aid) = 0 .
eq #aq(A1:Aid & Q:Qu,A2:Aid) =
   if (A1 = A2) then (s 0) + #aq(Q,A2) else #aq(Q,A2) fi .
-- label of an agent in an Aobs
op laga : Aobs Aid -> Label .
eq laga(((lb[A1:Aid]: L:Label) AS:Aobs),A2:Aid) = 
   if (A1 = A2) then L else laga(AS,A2) fi .
-- label of an agent in a state
op lags : State Aid -> Label .
eq lags(S:State,A:Aid) = laga(aos(S),A) .
}

-- ========================================================================
-- PREDcj with STATE for 'X :: TRIVE' by viewing Elt as State 
mod! STATEpcj {pr(PREDcj(STATE{sort Elt -> State}))}

-- ========================================================================
-- elemental predicates on states for defining intitial states
mod! STATEpred-init {ex(STATEfuns + STATEpcj)
-- at least one agent in a state
op aoa : -> Pname .
eq[aoa]: cj(aoa,S:State) = (#laos(aos(S)) > 0) .
-- no duplication of an Aid in a Aobs
op 1as : Aobs -> Bool .
eq 1as(empty) = true .
eq 1as((lb[A:Aid]: L:Label) AS:Aobs) = (#ass(AS,A) = 0) and 1as(AS) .
-- no duplication of an Aid in a state 
op 1a : -> Pname .
eq[1a]: cj(1a,S:State) = 1as(aos(S)) .
-- well formed states
op wfs : -> Pname .
eq[wfs]: wfs = aoa 1a .
-- the queue is empty
op qe : -> Pname .
eq[qe]: cj(qe,S:State) = (qu(S) = empQ) .
-- any Aid is in rs status, i.e. no ws, no cs
op allRs : -> Pname .
eq[allRs]: cj(allRs,S:State) = (#ls(S,ws)= 0) and (#ls(S,cs)= 0) .
}

-- ========================================================================
-- an initial state predicate init, that is
-- a predicate with (init(S:State) iff (S is a initial state))
mod! INIT {ex(STATEpred-init)
op init : -> PnameSeq .
eq init = wfs qe allRs .
}

-- ========================================================================
-- queues with head and tail operations
mod* AID-QUEUE-a {ex(AID-QUEUE)
-- head
op hd_ : Qu -> Aid .
eq hd(E:Aid & Q:Qu) = E .
** hd(empQ):Aid indicates an error element
** and no equations for it; an error handling method
-- tail
op tl_ : Qu -> Qu .
eq tl(E:Aid & Q:Qu) = Q .
** tl(empQ):Qu indicates an error queue
** and no equations for it; an error handling method
}

-- ========================================================================
-- predicates on states for an inductive invariant predicate
mod! STATEpred-inv {ex(STATEpred-init + AID-QUEUE-a)
-- mutual exclusion property: at most one agent is with cs
-- this is the goal predicate
op mx : -> Pname .
eq[mx]: cj(mx,S:State) = (#ls(S,cs) = 0) or (#ls(S,cs) = (s 0)) .
-- several predicate names for inductive invariants
ops qep rs ws cs : -> Pname .
-- if queue is empty
eq[qep]: cj(qep,(Q:Qu $ ((lb[A:Aid]: L:Label) AS:Aobs))) 
         = ((Q = empQ) implies (#lss(((lb[A]: L) AS),cs) = 0)) .
-- if agent is with rs
eq[:m-and rs]: cj(rs,(Q:Qu $ ((lb[A:Aid]: L:Label) AS:Aobs)))
               = ((L = rs) implies (#aq(Q,A) = 0)) .
** An equation like 'eq[:m-and ...]: l = r .' indicates that
** (1) left hand side l and right hand side r of the equation 
**     are of sort Bool 
** (2) if there are multiple matches m_1,...,m_k (k = 2,3,...)
**     (match m_i is a map from variables to terms 
**      and is extended to a map from terms to terms)
**     such that m_i(l) = t for a Boolean term t, 
**     the application of the equation 'l = r' to t is instantiated to
**     't = m_1(r) and-also m_2(r) and-also ... and-also m_k(r)'.
** Hence, applying the equation 'eq[:m-and rs]:...' to a Boolean term
** 'cj(rs,(q $ ((lb[a1]: l1) (lb[a2]: l2) as)))', we get the following
** instantiated equation.
**    cj(rs,(q $ ((lb[a1]: l1) (lb[a2]: l2) as)))
**    = ((l1 = rs) implies (#aq(q,a1) = 0))  and-also
**      ((l2 = rs) implies (#aq(q,a2) = 0)) .
** where 
**  '((l1 = rs) implies (#aq(q,a1) = 0))' is gotten 
**  with match {Q->q,A->a1,L->l1,AS->((lb[a2]: l2) as)} and
**  '((l2 = rs) implies (#aq(q,a2) = 0))' is gotten 
**  with match {Q->q,A->a2,L->l2,AS->((lb[a1]: l1) as)}.
-- if agent is with ws
eq[:m-and ws]: cj(ws,(Q:Qu $ ((lb[A:Aid]: L:Label) AS:Aobs))) 
        = ((L = ws) implies 
           ((#aq(Q,A) = (s 0)) and
            ((A = hd(Q)) implies (#lss((AS),cs) = 0)))) .
-- if agent is with cs
eq[:m-and cs]: cj(cs,(Q:Qu $ ((lb[A:Aid]: L:Label) AS:Aobs))) 
        = ((L = cs) implies ((A = hd(Q)) and 
                             (#aq(tl(Q),A) = 0) and 
                             (#lss((AS),cs) = 0))) .
}

-- ========================================================================
-- enhanced elementary functions on states 
-- for verifying a (p leads-to q) property
mod! STATEfuns-pq {ex(STATEfuns + PNAT*) 
-- the depth of the first appearence of an aid in a queue
op #daq : Qu Aid -> Nat.PNAT .
eq #daq(A1:Aid & Q:Qu,A2:Aid) = 
   if (A1 = A2) then 0 else s(#daq(Q,A2)) fi .
-- counter count of cs
op #ccs : State -> Nat.PNAT .
eq #ccs(S:State) = if (#ls(S,cs) > 0) then 0 else (s 0) fi .
-- decreasing Nat measure for the (p leads-to q) property
op #dms : State Aid -> Nat.PNAT .
eq #dms(S:State,A:Aid) 
   = ((s s s 0) * #daq(qu(S),A)) + #ls(S,rs) + #ccs(S) .
-- the transition:
-- (((b1 & q) $ (((lb [ b22 ] : ws) (lb [ b1 ] : cs)) as1)) ->
--         (q $ ((lb [ b1 ] : rs) ((lb [ b22 ] : ws) as1)))
-- increases (#ls(_,rs) + #ccs(_)) by (s s 0) 
-- decreases #daq(qu(_),b22)) by (s 0)
-- so we need ((s s s 0) * (s 0) = (s s s 0)) 
-- for proper decrease of #dms(_,b22)
}

-- ========================================================================
-- State with p,q,m 
-- for verifying a (p leads-to q) property
mod! PQMonST {
ex(STATEpcj + STATEfuns-pq)
ops p q : State Aid -> Bool .
op m : State Aid -> Nat.PNAT .
eq p(S:State,A:Aid) = (lags(S,A) = ws) .
eq q(S:State,A:Aid) = (lags(S,A) = cs) .
eq m(S:State,A:Aid) = #dms(S,A) .
}

-- ========================================================================
-- ExState with PQMonST/State and Aid/Date
-- and a new invariant on the ExState = (State % Date)
mod! EX-PQMonST {
pr((PCJ-EX-STATE(
            PQMonST{sort Ste -> State, sort Data -> Aid,
                    sort Pnm -> Pname, sort PnmSeq -> PnameSeq})))
-- if an agent is in the Qu then the agent is in Aobs
op qas : -> ExPname .
eq cj(qas,((Q:Qu $ AS:Aobs) % A:Aid)) 
   = ((#aq(Q, A) = s 0) implies not(#ass(AS, A) = 0)) .
}

-- ========================================================================
-- possible inductive invariant predicates
mod! INV {ex(EX-PQMonST + STATEpred-inv)
ops inv1 inv2 : -> PnameSeq .
ops inv3 : -> ExPnameSeq .
eq inv1 = wfs .
eq inv2 = mx qep rs ws cs .
eq inv3 = qas .
}

-- ========================================================================
-- this file provides feature qlock-prop
provide qlock-prop

-- ========================================================================
eof
** end of file