-- ========================================================================
--        QLOCK modules for defining 7 verification conditions
-- ========================================================================

-- ========================================================================
require genCheck
require qlock-prop

-- ========================================================================
mod! Q-INV-1 {pr(INV-1v(EX-PQMonST
                   {sort Ste -> ExState, 
                    sort Pnm -> ExPname, sort PnmSeq -> ExPnameSeq}))}

-- ========================================================================
mod! Q-INV-2 {pr(INV-2v(EX-PQMonST
                   {sort Ste -> ExState, 
                    sort Pnm -> ExPname, sort PnmSeq -> ExPnameSeq}))}

-- ========================================================================
mod! Q-INV-3 {pr(INV-3q(EX-PQMonST
                   {sort Ste -> ExState, 
                    sort Pnm -> ExPname, sort PnmSeq -> ExPnameSeq}))}

-- ========================================================================
mod! Q-PQ-1 {pr(PQ-1q(EX-PQMonST
                  {sort Ste -> ExState, sort Nat -> Nat.PNAT,
                   sort Pnm -> ExPname, sort PnmSeq -> ExPnameSeq}))}

-- ========================================================================
mod! Q-PQ-2 {pr(PQ-2q(EX-PQMonST
                  {sort Ste -> ExState, sort Nat -> Nat.PNAT,
                   sort Pnm -> ExPname, sort PnmSeq -> ExPnameSeq}))}

-- ========================================================================
mod! Q-PQ-3 {pr(PQ-3v(EX-PQMonST
                  {sort Ste -> ExState, sort Nat -> Nat.PNAT,
                   sort Pnm -> ExPname, sort PnmSeq -> ExPnameSeq}))}

-- ========================================================================
mod! Q-PQ-4 {pr(PQ-4v(EX-PQMonST
                  {sort Ste -> ExState, sort Nat -> Nat.PNAT,
                   sort Pnm -> ExPname, sort PnmSeq -> ExPnameSeq}))}

-- ========================================================================
provide qlock-genCheck

-- ========================================================================
eof