The name of the initial branch for new projects is now "main" instead of "master". Existing projects remain unchanged. More information: https://doku.lrz.de/display/PUBLIC/GitLab

Simplifier.hs 9.07 KB
Newer Older
1
module Solver.Simplifier (
2 3 4
     checkSubsumptionSat
    ,SimpleCut
    ,generateCuts
5
    ,greedySimplify
6 7 8
) where

import Data.SBV
9
import Data.Maybe
10 11 12
import Data.Ord (comparing)
import Data.List (minimumBy)
import Control.Arrow (second)
13 14
import Control.Monad
import Control.Monad.Identity
15 16 17 18
import qualified Data.Map as M
import qualified Data.Set as S

import Util
19
import Options
20
import Solver
21
import Solver.TransitionInvariant
22
import Property
23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44
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)

45 46 47
checkSubsumptionSat :: SimpleCut -> [SimpleCut] -> ConstraintProblem Bool [Transition]
checkSubsumptionSat c0 cs =
        let m = makeVarMap $ S.elems $ S.unions $ map cutTransitions (c0:cs)
48 49 50 51
        in  ("constraint subsumption", "subsumption",
            getNames m,
            \fm -> checkCuts c0 cs (fmap fm m),
            \fm -> getSubsumption (fmap fm m))
52 53 54 55

cutTransitions :: SimpleCut -> S.Set Transition
cutTransitions (c0, cs) = S.unions (c0:cs)

56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88
type SimpConfig = ([[SimpleCut] -> OptIO [SimpleCut]], SimpleCut, SimpleCut, Int)

simpWithoutFormula :: PetriNet -> Formula Transition -> SimpConfig
simpWithoutFormula net f =
        (
        [ return . simplifyCuts
        , return . removeImplicants
        , greedySimplify net f
        , return . combineCuts
        , simplifyBySubsumption
        ]
        , (S.empty, [])
        , second (S.fromList (transitions net) :) (formulaToCut f)
        , 2
        )

simpWithFormula :: PetriNet -> Formula Transition -> SimpConfig
simpWithFormula net f =
        (
        [ return . simplifyCuts
        , return . removeImplicants
        , return . filterInvariantTransitions net
        , greedySimplify net FTrue
        , return . combineCuts
        , simplifyBySubsumption
        ]
        , second (S.fromList (transitions net) :) (formulaToCut f)
        , (S.empty, [])
        , 2
        )

applySimpConfig :: SimpConfig -> [Cut] -> OptIO [SimpleCut]
applySimpConfig (simpFunctions, initialCut, afterCut, otfIndex) cuts = do
89
            simp <- opt optSimpFormula
90
            let (otfSimps, afterSimps) = splitAt otfIndex $ take simp simpFunctions
91 92 93
            let simpFunction = foldl (>=>) return afterSimps
            let otfFunction = foldl (>=>) return otfSimps
            let cnfCuts = map cutToSimpleDNFCuts cuts
94
            dnfCuts <- foldM (combine otfFunction) [initialCut] cnfCuts
95
            simpCuts <- simpFunction dnfCuts
96
            combine otfFunction [afterCut] simpCuts
97
        where
98 99 100
            combine simpFunction cs1 cs2 =
                simpFunction [ (c1c0 `S.union` c2c0, c1cs ++ c2cs)
                             | (c1c0, c1cs) <- cs1, (c2c0, c2cs) <- cs2 ]
101

102 103 104 105 106 107 108 109 110 111 112 113 114 115
generateCuts :: PetriNet -> Formula Transition -> [Cut] -> OptIO [SimpleCut]
generateCuts net f cuts = do
        let configs = [simpWithFormula, simpWithoutFormula]
        let tasks = map (\c -> applySimpConfig (c net f) cuts) configs
        rs <- parallelIO tasks
        return $ minimumBy (comparing length) rs

