Added s-component refinement with integrated cut

src/Main.hs

@@ -30,11 +30,10 @@ import Solver.TransitionInvariant
 import Solver.SubnetEmptyTrap
 import Solver.LivenessInvariant
 import Solver.SafetyInvariant
-import Solver.SComponent
+import Solver.SComponentWithCut
 import Solver.Simplifier
 --import Solver.CommFreeReachability
 
-
 writeFiles :: String -> PetriNet -> [Property] -> OptIO ()
 writeFiles basename net props = do
         format <- opt outputFormat
@@ -287,7 +286,7 @@ checkLivenessProperty net f = do
 getLivenessInvariant :: PetriNet -> Formula Transition -> [Cut] -> OptIO (Maybe [LivenessInvariant])
 getLivenessInvariant net f cuts = do
         simp <- opt optSimpFormula
-        dnfCuts <- generateCuts f cuts
+        dnfCuts <- generateCuts net f cuts
         verbosePut 2 $ "Number of " ++ (if simp > 0 then "simplified " else "") ++
                        "disjuncts: " ++ show (length dnfCuts)
         rs <- mapM (checkSat . checkLivenessInvariantSat net) dnfCuts
@@ -328,8 +327,8 @@ findLivenessRefinement net x = do
 
 findLivenessRefinementBySComponent :: PetriNet -> FiringVector ->
         OptIO (Maybe Cut)
-findLivenessRefinementBySComponent net x =
-        checkSatMin $ checkSComponentSat net x
+findLivenessRefinementBySComponent net x = do
+        checkSatMin $ checkSComponentWithCutSat net x
 
 findLivenessRefinementByEmptyTraps :: PetriNet -> Marking -> FiringVector ->
         [Trap] -> OptIO (Maybe Cut)
