{-# OPTIONS_GHC -fno-warn-name-shadowing #-} module Property (Property(..), Formula(..), negationNormalForm, eliminateModulo, Op(..), Term(..), PropResult(..), resultAnd, resultOr, resultNot, resultsAnd, resultsOr) where data Term a = Var a | Const Integer | Minus (Term a) | Term a :+: Term a | Term a :-: Term a | Term a :*: Term a deriving (Eq) instance (Show a) => Show (Term a) where show (Var x) = show x show (Const c) = show c show (Minus t) = "-" ++ show t show (t :+: u) = "(" ++ show t ++ " + " ++ show u ++ ")" show (t :-: u) = "(" ++ show t ++ " - " ++ show u ++ ")" show (t :*: u) = show t ++ " * " ++ show u instance Functor Term where fmap f (Var x) = Var (f x) fmap _ (Const c) = Const c fmap f (Minus t) = Minus (fmap f t) fmap f (t :+: u) = fmap f t :+: fmap f u fmap f (t :-: u) = fmap f t :-: fmap f u fmap f (t :*: u) = fmap f t :*: fmap f u data Op = Gt | Ge | Eq | Ne | Le | Lt | ModEq Integer | ModNe Integer deriving (Eq) instance Show Op where show Gt = ">" show Ge = "≥" show Eq = "=" show Ne = "≠" show Le = "≤" show Lt = "<" show (ModEq m) = "≡_" ++ show m show (ModNe m) = "≢_" ++ show m negateOp :: Op -> Op negateOp Gt = Le negateOp Ge = Lt negateOp Eq = Ne negateOp Ne = Eq negateOp Le = Gt negateOp Lt = Ge negateOp (ModEq m) = (ModNe m) negateOp (ModNe m) = (ModEq m) data Formula a = FTrue | FFalse | LinearInequation (Term a) Op (Term a) | Neg (Formula a) | Formula a :&: Formula a | Formula a :|: Formula a deriving (Eq) infixr 3 :&: infixr 2 :|: negationNormalForm :: Formula a -> Formula a negationNormalForm (Neg (FTrue)) = FFalse negationNormalForm (Neg (FFalse)) = FTrue negationNormalForm (Neg (g :&: h)) = (negationNormalForm (Neg g)) :|: (negationNormalForm (Neg h)) negationNormalForm (Neg (g :|: h)) = (negationNormalForm (Neg g)) :&: (negationNormalForm (Neg h)) negationNormalForm (Neg (LinearInequation u op t)) = LinearInequation u (negateOp op) t negationNormalForm (Neg (Neg g)) = negationNormalForm g negationNormalForm (g :&: h) = (negationNormalForm g) :&: (negationNormalForm h) negationNormalForm (g :|: h) = (negationNormalForm g) :|: (negationNormalForm h) negationNormalForm f@(LinearInequation _ _ _) = f negationNormalForm FTrue = FTrue negationNormalForm FFalse = FFalse eliminateModulo :: (Int -> a) -> Formula a -> (Formula a, [a]) eliminateModulo = eliminateModulo' 0 eliminateModulo' :: Int -> (Int -> a) -> Formula a -> (Formula a, [a]) eliminateModulo' _ _ (Neg g) = error "Formula not in negation normal form: cannot eliminate modulo" eliminateModulo' n makeVar (LinearInequation lhs (ModEq m) rhs) = let k = makeVar n in (LinearInequation lhs Eq (rhs :+: ((Const m) :*: (Var k))), [k]) eliminateModulo' n makeVar (LinearInequation lhs (ModNe m) rhs) = let j = makeVar (n + 1) k = makeVar n in ((LinearInequation lhs Eq (rhs :+: ((Var j) :+: ((Const m) :*: (Var k))))) :&: (LinearInequation (Const 0) Lt (Var j)) :&: (LinearInequation (Var j) Lt (Const m)), [k, j]) eliminateModulo' n makeVar (g :|: h) = let (g', ag) = eliminateModulo' n makeVar g (h', ah) = eliminateModulo' (n + length ag) makeVar h in (g' :|: h', ag ++ ah) eliminateModulo' n makeVar (g :&: h) = let (g', ag) = eliminateModulo' n makeVar g (h', ah) = eliminateModulo' (n + length ag) makeVar h in (g' :&: h', ag ++ ah) eliminateModulo' _ _ f = (f, []) instance (Show a) => Show (Formula a) where show FTrue = "true" show FFalse = "false" show (LinearInequation lhs op rhs) = show lhs ++ " " ++ show op ++ " " ++ show rhs show (Neg p) = "¬" ++ "(" ++ show p ++ ")" show (p :&: q) = "(" ++ show p ++ " ∧ " ++ show q ++ ")" show (p :|: q) = "(" ++ show p ++ " ∨ " ++ show q ++ ")" instance Functor Formula where fmap _ FTrue = FTrue fmap _ FFalse = FFalse fmap f (LinearInequation lhs op rhs) = LinearInequation (fmap f lhs) op (fmap f rhs) fmap f (Neg p) = Neg (fmap f p) fmap f (p :&: q) = fmap f p :&: fmap f q fmap f (p :|: q) = fmap f p :|: fmap f q data Property = LayeredTermination | StrongConsensus | StrongConsensusWithCorrectness instance Show Property where show LayeredTermination = "layered termination" show StrongConsensus = "strong consensus" show StrongConsensusWithCorrectness = "strong consensus with correctness" data PropResult = Satisfied | Unsatisfied | Unknown deriving (Eq) instance Show PropResult where show Satisfied = "satisfied" show Unsatisfied = "not satisfied" show Unknown = "may not be satisfied" resultAnd :: PropResult -> PropResult -> PropResult resultAnd Satisfied x = x resultAnd Unsatisfied _ = Unsatisfied resultAnd _ Unsatisfied = Unsatisfied resultAnd Unknown _ = Unknown resultOr :: PropResult -> PropResult -> PropResult resultOr Satisfied _ = Satisfied resultOr _ Satisfied = Satisfied resultOr Unsatisfied x = x resultOr Unknown _ = Unknown resultNot :: PropResult -> PropResult resultNot Satisfied = Unsatisfied resultNot Unsatisfied = Unsatisfied resultNot Unknown = Unknown resultsAnd :: [PropResult] -> PropResult resultsAnd = foldr resultAnd Satisfied resultsOr :: [PropResult] -> PropResult resultsOr = foldr resultOr Unsatisfied