Commit 51786760 authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Added more simplification after combining

parent cea035e6
......@@ -94,7 +94,8 @@ checkLivenessInvariantSat :: PetriNet -> Formula Transition -> SimpleCut -> Cons
checkLivenessInvariantSat net f (c0, cs) =
-- TODO: use own variables for formula cut
let (f0, fs) = formulaToCut f
cut = (c0 `S.union` f0, simplifyPositiveCut (cs ++ fs))
c0' = c0 `S.union` f0
cut = (c0', simplifyPositiveCut c0' (cs ++ fs))
namedCut = nameCut cut
names = cutNames net namedCut
myVarMap fvm = M.fromList $ names `zip` fmap fvm names
......
......@@ -117,10 +117,10 @@ generateCuts net f cuts = do
combineCuts :: [SimpleCut] -> [SimpleCut]
combineCuts cuts =
M.toList $ M.fromListWith combineFunc cuts
M.toList $ M.fromListWithKey combineFunc cuts
where
combineFunc cs cs' =
simplifyPositiveCut [ c `S.union` c' | c <- cs, c' <- cs' ]
combineFunc c0 cs cs' =
simplifyPositiveCut c0 [ c `S.union` c' | c <- cs, c' <- cs' ]
filterInvariantTransitions :: PetriNet -> [SimpleCut] -> [SimpleCut]
filterInvariantTransitions net =
......@@ -145,15 +145,15 @@ simplifyCuts = mapMaybe simplifyCut
simplifyCut :: SimpleCut -> Maybe SimpleCut
simplifyCut (c0, cs) =
let remove b a = a `S.difference` b
cs' = simplifyPositiveCut $ map (remove c0) cs
let cs' = simplifyPositiveCut c0 cs
in if any S.null cs' then
Nothing
else
Just (c0, cs')
simplifyPositiveCut :: [S.Set Transition] -> [S.Set Transition]
simplifyPositiveCut = removeWith S.isSubsetOf
simplifyPositiveCut :: S.Set Transition -> [S.Set Transition] -> [S.Set Transition]
simplifyPositiveCut c0 =
removeWith S.isSubsetOf . map (`S.difference` c0)
simplifyBySubsumption :: [SimpleCut] -> OptIO [SimpleCut]
simplifyBySubsumption = simplifyBySubsumption' []
......
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