Added greedy simplification for invariant

src/Main.hs

@@ -32,6 +32,7 @@ import Solver.LivenessInvariant
 import Solver.SafetyInvariant
 import Solver.SComponentWithCut
 import Solver.Simplifier
+import Solver.Interpolant
 --import Solver.CommFreeReachability
 
 writeFiles :: String -> PetriNet -> [Property] -> OptIO ()
@@ -289,6 +290,11 @@ getLivenessInvariant net f cuts = do
         dnfCuts <- generateCuts net f cuts
         verbosePut 2 $ "Number of " ++ (if simp > 0 then "simplified " else "") ++
                        "disjuncts: " ++ show (length dnfCuts)
+        --
+        --z <- conciliate (transitions net)
+        --    (checkSimpleCuts dnfCuts) (transitionVectorConstraints net)
+        --verbosePut 0 $ "Conciliated set: " ++ show z
+        --
         rs <- mapM (checkSat . checkLivenessInvariantSat net) dnfCuts
         let added = map (Just . cutToLivenessInvariant) cuts
         return $ sequence (rs ++ added)
@@ -327,7 +333,7 @@ findLivenessRefinement net x = do
 
 findLivenessRefinementBySComponent :: PetriNet -> FiringVector ->
         OptIO (Maybe Cut)
-findLivenessRefinementBySComponent net x = do
+findLivenessRefinementBySComponent net x =
         checkSatMin $ checkSComponentWithCutSat net x
 
 findLivenessRefinementByEmptyTraps :: PetriNet -> Marking -> FiringVector ->
@@ -353,15 +359,7 @@ 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

src/PetriNet.hs

@@ -9,7 +9,7 @@ module PetriNet
      pre,lpre,post,lpost,mpre,mpost,context,ghostTransitions,
      makePetriNet,makePetriNetWithTrans,
      makePetriNetFromStrings,makePetriNetWithTransFromStrings,Trap,Cut,
-     constructCut)
+     constructCut,SimpleCut)
 where
 
 import qualified Data.Map as M
@@ -27,6 +27,8 @@ instance Show Place where
 instance Show Transition where
         show (Transition t) = t
 
+type SimpleCut = (S.Set Transition, [S.Set Transition])
+
 type ContextMap a b = M.Map a ([(b, Integer)],[(b, Integer)])
 
 class (Ord a, Ord b) => Nodes a b | a -> b where

src/Solver/Simplifier.hs

@@ -2,6 +2,7 @@ module Solver.Simplifier (
      checkSubsumptionSat
     ,SimpleCut
     ,generateCuts
+    ,greedySimplify
 ) where
 
 import Data.SBV
@@ -12,11 +13,10 @@ import qualified Data.Set as S
 import Util
 import Options
 import Solver
+import Solver.TransitionInvariant
 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
 
@@ -54,7 +54,9 @@ generateCuts net f cuts = do
             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''
