Added on-the-fly simplification

src/Main.hs

@@ -287,33 +287,13 @@ checkLivenessProperty net f = do
 getLivenessInvariant :: PetriNet -> Formula Transition -> [Cut] -> OptIO (Maybe [LivenessInvariant])
 getLivenessInvariant net f cuts = do
         simp <- opt optSimpFormula
-        let dnfCuts = generateCuts f cuts
-        verbosePut 2 $ "Number of disjuncts: " ++ show (length dnfCuts)
---        let simpCuts = if simp then simplifyCuts dnfCuts else dnfCuts
-        let simpCuts = if simp then simplifyCuts dnfCuts else dnfCuts
-        verbosePut 2 $ "Number of simplified disjuncts (1): " ++ show (length simpCuts)
-        simpCuts' <- if simp then simplifyBySubsumption net [] simpCuts else return simpCuts
-        verbosePut 2 $ "Number of simplified disjuncts (2): " ++ show (length simpCuts')
-        rs <- mapM (checkSat . checkLivenessInvariantSat net) simpCuts'
+        dnfCuts <- generateCuts f cuts
+        verbosePut 2 $ "Number of " ++ (if simp > 0 then "simplified " else "") ++
+                       "disjuncts: " ++ show (length dnfCuts)
+        rs <- mapM (checkSat . checkLivenessInvariantSat net) dnfCuts
         let added = map (Just . cutToLivenessInvariant) cuts
         return $ sequence (rs ++ added)
 
-simplifyBySubsumption :: PetriNet -> [SimpleCut] -> [SimpleCut] -> OptIO [SimpleCut]
-simplifyBySubsumption _ acc [] = return $ reverse acc
-simplifyBySubsumption net acc (c0:cs) = do
-        r <- checkSat $ checkSubsumptionSat net c0 (acc ++ cs)
-        let acc' = case r of
-                    Nothing -> acc
-                    Just _ -> c0:acc
-        simplifyBySubsumption net acc' cs
-
-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)
-
 checkLivenessProperty' :: PetriNet ->
         Formula Transition -> [Cut] -> OptIO (Maybe FiringVector, [Cut])
 checkLivenessProperty' net f cuts = do

src/Options.hs

@@ -43,7 +43,7 @@ data Options = Options { inputFormat :: InputFormat
                        , optProperties :: [ImplicitProperty]
                        , optTransformations :: [NetTransformation]
                        , optRefine :: Bool
-                       , optSimpFormula :: Bool
+                       , optSimpFormula :: Int
                        , optRefinementType :: RefinementType
                        , optMinimizeRefinement :: Bool
                        , optInvariant :: Bool
@@ -61,7 +61,7 @@ startOptions = Options { inputFormat = PNET
                        , optProperties = []
                        , optTransformations = []
                        , optRefine = True
-                       , optSimpFormula = True
+                       , optSimpFormula = 2
                        , optRefinementType = SComponentRefinement
                        , optMinimizeRefinement = False
                        , optInvariant = False
@@ -220,12 +220,24 @@ options =
                }))
         "Do not use the properties given in the input file"
 
-        , Option "" ["no-simp"]
+        , Option "" ["simp-0"]
         (NoArg (\opt -> Right opt {
-                   optSimpFormula = False
+                   optSimpFormula = 0
                }))
         "Do not simplify formula for invariant generation"
 
+        , Option "" ["simp-1"]
+        (NoArg (\opt -> Right opt {
+                   optSimpFormula = 1
+               }))
+        "Use simplification level 1 for invariant generation"
+
+        , Option "" ["simp-2"]
+        (NoArg (\opt -> Right opt {
+                   optSimpFormula = 2
+               }))
+        "Use simplification level 2 for invariant generation"
+
         , Option "" ["minimize-refinement"]
         (NoArg (\opt -> Right opt {
                    optMinimizeRefinement = True

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 (sort,(\\))
+import Data.List ((\\))
 
 import Util
 

src/Solver/LivenessInvariant.hs

 module Solver.LivenessInvariant (
     checkLivenessInvariantSat
   , LivenessInvariant
-  , generateCuts
-  , simplifyCuts
   , cutToLivenessInvariant
   , SimpleCut
 ) where
@@ -14,7 +12,7 @@ import qualified Data.Set as S
 
 import Util
 import Solver
-import Property
+import Solver.Simplifier
 import PetriNet
 
 data LivenessInvariant =
@@ -44,85 +42,26 @@ instance Show LivenessInvariant where
                     "[" ++ showSimpleCuts cs ++ "]: " ++
                     show ps
 
-type SimpleCut = (S.Set Transition, [S.Set Transition])
 type NamedCut = (S.Set Transition, [(String, S.Set Transition)])
 
 placeName :: Place -> String
 placeName p = "@p" ++ show p
 
-generateCuts :: Formula Transition -> [Cut] -> [SimpleCut]
-generateCuts f cuts =
-            foldl combine [formulaToCut f] (map cutToSimpleDNFCuts cuts)
-        where
-            combine cs1 cs2 = [ (c1c0 `S.union` c2c0, c1cs ++ c2cs)
-                              | (c1c0, c1cs) <- cs1, (c2c0, c2cs) <- cs2 ]
-
-simplifyCuts :: [SimpleCut] -> [SimpleCut]
-simplifyCuts = removeWith isMoreGeneralCut . concatMap simplifyCut
-
-simplifyCut :: SimpleCut -> [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
-                []
-            else
-                [(c0, cs')]
-
 nameCut :: SimpleCut -> NamedCut
 nameCut (c0, cs) = (c0, numPref "@comp" `zip` cs)
 
-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)
-
-isMoreGeneralCut :: SimpleCut -> SimpleCut -> Bool
-isMoreGeneralCut (c1c0, c1cs) (c2c0, c2cs) =
-        c1c0 `S.isSubsetOf` c2c0 && all (\c1 -> any (`S.isSubsetOf` c1) c2cs) c1cs
-
 cutNames :: PetriNet -> NamedCut -> [String]
 cutNames net (_, c) =
         ["@yone", "@comp0"] ++
         map placeName (places net) ++
         map fst c
 
-cutToSimpleDNFCuts :: Cut -> [SimpleCut]
-cutToSimpleDNFCuts (ts, u) = (S.empty, [S.fromList u]) : map (\(_, t) -> (S.fromList t, [])) ts
-
 cutToSimpleCNFCut :: Cut -> SimpleCut
 cutToSimpleCNFCut (ts, u) = (S.fromList u, map (\(_, t) -> S.fromList t) ts)
 
 toSimpleCut :: NamedCut -> SimpleCut
 toSimpleCut (c0, ncs) = (c0, map snd ncs)
 
-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
-
 checkLivenessInvariant :: PetriNet -> NamedCut -> SIMap String -> SBool
 checkLivenessInvariant net (comp0, comps) m =
             bAnd (map checkTransition (transitions net)) &&&

src/Solver/Simplifier.hs

 module Solver.Simplifier (
-    checkSubsumptionSat
+     checkSubsumptionSat
+    ,SimpleCut
+    ,generateCuts
 ) where
 
 import Data.SBV
 import qualified Data.Map as M
 import qualified Data.Set as S
+import Control.Monad
 
 import Util
+import Options
 import Solver
-import Solver.LivenessInvariant
+import Property
 import PetriNet
 
+type SimpleCut = (S.Set Transition, [S.Set Transition])
+
 checkTransPositive :: SBMap Transition -> S.Set Transition -> SBool
 checkTransPositive m ts = bOr $ map (val m) $ S.elems ts
 
@@ -31,10 +37,89 @@ checkCuts c0 cs m = checkCutPositive m c0 &&& bAnd (map (checkCutNegative m) cs)
 getSubsumption :: BMap Transition -> [Transition]
 getSubsumption m = M.keys (M.filter id m)
 
-checkSubsumptionSat :: PetriNet -> SimpleCut -> [SimpleCut] -> ConstraintProblem Bool [Transition]
-checkSubsumptionSat net c0 cs =
-        let m = makeVarMap $ transitions net
+checkSubsumptionSat :: SimpleCut -> [SimpleCut] -> ConstraintProblem Bool [Transition]
+checkSubsumptionSat c0 cs =
+        let m = makeVarMap $ S.elems $ S.unions $ map cutTransitions (c0:cs)
         in  ("constraint subsumption", "subsumption",
             getNames m,
             \fm -> checkCuts c0 cs (fmap fm m),
             \fm -> getSubsumption (fmap fm m))
+
+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)
+        where
+            combine cs1 cs2 = do
+                simp <- opt optSimpFormula
+                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''
+
+simplifyCuts :: [SimpleCut] -> [SimpleCut]
+simplifyCuts = removeWith isMoreGeneralCut . concatMap simplifyCut
+
+simplifyCut :: SimpleCut -> [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
+                []
+            else
+                [(c0, cs')]
+
+simplifyBySubsumption :: [SimpleCut] -> OptIO [SimpleCut]
+simplifyBySubsumption = simplifyBySubsumption' []
+
+simplifyBySubsumption' :: [SimpleCut] -> [SimpleCut] -> OptIO [SimpleCut]
+simplifyBySubsumption' acc [] = return $ reverse acc
+simplifyBySubsumption' acc (c0:cs) = do
+        r <- checkSat $ checkSubsumptionSat c0 (acc ++ cs)
+        let acc' = case r of
+                    Nothing -> acc
+                    Just _ -> c0:acc
+        simplifyBySubsumption' acc' cs
+
+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)
+
+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
+
+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
+