Added method and option for boolean transition invariant

src/Main.hs

@@ -30,6 +30,7 @@ import Solver
 import Solver.StateEquation
 import Solver.TrapConstraints
 import Solver.TransitionInvariant
+import Solver.BooleanTransitionInvariant
 import Solver.SubnetEmptyTrap
 import Solver.LivenessInvariant
 import Solver.SafetyInvariant
@@ -347,7 +348,10 @@ getLivenessInvariant net f cuts = do
 checkLivenessProperty' :: PetriNet ->
         Formula Transition -> [Cut] -> OptIO (Maybe FiringVector, [Cut])
 checkLivenessProperty' net f cuts = do
-        r <- checkSat $ checkTransitionInvariantSat net f cuts
+        boolConst <- opt optBoolConst
+        r <- if boolConst
+                then checkSat $ checkBooleanTransitionInvariantSat net f cuts
+                else checkSat $ checkTransitionInvariantSat net f cuts
         case r of
             Nothing -> return (Nothing, cuts)
             Just x -> do

src/Options.hs

@@ -47,6 +47,7 @@ data Options = Options { inputFormat :: InputFormat
                        , optMinimizeRefinement :: Int
                        , optAuto :: Bool
                        , optInvariant :: Bool
+                       , optBoolConst :: Bool
                        , optOutput :: Maybe String
                        , outputFormat :: OutputFormat
                        , optUseProperties :: Bool
@@ -65,6 +66,7 @@ startOptions = Options { inputFormat = PNET
                        , optMinimizeRefinement = 0
                        , optAuto = False
                        , optInvariant = False
+                       , optBoolConst = False
                        , optOutput = Nothing
                        , outputFormat = OutLOLA
                        , optUseProperties = True
@@ -179,6 +181,11 @@ options =
         (NoArg (\opt -> Right opt { optInvariant = True }))
         "Generate an invariant"
 
+        , Option "" ["bool-const"]
+        (NoArg (\opt -> Right opt { optBoolConst = True }))
+        ("Use boolean constraints instead of integer ones\n" ++
+         "  for transition invariant")
+
         , Option "r" ["refinement"]
         (ReqArg (\arg opt -> case reads arg :: [(Int, String)] of
                     [(0, "")] -> Right opt { optRefinementType = Nothing }

src/Solver/BooleanTransitionInvariant.hs

+module Solver.BooleanTransitionInvariant
+    (checkBooleanTransitionInvariantSat
+    ,checkBooleanTransitionInvariantWithSimpleCutSat)
+where
+
+import Data.SBV
+import Data.List
+import qualified Data.Map as M
+import qualified Data.Set as S
+
+import Util
+import PetriNet
+import Property
+import Solver
+import Solver.Simplifier
+
+tInvariantConstraints :: PetriNet -> SBMap Transition -> SBool
+tInvariantConstraints net x =
+            bAnd $ map checkTransitionEquation $ places net
+        where checkTransitionEquation p =
+                  let incoming = map (val x) $ pre net p \\ post net p
+                      outgoing = map (val x) $ post net p \\ pre net p
+                  in  bOr outgoing ==> bOr incoming
+
+finalInvariantConstraints :: SBMap Transition -> SBool
+finalInvariantConstraints x = bOr $ vals x
+
+transitionVectorConstraints :: PetriNet -> SBMap Transition -> SBool
+transitionVectorConstraints net x =
+        finalInvariantConstraints x &&&
+        tInvariantConstraints net x
+
+formulaAndRefinementConstraints :: SimpleCut -> [Cut] -> SBMap Transition -> SBool
+formulaAndRefinementConstraints fcut cuts x =
+        checkCuts cuts x &&&
+        checkSimpleCut fcut x
+
+checkSimpleCut :: SimpleCut -> SBMap Transition -> SBool
+checkSimpleCut (t0, cs) x =
+            checkNegative (S.toList t0) &&& bAnd (map (checkPositive . S.toList) cs)
+        where checkNegative ts = bAnd (map (bnot . val x) ts)
+              checkPositive ts = bOr (map (val x) ts)
+
+checkCuts :: [Cut] -> SBMap Transition -> SBool
+checkCuts cuts x = bAnd $ map checkCut cuts
+        where checkCut (ts, u) =
+                  let cPre = map (bOr . map (val x) . snd) ts
+                      cPost = map (val x) u
+                  in  bAnd cPre ==> bOr cPost
+
+checkBooleanTransitionInvariant :: PetriNet -> SimpleCut ->
+        [Cut] -> SBMap Transition -> SBool
+checkBooleanTransitionInvariant net fcut cuts x =
+        transitionVectorConstraints net x &&&
+        formulaAndRefinementConstraints fcut cuts x
+
+checkBooleanTransitionInvariantSat :: PetriNet -> Formula Transition -> [Cut] ->
+        ConstraintProblem Bool FiringVector
+checkBooleanTransitionInvariantSat net f cuts =
+        let x = makeVarMap $ transitions net
+            fcut = formulaToCut f
+        in  ("transition invariant constraints", "transition invariant",
+            getNames x,
+            \fm -> checkBooleanTransitionInvariant net fcut cuts (fmap fm x),
+            \fm -> firingVectorFromAssignment (fmap fm x))
+
+checkBooleanTransitionInvariantWithSimpleCut :: PetriNet -> SimpleCut ->
+        SimpleCut -> SBMap Transition -> SBool
+checkBooleanTransitionInvariantWithSimpleCut net fcut cut x =
+        transitionVectorConstraints net x &&&
+        checkSimpleCut fcut x &&&
+        checkSimpleCut cut x
+
+checkBooleanTransitionInvariantWithSimpleCutSat :: PetriNet -> Formula Transition -> SimpleCut ->
+        ConstraintProblem Bool FiringVector
+checkBooleanTransitionInvariantWithSimpleCutSat net f cut =
+        let x = makeVarMap $ transitions net
+            fcut = formulaToCut f
+        in  ("transition invariant constraints with simple cut", "transition invariant",
+            getNames x,
+            \fm -> checkBooleanTransitionInvariantWithSimpleCut net fcut cut (fmap fm x),
+            \fm -> firingVectorFromAssignment (fmap fm x))
+
+firingVectorFromAssignment :: BMap Transition -> FiringVector
+firingVectorFromAssignment x = makeVector $ M.map (const 1) $ M.filter id x
+

src/Solver/Simplifier.hs

 module Solver.Simplifier (
      checkSubsumptionSat
-    ,SimpleCut
     ,generateCuts
     ,greedySimplify
     ,formulaToCut