added u-trap refinement

src/Main.hs

@@ -452,45 +452,44 @@ checkConstraintProperty net cp =
 
 checkTerminalMarkingsUniqueConsensusProperty :: PetriNet -> OptIO PropResult
 checkTerminalMarkingsUniqueConsensusProperty net = do
-        r <- checkTerminalMarkingsUniqueConsensusProperty' net (fixedTraps net) (fixedSiphons net) []
+        r <- checkTerminalMarkingsUniqueConsensusProperty' net (fixedTraps net) [] (fixedSiphons net) []
         case r of
-            (Nothing, _, _, _) -> return Satisfied
-            (Just _, _, _, _) -> return Unknown
+            (Nothing, _, _, _, _) -> return Satisfied
+            (Just _, _, _, _, _) -> return Unknown
 
 checkTerminalMarkingsUniqueConsensusProperty' :: PetriNet ->
-        [Trap] -> [Siphon] -> [StableInequality] ->
-        OptIO (Maybe TerminalMarkingsUniqueConsensusCounterExample, [Trap], [Siphon], [StableInequality])
-checkTerminalMarkingsUniqueConsensusProperty' net traps siphons inequalities = do
-        r <- checkSat $ checkTerminalMarkingsUniqueConsensusSat net traps siphons inequalities
+        [Trap] -> [Trap] -> [Siphon] -> [StableInequality] ->
+        OptIO (Maybe TerminalMarkingsUniqueConsensusCounterExample, [Trap], [Trap], [Siphon], [StableInequality])
+checkTerminalMarkingsUniqueConsensusProperty' net traps utraps usiphons inequalities = do
+        r <- checkSat $ checkTerminalMarkingsUniqueConsensusSat net traps utraps usiphons inequalities
         case r of
-            Nothing -> return (Nothing, traps, siphons, inequalities)
+            Nothing -> return (Nothing, traps, utraps, usiphons, inequalities)
             Just c -> do
                 refine <- opt optRefinementType
                 if isJust refine then
-                    refineTerminalMarkingsUniqueConsensusProperty net traps siphons inequalities c
+                    refineTerminalMarkingsUniqueConsensusProperty net traps utraps usiphons inequalities c
                 else
-                    return (Just c, traps, siphons, inequalities)
+                    return (Just c, traps, utraps, usiphons, inequalities)
 
 refineTerminalMarkingsUniqueConsensusProperty :: PetriNet ->
-        [Trap] -> [Siphon] -> [StableInequality] -> TerminalMarkingsUniqueConsensusCounterExample ->
-        OptIO (Maybe TerminalMarkingsUniqueConsensusCounterExample, [Trap], [Siphon], [StableInequality])
-refineTerminalMarkingsUniqueConsensusProperty net traps siphons inequalities c@(m0, m1, m2, x1, x2) = do
-        r1 <- checkSatMin $ Solver.TerminalMarkingsUniqueConsensus.findUnmarkedTrapSat net m0 m1 m2 x1 x2
+        [Trap] -> [Trap] -> [Siphon] -> [StableInequality] -> TerminalMarkingsUniqueConsensusCounterExample ->
+        OptIO (Maybe TerminalMarkingsUniqueConsensusCounterExample, [Trap], [Trap], [Siphon], [StableInequality])
+refineTerminalMarkingsUniqueConsensusProperty net traps utraps usiphons inequalities c@(m0, m1, m2, x1, x2) = do
+        r1 <- checkSatMin $ Solver.TerminalMarkingsUniqueConsensus.findTrapConstraintsSat net m0 m1 m2
         case r1 of
             Nothing -> do
-                r2 <- checkSatMin $ Solver.TerminalMarkingsUniqueConsensus.findGeneralizedSiphonConstraintsSat net m0 m1 m2 x1 x2
+                r2 <- checkSatMin $ Solver.TerminalMarkingsUniqueConsensus.findUSiphonConstraintsSat net m0 m1 m2 x1 x2
                 case r2 of
                     Nothing -> do
