Using better cuts for S-component refinement

src/Main.hs

@@ -474,7 +474,7 @@ checkSafetyPropertyBySafetyRef verbosity net refine f traps = do
                     return Unknown
 
 checkLivenessProperty :: Int -> PetriNet -> Bool ->
-        Formula -> [([String],[String])] -> IO PropResult
+        Formula -> [SCompCut] -> IO PropResult
 checkLivenessProperty verbosity net refine f strans = do
         r <- checkSat $ checkTransitionInvariantSat net f strans
         case r of
@@ -491,13 +491,13 @@ checkLivenessProperty verbosity net refine f strans = do
                             verbosePut verbosity 1 "No S-component found"
                             return Unknown
                         Just as -> do
-                            let sOutIn = getSComponentOutIn net ax as
+                            let sCompsCut = getSComponentCompsCut net ax as
                             verbosePut verbosity 1 "S-component found"
-                            verbosePut verbosity 2 $ "Out/In: " ++ show sOutIn
+                            verbosePut verbosity 2 $ "Comps/Cut: " ++ show sCompsCut
                             verbosePut verbosity 3 $ "S-Component assignment: " ++
                                                       show as
                             checkLivenessProperty verbosity net refine f
-                                                  (sOutIn:strans)
+                                                  (sCompsCut:strans)
                 else
                     return Unknown
 

src/Solver/LivenessInvariant.hs

+module Solver.LivenessInvariant (
+    checkLivenessInvariant
+  , checkLivenessInvariantSat
+  , getLivenessInvariant
+  , PlaceVector
+  , LivenessInvariant
+) where
+
+type PlaceVector [(String,Integer)]
+type LivenessInvariant = [PlaceVector]
+
+checkLivenessInvariant :: PetriNet -> [String] -> ModelI -> ModelSI -> SBool
+checkLivenessInvariant net fired ax m =
+        checkPrePostPlaces net m &&&
+        checkPrePostTransitions net m &&&
+        checkSubsetTransitions fired m &&&
+        checkNotEmpty fired m &&&
+        checkClosed net ax m &&&
+        checkTokens net m &&&
+        checkBinary m
+
+checkLivenessInvariantSat :: PetriNet -> [String] -> ModelI ->
+        ([String], ModelSI -> SBool)
+checkLivenessInvariantSat net fired ax =
+
+getLivenessInvariant :: PetriNet -> ModelI -> ModelI -> LivenessInvariant
+getLivenessInvariant net ax as =

src/Solver/SComponent.hs

 module Solver.SComponent
     (checkSComponent,checkSComponentSat,
-     getSComponentOutIn)
+     getSComponentOutIn,
+     getSComponentCompsCut,
+     SCompCut)
 where
 
 import Data.SBV
@@ -9,6 +11,8 @@ import Data.List (partition)
 import PetriNet
 import Solver
 
+type SCompCut = ([String], [String], [String])
+
 checkPrePostPlaces :: PetriNet -> ModelSI -> SBool
 checkPrePostPlaces net m =
             bAnd $ map checkPrePostPlace $ places net
@@ -72,3 +76,10 @@ getSComponentOutIn :: PetriNet -> ModelI -> ModelI -> ([String], [String])
 getSComponentOutIn net ax as =
         partition (cElem ax) $ filter (cElem as) (transitions net)
 
+-- TODO: use strongly connected components and min cuts
+getSComponentCompsCut :: PetriNet -> ModelI -> ModelI -> SCompCut
+getSComponentCompsCut net ax as =
+        let (t, u) = partition (cElem ax) $ filter (cElem as) (transitions net)
+            (t1, t2) = partition (cElem as . prime) t
+        in  (t1, t2, u)
+

src/Solver/TransitionInvariant.hs

@@ -8,6 +8,7 @@ import Data.SBV
 import PetriNet
 import Property
 import Solver
+import Solver.SComponent
 import Solver.Formula
 
 tInvariantConstraints :: PetriNet -> ModelSI -> SBool
@@ -25,14 +26,15 @@ finalInvariantConstraints m = sum (mValues m) .> 0
 nonnegativityConstraints :: ModelSI -> SBool
 nonnegativityConstraints m = bAnd $ map (.>= 0) $ mValues m
 
-checkSComponentTransitions :: [([String],[String])] -> ModelSI -> SBool
-checkSComponentTransitions strans m = bAnd $ map checkInOut strans
-        where checkInOut (sOut,sIn) =
-                bAnd (map (\t -> mVal m t .> 0) sOut) ==>
-                bOr (map (\t -> mVal m t .> 0) sIn)
+checkSComponentTransitions :: [SCompCut] -> ModelSI -> SBool
+checkSComponentTransitions strans m = bAnd $ map checkCompsCut strans
+        where checkCompsCut (t1,t2,u) =
+                bOr (map (\t -> mVal m t .> 0) t1) &&&
+                bOr (map (\t -> mVal m t .> 0) t2) ==>
+                bOr (map (\t -> mVal m t .> 0) u)
 
-checkTransitionInvariant :: PetriNet -> Formula -> [([String],[String])] ->
-        ModelSI -> SBool
+checkTransitionInvariant :: PetriNet -> Formula ->
+        [SCompCut] -> ModelSI -> SBool
 checkTransitionInvariant net f strans m =
         tInvariantConstraints net m &&&
         nonnegativityConstraints m &&&
@@ -40,8 +42,8 @@ checkTransitionInvariant net f strans m =
         checkSComponentTransitions strans m &&&
         evaluateFormula f m
 
-checkTransitionInvariantSat :: PetriNet -> Formula -> [([String],[String])] ->
-        ([String], ModelSI -> SBool)
+checkTransitionInvariantSat :: PetriNet -> Formula ->
+        [SCompCut] -> ([String], ModelSI -> SBool)
 checkTransitionInvariantSat net f strans =
         (transitions net, checkTransitionInvariant net f strans)