-- ========================================================================
--        ABP modules for defining 3 verification conditions
-- ========================================================================

-- ========================================================================
require genCheck
require abp-prop

-- ========================================================================
mod! ABP-INV-1 {pr(INV-1v(STATE
                   {sort Ste -> PreState, 
                    sort Pnm -> Pname, sort PnmSeq -> PnameSeq}))}

-- ========================================================================
mod! ABP-INV-2 {pr(INV-2v(STATE
                   {sort Ste -> PreState, 
                    sort Pnm -> Pname, sort PnmSeq -> PnameSeq}))}

-- ========================================================================
mod! ABP-INV-3 {pr(INV-3q(STATE
                   {sort Ste -> PreState, 
                    sort Pnm -> Pname, sort PnmSeq -> PnameSeq}))}

-- ========================================================================
provide abp-genCheck

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