-                        return (Just c, traps, siphons, inequalities)
---                        r3 <- checkSat $ Solver.TerminalMarkingsUniqueConsensus.checkGeneralizedCoTrapSat net m0 m1 m2 x1 x2
---                        case r3 of
---                            Nothing -> return (Just c, traps, siphons, inequalities)
---                            Just inequality ->
---                                checkTerminalMarkingsUniqueConsensusProperty' net traps siphons (inequality:inequalities)
-                    Just siphon ->
-                        checkTerminalMarkingsUniqueConsensusProperty' net traps (siphon:siphons) inequalities
+                        r3 <- checkSatMin $ Solver.TerminalMarkingsUniqueConsensus.findUTrapConstraintsSat net m0 m1 m2 x1 x2
+                        case r3 of
+                            Nothing -> return (Just c, traps, utraps, usiphons, inequalities)
+                            Just utrap ->
+                                checkTerminalMarkingsUniqueConsensusProperty' net traps (utrap:utraps) usiphons inequalities
+                    Just usiphon ->
+                        checkTerminalMarkingsUniqueConsensusProperty' net traps utraps (usiphon:usiphons) inequalities
             Just trap ->
-                checkTerminalMarkingsUniqueConsensusProperty' net (trap:traps) siphons inequalities
+                checkTerminalMarkingsUniqueConsensusProperty' net (trap:traps) utraps usiphons inequalities
 
 checkTerminalMarkingReachableProperty :: PetriNet -> OptIO PropResult
 checkTerminalMarkingReachableProperty net = do

src/Solver/TerminalMarkingsUniqueConsensus.hs

@@ -3,8 +3,9 @@
 module Solver.TerminalMarkingsUniqueConsensus
     (checkTerminalMarkingsUniqueConsensusSat,
      TerminalMarkingsUniqueConsensusCounterExample,
-     findUnmarkedTrapSat,
-     findGeneralizedSiphonConstraintsSat,
+     findTrapConstraintsSat,
+     findUTrapConstraintsSat,
+     findUSiphonConstraintsSat,
      checkGeneralizedCoTrapSat,
      StableInequality)
 where
@@ -50,26 +51,51 @@ differentConsensusConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SBool
 differentConsensusConstraints net m1 m2 =
         (sum (mval m1 (yesStates net)) .> 0 &&& sum (mval m2 (noStates net)) .> 0)
 
-checkTrap :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> Trap -> SBool
-checkTrap net m0 m1 m2 x1 x2 trap =
+unmarkedByMarking :: [Place] -> SIMap Place -> SBool
+unmarkedByMarking r m = sum (mval m r) .== 0
+
+markedByMarking :: [Place] -> SIMap Place -> SBool
+markedByMarking r m = sum (mval m r) .> 0
+
+sequenceNotIn :: [Transition] -> SIMap Transition -> SBool
+sequenceNotIn u x = sum (mval x u) .== 0
+
+sequenceIn :: [Transition] -> SIMap Transition -> SBool
+sequenceIn u x = sum (mval x u) .> 0
+
+checkTrap :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> Trap -> SBool
+checkTrap net m0 m1 m2 trap =
             (markedByMarking m0 ==> (markedByMarking m1 &&& markedByMarking m2))
         where markedByMarking m = sum (mval m trap) .> 0
               markedBySequence x = sum (mval x (mpre net trap)) .> 0
 
-checkTrapConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> [Trap] -> SBool
-checkTrapConstraints net m0 m1 m2 x1 x2 traps =
-        bAnd $ map (checkTrap net m0 m1 m2 x1 x2) traps
-
-checkGeneralizedSiphon :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> Siphon -> SBool
-checkGeneralizedSiphon net m0 m1 m2 x1 x2 siphon =
-            ((unmarkedByMarking m0 &&& unmarkedBySequence x1) ==> (unmarkedByMarking m1)) &&&
-            ((unmarkedByMarking m0 &&& unmarkedBySequence x2) ==> (unmarkedByMarking m2))
-        where unmarkedByMarking m = sum (mval m siphon) .== 0
-              unmarkedBySequence x = sum [ val x t | t <- (mpre net siphon \\ mpost net siphon) ] .== 0
-
-checkGeneralizedSiphonConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> [Siphon] -> SBool
-checkGeneralizedSiphonConstraints net m0 m1 m2 x1 x2 siphons =
-        bAnd $ map (checkGeneralizedSiphon net m0 m1 m2 x1 x2) siphons
+checkTrapConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> [Trap] -> SBool
+checkTrapConstraints net m0 m1 m2 traps =
+        bAnd $ map (checkTrap net m0 m1 m2) traps
+
+checkUTrap :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> Trap -> SBool
+checkUTrap net m0 m1 m2 x1 x2 utrap =
+            ((unmarkedByMarking utrap m0) ||| (
+                ((sequenceIn u x1) ||| (markedByMarking utrap m1)) &&&
+                ((sequenceIn u x2) ||| (markedByMarking utrap m2))
+            ))
+        where u = (mpost net utrap \\ mpre net utrap)
+
+checkUTrapConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> [Trap] -> SBool
+checkUTrapConstraints net m0 m1 m2 x1 x2 traps =
+        bAnd $ map (checkUTrap net m0 m1 m2 x1 x2) traps
+
+checkUSiphon :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> Siphon -> SBool
+checkUSiphon net m0 m1 m2 x1 x2 usiphon =
+            ((markedByMarking usiphon m0) ||| (
+                ((sequenceIn u x1) ||| (unmarkedByMarking usiphon m1)) &&&
+                ((sequenceIn u x2) ||| (unmarkedByMarking usiphon m2))
+            ))
+        where u = (mpre net usiphon \\ mpost net usiphon)
+
+checkUSiphonConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> [Siphon] -> SBool
+checkUSiphonConstraints net m0 m1 m2 x1 x2 siphons =
+        bAnd $ map (checkUSiphon net m0 m1 m2 x1 x2) siphons
 
 checkInequalityConstraint :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> StableInequality -> SBool
 checkInequalityConstraint net m0 m1 m2 (k, c) =
@@ -81,8 +107,8 @@ checkInequalityConstraints net m0 m1 m2 inequalities =
         bAnd [ checkInequalityConstraint net m0 m1 m2 i | i <- inequalities ]
 
 checkTerminalMarkingsUniqueConsensus :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition ->
-        [Trap] -> [Siphon] -> [StableInequality] -> SBool
-checkTerminalMarkingsUniqueConsensus net m0 m1 m2 x1 x2 traps siphons inequalities =
+        [Trap] -> [Trap] -> [Siphon] -> [StableInequality] -> SBool
+checkTerminalMarkingsUniqueConsensus net m0 m1 m2 x1 x2 traps utraps usiphons inequalities =
         stateEquationConstraints net m0 m1 x1 &&&
         stateEquationConstraints net m0 m2 x2 &&&
         initialMarkingConstraints net m0 &&&
@@ -94,12 +120,13 @@ checkTerminalMarkingsUniqueConsensus net m0 m1 m2 x1 x2 traps siphons inequaliti
         terminalConstraints net m1 &&&
         terminalConstraints net m2 &&&
         differentConsensusConstraints net m1 m2 &&&
-        checkTrapConstraints net m0 m1 m2 x1 x2 traps &&&
-        checkGeneralizedSiphonConstraints net m0 m1 m2 x1 x2 siphons &&&
+        checkTrapConstraints net m0 m1 m2 traps &&&
+        checkUTrapConstraints net m0 m1 m2 x1 x2 utraps &&&
+        checkUSiphonConstraints net m0 m1 m2 x1 x2 usiphons &&&
         checkInequalityConstraints net m0 m1 m2 inequalities
 
