Added constraints to find an s-component

src/Main.hs

@@ -18,7 +18,6 @@ checkSafetyProperty net f traps = do
         case r of
             Nothing -> return True
             Just a -> do
-                --print a
                 let assigned = markedPlacesFromAssignment net a
                 putStrLn $ "Assignment found marking " ++ show assigned
                 rt <- checkSat $ checkTrapSat net assigned
@@ -52,6 +51,7 @@ checkLivenessProperty net f = do
 
 checkProperty :: PetriNet -> Property -> IO Bool
 checkProperty net p = do
+        --putStrLn $ "\nChecking " ++ showPropertyName p
         r <- case ptype p of
             Safety -> checkSafetyProperty net (pformula p) []
             Liveness -> checkLivenessProperty net (pformula p)
@@ -67,10 +67,7 @@ main = do
         putStrLn $ "Reading \"" ++ file ++ "\""
         (net,properties) <- parseFile file
         putStrLn $ "Analyzing " ++ showNetName net
-        rs <- mapM (\p -> do
-                      putStrLn $ "\nChecking " ++ showPropertyName p
-                      checkProperty net p
-                  ) properties
+        rs <- mapM (checkProperty net) properties
         if and rs then
             exitSuccess
         else

src/Solver/SComponent.hs

+module Solver.SComponent
+    (checkSComponent,checkSComponentSat)
+where
+
+import Data.SBV
+import qualified Data.Map as M
+
+import PetriNet
+import Solver
+
+mElem :: ModelSI -> String -> SBool
+mElem m x = (m M.! x) .== 1
+
+mNotElem :: ModelSI -> String -> SBool
+mNotElem m x = (m M.! x) .== 0
+
+countElem :: ModelSI -> [String] -> SInteger
+countElem m xs = sum $ map (m M.!) xs
+
+prime :: String -> String
+prime = ('\'':)
+
+checkPrePostPlaces :: PetriNet -> ModelSI -> SBool
+checkPrePostPlaces net m =
+            bAnd $ map checkPrePostPlace $ places net
+        where checkPrePostPlace p =
+                let incoming = map (mElem m) $ pre net p
+                    outgoing = map (mElem m) $ post net p
+                in  mElem m p ==> bAnd incoming &&& bAnd outgoing
+
+checkPrePostTransitions :: PetriNet -> ModelSI -> SBool
+checkPrePostTransitions net m =
+            bAnd $ map checkPrePostTransition $ transitions net
+        where checkPrePostTransition t =
+                let incoming = countElem m $ pre net t
+                    outgoing = countElem m $ post net t
+                in  mElem m t ==> incoming .== 1 &&& outgoing .== 1
+
+checkSubsetTransitions :: [String] -> ModelSI -> SBool
+checkSubsetTransitions fired m =
+            bAnd (map checkTransition fired) &&&
+            countElem m (map prime fired) .< countElem m fired
+        where checkTransition t =
+                mElem m (prime t) ==> mElem m t
+
+checkNotEmpty :: [String] -> ModelSI -> SBool
+checkNotEmpty fired m = countElem m (map prime fired) .> 0
+
+checkClosed :: PetriNet -> ModelI -> ModelSI -> SBool
+checkClosed net a m =
+            bAnd (map checkPlaceClosed (places net))
+        where checkPlaceClosed p = mElem m p ==>
+                        bAnd (map checkTransition
+                             [(t,t') | t <- pre net p, t' <- post net p,
+                                       a M.! t > 0  , a M.! t' > 0 ])
+              checkTransition (t,t') =
+                  mElem m (prime t) &&& mElem m t' ==> mElem m (prime t')
+
+checkBinary :: ModelSI -> SBool
+checkBinary m = bAnd $ map (\x -> x .== 0 ||| x .== 1) $ M.elems m
+
+checkSComponent :: PetriNet -> [String] -> ModelI -> ModelSI -> SBool
+checkSComponent net fired a m =
+        checkPrePostPlaces net m &&&
+        checkPrePostTransitions net m &&&
+        checkSubsetTransitions fired m &&&
+        checkNotEmpty fired m &&&
+        checkClosed net a m &&&
+        checkBinary m
+
+checkSComponentSat :: PetriNet -> ModelI -> ([String], ModelSI -> SBool)
+checkSComponentSat net a =
+        let fired = M.keys $ M.filter (> 0) a
+        in  (places net ++ transitions net ++ map prime fired,
+             checkSComponent net fired a)