Commit 48963ebf authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Rewrote simplifier to add formula after first round of simplifications

parent 7610121c
...@@ -53,20 +53,39 @@ cutTransitions (c0, cs) = S.unions (c0:cs) ...@@ -53,20 +53,39 @@ cutTransitions (c0, cs) = S.unions (c0:cs)
generateCuts :: PetriNet -> Formula Transition -> [Cut] -> OptIO [SimpleCut] generateCuts :: PetriNet -> Formula Transition -> [Cut] -> OptIO [SimpleCut]
generateCuts net f cuts = do generateCuts net f cuts = do
simp <- opt optSimpFormula simp <- opt optSimpFormula
let simpFunctions = let simpFunctions =
[ return . simplifyCuts [ return . simplifyCuts
, return . removeImplicants , return . removeImplicants
, return . filterInvariantTransitions net
, simplifyBySubsumption , simplifyBySubsumption
, greedySimplify net , greedySimplify net f
, simplifyBySubsumption , simplifyBySubsumption
] ]
let (otfSimps, afterSimps) = splitAt 2 $ take simp simpFunctions let (otfSimps, afterSimps) = splitAt 2 $ take simp simpFunctions
let simpFunction = foldl (>=>) return $ reverse afterSimps let simpFunction = foldl (>=>) return afterSimps
let otfFunction = foldl (>=>) return $ reverse otfSimps let otfFunction = foldl (>=>) return otfSimps
let cnfCuts = [formulaToCut f] : map cutToSimpleDNFCuts cuts let cnfCuts = map cutToSimpleDNFCuts cuts
dnfCuts <- foldM (combine otfFunction) [(S.empty, [])] cnfCuts dnfCuts <- foldM (combine otfFunction) [(S.empty, [])] cnfCuts
simpFunction dnfCuts 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'
where where
combine simpFunction cs1 cs2 = combine simpFunction cs1 cs2 =
simpFunction [ (c1c0 `S.union` c2c0, c1cs ++ c2cs) simpFunction [ (c1c0 `S.union` c2c0, c1cs ++ c2cs)
...@@ -81,7 +100,7 @@ filterTransitions :: S.Set Transition -> SimpleCut -> (Bool, SimpleCut) ...@@ -81,7 +100,7 @@ filterTransitions :: S.Set Transition -> SimpleCut -> (Bool, SimpleCut)
filterTransitions ts (c0, cs) = filterTransitions ts (c0, cs) =
let c0' = c0 `S.difference` ts let c0' = c0 `S.difference` ts
cs' = filter (S.null . S.intersection ts) cs cs' = filter (S.null . S.intersection ts) cs
changed = not $ all (S.null . S.intersection ts) cs changed = c0 /= c0' || cs /= cs'
in (changed, (c0', cs')) in (changed, (c0', cs'))
invariantTransitions :: PetriNet -> [Transition] invariantTransitions :: PetriNet -> [Transition]
...@@ -168,28 +187,28 @@ formulaToCut = transformF ...@@ -168,28 +187,28 @@ formulaToCut = transformF
transformTerm t = transformTerm t =
error $ "term not supported for invariant: " ++ show t error $ "term not supported for invariant: " ++ show t
checkCut :: PetriNet -> SimpleCut -> OptIO Bool checkCut :: PetriNet -> Formula Transition -> SimpleCut -> OptIO Bool
checkCut net cut = do checkCut net f cut =
r <- checkSat $ checkTransitionInvariantWithSimpleCutSat net cut liftM isNothing $ checkSat $ checkTransitionInvariantWithSimpleCutSat net f cut
return $ isNothing r
greedySimplifyCut :: PetriNet -> Bool -> SimpleCut -> SimpleCut-> OptIO (Bool, SimpleCut) greedySimplifyCut :: PetriNet -> Formula Transition -> Bool -> SimpleCut ->
greedySimplifyCut net changed cutAcc@(c0Acc, csAcc) (c0, cs) = SimpleCut-> OptIO (Bool, SimpleCut)
greedySimplifyCut net f changed cutAcc@(c0Acc, csAcc) (c0, cs) =
case (S.null c0, cs) of case (S.null c0, cs) of
(True, []) -> return (changed, cutAcc) (True, []) -> return (changed, cutAcc)
(False, _) -> do (False, _) -> do
let (c, c0') = S.deleteFindMin c0 let (c, c0') = S.deleteFindMin c0
let cut = (c0Acc `S.union` c0', csAcc ++ cs) let cut = (c0Acc `S.union` c0', csAcc ++ cs)
r <- checkCut net cut r <- checkCut net f cut
greedySimplifyCut net (r || changed) greedySimplifyCut net f (r || changed)
(if r then cutAcc else (S.insert c c0Acc, csAcc)) (c0', cs) (if r then cutAcc else (S.insert c c0Acc, csAcc)) (c0', cs)
(True, c:cs') -> do (True, c:cs') -> do
let cut = (c0Acc `S.union` c0, csAcc ++ cs') let cut = (c0Acc `S.union` c0, csAcc ++ cs')
r <- checkCut net cut r <- checkCut net f cut
greedySimplifyCut net (r || changed) greedySimplifyCut net f (r || changed)
(if r then cutAcc else (c0Acc, c:csAcc)) (c0, cs') (if r then cutAcc else (c0Acc, c:csAcc)) (c0, cs')
greedySimplify :: PetriNet -> [SimpleCut] -> OptIO [SimpleCut] greedySimplify :: PetriNet -> Formula Transition -> [SimpleCut] -> OptIO [SimpleCut]
greedySimplify net = greedySimplify net f =
simplifyWithFilter (greedySimplifyCut net False (S.empty, [])) isMoreGeneralCut simplifyWithFilter (greedySimplifyCut net f False (S.empty, [])) isMoreGeneralCut
...@@ -72,19 +72,20 @@ checkTransitionInvariantSat net f cuts = ...@@ -72,19 +72,20 @@ checkTransitionInvariantSat net f cuts =
\fm -> checkTransitionInvariant net f cuts (fmap fm x), \fm -> checkTransitionInvariant net f cuts (fmap fm x),
\fm -> firingVectorFromAssignment (fmap fm x)) \fm -> firingVectorFromAssignment (fmap fm x))
checkTransitionInvariantWithSimpleCut :: PetriNet -> checkTransitionInvariantWithSimpleCut :: PetriNet -> Formula Transition ->
SimpleCut -> SIMap Transition -> SBool SimpleCut -> SIMap Transition -> SBool
checkTransitionInvariantWithSimpleCut net cut x = checkTransitionInvariantWithSimpleCut net f cut x =
transitionVectorConstraints net x &&& transitionVectorConstraints net x &&&
evaluateFormula f x &&&
checkSimpleCut cut x checkSimpleCut cut x
checkTransitionInvariantWithSimpleCutSat :: PetriNet -> SimpleCut -> checkTransitionInvariantWithSimpleCutSat :: PetriNet -> Formula Transition -> SimpleCut ->
ConstraintProblem Integer FiringVector ConstraintProblem Integer FiringVector
checkTransitionInvariantWithSimpleCutSat net cut = checkTransitionInvariantWithSimpleCutSat net f cut =
let x = makeVarMap $ transitions net let x = makeVarMap $ transitions net
in ("transition invariant constraints with simple cut", "transition invariant", in ("transition invariant constraints with simple cut", "transition invariant",
getNames x, getNames x,
\fm -> checkTransitionInvariantWithSimpleCut net cut (fmap fm x), \fm -> checkTransitionInvariantWithSimpleCut net f cut (fmap fm x),
\fm -> firingVectorFromAssignment (fmap fm x)) \fm -> firingVectorFromAssignment (fmap fm x))
firingVectorFromAssignment :: IMap Transition -> FiringVector firingVectorFromAssignment :: IMap Transition -> FiringVector
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment