changed unique terminal marking to terminal markings have a unique consensus

src/Main.hs

@@ -38,7 +38,7 @@ import Solver.SafetyInvariant
 import Solver.SComponentWithCut
 import Solver.SComponent
 import Solver.Simplifier
-import Solver.UniqueTerminalMarking
+import Solver.TerminalMarkingsUniqueConsensus
 import Solver.NonConsensusState
 import Solver.TerminalMarkingReachable
 --import Solver.Interpolant
@@ -218,8 +218,8 @@ makeImplicitProperty _ StructFinalPlace =
         Property "final place" $ Structural FinalPlace
 makeImplicitProperty _ StructCommunicationFree =
         Property "communication free" $ Structural CommunicationFree
-makeImplicitProperty _ UniqueTerminalMarking =
-        Property "unique terminal marking" $ Constraint UniqueTerminalMarkingConstraint
+makeImplicitProperty _ TerminalMarkingsUniqueConsensus =
+        Property "terminal markings have a unique consensus" $ Constraint TerminalMarkingsUniqueConsensusConstraint
 makeImplicitProperty _ NonConsensusState =
         Property "non-consensus state" $ Constraint NonConsensusStateConstraint
 makeImplicitProperty _ TerminalMarkingReachable =
@@ -450,46 +450,46 @@ checkStructuralProperty net struct =
 checkConstraintProperty :: PetriNet -> ConstraintProperty -> OptIO PropResult
 checkConstraintProperty net cp =
         case cp of
-            UniqueTerminalMarkingConstraint -> checkUniqueTerminalMarkingProperty net
+            TerminalMarkingsUniqueConsensusConstraint -> checkTerminalMarkingsUniqueConsensusProperty net
             NonConsensusStateConstraint -> checkNonConsensusStateProperty net
             TerminalMarkingReachableConstraint -> checkTerminalMarkingReachableProperty net
 
-checkUniqueTerminalMarkingProperty :: PetriNet -> OptIO PropResult
-checkUniqueTerminalMarkingProperty net = do
-        r <- checkUniqueTerminalMarkingProperty' net (fixedTraps net) (fixedSiphons net)
+checkTerminalMarkingsUniqueConsensusProperty :: PetriNet -> OptIO PropResult
+checkTerminalMarkingsUniqueConsensusProperty net = do
+        r <- checkTerminalMarkingsUniqueConsensusProperty' net (fixedTraps net) (fixedSiphons net)
         case r of
             (Nothing, _, _) -> return Satisfied
             (Just _, _, _) -> return Unknown
 
-checkUniqueTerminalMarkingProperty' :: PetriNet ->
+checkTerminalMarkingsUniqueConsensusProperty' :: PetriNet ->
         [Trap] -> [Siphon] ->
-        OptIO (Maybe UniqueTerminalMarkingCounterExample, [Trap], [Siphon])
-checkUniqueTerminalMarkingProperty' net traps siphons = do
-        r <- checkSat $ checkUniqueTerminalMarkingSat net traps siphons
+        OptIO (Maybe TerminalMarkingsUniqueConsensusCounterExample, [Trap], [Siphon])
+checkTerminalMarkingsUniqueConsensusProperty' net traps siphons = do
+        r <- checkSat $ checkTerminalMarkingsUniqueConsensusSat net traps siphons
         case r of
             Nothing -> return (Nothing, traps, siphons)
             Just c -> do
                 refine <- opt optRefinementType
                 if isJust refine then
-                    refineUniqueTerminalMarkingProperty net traps siphons c
+                    refineTerminalMarkingsUniqueConsensusProperty net traps siphons c
                 else
                     return (Just c, traps, siphons)
 
-refineUniqueTerminalMarkingProperty :: PetriNet ->
-        [Trap] -> [Siphon] -> UniqueTerminalMarkingCounterExample ->
-        OptIO (Maybe UniqueTerminalMarkingCounterExample, [Trap], [Siphon])
-refineUniqueTerminalMarkingProperty net traps siphons c@(m0, m1, m2, x1, x2) = do
-        r1 <- checkSatMin $ Solver.UniqueTerminalMarking.checkUnmarkedTrapSat net m0 m1 m2 x1 x2
+refineTerminalMarkingsUniqueConsensusProperty :: PetriNet ->
+        [Trap] -> [Siphon] -> TerminalMarkingsUniqueConsensusCounterExample ->
+        OptIO (Maybe TerminalMarkingsUniqueConsensusCounterExample, [Trap], [Siphon])
+refineTerminalMarkingsUniqueConsensusProperty net traps siphons c@(m0, m1, m2, x1, x2) = do
+        r1 <- checkSatMin $ Solver.TerminalMarkingsUniqueConsensus.checkUnmarkedTrapSat net m0 m1 m2 x1 x2
         case r1 of
             Nothing -> do
