package RuleAssertionsEspositoOK(sysRuleAssertionsEspositoOK) where

-- `setF' should not fire unless `setT' is not applicable.
-- Expect assertion to hold.

sysRuleAssertionsEspositoOK :: Module Empty
sysRuleAssertionsEspositoOK =
    module
        a :: Reg Bool
        a <- mkReg True
        addRules $ setT a <+ setF a <+ flip a

setT :: Reg Bool -> Rules
setT a = rules {-# ASSERT fire when enabled #-} "setT": when True ==> a := True

setF :: Reg Bool -> Rules
setF a = rules "setF": when True ==> a := True

flip :: Reg Bool -> Rules
flip a = rules "flip": when True ==> a := not a