Added option and basic solver for unique terminal marking

src/Main.hs

@@ -37,6 +37,7 @@ import Solver.SafetyInvariant
 import Solver.SComponentWithCut
 import Solver.SComponent
 import Solver.Simplifier
+import Solver.UniqueTerminalMarking
 --import Solver.Interpolant
 --import Solver.CommFreeReachability
 
@@ -214,6 +215,8 @@ makeImplicitProperty _ StructFinalPlace =
         Property "final place" $ Structural FinalPlace
 makeImplicitProperty _ StructCommunicationFree =
         Property "communication free" $ Structural CommunicationFree
+makeImplicitProperty _ UniqueTerminalMarking =
+        Property "unique terminal marking" $ Constraint UniqueTerminalMarkingConstraint
 
 checkProperty :: PetriNet -> Property -> OptIO PropResult
 checkProperty net p = do
@@ -223,6 +226,7 @@ checkProperty net p = do
             (Safety pf) -> checkSafetyProperty net pf
             (Liveness pf) -> checkLivenessProperty net pf
             (Structural ps) -> checkStructuralProperty net ps
+            (Constraint pc) -> checkConstraintProperty net pc
         verbosePut 0 $ showPropertyName p ++ " " ++
             case r of
                 Satisfied -> "is satisfied."
@@ -436,6 +440,15 @@ checkStructuralProperty net struct =
         else
             return Unsatisfied
 
+checkConstraintProperty :: PetriNet -> ConstraintProperty -> OptIO PropResult
+checkConstraintProperty net cp = do
+        let c = case cp of
+                 UniqueTerminalMarkingConstraint -> checkUniqueTerminalMarkingSat
+        r <- checkSat $ c net
+        case r of
+            Nothing -> return Satisfied
+            Just _ -> return Unknown
+
 main :: IO ()
 main = do
         putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"

src/Options.hs

@@ -31,6 +31,7 @@ data ImplicitProperty = Termination
                       | StructParallel
                       | StructFinalPlace
                       | StructCommunicationFree
+                      | UniqueTerminalMarking
                       deriving (Show,Read)
 
 data RefinementType = TrapRefinement | SComponentRefinement | SComponentWithCutRefinement
@@ -177,6 +178,12 @@ options =
                }))
         "Prove that the net is communication-free"
 
+        , Option "" ["unique-terminal-marking"]
+        (NoArg (\opt -> Right opt {
+                   optProperties = UniqueTerminalMarking : optProperties opt
+               }))
+        "Prove that all markings of the net have a unique terminal marking"
+
         , Option "i" ["invariant"]
         (NoArg (\opt -> Right opt { optInvariant = True }))
         "Generate an invariant"

src/Property.hs

@@ -6,6 +6,7 @@ module Property
      renameProperty,
      PropertyType(..),
      PropertyContent(..),
+     ConstraintProperty(..),
      Formula(..),
      Op(..),
      Term(..),
@@ -89,20 +90,30 @@ instance Functor Formula where
 data PropertyType = SafetyType
                   | LivenessType
                   | StructuralType
+                  | ConstraintType
+
+data ConstraintProperty = UniqueTerminalMarkingConstraint
 
 data PropertyContent = Safety (Formula Place)
                   | Liveness (Formula Transition)
                   | Structural Structure
+                  | Constraint ConstraintProperty
 
+-- TODO: use Show instance
 showPropertyType :: PropertyContent -> String
 showPropertyType (Safety _) = "safety"
 showPropertyType (Liveness _) = "liveness"
 showPropertyType (Structural _) = "structural"
+showPropertyType (Constraint _) = "constraint"
+
+showConstraintProperty :: ConstraintProperty -> String
+showConstraintProperty UniqueTerminalMarkingConstraint = "unique terminal marking"
 
 showPropertyContent :: PropertyContent -> String
 showPropertyContent (Safety f) = show f
 showPropertyContent (Liveness f) = show f
 showPropertyContent (Structural s) = show s
+showPropertyContent (Constraint c) = showConstraintProperty c
 
 data Property = Property {
         pname :: String,
@@ -119,7 +130,7 @@ renameProperty f (Property pn (Safety pf)) =
         Property pn (Safety (fmap (renamePlace f) pf))
 renameProperty f (Property pn (Liveness pf)) =
         Property pn (Liveness (fmap (renameTransition f) pf))
-renameProperty _ (Property pn (Structural pc)) = Property pn (Structural pc)
+renameProperty _ p = p
 
 showPropertyName :: Property -> String
 showPropertyName p = showPropertyType (pcont p) ++ " property" ++

src/Solver/UniqueTerminalMarking.hs

+module Solver.UniqueTerminalMarking
+    (checkUniqueTerminalMarkingSat)
+where
+
+import Data.SBV
+
+import Util
+import PetriNet
+import Property
+import Solver
+
+placeConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Transition -> SBool
+placeConstraints net m1 m2 x =
+            bAnd $ map checkPlaceEquation $ places net
+        where checkPlaceEquation p =
+                let incoming = map addTransition $ lpre net p
+                    outgoing = map addTransition $ lpost net p
+                in  val m1 p + sum incoming - sum outgoing .== val m2 p
+              addTransition (t,w) = literal w * val x t
+
+nonNegativityConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SBool
+nonNegativityConstraints net m1 m2 =
+            let m1nn = map (checkVal m1) $ places net
+                m2nn = map (checkVal m1) $ places net
+            in  bAnd m1nn &&& bAnd m2nn
+        where checkVal mapping n = val mapping n .>= 0
+
+checkUniqueTerminalMarking :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Transition -> SBool
+checkUniqueTerminalMarking net m1 m2 x =
+        placeConstraints net m1 m2 x &&&
+        nonNegativityConstraints net m1 m2
+
+checkUniqueTerminalMarkingSat :: PetriNet -> ConstraintProblem Integer (Marking, Marking)
+checkUniqueTerminalMarkingSat net =
+        let m1 = makeVarMap $ places net
+            m2 = makeVarMapWith prime $ places net
+            x  = makeVarMap $ transitions net
+        in  ("unique terminal marking", "pair of markings",
+             getNames m1 ++ getNames m2 ++ getNames x,
+             \fm -> checkUniqueTerminalMarking net (fmap fm m1) (fmap fm m2) (fmap fm x),
+             \fm -> markingsFromAssignment (fmap fm m1) (fmap fm m2))
+
+markingsFromAssignment :: IMap Place -> IMap Place -> (Marking, Marking)
+markingsFromAssignment m1 m2 = (makeVector m1, makeVector m2)
+