combineCuts :: [SimpleCut] -> [SimpleCut]
combineCuts cuts =
            M.toList $ M.fromListWith combineFunc cuts
        where
            combineFunc cs cs' =
                simplifyPositiveCut [ c `S.union` c' | c <- cs, c' <- cs' ]

116
filterInvariantTransitions :: PetriNet -> [SimpleCut] -> [SimpleCut]
117
filterInvariantTransitions net =
118
        let ts = S.fromList $ invariantTransitions net
119
        in  runIdentity . simplifyWithFilter (return . filterTransitions ts) isMoreGeneralCut
120

121
filterTransitions :: S.Set Transition -> SimpleCut -> (Bool, SimpleCut)
122 123 124
filterTransitions ts (c0, cs) =
        let c0' = c0 `S.difference` ts
            cs' = filter (S.null . S.intersection ts) cs
125
            changed = c0 /= c0' || cs /= cs'
126
        in  (changed, (c0', cs'))
127 128 129

invariantTransitions :: PetriNet -> [Transition]
invariantTransitions net = filter (\t -> lpre net t == lpost net t) $ transitions net
130

131 132 133
removeImplicants :: [SimpleCut] -> [SimpleCut]
removeImplicants = removeWith isMoreGeneralCut

134
simplifyCuts :: [SimpleCut] -> [SimpleCut]
135
simplifyCuts = mapMaybe simplifyCut
136

137
simplifyCut :: SimpleCut -> Maybe SimpleCut
138 139
simplifyCut (c0, cs) =
        let remove b a = a `S.difference` b
140
            cs' = simplifyPositiveCut $ map (remove c0) cs
141
        in  if any S.null cs' then
142
                Nothing
143
            else
144
                Just (c0, cs')
145

146 147 148
simplifyPositiveCut :: [S.Set Transition] -> [S.Set Transition]
simplifyPositiveCut = removeWith S.isSubsetOf 

149 150 151 152 153 154
simplifyBySubsumption :: [SimpleCut] -> OptIO [SimpleCut]
simplifyBySubsumption = simplifyBySubsumption' []

simplifyBySubsumption' :: [SimpleCut] -> [SimpleCut] -> OptIO [SimpleCut]
simplifyBySubsumption' acc [] = return $ reverse acc
simplifyBySubsumption' acc (c0:cs) = do
155
        -- TODO: check with prime implicants
156 157 158 159 160 161
        r <- checkSat $ checkSubsumptionSat c0 (acc ++ cs)
        let acc' = case r of
                    Nothing -> acc
                    Just _ -> c0:acc
        simplifyBySubsumption' acc' cs

162 163 164 165 166 167 168 169 170 171 172 173
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)

174 175 176 177
removeWith :: (a -> a -> Bool) -> [a] -> [a]
removeWith f = removeCuts' []
        where
            removeCuts' acc [] = reverse acc
178 179
            removeCuts' acc (x:xs) = removeCuts' (x : notFilter x acc) (notFilter x xs)
            notFilter x = filter (not . f x)
180

181
-- c1 `isMoreGeneralCut` c2 <=> (c2 => c1)
182 183 184 185 186 187 188
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

189
-- TODO: allow formulas with or
190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214
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

215 216 217
checkCut :: PetriNet -> Formula Transition -> SimpleCut -> OptIO Bool
checkCut net f cut =
        liftM isNothing $ checkSat $ checkTransitionInvariantWithSimpleCutSat net f cut
218

219 220 221
greedySimplifyCut :: PetriNet -> Formula Transition -> Bool -> SimpleCut ->
        SimpleCut-> OptIO (Bool, SimpleCut)
greedySimplifyCut net f changed cutAcc@(c0Acc, csAcc) (c0, cs) =
222
        case (S.null c0, cs) of
223
            (True, []) -> return (changed, cutAcc)
224 225 226
            (False, _) -> do
                let (c, c0') = S.deleteFindMin c0
                let cut = (c0Acc `S.union` c0', csAcc ++ cs)
227 228
                r <- checkCut net f cut
                greedySimplifyCut net f (r || changed)
229
                    (if r then cutAcc else (S.insert c c0Acc, csAcc)) (c0', cs)
230 231
            (True, c:cs') -> do
                let cut = (c0Acc `S.union` c0, csAcc ++ cs')
232 233
                r <- checkCut net f cut
                greedySimplifyCut net f (r || changed)
234
                    (if r then cutAcc else (c0Acc, c:csAcc)) (c0, cs')
235

236 237 238
greedySimplify :: PetriNet -> Formula Transition -> [SimpleCut] -> OptIO [SimpleCut]
greedySimplify net f =
        simplifyWithFilter (greedySimplifyCut net f False (S.empty, [])) isMoreGeneralCut
239