Added reachability decision procedure for communication-free nets

src/Main.hs

@@ -30,6 +30,7 @@ import Solver.StateEquation
 import Solver.TrapConstraints
 import Solver.TransitionInvariant
 import Solver.SComponent
+import Solver.CommFreeReachability
 
 data InputFormat = PNET | LOLA | TPN | MIST deriving (Show,Read)
 data OutputFormat = OutLOLA | OutSARA | OutSPEC | OutDOT deriving (Show,Read)
@@ -39,6 +40,7 @@ data NetTransformation = TerminationByReachability
 
 data ImplicitProperty = Termination
                       | DeadlockFree | DeadlockFreeUnlessFinal
+                      | FinalStateUnreachable
                       | ProperTermination
                       | Safe | Bounded Integer
                       | StructFreeChoice
@@ -133,6 +135,12 @@ options =
         ("Prove that the net is deadlock-free\n" ++
          "unless it is in the final marking")
 
+        , Option "" ["final-state-unreachable"]
+        (NoArg (\opt -> Right opt {
+                   optProperties = FinalStateUnreachable : optProperties opt
+               }))
+        "Prove that the final state is unreachable"
+
         , Option "" ["safe"]
         (NoArg (\opt -> Right opt {
                    optProperties = Safe : optProperties opt
@@ -316,8 +324,7 @@ placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w)
 transformNet :: (PetriNet, [Property]) -> NetTransformation ->
                (PetriNet, [Property])
 transformNet (net, props) TerminationByReachability =
-        let prime = ('\'':)
-            ps = ["'sigma", "'m1", "'m2"] ++
+        let ps = ["'sigma", "'m1", "'m2"] ++
                  places net ++ map prime (places net)
             is = [("'m1", 1)] ++
                  initials net ++ map (first prime) (initials net)
@@ -374,6 +381,11 @@ makeImplicitProperty net DeadlockFreeUnlessFinal =
             (foldl (:&:) FTrue  (map (\p -> placeOp Eq (p,0)) finals) :|:
              foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals)) :&:
             pf
+makeImplicitProperty net FinalStateUnreachable =
+        let (finals, nonfinals) = partition (null . lpost net) (places net)
+        in  Property "final state unreachable" $ Safety $
+             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) finals) :&:
+             foldl (:&:) FTrue (map (\p -> placeOp Eq (p,0)) nonfinals)
 makeImplicitProperty net (Bounded k) =
         Property (show k ++ "-bounded") $ Safety $
             foldl (:|:) FFalse
@@ -397,7 +409,7 @@ checkProperty verbosity net refine p = do
         verbosePut verbosity 1 $ "\nChecking " ++ showPropertyName p
         verbosePut verbosity 3 $ show p
         r <- case pcont p of
-            (Safety pf) -> checkSafetyProperty verbosity net refine pf []
+            (Safety pf) -> checkSafetyProperty verbosity net refine pf
             (Liveness pf) -> checkLivenessProperty verbosity net refine pf []
             (Structural ps) -> checkStructuralProperty verbosity net ps
         verbosePut verbosity 0 $ showPropertyName p ++ " " ++
@@ -408,8 +420,27 @@ checkProperty verbosity net refine p = do
         return r
 
 checkSafetyProperty :: Int -> PetriNet -> Bool ->
+        Formula -> IO PropResult
+checkSafetyProperty verbosity net refine f =
+        if checkCommunicationFree net then do
+            verbosePut verbosity 1 "Net found to be communication-free"
+            checkSafetyPropertyByCommFree verbosity net f
+        else
+            checkSafetyPropertyBySafetyRef verbosity net refine f []
+
+checkSafetyPropertyByCommFree :: Int -> PetriNet -> Formula -> IO PropResult
+checkSafetyPropertyByCommFree verbosity net f = do
+        r <- checkSat $ checkCommFreeReachabilitySat net f
+        case r of
+            Nothing -> return Satisfied
+            Just a -> do
+                verbosePut verbosity 1 "Assignment found"
+                verbosePut verbosity 3 $ "Assignment: " ++ show a
+                return Unsatisfied
+
+checkSafetyPropertyBySafetyRef :: Int -> PetriNet -> Bool ->
         Formula -> [[String]] -> IO PropResult
-checkSafetyProperty verbosity net refine f traps = do
+checkSafetyPropertyBySafetyRef verbosity net refine f traps = do
         r <- checkSat $ checkStateEquationSat net f traps
         case r of
             Nothing -> return Satisfied
@@ -431,8 +462,8 @@ checkSafetyProperty verbosity net refine f traps = do
                                                       show trap
                             verbosePut verbosity 3 $ "Trap assignment: " ++
                                                       show at
-                            checkSafetyProperty verbosity net refine f
-                                                (trap:traps)
+                            checkSafetyPropertyBySafetyRef verbosity net
+                                                refine f (trap:traps)
                 else
                     return Unknown
 