-                r2 <- checkSatMin $ Solver.UniqueTerminalMarking.checkUnmarkedSiphonSat net m0 m1 m2 x1 x2
+                r2 <- checkSatMin $ Solver.TerminalMarkingsUniqueConsensus.checkUnmarkedSiphonSat net m0 m1 m2 x1 x2
                 case r2 of
                     Nothing ->
                         return (Just c, traps, siphons)
                     Just siphon ->
-                        checkUniqueTerminalMarkingProperty' net traps (siphon:siphons)
+                        checkTerminalMarkingsUniqueConsensusProperty' net traps (siphon:siphons)
             Just trap ->
-                checkUniqueTerminalMarkingProperty' net (trap:traps) siphons
+                checkTerminalMarkingsUniqueConsensusProperty' net (trap:traps) siphons
 
 checkNonConsensusStateProperty :: PetriNet -> OptIO PropResult
 checkNonConsensusStateProperty net = do

src/Options.hs

@@ -31,7 +31,7 @@ data ImplicitProperty = Termination
                       | StructParallel
                       | StructFinalPlace
                       | StructCommunicationFree
-                      | UniqueTerminalMarking
+                      | TerminalMarkingsUniqueConsensus
                       | NonConsensusState
                       | TerminalMarkingReachable
                       deriving (Show,Read)
@@ -180,11 +180,11 @@ options =
                }))
         "Prove that the net is communication-free"
 
-        , Option "" ["unique-terminal-marking"]
+        , Option "" ["terminal-markings-unique-consensus"]
         (NoArg (\opt -> Right opt {
-                   optProperties = UniqueTerminalMarking : optProperties opt
+                   optProperties = TerminalMarkingsUniqueConsensus : optProperties opt
                }))