@@ -354,9 +353,18 @@ findLivenessRefinementByEmptyTraps net m x traps = do
                         return $ Just cut
                     (Just m', _) ->
                         findLivenessRefinementByEmptyTraps net m' x traps'
-
+{-
+generateLivenessRefinementFromSComponent :: PetriNet -> FiringVector -> [[Place]] ->
+        [Place] -> [Transition] -> OptIO Cut
+generateLivenessRefinementFromSComponent net components ps ts = do
+        r <- checkSatMin $ checkMultiWayCutSat net components ps ts
+        case r of
+            Nothing -> error "Could not find a cut, this should not happen"
+            Just ts -> (ts
+-}
 generateLivenessRefinement :: PetriNet -> FiringVector -> [Trap] -> OptIO Cut
 generateLivenessRefinement net x traps = do
+        -- TODO: also use better cuts for traps
         let cut = constructCut net x traps
         verbosePut 3 $ "- cut: " ++ show cut
         return cut

src/PetriNet.hs

@@ -15,7 +15,7 @@ where
 import qualified Data.Map as M
 import qualified Data.Set as S
 import Control.Arrow (first,(***))
-import Data.List ((\\))
+import Data.List (sort,(\\))
 
 import Util
 
@@ -99,18 +99,19 @@ instance Show PetriNet where
                           show l ++ " -> " ++ show s ++ " -> " ++ show r
 
 -- TODO: better cuts, scc, min cut?
-{-
+
 constructCut:: PetriNet -> FiringVector -> [Trap] -> Cut
 constructCut net _ traps = (trapComponents, trapOutputs)
         where trapComponent trap = (sort trap, sort (mpre net trap) \\ trapOutputs)
               trapComponents = listSet $ map trapComponent traps
               trapOutput trap = mpost net trap \\ mpre net trap
               trapOutputs = listSet $ concatMap trapOutput traps
--}
+{-
 constructCut:: PetriNet -> FiringVector -> [Trap] -> Cut
 constructCut net x _ = (map (\t -> ([],[t])) tPositive, tNegative)
         where tPositive = elems x
               tNegative = transitions net \\ tPositive
+-}
 
 renamePlace :: (String -> String) -> Place -> Place
 renamePlace f (Place p) = Place (f p)

src/Solver.hs

@@ -47,8 +47,8 @@ checkSat (problemName, resultName, vars, constraint, interpretation) = do
                 verbosePut 4 $ "- raw model: " ++ show rawModel
                 return $ Just model
 
-checkSatMin :: (SatModel a, SymWord a, Show a, Show b) =>
-        (Maybe Integer -> ConstraintProblem a (b, Integer)) -> OptIO (Maybe b)
+checkSatMin :: (SatModel a, SymWord a, Show a, Show b, Show c) =>
+        (Maybe c -> ConstraintProblem a (b, c)) -> OptIO (Maybe b)
 checkSatMin minProblem = do
         optMin <- opt optMinimizeRefinement
         r0 <- checkSat $ minProblem Nothing

src/Solver/GeneralSComponent.hs

+module Solver.GeneralSComponent
+    (checkGeneralSComponentSat)
+where
+
+import Data.SBV
+import Data.List (genericLength)
+import qualified Data.Map as M
+
+import Util
+import PetriNet
+import Solver
+
+checkPrePostPlaces :: PetriNet -> SIMap Place -> SIMap Transition ->
+        SBool
+checkPrePostPlaces net p' t' =
+            bAnd $ map checkPrePostPlace $ places net
+        where checkPrePostPlace p =
+                  let incoming = map (positiveVal t') $ pre net p
+                      outgoing = map (positiveVal t') $ post net p
+                      pVal = positiveVal p' p
+                  in  pVal ==> bAnd incoming &&& bAnd outgoing
+
+checkPrePostTransitions :: PetriNet -> SIMap Place -> SIMap Transition ->
+        SBool
+checkPrePostTransitions net p' t' =
+            bAnd $ map checkPrePostTransition $ transitions net
+        where checkPrePostTransition t =
+                  let incoming = mval p' $ pre net t
+                      outgoing = mval p' $ post net t
+                      tVal = positiveVal t' t
+                  in  tVal ==> sum incoming .== 1 &&& sum outgoing .== 1
+
+checkMinimum :: FiringVector -> SIMap Transition -> SBool
+checkMinimum x yt = bOr $ map checkTransition $ elems x
+        where checkTransition t = val yt t .== 1
+
+checkMaximum :: FiringVector -> SIMap Transition -> SInteger -> SBool
+checkMaximum x yt k = bOr $ map checkTransition $ elems x
+        where checkTransition t = val yt t .== k
+
+checkNext :: FiringVector -> SIMap Transition -> SInteger -> SBool
+checkNext x yt k = bAnd $ map checkTransition $ elems x
+        where checkTransition t = val yt t .< k ==> bOr (map checkNextVal (elems x))
+                  where checkNextVal t' = val yt t' .== val yt t + 1
+
+checkSubset :: PetriNet -> SIMap Place -> SIMap Transition ->
+        SIMap Place -> SIMap Transition -> SBool
+checkSubset net p' t' yp yt =
+            bAnd (map (checkSub yp p') (places net)) &&&
+            bAnd (map (checkSub yt t') (transitions net))
+        where checkSub xs ys x = positiveVal xs x ==> positiveVal ys x
+
+checkClosed :: PetriNet -> SIMap Place -> SIMap Transition ->
+        SIMap Place -> SIMap Transition -> SBool
+checkClosed net p' t' yp yt =
+            bAnd (map checkPlaceClosed (places net)) &&&
+            bAnd (map checkTransitionClosed (transitions net))
+        where checkPlaceClosed p =
+                  let pVal = positiveVal p' p
+                      postVal = bAnd $ map checkTransition $ pre net p ++ post net p
+                      checkTransition t = positiveVal yt t ==> val yt t .== val yp p
+                  in  pVal ==> postVal
+              checkTransitionClosed t =
+                  let tVal = positiveVal yt t
+                      postVal = bAnd $ map checkPlace $ pre net t ++ post net t
+                      checkPlace p = positiveVal p' p ==> val yt t .== val yp p
+                  in  tVal ==> postVal
+
+checkZeroUnused :: FiringVector -> SIMap Transition -> SIMap Transition -> SBool
+checkZeroUnused x t' yt =
+            bAnd (map checkTransition (elems x))
+        where checkTransition t = val yt t .>= val t' t
+
+checkTokens :: PetriNet -> SIMap Place -> SInteger -> SBool
+checkTokens net p' k =
+            sum (map addPlace $ linitials net) .< k
+        where addPlace (p,i) = literal i * val p' p
+
+checkBinary :: SIMap Place -> SIMap Transition -> SBool
+checkBinary p' t' = checkBins p' &&& checkBins t'
+        where checkBins xs = bAnd $ map (\x -> x .== 0 ||| x .== 1) $ vals xs
+
+checkCut :: PetriNet -> SIMap Transition -> SIMap Transition -> SIMap Transition -> SBool
+checkCut net t' yt cut =
+            bAnd $ map checkTransition $ transitions net
+        where checkTransition t =
+                let pos = val yt t .== 0 &&& val t' t .> 0 ==> val cut t .== 1
+                    neg = val yt t .> 0 ||| val t' t .== 0 ==> val cut t .== 0
+                in  pos &&& neg
+
+checkNonNegativityConstraints :: SIMap Place -> SIMap Transition -> SBool
+checkNonNegativityConstraints yp yt = checkNN yp &&& checkNN yt
+        where checkNN xs = bAnd $ map (.>= 0) $ vals xs
+
+checkSizeLimit :: SIMap Place -> SIMap Transition -> SIMap Transition ->
+        Maybe (Integer, Integer) -> SBool
+checkSizeLimit _ _ _ Nothing = true
+checkSizeLimit p' _ cut (Just (pSize, cutSize)) =
+        let pSizeNext = sumVal p'
+            cutSizeNext = sumVal cut
+            pSizeNow = literal pSize
+            cutSizeNow = literal cutSize
+--            checkTransition (t, tVal) = val cut t .<= literal tVal
+--        in  bAnd (map checkTransition cutMap) &&& cutSizeNext .< cutSizeNow
+--        in  (pSizeNext .< pSizeNow) ||| (pSizeNext .== pSizeNow &&& cutSizeNext .< cutSizeNow)
+--        in  (cutSizeNext .< cutSizeNow) ||| (cutSizeNext .== cutSizeNow &&& pSizeNext .< pSizeNow)
+        in  (cutSizeNext .< cutSizeNow)
+
+checkSComponent :: PetriNet -> FiringVector -> Maybe (Integer, Integer) -> SIMap Place ->
+        SIMap Transition -> SIMap Place -> SIMap Transition -> SIMap Transition ->
+        SInteger -> SBool
+checkSComponent net x sizeLimit p' t' yp yt cut k =
+        checkPrePostPlaces net p' t' &&&
+        checkPrePostTransitions net p' t' &&&
+        checkMinimum x yt &&&
+        checkMaximum x yt k &&&
+        checkNext x yt k &&&
+        checkSubset net p' t' yp yt &&&
+        checkZeroUnused x t' yt &&&
+        checkSizeLimit p' t' cut sizeLimit &&&
+        checkClosed net p' t' yp yt &&&
+        checkTokens net p' k &&&
+        checkBinary p' t' &&&
+        checkNonNegativityConstraints yp yt &&&
+        checkCut net t' yt cut
+
+checkGeneralSComponentSat :: PetriNet -> FiringVector -> Maybe (Integer, Integer) ->
+        ConstraintProblem Integer (Cut, (Integer, Integer))
+checkGeneralSComponentSat net x sizeLimit =
+        let p' = makeVarMap $ places net
+            t' = makeVarMap $ transitions net
+            yp = makeVarMapWith prime $ places net
+            yt = makeVarMapWith prime $ transitions net
+            cut = makeVarMapWith (prime . prime) $ transitions net
+        in  ("general S-component constraints", "cut",
+            ["@k"] ++ getNames p' ++ getNames t' ++ getNames yp ++ getNames yt ++ getNames cut,
+            \fm -> checkSComponent net x sizeLimit (fmap fm p') (fmap fm t')
+                    (fmap fm yp) (fmap fm yt) (fmap fm cut) (fm "@k"),
+            \fm -> cutFromAssignment net x (fmap fm p') (fmap fm t')
+                    (fmap fm yp) (fmap fm yt) (fmap fm cut) (fm "@k"))
+
+cutFromAssignment :: PetriNet -> FiringVector -> IMap Place -> IMap Transition ->
+        IMap Place -> IMap Transition -> IMap Transition -> Integer ->
+        (Cut, (Integer, Integer))
+cutFromAssignment net x p' t' yp yt cut k =
+        let ps = M.keys $ M.filter (> 0) p'
+            ts = M.keys $ M.filter (> 0) t'
+            cs = M.keys $ M.filter (> 0) cut
+            filterComp i = M.keys . M.filter (== i)
+            components = map (\i -> (filterComp i yp, filterComp i yt)) [1..k]
+            psy = map (\p -> (yp M.! p, ([p],[]))) ps
+            tsy = map (\t -> (yt M.! t, ([],[t]))) ts
+            myInsert curMap (kVal, (ps', ts')) = M.insertWith insertPair kVal (ps', ts') curMap
+            insertPair (ps'', ts'') (ps', ts') = (ps' ++ ps'', ts' ++ ts'')
+            compMap = foldl myInsert M.empty (psy ++ tsy)
+        in  ((components, cs), (genericLength ps, genericLength cs))

src/Solver/MultiwayCut.hs

+module Solver.MultiwayCut
+    (checkMultiwayCutSat)
+where
+
+import Data.SBV
+import qualified Data.Map as M
+import qualified Data.Set as S
+
+import Util
+import Solver
+import PetriNet
+
+checkConnection :: PetriNet -> S.Set Place ->
+        SIMap Place -> SIMap Transition -> Place -> SBool
+checkConnection net ps m x p =
+            bAnd $ map checkTransition $ post net p
+        where checkTransition t =
+                let p' = S.elemAt 0 $ S.fromList (post net t) `S.intersection` ps
+                in  val x t .> 0 ==> val m p .== val m p'
+
+checkConnections :: PetriNet -> S.Set Place ->
+        SIMap Place -> SIMap Transition -> SBool
+checkConnections net ps m x =
+        bAnd $ map (checkConnection net ps m x) $ S.toList ps
+
+checkSizeLimit :: SIMap Transition -> Maybe Integer -> SBool
+checkSizeLimit _ Nothing = true
+checkSizeLimit x (Just size) = (.< literal size) $ sumVal x
+
+checkBinary :: SIMap Transition -> SBool
+checkBinary = bAnd . map (\x -> x .== 0 ||| x .== 1) . vals
+
+checkNonNegativityConstraints :: SIMap Place -> SBool
+checkNonNegativityConstraints = bAnd . map (.>= 0) . vals
+
+checkComponents :: [(Place, Integer)] -> SIMap Place -> SBool
+checkComponents componentMap m = bAnd $ map checkComponent componentMap
+        where checkComponent (p, n) = val m p .== literal n
+
+checkMultiwayCut :: PetriNet -> [(Place, Integer)] -> S.Set Place ->
+        SIMap Place -> SIMap Transition -> Maybe Integer -> SBool
+checkMultiwayCut net componentMap ps m x sizeLimit =
+        checkConnections net ps m x &&&
+        checkComponents componentMap m &&&
+        checkBinary x &&&
+        checkNonNegativityConstraints m &&&
+        checkSizeLimit x sizeLimit
+
+getMultiwayCut :: [[Place]] -> [Place] -> [Transition] -> IMap Transition -> ([Transition], Integer)
+getMultiwayCut componentMap ps ts x =
+            let tCut = M.keys (M.filter (> 0) x)
+                cutSize = length tCut
+            in  (tCut, cutSize)
+
+makeComponentMap :: (Ord a) => [[a]] -> [(a, Integer)]
+makeComponentMap ps = concat $ zipWith zip ps $ map repeat [1..]
+
+checkMultiwayCutSat :: PetriNet -> [[Place]] -> [Place] -> [Transition] -> Maybe Integer ->
+        ConstraintProblem Integer ([Transition], Integer)
+checkMultiwayCutSat net placeComponents ps ts sizeLimit =
+        let m = makeVarMap ps
+            x = makeVarMap ts
+            componentMap = makeComponentMap placeComponents
+            placeSet = S.fromList ps
+        in  ("multiway cut", "multiway cut",
+            getNames m ++ getNames x,
+            \fm -> checkMultiwayCut net componentMap placeSet
+                    (fmap fm m) (fmap fm x) sizeLimit,
+            \fm -> getMultiwayCut componentMap ps ts (fmap fm x))
+

src/Solver/SComponentWithCut.hs

+module Solver.SComponentWithCut
+    (checkSComponentWithCutSat)
+where
+
+import Data.SBV
+import Data.List (genericLength)
+import qualified Data.Map as M
+
+import Util
+import PetriNet
+import Solver
+
+type SizeIndicator = (Integer, Integer, Integer, Integer, Integer)
+
+checkPrePostPlaces :: PetriNet -> SIMap Place -> SIMap Place ->
+        SIMap Transition -> SIMap Transition -> SIMap Transition ->
+        SBool
+checkPrePostPlaces net p1 p2 t0 t1 t2 =
+            bAnd (map (checkPrePostPlace p1 [t0,t1]) (places net)) &&&
+            bAnd (map (checkPrePostPlace p2 [t0,t2]) (places net))
+        where checkPrePostPlace ps ts p =
+                  let incoming = map (checkIn ts) $ pre net p
+                      outgoing = map (checkIn ts) $ post net p
+                  in  val ps p .== 1 ==> bAnd incoming &&& bAnd outgoing
+              checkIn xs x = sum (map (`val` x) xs) .== 1
+
+checkPrePostTransitions :: PetriNet -> SIMap Place -> SIMap Place ->
+        SIMap Transition -> SIMap Transition -> SIMap Transition ->
+        SBool
+checkPrePostTransitions net p1 p2 t0 t1 t2 =
+            bAnd (map (checkPrePostTransition t0 [p1,p2]) (transitions net)) &&&
+            bAnd (map (checkPrePostTransition t1 [p1]) (transitions net)) &&&
+            bAnd (map (checkPrePostTransition t2 [p2]) (transitions net))
+        where checkPrePostTransition ts ps t =
+                  let incoming = checkInOne ps $ pre net t
+                      outgoing = checkInOne ps $ post net t
+                  in  val ts t .== 1 ==> incoming &&& outgoing
+              checkInOne xs x = sum (concatMap (`mval` x) xs) .== 1
+
+checkComponents :: FiringVector -> SIMap Transition -> SIMap Transition -> SBool
+checkComponents x t1 t2 = checkComponent t1 &&& checkComponent t2
+        where checkTransition ts t = val ts t .== 1
+              checkComponent ts = bOr $ map (checkTransition ts) $ elems x
+
+checkZeroUnused :: FiringVector -> SIMap Transition -> SBool
+checkZeroUnused x t0 = bAnd (map checkTransition (elems x))
+        where checkTransition t = val t0 t .== 0
+
+checkTokens :: PetriNet -> SIMap Place -> SIMap Place -> SBool
+checkTokens net p1 p2 =
+            sum (map addPlace $ linitials net) .== 1
+        where addPlace (p,i) = literal i * (val p1 p + val p2 p)
+
+checkDisjunct :: PetriNet ->
+        SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> SIMap Transition ->
+        SBool
+checkDisjunct net p1 p2 t0 t1 t2 =
+            bAnd (map checkPlace (places net)) &&&
+            bAnd (map checkTransition (transitions net))
+        where checkPlace p = val p1 p + val p2 p .<= 1
+              checkTransition t = val t0 t + val t1 t + val t2 t .<= 1
+
+checkBinary :: SIMap Place -> SIMap Place -> SIMap Transition ->
+        SIMap Transition -> SIMap Transition -> SBool
+checkBinary p1 p2 t0 t1 t2 =
+            checkBins p1 &&& checkBins p2 &&& checkBins t0 &&& checkBins t1 &&& checkBins t2
+        where checkBins xs = bAnd $ map (\x -> x .== 0 ||| x .== 1) $ vals xs
+
+checkSizeLimit ::
+        SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> SIMap Transition ->
+        Maybe SizeIndicator -> SBool
+checkSizeLimit _ _ _ _ _ Nothing = true
+checkSizeLimit p1 p2 t0 t1 t2 (Just (p1Size, p2Size, t0Size, t1Size, t2Size)) =
+        let p1SizeNext = sumVal p1
+            p2SizeNext = sumVal p2
+            t0SizeNext = sumVal t0
+            t1SizeNext = sumVal t1
+            t2SizeNext = sumVal t2
+            p1SizeNow = literal p1Size
+            p2SizeNow = literal p2Size
+            t0SizeNow = literal t0Size
+            t1SizeNow = literal t1Size
+            t2SizeNow = literal t2Size
+        in  (p1SizeNext + p2SizeNext .< p1SizeNow + p2SizeNow) |||
+            (p1SizeNext + p2SizeNext .== p1SizeNow + p2SizeNow &&& t0SizeNext .< t0SizeNow) |||
+            (p1SizeNext + p2SizeNext .== p1SizeNow + p2SizeNow &&& t0SizeNext .== t0SizeNow &&&
+            ((t1SizeNext .> t1SizeNow &&& t2SizeNext .>= t2SizeNow) |||
+            (t1SizeNext .>= t1SizeNow &&& t2SizeNext .> t2SizeNow)))
+--        in  (t0SizeNext .< t0SizeNow) |||
+--            (t0SizeNext .== t0SizeNow &&& t1SizeNext .> t1SizeNow &&& t2SizeNext .>= t2SizeNow) |||
+--            (t0SizeNext .== t0SizeNow &&& t1SizeNext .>= t1SizeNow &&& t2SizeNext .> t2SizeNow)
+
+checkSComponent :: PetriNet -> FiringVector -> Maybe SizeIndicator ->
+        SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> SIMap Transition ->
+        SBool
+checkSComponent net x sizeLimit p1 p2 t0 t1 t2 =
+        checkPrePostPlaces net p1 p2 t0 t1 t2 &&&
+        checkPrePostTransitions net p1 p2 t0 t1 t2 &&&
+        checkZeroUnused x t0 &&&
+        checkComponents x t1 t2 &&&
+        checkSizeLimit p1 p2 t0 t1 t2 sizeLimit &&&
+        checkTokens net p1 p2 &&&
+        checkBinary p1 p2 t0 t1 t2 &&&
+        checkDisjunct net p1 p2 t0 t1 t2
+
+checkSComponentWithCutSat :: PetriNet -> FiringVector -> Maybe SizeIndicator ->
+        ConstraintProblem Integer (Cut, SizeIndicator)
+checkSComponentWithCutSat net x sizeLimit =
+        let p1 = makeVarMapWith ("P1@"++) $ places net
+            p2 = makeVarMapWith ("P2@"++) $ places net
+            t0 = makeVarMapWith ("T0@"++) $ transitions net
+            t1 = makeVarMapWith ("T1@"++) $ transitions net
+            t2 = makeVarMapWith ("T2@"++) $ transitions net
+        in  ("general S-component constraints", "cut",
+            getNames p1 ++ getNames p2 ++ getNames t0 ++ getNames t1 ++ getNames t2,
+            \fm -> checkSComponent net x sizeLimit
+                    (fmap fm p1) (fmap fm p2) (fmap fm t0) (fmap fm t1) (fmap fm t2),
+            \fm -> cutFromAssignment
+                    (fmap fm p1) (fmap fm p2) (fmap fm t0) (fmap fm t1) (fmap fm t2))
+
+cutFromAssignment ::
+        IMap Place -> IMap Place -> IMap Transition -> IMap Transition -> IMap Transition ->
+        (Cut, SizeIndicator)
+cutFromAssignment p1m p2m t0m t1m t2m =
+        let p1 = M.keys $ M.filter (> 0) p1m
+            p2 = M.keys $ M.filter (> 0) p2m
+            t0 = M.keys $ M.filter (> 0) t0m
+            t1 = M.keys $ M.filter (> 0) t1m
+            t2 = M.keys $ M.filter (> 0) t2m
+        in  (([(p1,t1),(p2,t2)], t0), (genericLength p1, genericLength p2,
+                genericLength t0, genericLength t1, genericLength t2))

src/Solver/Simplifier.hs

@@ -5,9 +5,9 @@ module Solver.Simplifier (
 ) where
 
 import Data.SBV
+import Data.Maybe
 import qualified Data.Map as M
 import qualified Data.Set as S
-import Control.Monad
 
 import Util
 import Options
@@ -48,29 +48,44 @@ checkSubsumptionSat c0 cs =
 cutTransitions :: SimpleCut -> S.Set Transition
 cutTransitions (c0, cs) = S.unions (c0:cs)
 
-generateCuts :: Formula Transition -> [Cut] -> OptIO [SimpleCut]
-generateCuts f cuts =
-            foldM combine [formulaToCut f] (map cutToSimpleDNFCuts cuts)
+generateCuts :: PetriNet -> Formula Transition -> [Cut] -> OptIO [SimpleCut]
+generateCuts net f cuts = do
+            simp <- opt optSimpFormula
+            let cs = [formulaToCut f] : map cutToSimpleDNFCuts cuts
+            let cs' = foldl1 (combine simp) cs
+            let cs'' = if simp > 1 then filterInvariantTransitions net cs' else cs'
+            if simp > 1 then simplifyBySubsumption (simplifyCuts cs'') else return cs''
         where
-            combine cs1 cs2 = do
-                simp <- opt optSimpFormula
+            combine simp cs1 cs2 =
                 let cs  = [ (c1c0 `S.union` c2c0, c1cs ++ c2cs)
                          | (c1c0, c1cs) <- cs1, (c2c0, c2cs) <- cs2 ]
-                let cs'  = if simp > 0 then simplifyCuts cs else cs
-                let cs'' = if simp > 1 then simplifyBySubsumption cs' else return cs'
-                cs''
+                in  if simp > 0 then simplifyCuts cs else cs
+
+filterInvariantTransitions :: PetriNet -> [SimpleCut] -> [SimpleCut]
+filterInvariantTransitions net cuts =
+        let ts = S.fromList $ invariantTransitions net
+        in  map (filterTransitions ts) cuts
+
+filterTransitions :: S.Set Transition -> SimpleCut -> SimpleCut
+filterTransitions ts (c0, cs) =
+        let c0' = c0 `S.difference` ts
+            cs' = filter (S.null . S.intersection ts) cs
+        in  (c0', cs')
+
+invariantTransitions :: PetriNet -> [Transition]
+invariantTransitions net = filter (\t -> lpre net t == lpost net t) $ transitions net
 
 simplifyCuts :: [SimpleCut] -> [SimpleCut]
-simplifyCuts = removeWith isMoreGeneralCut . concatMap simplifyCut
+simplifyCuts = removeWith isMoreGeneralCut . mapMaybe simplifyCut
 
-simplifyCut :: SimpleCut -> [SimpleCut]
+simplifyCut :: SimpleCut -> Maybe SimpleCut
 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
-                []
+                Nothing
             else
-                [(c0, cs')]
+                Just (c0, cs')
 
 simplifyBySubsumption :: [SimpleCut] -> OptIO [SimpleCut]
 simplifyBySubsumption = simplifyBySubsumption' []
@@ -78,6 +93,7 @@ simplifyBySubsumption = simplifyBySubsumption' []
 simplifyBySubsumption' :: [SimpleCut] -> [SimpleCut] -> OptIO [SimpleCut]
 simplifyBySubsumption' acc [] = return $ reverse acc
 simplifyBySubsumption' acc (c0:cs) = do
+        -- TODO: check with prime implicants
         r <- checkSat $ checkSubsumptionSat c0 (acc ++ cs)
         let acc' = case r of
                     Nothing -> acc
@@ -88,8 +104,8 @@ removeWith :: (a -> a -> Bool) -> [a] -> [a]
 removeWith f = removeCuts' []
         where
             removeCuts' acc [] = reverse acc
-            removeCuts' acc (x:xs) = removeCuts' (x : cutFilter x acc) (cutFilter x xs)
-            cutFilter cut = filter (not . f cut)
+            removeCuts' acc (x:xs) = removeCuts' (x : notFilter x acc) (notFilter x xs)
+            notFilter x = filter (not . f x)
 
 isMoreGeneralCut :: SimpleCut -> SimpleCut -> Bool
 isMoreGeneralCut (c1c0, c1cs) (c2c0, c2cs) =
@@ -98,6 +114,7 @@ isMoreGeneralCut (c1c0, c1cs) (c2c0, c2cs) =
 cutToSimpleDNFCuts :: Cut -> [SimpleCut]
 cutToSimpleDNFCuts (ts, u) = (S.empty, [S.fromList u]) : map (\(_, t) -> (S.fromList t, [])) ts
 
+-- TODO: allow formulas with or
 formulaToCut :: Formula Transition -> SimpleCut
 formulaToCut = transformF
         where