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