Simplifier.hs 8.49 KB
Newer Older
 Philipp Meyer committed Feb 03, 2015 1 ``````module Solver.Simplifier ( `````` Philipp Meyer committed Feb 05, 2015 2 3 4 `````` checkSubsumptionSat ,SimpleCut ,generateCuts `````` Philipp Meyer committed Feb 11, 2015 5 `````` ,greedySimplify `````` Philipp Meyer committed Feb 03, 2015 6 7 8 ``````) where import Data.SBV `````` Philipp Meyer committed Feb 11, 2015 9 ``````import Data.Maybe `````` Philipp Meyer committed Feb 12, 2015 10 11 ``````import Control.Monad import Control.Monad.Identity `````` Philipp Meyer committed Feb 03, 2015 12 13 14 15 ``````import qualified Data.Map as M import qualified Data.Set as S import Util `````` Philipp Meyer committed Feb 05, 2015 16 ``````import Options `````` Philipp Meyer committed Feb 03, 2015 17 ``````import Solver `````` Philipp Meyer committed Feb 11, 2015 18 ``````import Solver.TransitionInvariant `````` Philipp Meyer committed Feb 05, 2015 19 ``````import Property `````` Philipp Meyer committed Feb 03, 2015 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 ``````import PetriNet checkTransPositive :: SBMap Transition -> S.Set Transition -> SBool checkTransPositive m ts = bOr \$ map (val m) \$ S.elems ts checkTransNegative :: SBMap Transition -> S.Set Transition -> SBool checkTransNegative m ts = bAnd \$ map (bnot . val m) \$ S.elems ts checkCutPositive :: SBMap Transition -> SimpleCut -> SBool checkCutPositive m (c0, cs) = checkTransNegative m c0 &&& bAnd (map (checkTransPositive m) cs) checkCutNegative :: SBMap Transition -> SimpleCut -> SBool checkCutNegative m (c0, cs) = checkTransPositive m c0 ||| bOr (map (checkTransNegative m) cs) checkCuts :: SimpleCut -> [SimpleCut] -> SBMap Transition -> SBool checkCuts c0 cs m = checkCutPositive m c0 &&& bAnd (map (checkCutNegative m) cs) getSubsumption :: BMap Transition -> [Transition] getSubsumption m = M.keys (M.filter id m) `````` Philipp Meyer committed Feb 05, 2015 42 43 44 ``````checkSubsumptionSat :: SimpleCut -> [SimpleCut] -> ConstraintProblem Bool [Transition] checkSubsumptionSat c0 cs = let m = makeVarMap \$ S.elems \$ S.unions \$ map cutTransitions (c0:cs) `````` Philipp Meyer committed Feb 03, 2015 45 46 47 48 `````` in ("constraint subsumption", "subsumption", getNames m, \fm -> checkCuts c0 cs (fmap fm m), \fm -> getSubsumption (fmap fm m)) `````` Philipp Meyer committed Feb 05, 2015 49 50 51 52 `````` cutTransitions :: SimpleCut -> S.Set Transition cutTransitions (c0, cs) = S.unions (c0:cs) `````` Philipp Meyer committed Feb 11, 2015 53 54 55 ``````generateCuts :: PetriNet -> Formula Transition -> [Cut] -> OptIO [SimpleCut] generateCuts net f cuts = do simp <- opt optSimpFormula `````` Philipp Meyer committed Feb 13, 2015 56 `````` `````` Philipp Meyer committed Feb 12, 2015 57 58 59 60 `````` let simpFunctions = [ return . simplifyCuts , return . removeImplicants , simplifyBySubsumption `````` Philipp Meyer committed Feb 13, 2015 61 `````` , greedySimplify net f `````` Philipp Meyer committed Feb 12, 2015 62 63 64 `````` , simplifyBySubsumption ] let (otfSimps, afterSimps) = splitAt 2 \$ take simp simpFunctions `````` Philipp Meyer committed Feb 13, 2015 65 66 67 `````` let simpFunction = foldl (>=>) return afterSimps let otfFunction = foldl (>=>) return otfSimps let cnfCuts = map cutToSimpleDNFCuts cuts `````` Philipp Meyer committed Feb 12, 2015 68 `````` dnfCuts <- foldM (combine otfFunction) [(S.empty, [])] cnfCuts `````` Philipp Meyer committed Feb 13, 2015 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 `````` simpCuts <- simpFunction dnfCuts let simpFunctions' = [ return . simplifyCuts , return . removeImplicants , return . filterInvariantTransitions net , simplifyBySubsumption , greedySimplify net FTrue , simplifyBySubsumption ] let (otfSimps', afterSimps') = splitAt 2 \$ take simp simpFunctions' let simpFunction' = foldl (>=>) return afterSimps' let otfFunction' = foldl (>=>) return otfSimps' let (fc0, fcs) = formulaToCut f let addedTransitions = S.fromList (transitions net) let addedCut = (fc0, addedTransitions : fcs) simpCutsWithFormula <- combine otfFunction' [addedCut] simpCuts simpCuts' <- simpFunction' simpCutsWithFormula return simpCuts' `````` Philipp Meyer committed Feb 05, 2015 89 `````` where `````` Philipp Meyer committed Feb 12, 2015 90 91 92 `````` combine simpFunction cs1 cs2 = simpFunction [ (c1c0 `S.union` c2c0, c1cs ++ c2cs) | (c1c0, c1cs) <- cs1, (c2c0, c2cs) <- cs2 ] `````` Philipp Meyer committed Feb 11, 2015 93 94 `````` filterInvariantTransitions :: PetriNet -> [SimpleCut] -> [SimpleCut] `````` Philipp Meyer committed Feb 12, 2015 95 ``````filterInvariantTransitions net = `````` Philipp Meyer committed Feb 11, 2015 96 `````` let ts = S.fromList \$ invariantTransitions net `````` Philipp Meyer committed Feb 12, 2015 97 `````` in runIdentity . simplifyWithFilter (return . filterTransitions ts) isMoreGeneralCut `````` Philipp Meyer committed Feb 11, 2015 98 `````` `````` Philipp Meyer committed Feb 12, 2015 99 ``````filterTransitions :: S.Set Transition -> SimpleCut -> (Bool, SimpleCut) `````` Philipp Meyer committed Feb 11, 2015 100 101 102 ``````filterTransitions ts (c0, cs) = let c0' = c0 `S.difference` ts cs' = filter (S.null . S.intersection ts) cs `````` Philipp Meyer committed Feb 13, 2015 103 `````` changed = c0 /= c0' || cs /= cs' `````` Philipp Meyer committed Feb 12, 2015 104 `````` in (changed, (c0', cs')) `````` Philipp Meyer committed Feb 11, 2015 105 106 107 `````` invariantTransitions :: PetriNet -> [Transition] invariantTransitions net = filter (\t -> lpre net t == lpost net t) \$ transitions net `````` Philipp Meyer committed Feb 05, 2015 108 `````` `````` Philipp Meyer committed Feb 12, 2015 109 110 111 ``````removeImplicants :: [SimpleCut] -> [SimpleCut] removeImplicants = removeWith isMoreGeneralCut `````` Philipp Meyer committed Feb 05, 2015 112 ``````simplifyCuts :: [SimpleCut] -> [SimpleCut] `````` Philipp Meyer committed Feb 12, 2015 113 ``````simplifyCuts = mapMaybe simplifyCut `````` Philipp Meyer committed Feb 05, 2015 114 `````` `````` Philipp Meyer committed Feb 11, 2015 115 ``````simplifyCut :: SimpleCut -> Maybe SimpleCut `````` Philipp Meyer committed Feb 05, 2015 116 117 118 119 ``````simplifyCut (c0, cs) = let remove b a = a `S.difference` b cs' = removeWith S.isSubsetOf \$ map (remove c0) cs in if any S.null cs' then `````` Philipp Meyer committed Feb 11, 2015 120 `````` Nothing `````` Philipp Meyer committed Feb 05, 2015 121 `````` else `````` Philipp Meyer committed Feb 11, 2015 122 `````` Just (c0, cs') `````` Philipp Meyer committed Feb 05, 2015 123 124 125 126 127 128 129 `````` simplifyBySubsumption :: [SimpleCut] -> OptIO [SimpleCut] simplifyBySubsumption = simplifyBySubsumption' [] simplifyBySubsumption' :: [SimpleCut] -> [SimpleCut] -> OptIO [SimpleCut] simplifyBySubsumption' acc [] = return \$ reverse acc simplifyBySubsumption' acc (c0:cs) = do `````` Philipp Meyer committed Feb 11, 2015 130 `````` -- TODO: check with prime implicants `````` Philipp Meyer committed Feb 05, 2015 131 132 133 134 135 136 `````` r <- checkSat \$ checkSubsumptionSat c0 (acc ++ cs) let acc' = case r of Nothing -> acc Just _ -> c0:acc simplifyBySubsumption' acc' cs `````` Philipp Meyer committed Feb 12, 2015 137 138 139 140 141 142 143 144 145 146 147 148 ``````simplifyWithFilter :: (Monad m) => (a -> m (Bool, a)) -> (a -> a -> Bool) -> [a] -> m [a] simplifyWithFilter simp f = simpFilter [] where simpFilter acc [] = return \$ reverse acc simpFilter acc (x:xs) = do (changed, x') <- simp x if changed then simpFilter (x' : notFilter x' acc) (notFilter x' xs) else simpFilter (x' : acc) xs notFilter x = filter (not . f x) `````` Philipp Meyer committed Feb 05, 2015 149 150 151 152 ``````removeWith :: (a -> a -> Bool) -> [a] -> [a] removeWith f = removeCuts' [] where removeCuts' acc [] = reverse acc `````` Philipp Meyer committed Feb 11, 2015 153 154 `````` removeCuts' acc (x:xs) = removeCuts' (x : notFilter x acc) (notFilter x xs) notFilter x = filter (not . f x) `````` Philipp Meyer committed Feb 05, 2015 155 `````` `````` Philipp Meyer committed Feb 12, 2015 156 ``````-- c1 `isMoreGeneralCut` c2 <=> (c2 => c1) `````` Philipp Meyer committed Feb 05, 2015 157 158 159 160 161 162 163 ``````isMoreGeneralCut :: SimpleCut -> SimpleCut -> Bool isMoreGeneralCut (c1c0, c1cs) (c2c0, c2cs) = c1c0 `S.isSubsetOf` c2c0 && all (\c1 -> any (`S.isSubsetOf` c1) c2cs) c1cs cutToSimpleDNFCuts :: Cut -> [SimpleCut] cutToSimpleDNFCuts (ts, u) = (S.empty, [S.fromList u]) : map (\(_, t) -> (S.fromList t, [])) ts `````` Philipp Meyer committed Feb 11, 2015 164 ``````-- TODO: allow formulas with or `````` Philipp Meyer committed Feb 05, 2015 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 ``````formulaToCut :: Formula Transition -> SimpleCut formulaToCut = transformF where transformF FTrue = (S.empty, []) transformF (p :&: q) = let (p0, ps) = transformF p (q0, qs) = transformF q in (p0 `S.union` q0, ps ++ qs) transformF (LinearInequation ts Gt (Const 0)) = (S.empty, [transformTerm ts]) transformF (LinearInequation ts Ge (Const 1)) = (S.empty, [transformTerm ts]) transformF (LinearInequation ts Eq (Const 0)) = (transformTerm ts, []) transformF (LinearInequation ts Le (Const 0)) = (transformTerm ts, []) transformF (LinearInequation ts Lt (Const 1)) = (transformTerm ts, []) transformF f = error \$ "formula not supported for invariant: " ++ show f transformTerm (t :+: u) = transformTerm t `S.union` transformTerm u transformTerm (Var x) = S.singleton x transformTerm t = error \$ "term not supported for invariant: " ++ show t `````` Philipp Meyer committed Feb 13, 2015 190 191 192 ``````checkCut :: PetriNet -> Formula Transition -> SimpleCut -> OptIO Bool checkCut net f cut = liftM isNothing \$ checkSat \$ checkTransitionInvariantWithSimpleCutSat net f cut `````` Philipp Meyer committed Feb 11, 2015 193 `````` `````` Philipp Meyer committed Feb 13, 2015 194 195 196 ``````greedySimplifyCut :: PetriNet -> Formula Transition -> Bool -> SimpleCut -> SimpleCut-> OptIO (Bool, SimpleCut) greedySimplifyCut net f changed cutAcc@(c0Acc, csAcc) (c0, cs) = `````` Philipp Meyer committed Feb 11, 2015 197 `````` case (S.null c0, cs) of `````` Philipp Meyer committed Feb 12, 2015 198 `````` (True, []) -> return (changed, cutAcc) `````` Philipp Meyer committed Feb 11, 2015 199 200 201 `````` (False, _) -> do let (c, c0') = S.deleteFindMin c0 let cut = (c0Acc `S.union` c0', csAcc ++ cs) `````` Philipp Meyer committed Feb 13, 2015 202 203 `````` r <- checkCut net f cut greedySimplifyCut net f (r || changed) `````` Philipp Meyer committed Feb 12, 2015 204 `````` (if r then cutAcc else (S.insert c c0Acc, csAcc)) (c0', cs) `````` Philipp Meyer committed Feb 11, 2015 205 206 `````` (True, c:cs') -> do let cut = (c0Acc `S.union` c0, csAcc ++ cs') `````` Philipp Meyer committed Feb 13, 2015 207 208 `````` r <- checkCut net f cut greedySimplifyCut net f (r || changed) `````` Philipp Meyer committed Feb 12, 2015 209 `````` (if r then cutAcc else (c0Acc, c:csAcc)) (c0, cs') `````` Philipp Meyer committed Feb 11, 2015 210 `````` `````` Philipp Meyer committed Feb 13, 2015 211 212 213 ``````greedySimplify :: PetriNet -> Formula Transition -> [SimpleCut] -> OptIO [SimpleCut] greedySimplify net f = simplifyWithFilter (greedySimplifyCut net f False (S.empty, [])) isMoreGeneralCut `````` Philipp Meyer committed Feb 11, 2015 214