-checkTerminalMarkingsUniqueConsensusSat :: PetriNet -> [Trap] -> [Siphon] -> [StableInequality] -> ConstraintProblem Integer TerminalMarkingsUniqueConsensusCounterExample
-checkTerminalMarkingsUniqueConsensusSat net traps siphons inequalities =
+checkTerminalMarkingsUniqueConsensusSat :: PetriNet -> [Trap] -> [Trap] -> [Siphon] -> [StableInequality] -> ConstraintProblem Integer TerminalMarkingsUniqueConsensusCounterExample
+checkTerminalMarkingsUniqueConsensusSat net traps utraps usiphons inequalities =
         let m0 = makeVarMap $ places net
             m1 = makeVarMapWith prime $ places net
             m2 = makeVarMapWith (prime . prime) $ places net
@@ -107,7 +134,7 @@ checkTerminalMarkingsUniqueConsensusSat net traps siphons inequalities =
             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 -> checkTerminalMarkingsUniqueConsensus net (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2) traps siphons inequalities,
+             \fm -> checkTerminalMarkingsUniqueConsensus net (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2) traps utraps usiphons inequalities,
              \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 -> TerminalMarkingsUniqueConsensusCounterExample
@@ -116,17 +143,25 @@ markingsFromAssignment m0 m1 m2 x1 x2 =
 
 -- trap and siphon refinement constraints
 
-generalizedSiphonConstraints :: PetriNet -> FiringVector -> SIMap Place -> SBool
-generalizedSiphonConstraints net x b =
-            bAnd [ siphonConstraint t | t <- elems x ]
-        where siphonConstraint t =
-                sum (mval b $ post net t) .> 0 ==> sum (mval b $ pre net t) .> 0
+trapConstraint :: PetriNet -> SIMap Place -> Transition -> SBool
+trapConstraint net b t =
+        sum (mval b $ pre net t) .> 0 ==> sum (mval b $ post net t) .> 0
+
+siphonConstraint :: PetriNet -> SIMap Place -> Transition -> SBool
+siphonConstraint net b t =
+        sum (mval b $ post net t) .> 0 ==> sum (mval b $ pre net t) .> 0
 
 trapConstraints :: PetriNet -> SIMap Place -> SBool
 trapConstraints net b =
-            bAnd $ map trapConstraint $ transitions net
-        where trapConstraint t =
-                  sum (mval b $ pre net t) .> 0 ==> sum (mval b $ post net t) .> 0
+        bAnd $ map (trapConstraint net b) $ transitions net
+
+uTrapConstraints :: PetriNet -> FiringVector -> SIMap Place -> SBool
+uTrapConstraints net x b =
+        bAnd $ map (trapConstraint net b) $ elems x
+
+uSiphonConstraints :: PetriNet -> FiringVector -> SIMap Place -> SBool
+uSiphonConstraints net x b =
+        bAnd $ map (siphonConstraint net b) $ elems x
 
 placesMarkedByMarking :: PetriNet -> Marking -> SIMap Place -> SBool
 placesMarkedByMarking net m b = sum (mval b $ elems m) .> 0
@@ -165,40 +200,59 @@ minimizeMethod 1 curSize = "size smaller than " ++ show curSize
 minimizeMethod 2 curSize = "size larger than " ++ show curSize
 minimizeMethod _ _ = error "minimization method not supported"
 
-findUnmarkedTrap :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> SIMap Place -> Maybe (Int, Integer) -> SBool
-findUnmarkedTrap net m0 m1 m2 x1 x2 b sizeLimit =
+findTrap :: PetriNet -> Marking -> Marking -> Marking -> SIMap Place -> Maybe (Int, Integer) -> SBool
+findTrap net m0 m1 m2 b sizeLimit =
         placesMarkedByMarking net m0 b &&&
         checkSizeLimit b sizeLimit &&&
         checkBinary b &&&
         trapConstraints net b &&&
         ((placesUnmarkedByMarking net m1 b ||| placesUnmarkedByMarking net m2 b))
 