src/Solver.hs

 {-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
 
 module Solver
-    (checkSat,ModelSI,ModelSB,ModelI,ModelB,
+    (prime,checkSat,ModelSI,ModelSB,ModelI,ModelB,
      Model(..),mVal,mValues,mElemsWith,mElemSum,SModel(..),CModel(..))
 where
 
@@ -18,6 +18,9 @@ type ModelSB = Model SBool
 type ModelI = Model Integer
 type ModelB = Model Bool
 
+prime :: String -> String
+prime = ('\'':)
+
 mVal :: Model a -> String -> a
 mVal m x = M.findWithDefault (error ("key not found: " ++ x)) x (getMap m)
 

src/Solver/CommFreeReachability.hs

+module Solver.CommFreeReachability
+    (checkCommFreeReachability,checkCommFreeReachabilitySat)
+where
+
+import Data.SBV
+
+import PetriNet
+import Property
+import Solver
+import Solver.StateEquation
+import Debug.Trace
+
+checkSubnet :: PetriNet -> ModelSI -> SBool
+checkSubnet net m =
+            bAnd $ map checkPrePost $ transitions net
+        where checkPrePost t =
+                  let preCond = bAnd $ map checkNonNegativity $ pre net t
+                      postCond = bAnd $ map checkNonNegativity $ post net t
+                  in  mVal m t .> 0 ==> preCond &&& postCond
+              checkNonNegativity p = mVal m (prime p) .>= 0
+
+checkRoots :: PetriNet -> ModelSI -> SBool
+checkRoots net m =
+            bAnd $ map checkRoot $ places net
+        where checkRoot p =
+                  mVal m (prime p) .== 0 ==> fromBool (initial net p > 0)
+
+checkNodes :: PetriNet -> ModelSI -> SBool
+checkNodes net m =
+            bAnd $ map checkNode $ places net
+        where checkNode p =
+                      mVal m (prime p) .> 0 ==> bOr (map checkPreCond (pre net p))
+                  where checkPreCond t =
+                           trace ("checking '" ++ p ++ " > 0 => '" ++ p ++ " > '" ++ head (pre net t)
+                                  ++ " ^ " ++ t ++ " > 0")
+                           (mVal m (prime p) .>
+                              mVal m (prime (head (pre net t))) &&&
+                           mVal m t .> 0)
+
+checkMarkableSubnet :: PetriNet -> ModelSI -> SBool
+checkMarkableSubnet net m =
+        checkSubnet net m &&&
+        checkRoots net m &&&
+        checkNodes net m
+
+checkCommFreeReachability :: PetriNet -> Formula -> ModelSI -> SBool
+checkCommFreeReachability net f m =
+        checkStateEquation net f [] m &&&
+        checkMarkableSubnet net m
+
+checkCommFreeReachabilitySat :: PetriNet -> Formula ->
+        ([String], ModelSI -> SBool)
+checkCommFreeReachabilitySat net f =
+        (places net ++ transitions net ++ map prime (places net),
+         checkCommFreeReachability net f)

src/Solver/SComponent.hs

@@ -9,9 +9,6 @@ import Data.List (partition)
 import PetriNet
 import Solver
 
-prime :: String -> String
-prime = ('\'':)
-
 checkPrePostPlaces :: PetriNet -> ModelSI -> SBool
 checkPrePostPlaces net m =
             bAnd $ map checkPrePostPlace $ places net

src/Solver/StateEquation.hs

@@ -19,8 +19,11 @@ placeConstraints net m = bAnd $ map checkPlaceEquation $ places net
                 in  pinit + sum incoming - sum outgoing .== mVal m p
               addTransition (t,w) = literal w * mVal m t
 
-nonnegativityConstraints ::  ModelSI -> SBool
-nonnegativityConstraints m = bAnd $ map (.>= 0) $ mValues m
+nonNegativityConstraints :: PetriNet -> ModelSI -> SBool
+nonNegativityConstraints net m =
+            bAnd (map checkNonNegativity (places net)) &&&
+            bAnd (map checkNonNegativity (transitions net))
+        where checkNonNegativity x = mVal m x .>= 0
 
 checkTraps :: [[String]] -> ModelSI -> SBool
 checkTraps traps m = bAnd $ map checkTrapDelta traps
@@ -29,7 +32,7 @@ checkTraps traps m = bAnd $ map checkTrapDelta traps
 checkStateEquation :: PetriNet -> Formula -> [[String]] -> ModelSI -> SBool
 checkStateEquation net f traps m =
         placeConstraints net m &&&
-        nonnegativityConstraints m &&&
+        nonNegativityConstraints net m &&&
         checkTraps traps m &&&
         evaluateFormula f m
 

src/Structure.hs

 module Structure
     (Structure(..),
      checkStructure,
-     checkParallelT)
+     checkParallelT,
+     checkCommunicationFree)
 where
 
 import PetriNet
@@ -29,7 +30,10 @@ checkStructure net FinalPlace =
             length (filter finalPlace (places net)) == 1
         where finalPlace p = null (post net p) &&
                   all (\t -> length (post net t) == 1) (pre net p)
-checkStructure net CommunicationFree =
+checkStructure net CommunicationFree = checkCommunicationFree net
+
+checkCommunicationFree :: PetriNet -> Bool
+checkCommunicationFree net =
             all checkTransition (transitions net) &&
             all checkWeights (transitions net)
         where checkTransition t = length (pre net t) == 1