-        "Prove that all markings of the net have a unique terminal marking"
+        "Prove that terminal markings have a unique consensus"
 
         , Option "" ["non-consensus-state"]
         (NoArg (\opt -> Right opt {

src/Property.hs

@@ -92,12 +92,12 @@ data PropertyType = SafetyType
                   | StructuralType
                   | ConstraintType
 
-data ConstraintProperty = UniqueTerminalMarkingConstraint
+data ConstraintProperty = TerminalMarkingsUniqueConsensusConstraint
                         | NonConsensusStateConstraint
                         | TerminalMarkingReachableConstraint
 
 instance Show ConstraintProperty where
-        show UniqueTerminalMarkingConstraint = "unique terminal marking"
+        show TerminalMarkingsUniqueConsensusConstraint = "terminal markings have a unique consensus"
         show NonConsensusStateConstraint = "non-consensus state"
         show TerminalMarkingReachableConstraint = "terminal marking reachable"
 

src/Solver/UniqueTerminalMarking.hs → src/Solver/TerminalMarkingsUniqueConsensus.hs

 {-# LANGUAGE FlexibleContexts #-}
 
-module Solver.UniqueTerminalMarking
-    (checkUniqueTerminalMarkingSat,
-     UniqueTerminalMarkingCounterExample,
+module Solver.TerminalMarkingsUniqueConsensus
+    (checkTerminalMarkingsUniqueConsensusSat,
+     TerminalMarkingsUniqueConsensusCounterExample,
      checkUnmarkedTrapSat,
      checkUnmarkedSiphonSat)
 where
 
 import Data.SBV
 import qualified Data.Map as M
+import Data.List ((\\))
 
 import Util
 import PetriNet
 import Property
 import Solver
 
-type UniqueTerminalMarkingCounterExample = (Marking, Marking, Marking, FiringVector, FiringVector)
+type TerminalMarkingsUniqueConsensusCounterExample = (Marking, Marking, Marking, FiringVector, FiringVector)
 
 stateEquationConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Transition -> SBool
 stateEquationConstraints net m0 m x =
@@ -37,13 +38,14 @@ terminalConstraints net m =
         where checkTransition t = bOr $ map checkPlace $ lpre net t
               checkPlace (p,w) = val m p .<= literal (fromInteger (w - 1))
 
-nonEqualityConstraints :: (Ord a, Show a) => PetriNet -> SIMap a -> SIMap a -> SBool
-nonEqualityConstraints net m1 m2 =
-            if elemsSet m1 /= elemsSet m2 then
-                false
-            else
-                bOr $ map checkNonEquality $ elems m1
-        where checkNonEquality x = val m1 x ./= val m2 x
+initialMarkingConstraints :: PetriNet -> SIMap Place -> SBool
+initialMarkingConstraints net m0 =
+        sum (mval m0 (places net \\ initials net)) .== 0
+
+differentConsensusConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SBool
+differentConsensusConstraints net m1 m2 =
+        (sum (mval m1 (yesStates net)) .> 0 &&& sum (mval m2 (noStates net)) .> 0) |||
+        (sum (mval m1 (noStates net)) .> 0 &&& sum (mval m2 (yesStates net)) .> 0)
 
 checkTrap :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> Trap -> SBool
 checkTrap net m0 m1 m2 x1 x2 trap =
@@ -67,10 +69,11 @@ checkSiphonConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place
 checkSiphonConstraints net m0 m1 m2 x1 x2 siphons =
         bAnd $ map (checkSiphon net m0 m1 m2 x1 x2) siphons
 
-checkUniqueTerminalMarking :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition ->
+checkTerminalMarkingsUniqueConsensus :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition ->
         [Trap] -> [Siphon] -> SBool
-checkUniqueTerminalMarking net m0 m1 m2 x1 x2 traps siphons =
-        nonEqualityConstraints net m1 m2 &&&
+checkTerminalMarkingsUniqueConsensus net m0 m1 m2 x1 x2 traps siphons =
+        initialMarkingConstraints net m0 &&&
+        differentConsensusConstraints net m1 m2 &&&
         stateEquationConstraints net m0 m1 x1 &&&
         stateEquationConstraints net m0 m2 x2 &&&
         nonNegativityConstraints m0 &&&
@@ -83,8 +86,8 @@ checkUniqueTerminalMarking net m0 m1 m2 x1 x2 traps siphons =
         checkTrapConstraints net m0 m1 m2 x1 x2 traps &&&
         checkSiphonConstraints net m0 m1 m2 x1 x2 siphons
 
-checkUniqueTerminalMarkingSat :: PetriNet -> [Trap] -> [Siphon] -> ConstraintProblem Integer UniqueTerminalMarkingCounterExample
-checkUniqueTerminalMarkingSat net traps siphons =
+checkTerminalMarkingsUniqueConsensusSat :: PetriNet -> [Trap] -> [Siphon] -> ConstraintProblem Integer TerminalMarkingsUniqueConsensusCounterExample
+checkTerminalMarkingsUniqueConsensusSat net traps siphons =
         let m0 = makeVarMap $ places net
             m1 = makeVarMapWith prime $ places net
             m2 = makeVarMapWith (prime . prime) $ places net
@@ -92,10 +95,10 @@ checkUniqueTerminalMarkingSat net traps siphons =
             x2 = makeVarMapWith prime $ transitions net
         in  ("unique terminal marking", "(m0, m1, m2, x1, x2)",
              getNames m0 ++ getNames m1 ++ getNames m2 ++ getNames x1 ++ getNames x2,
-             \fm -> checkUniqueTerminalMarking net (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2) traps siphons,
+             \fm -> checkTerminalMarkingsUniqueConsensus net (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2) traps siphons,
              \fm -> markingsFromAssignment (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2))
 
-markingsFromAssignment :: IMap Place -> IMap Place -> IMap Place -> IMap Transition -> IMap Transition -> UniqueTerminalMarkingCounterExample
+markingsFromAssignment :: IMap Place -> IMap Place -> IMap Place -> IMap Transition -> IMap Transition -> TerminalMarkingsUniqueConsensusCounterExample
 markingsFromAssignment m0 m1 m2 x1 x2 =
         (makeVector m0, makeVector m1, makeVector m2, makeVector x1, makeVector x2)