-findUnmarkedTrapSat :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> MinConstraintProblem Integer Trap Integer
-findUnmarkedTrapSat net m0 m1 m2 x1 x2 =
+findTrapConstraintsSat :: PetriNet -> Marking -> Marking -> Marking -> MinConstraintProblem Integer Trap Integer
+findTrapConstraintsSat net m0 m1 m2 =
+        let b = makeVarMap $ places net
+        in  (minimizeMethod, \sizeLimit ->
+            ("trap marked in m0 and unmarked in m1 or m2", "trap",
+             getNames b,
+             \fm -> findTrap net m0 m1 m2 (fmap fm b) sizeLimit,
+             \fm -> placesFromAssignment (fmap fm b)))
+
+findUTrapConstraints :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> SIMap Place -> Maybe (Int, Integer) -> SBool
+findUTrapConstraints net m0 m1 m2 x1 x2 b sizeLimit =
+        placesMarkedByMarking net m0 b &&&
+        checkSizeLimit b sizeLimit &&&
+        checkBinary b &&&
+        (
+            (uTrapConstraints net x1 b &&& placesUnmarkedByMarking net m1 b) |||
+            (uTrapConstraints net x2 b &&& placesUnmarkedByMarking net m2 b)
+        )
+
+findUTrapConstraintsSat :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> MinConstraintProblem Integer Trap Integer
+findUTrapConstraintsSat net m0 m1 m2 x1 x2 =
         let b = makeVarMap $ places net
         in  (minimizeMethod, \sizeLimit ->
-            ("trap marked in m and unmarked in m1 or m2, or marked by x1 and unmarked in m1, or marked by x2 and unmarked in m2", "trap",
+            ("u-trap (w.r.t. x1 or x2) marked in m0 and not marked in m1 or m2", "u-trap",
              getNames b,
-             \fm -> findUnmarkedTrap net m0 m1 m2 x1 x2 (fmap fm b) sizeLimit,
+             \fm -> findUTrapConstraints net m0 m1 m2 x1 x2 (fmap fm b) sizeLimit,
              \fm -> placesFromAssignment (fmap fm b)))
 
-findGeneralizedSiphonConstraints :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> SIMap Place -> Maybe (Int, Integer) -> SBool
-findGeneralizedSiphonConstraints net m0 m1 m2 x1 x2 b sizeLimit =
+findUSiphonConstraints :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> SIMap Place -> Maybe (Int, Integer) -> SBool
+findUSiphonConstraints net m0 m1 m2 x1 x2 b sizeLimit =
         placesUnmarkedByMarking net m0 b &&&
         checkSizeLimit b sizeLimit &&&
         checkBinary b &&&
         (
-            (generalizedSiphonConstraints net x1 b &&& placesMarkedByMarking net m1 b) |||
-            (generalizedSiphonConstraints net x2 b &&& placesMarkedByMarking net m2 b)
+            (uSiphonConstraints net x1 b &&& placesMarkedByMarking net m1 b) |||
+            (uSiphonConstraints net x2 b &&& placesMarkedByMarking net m2 b)
         )
 
-findGeneralizedSiphonConstraintsSat :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> MinConstraintProblem Integer Siphon Integer
-findGeneralizedSiphonConstraintsSat net m0 m1 m2 x1 x2 =
+findUSiphonConstraintsSat :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> MinConstraintProblem Integer Siphon Integer
+findUSiphonConstraintsSat net m0 m1 m2 x1 x2 =
         let b = makeVarMap $ places net
         in  (minimizeMethod, \sizeLimit ->
-            ("siphon (w.r.t. x1 or x2) not marked in m0 and marked in m1 or m2", "siphon",
+            ("u-siphon (w.r.t. x1 or x2) not marked in m0 and marked in m1 or m2", "u-siphon",
              getNames b,
-             \fm -> findGeneralizedSiphonConstraints net m0 m1 m2 x1 x2 (fmap fm b) sizeLimit,
+             \fm -> findUSiphonConstraints net m0 m1 m2 x1 x2 (fmap fm b) sizeLimit,
              \fm -> placesFromAssignment (fmap fm b)))
 
 placesFromAssignment :: IMap Place -> ([Place], Integer)