+            let cs''' = if simp > 1 then simplifyCuts cs'' else cs''
+            cs'''' <- if simp > 1 then mapM (greedySimplify net) cs''' else return cs'''
+            if simp > 1 then simplifyBySubsumption (simplifyCuts cs'''') else return cs''''
         where
             combine simp cs1 cs2 =
                 let cs  = [ (c1c0 `S.union` c2c0, c1cs ++ c2cs)
@@ -140,3 +142,28 @@ formulaToCut = transformF
             transformTerm t =
                 error $ "term not supported for invariant: " ++ show t
 
+checkCut :: PetriNet -> SimpleCut -> OptIO Bool
+checkCut net cut = do
+        verbosePut 0 $ "checking cut " ++ show cut
+        r <- checkSat $ checkTransitionInvariantWithSimpleCutSat net cut
+        return $ isNothing r
+
+greedySimplifyCut :: PetriNet -> SimpleCut -> SimpleCut-> OptIO SimpleCut
+greedySimplifyCut net cutAcc@(c0Acc, csAcc) (c0, cs) =
+        case (S.null c0, cs) of
+            (True, []) -> return cutAcc
+            (False, _) -> do
+                let (c, c0') = S.deleteFindMin c0
+                let cut = (c0Acc `S.union` c0', csAcc ++ cs)
+                r <- checkCut net cut
+                greedySimplifyCut net (if r then cutAcc else (S.insert c c0Acc, csAcc)) (c0', cs)
+            (True, c:cs') -> do
+                let cut = (c0Acc `S.union` c0, csAcc ++ cs')
+                r <- checkCut net cut
+                greedySimplifyCut net (if r then cutAcc else (c0Acc, c:csAcc)) (c0, cs')
+
+greedySimplify :: PetriNet -> SimpleCut -> OptIO SimpleCut
+greedySimplify net cut = do
+        verbosePut 0 $ "simplifying cut " ++ show cut
+        greedySimplifyCut net (S.empty, []) cut
+

src/Solver/TransitionInvariant.hs

 module Solver.TransitionInvariant
-    (checkTransitionInvariantSat)
+    (checkTransitionInvariantSat
+    ,checkTransitionInvariantWithSimpleCutSat
+    ,tInvariantConstraints
+    ,finalInvariantConstraints
+    ,nonnegativityConstraints
+    ,transitionVectorConstraints
+    ,formulaAndRefinementConstraints
+    ,checkSimpleCut)
 where
 
 import Data.SBV
+import qualified Data.Set as S
 
 import Util
 import PetriNet
@@ -25,6 +33,23 @@ finalInvariantConstraints x = sum (vals x) .> 0
 nonnegativityConstraints :: SIMap Transition -> SBool
 nonnegativityConstraints x = bAnd $ map (.>= 0) (vals x)
 
+transitionVectorConstraints :: PetriNet -> SIMap Transition -> SBool
+transitionVectorConstraints net x =
+        nonnegativityConstraints x &&&
+        finalInvariantConstraints x &&&
+        tInvariantConstraints net x
+
+formulaAndRefinementConstraints :: Formula Transition -> [Cut] -> SIMap Transition -> SBool
+formulaAndRefinementConstraints f cuts x =
+        checkCuts cuts x &&&
+        evaluateFormula f x
+
+checkSimpleCut :: SimpleCut -> SIMap Transition -> SBool
+checkSimpleCut (t0, cs) x =
+            checkNegative (S.toList t0) &&& bAnd (map (checkPositive . S.toList) cs)
+        where checkNegative ts = sum (mval x ts) .== 0
+              checkPositive ts = sum (mval x ts) .> 0
+
 checkCuts :: [Cut] -> SIMap Transition -> SBool
 checkCuts cuts x = bAnd $ map checkCut cuts
         where checkCut (ts, u) =
@@ -35,11 +60,8 @@ checkCuts cuts x = bAnd $ map checkCut cuts
 checkTransitionInvariant :: PetriNet -> Formula Transition ->
         [Cut] -> SIMap Transition -> SBool
 checkTransitionInvariant net f cuts x =
-        tInvariantConstraints net x &&&
-        nonnegativityConstraints x &&&
-        finalInvariantConstraints x &&&
-        checkCuts cuts x &&&
-        evaluateFormula f x
+        transitionVectorConstraints net x &&&
+        formulaAndRefinementConstraints f cuts x
 
 checkTransitionInvariantSat :: PetriNet -> Formula Transition -> [Cut] ->
         ConstraintProblem Integer FiringVector
@@ -50,6 +72,21 @@ checkTransitionInvariantSat net f cuts =
             \fm -> checkTransitionInvariant net f cuts (fmap fm x),
             \fm -> firingVectorFromAssignment (fmap fm x))
 
+checkTransitionInvariantWithSimpleCut :: PetriNet ->
+        SimpleCut -> SIMap Transition -> SBool
+checkTransitionInvariantWithSimpleCut net cut x =
+        transitionVectorConstraints net x &&&
+        checkSimpleCut cut x
+
+checkTransitionInvariantWithSimpleCutSat :: PetriNet -> SimpleCut ->
+        ConstraintProblem Integer FiringVector
+checkTransitionInvariantWithSimpleCutSat net cut =
+        let x = makeVarMap $ transitions net
+        in  ("transition invariant constraints with simple cut", "transition invariant",
+            getNames x,
+            \fm -> checkTransitionInvariantWithSimpleCut net cut (fmap fm x),
+            \fm -> firingVectorFromAssignment (fmap fm x))
+
 firingVectorFromAssignment :: IMap Transition -> FiringVector
 firingVectorFromAssignment = makeVector