-- ========================================================================
--            QLOCK Proof score for invariant properties
--                the third verification condition 
-- ========================================================================

-- ========================================================================
require qlock-genCheck
require qlock-genStTerm
require qlock-constAndLitl
require qlock-factTbu

-- ========================================================================
mod! Q-INV-3-genCheck {ex(Q-INV-3 + GENstTerm + CONSTandLITL)
-- if an agent is in the Qu then the agent is in Aobs
ops sst1 sst2 sst3 : -> SqSqTr .
eq sst1 =
 [(g("_%_")[(g("_$_")[empQ,(g("lb[_]:__")[b1,rs,as])]),
            (b1;b2)]),SS:ExState,CC:Bool]
        || 
 [(g("_%_")[(g("_$_")[(b1 & q),(g("lb[_]:__")[(b1;b2),rs,as])]),
            (b1;b2;b3)]),SS,CC]
.
eq sst2 = 
 [(g("_%_")[(g("_$_")[(b1 & q),(g("lb[_]:__")[b1,ws,as])]),
            (b1;b2)]),SS:ExState,CC:Bool]
.
eq sst3 =
 [(g("_%_")[(g("_$_")[(b1 & q),(g("lb[_]:__")[(b1;b2),cs,as])]),
            (b1;b2;b3)]),SS:ExState,CC:Bool]
.
op ck : -> IndTr . eq ck = check(sst1 || sst2 || sst3) .
}
-- ========================================================================
-- Generate&Check-T1  
open Q-INV-3-genCheck . pr(QLOCKsys1 + INV + FACTtbu)  
  eq pre = inv1 inv2 inv3 . eq post = inv1 inv2 inv3 .
  red ck . close 
-- ========================================================================
-- Generate&Check-T2
open Q-INV-3-genCheck . pr(WT + INV + FACTtbu)  
  eq pre = inv1 inv2 inv3 . eq post = inv1 inv2 inv3 .
  red check(sst1) . close 
open Q-INV-3-genCheck . pr(TY + INV + FACTtbu)  
  eq pre = inv1 inv2 inv3 . eq post = inv1 inv2 inv3 .
  red check(sst2) . close 
open Q-INV-3-genCheck .  pr(EXc + INV + FACTtbu) 
  eq pre = inv1 inv2 inv3 . eq post = inv1 inv2 inv3 .
  red check(sst3) . close 

-- ========================================================================
eof
** end of file
** the system reads the input file until this key word
** the text after this is comment and not be read by the system

-- ========================================================================
-- covering state patterns for QLOCK
-- ========================================================================
--
-- the following shows left hand sides of 
-- the three transition rules of QLOCK
--
-- [wt]  l1 =           (Q:Qu  $ ((lb[A:Aid]:  rs) AS:Aobs))
-- [ty]  l2 =  ((A:Aid & Q:Qu) $ ((lb[A]:      ws) AS:Aobs))
-- [exc] l3 = ((A1:Aid & Q:Qu) $ ((lb[A2:Aid]: cs) AS:Aobs))
--
--
-- let op q : -> Qu . op as : -> Aobs . ops b1 b2 : -> AidLt .
-- then the following state patterns t1,...,t6 are covering 
-- the left hand sides of the transition rules

ex(CONSTandLITL)
ops t1 t2 t3 t4 t5 t6 : -> State .
-- covering l1
eq t1 =     (empQ $ ((lb[b1]: rs) as)) .  -- wt
eq t2 = ((b1 & q) $ ((lb[b1]: rs) as)) .  -- wt
eq t3 = ((b1 & q) $ ((lb[b2]: rs) as)) .  -- wt
-- covering l2
eq t4 = ((b1 & q) $ ((lb[b1]: ws) as)) .  -- ty
-- covering l3
eq t5 = ((b1 & q) $ ((lb[b1]: cs) as)) .  -- exc
eq t6 = ((b1 & q) $ ((lb[b2]: cs) as)) .  -- exc

-- ========================================================================

 [(g("_%_")[(g("_$_")[empQ,(g("lb[_]:__")[b1,rs,as])]),
            (b1;b2)]),SS:ExState,CC:Bool] 
        || 
 [(g("_%_")[(g("_$_")[(b1 & q),(g("lb[_]:__")[(b1;b2),rs,as])]),
            (b1;b2;b3)]),SS,CC]
        ||

 [(g("_%_")[(g("_$_")[(b1 & q),(g("lb[_]:__")[b1,ws,as])]),
            (b1;b2)]),SS,CC]
        ||

 [(g("_%_")[(g("_$_")[(b1 & q),(g("lb[_]:__")[(b1;b2),cs,as])]),
            (b1;b2;b3)]),SS,CC]
=red=>
    [ (((empQ $ ((lb [ b1 ] : rs) as)) % b1) , SS , CC) ] || 
    [ (((empQ $ ((lb [ b1 ] : rs) as)) % b2) , SS , CC) ] || 
[ ((((b1 & q) $ ((lb [ b1 ] : rs) as)) % b1) , SS , CC) ] || 
[ ((((b1 & q) $ ((lb [ b2 ] : rs) as)) % b1) , SS , CC) ] || 
[ ((((b1 & q) $ ((lb [ b1 ] : rs) as)) % b2) , SS , CC) ] || 
[ ((((b1 & q) $ ((lb [ b2 ] : rs) as)) % b2) , SS , CC) ] || 
[ ((((b1 & q) $ ((lb [ b1 ] : rs) as)) % b3) , SS , CC) ] || 
[ ((((b1 & q) $ ((lb [ b2 ] : rs) as)) % b3) , SS , CC) ] || 

[ ((((b1 & q) $ ((lb [ b1 ] : ws) as)) % b1) , SS , CC) ] || 
[ ((((b1 & q) $ ((lb [ b1 ] : ws) as)) % b2) , SS , CC) ] || 

[ ((((b1 & q) $ ((lb [ b1 ] : cs) as)) % b1) , SS , CC) ] || 
[ ((((b1 & q) $ ((lb [ b2 ] : cs) as)) % b1) , SS , CC) ] || 
[ ((((b1 & q) $ ((lb [ b1 ] : cs) as)) % b2) , SS , CC) ] || 
[ ((((b1 & q) $ ((lb [ b2 ] : cs) as)) % b2) , SS , CC) ] || 
[ ((((b1 & q) $ ((lb [ b1 ] : cs) as)) % b3) , SS , CC) ] || 
[ ((((b1 & q) $ ((lb [ b2 ] : cs) as)) % b3) , SS , CC) ]

-- ========================================================================