Starting from 2021-07-01, all LRZ GitLab users will be required to explicitly accept the GitLab Terms of Service. Please see the detailed information at https://doku.lrz.de/display/PUBLIC/GitLab and make sure that your projects conform to the requirements.

Simplifier.hs 8.49 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
import Control.Monad
import Control.Monad.Identity
12 13 14 15
import qualified Data.Map as M
import qualified Data.Set as S

import Util
16
import Options
17
import Solver
18
import Solver.TransitionInvariant
19
import Property
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)

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

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

53 54 55
generateCuts :: PetriNet -> Formula Transition -> [Cut] -> OptIO [SimpleCut]
generateCuts net f cuts = do
            simp <- opt optSimpFormula
56

57 58 59 60
            let simpFunctions =
                    [ return . simplifyCuts
                    , return . removeImplicants
                    , simplifyBySubsumption
61
                    , greedySimplify net f
62 63 64
                    , simplifyBySubsumption
                    ]
            let (otfSimps, afterSimps) = splitAt 2 $ take simp simpFunctions
65 66 67
            let simpFunction = foldl (>=>) return afterSimps
            let otfFunction = foldl (>=>) return otfSimps
            let cnfCuts = map cutToSimpleDNFCuts cuts
68
            dnfCuts <- foldM (combine otfFunction) [(S.empty, [])] cnfCuts
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'
89
        where
90 91 92
            combine simpFunction cs1 cs2 =
                simpFunction [ (c1c0 `S.union` c2c0, c1cs ++ c2cs)
                             | (c1c0, c1cs) <- cs1, (c2c0, c2cs) <- cs2 ]
93 94

filterInvariantTransitions :: PetriNet -> [SimpleCut] -> [SimpleCut]
95
filterInvariantTransitions net =
96
        let ts = S.fromList $ invariantTransitions net
97
        in  runIdentity . simplifyWithFilter (return . filterTransitions ts) isMoreGeneralCut
98

99
filterTransitions :: S.Set Transition -> SimpleCut -> (Bool, SimpleCut)
100 101 102
filterTransitions ts (c0, cs) =
        let c0' = c0 `S.difference` ts
            cs' = filter (S.null . S.intersection ts) cs
103
            changed = c0 /= c0' || cs /= cs'
104
        in  (changed, (c0', cs'))
105 106 107

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

109 110 111
removeImplicants :: [SimpleCut] -> [SimpleCut]
removeImplicants = removeWith isMoreGeneralCut

112
simplifyCuts :: [SimpleCut] -> [SimpleCut]
113
simplifyCuts = mapMaybe simplifyCut
114

115
simplifyCut :: SimpleCut -> Maybe SimpleCut
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
120
                Nothing
121
            else
122
                Just (c0, cs')
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
130
        -- TODO: check with prime implicants
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

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)

149 150 151 152
removeWith :: (a -> a -> Bool) -> [a] -> [a]
removeWith f = removeCuts' []
        where
            removeCuts' acc [] = reverse acc
153 154
            removeCuts' acc (x:xs) = removeCuts' (x : notFilter x acc) (notFilter x xs)
            notFilter x = filter (not . f x)
155

156
-- c1 `isMoreGeneralCut` c2 <=> (c2 => c1)
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

164
-- TODO: allow formulas with or
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

190 191 192
checkCut :: PetriNet -> Formula Transition -> SimpleCut -> OptIO Bool
checkCut net f cut =
        liftM isNothing $ checkSat $ checkTransitionInvariantWithSimpleCutSat net f cut
193

194 195 196
greedySimplifyCut :: PetriNet -> Formula Transition -> Bool -> SimpleCut ->
        SimpleCut-> OptIO (Bool, SimpleCut)
greedySimplifyCut net f changed cutAcc@(c0Acc, csAcc) (c0, cs) =
197
        case (S.null c0, cs) of
198
            (True, []) -> return (changed, cutAcc)
199 200 201
            (False, _) -> do
                let (c, c0') = S.deleteFindMin c0
                let cut = (c0Acc `S.union` c0', csAcc ++ cs)
202 203
                r <- checkCut net f cut
                greedySimplifyCut net f (r || changed)
204
                    (if r then cutAcc else (S.insert c c0Acc, csAcc)) (c0', cs)
205 206
            (True, c:cs') -> do
                let cut = (c0Acc `S.union` c0, csAcc ++ cs')
207 208
                r <- checkCut net f cut
                greedySimplifyCut net f (r || changed)
209
                    (if r then cutAcc else (c0Acc, c:csAcc)) (c0, cs')
210

211 212 213
greedySimplify :: PetriNet -> Formula Transition -> [SimpleCut] -> OptIO [SimpleCut]
greedySimplify net f =
        simplifyWithFilter (greedySimplifyCut net f False (S.empty, [])) isMoreGeneralCut
214