Extended solver logic for safety and liveness properties

src/Main.hs

@@ -8,38 +8,47 @@ import PetriNet
 import Property
 import Solver
 import Solver.StateEquation
-import Solver.TransitionInvariant
 import Solver.TrapConstraints
+import Solver.TransitionInvariant
+import Solver.SComponent
 
 checkSafetyProperty :: PetriNet -> Formula -> [[String]] -> IO Bool
 checkSafetyProperty net f traps = do
-    r <- checkSat $ checkStateEquationSat net f traps
-    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
-            case rt of
-                Nothing -> do
-                    putStrLn "No trap found."
-                    return False
-                Just at -> do
-                    let trap = trapFromAssignment at
-                    putStrLn $ "Trap found with places " ++ show trap
-                    checkSafetyProperty net f (trap:traps)
+        r <- checkSat $ checkStateEquationSat net f traps
+        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
+                case rt of
+                    Nothing -> do
+                        putStrLn "No trap found."
+                        return False
+                    Just at -> do
+                        let trap = trapFromAssignment at
+                        putStrLn $ "Trap found with places " ++ show trap
+                        checkSafetyProperty net f (trap:traps)
 
 checkLivenessProperty :: PetriNet -> Formula -> IO Bool
 checkLivenessProperty net f = do
         r <- checkSat $ checkTransitionInvariantSat net f
         case r of
             Nothing -> return True
-            Just m -> do
-                putStrLn "Assignment found:"
-                print m
-                return False
-
+            Just a -> do
+                let fired = firedTransitionsFromAssignment a
+                putStrLn $ "Assignment found firing " ++ show fired
+                rt <- checkSat $ checkSComponentSat net a
+                case rt of
+                    Nothing -> do
+                        putStrLn "No S-component found"
+                        return False
+                    Just at -> do
+                        --let trap = trapFromAssignment at
+                        putStrLn $ "S-component found: " ++ show at
+                        -- checkLivenessProperty net f (trap:traps)
+                        return False
 
 checkProperty :: PetriNet -> Property -> IO Bool
 checkProperty net p = do

src/Solver/StateEquation.hs

@@ -12,8 +12,7 @@ import Solver
 import Solver.Formula
 
 placeConstraints :: PetriNet -> ModelSI -> SBool
-placeConstraints net m =
-            bAnd $ map checkPlaceEquation $ places net
+placeConstraints net m = bAnd $ map checkPlaceEquation $ places net
         where checkPlaceEquation p =
                 let incoming = map addTransition $ lpre net p
                     outgoing = map addTransition $ lpost net p
@@ -21,20 +20,17 @@ placeConstraints net m =
                 in  pinit + sum incoming - sum outgoing .== (m M.! p)
               addTransition (t,w) = literal w * (m M.! t)
 
-nonnegativityConstraints :: PetriNet -> ModelSI -> SBool
-nonnegativityConstraints net m =
-            bAnd $ map checkPT $ places net ++ transitions net
-        where checkPT x = (m M.! x) .>= 0
+nonnegativityConstraints ::  ModelSI -> SBool
+nonnegativityConstraints m = bAnd $ map (.>= 0) $ M.elems m
 
 checkTraps :: [[String]] -> ModelSI -> SBool
-checkTraps traps m =
-            bAnd $ map checkTrapDelta traps
+checkTraps traps m = bAnd $ map checkTrapDelta traps
         where checkTrapDelta trap = sum (map (m M.!) trap) .>= 1
 
 checkStateEquation :: PetriNet -> Formula -> [[String]] -> ModelSI -> SBool
 checkStateEquation net f traps m =
         placeConstraints net m &&&
-        nonnegativityConstraints net m &&&
+        nonnegativityConstraints m &&&
         checkTraps traps m &&&
         evaluateFormula f m
 

src/Solver/TransitionInvariant.hs

 module Solver.TransitionInvariant
-    (checkTransitionInvariant,checkTransitionInvariantSat)
+    (checkTransitionInvariant,checkTransitionInvariantSat,
+     firedTransitionsFromAssignment)
 where
 
 import Data.SBV
@@ -14,22 +15,27 @@ tInvariantConstraints :: PetriNet -> ModelSI -> SBool
 tInvariantConstraints net m =
             bAnd $ map checkTransitionEquation $ places net
         where checkTransitionEquation p =
-                let incoming = map addPlace $ lpre net p
-                    outgoing = map addPlace $ lpost net p
+                let incoming = map addTransition $ lpre net p
+                    outgoing = map addTransition $ lpost net p
                 in  sum outgoing - sum incoming .>= 0
-              addPlace (t,w) = literal w * (m M.! t)
+              addTransition (t,w) = literal w * (m M.! t)
 
-nonnegativityConstraints :: PetriNet -> ModelSI -> SBool
-nonnegativityConstraints net m =
-            bAnd $ map checkT $ transitions net
-        where checkT t = (m M.! t) .>= 0
+finalInvariantConstraints :: ModelSI -> SBool
+finalInvariantConstraints m = sum (M.elems m) .> 0
+
+nonnegativityConstraints :: ModelSI -> SBool
+nonnegativityConstraints m = bAnd $ map (.>= 0) $ M.elems m
 
 checkTransitionInvariant :: PetriNet -> Formula -> ModelSI -> SBool
 checkTransitionInvariant net f m =
         tInvariantConstraints net m &&&
-        nonnegativityConstraints net m &&&
+        nonnegativityConstraints m &&&
+        finalInvariantConstraints m &&&
         evaluateFormula f m
 
 checkTransitionInvariantSat :: PetriNet -> Formula -> ([String], ModelSI -> SBool)
 checkTransitionInvariantSat net f =
         (transitions net, checkTransitionInvariant net f)
+
+firedTransitionsFromAssignment :: ModelI -> [String]
+firedTransitionsFromAssignment a = M.keys $ M.filter ( > 0) a