added basis for checking reachability of a terminal marking

src/Main.hs

@@ -26,6 +26,7 @@ import qualified Printer.SPEC as SPECPrinter
 import qualified Printer.DOT as DOTPrinter
 import Property
 import Structure
+import StructuralComputation
 import Solver
 import Solver.StateEquation
 import Solver.TrapConstraints
@@ -39,6 +40,7 @@ import Solver.SComponent
 import Solver.Simplifier
 import Solver.UniqueTerminalMarking
 import Solver.NonConsensusState
+import Solver.TerminalMarkingReachable
 --import Solver.Interpolant
 --import Solver.CommFreeReachability
 
@@ -220,6 +222,8 @@ makeImplicitProperty _ UniqueTerminalMarking =
         Property "unique terminal marking" $ Constraint UniqueTerminalMarkingConstraint
 makeImplicitProperty _ NonConsensusState =
         Property "non-consensus state" $ Constraint NonConsensusStateConstraint
+makeImplicitProperty _ TerminalMarkingReachable =
+        Property "terminal marking reachable" $ Constraint TerminalMarkingReachableConstraint
 
 checkProperty :: PetriNet -> Property -> OptIO PropResult
 checkProperty net p = do
@@ -448,6 +452,7 @@ checkConstraintProperty net cp =
         case cp of
             UniqueTerminalMarkingConstraint -> checkUniqueTerminalMarkingProperty net
             NonConsensusStateConstraint -> checkNonConsensusStateProperty net
+            TerminalMarkingReachableConstraint -> checkTerminalMarkingReachableProperty net
 
 checkUniqueTerminalMarkingProperty :: PetriNet -> OptIO PropResult
 checkUniqueTerminalMarkingProperty net = do
@@ -523,6 +528,32 @@ refineNonConsensusStateProperty net traps siphons c@(m0, m, x) = do
             Just trap ->
                 checkNonConsensusStateProperty' net (trap:traps) siphons
 
+checkTerminalMarkingReachableProperty :: PetriNet -> OptIO PropResult
+checkTerminalMarkingReachableProperty net = do
+        let triplets = generateTriplets net
+        let trivialTriplets = filter trivialTriplet triplets
+        let nonTrivialTriplets = filter (not . trivialTriplet) triplets
+        let emptyTriplets = filter emptyTriplet triplets
+        let nonTrivialNonEmptyTriplets = filter (not . emptyTriplet) nonTrivialTriplets
+        liftIO $ putStrLn $ "All triplets (" ++ show (length triplets) ++ "):"
+        liftIO $ putStrLn $ unlines $ map show triplets
+        liftIO $ putStrLn $ "Trivial triplets (" ++ show (length trivialTriplets) ++ "):"
+        liftIO $ putStrLn $ unlines $ map show trivialTriplets
+        liftIO $ putStrLn $ "Empty triplets (" ++ show (length emptyTriplets) ++ "):"
+        liftIO $ putStrLn $ unlines $ map show emptyTriplets
+        liftIO $ putStrLn $ "Non-trivial, non-empty triplets (" ++ show (length nonTrivialNonEmptyTriplets) ++ "):"
+        liftIO $ putStrLn $ unlines $ map show nonTrivialNonEmptyTriplets
+        return Satisfied
+        r <- checkSat $ checkTerminalMarkingReachableSat net nonTrivialTriplets 2
+        case r of
+            Nothing -> return Unknown
+            Just inv -> do
+                invariant <- opt optInvariant
+                if invariant then
+                    printInvariant (Just inv, [])
+                else
+                    return Satisfied
+
 main :: IO ()
 main = do
         putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"

src/Options.hs

@@ -33,6 +33,7 @@ data ImplicitProperty = Termination
                       | StructCommunicationFree
                       | UniqueTerminalMarking
                       | NonConsensusState
+                      | TerminalMarkingReachable
                       deriving (Show,Read)
 
 data RefinementType = TrapRefinement | SComponentRefinement | SComponentWithCutRefinement
@@ -191,6 +192,12 @@ options =
                }))
         "Prove that no non-consensus terminal state is reachable from an initial marking"
 
+        , Option "" ["terminal-marking-reachable"]
+        (NoArg (\opt -> Right opt {
+                   optProperties = TerminalMarkingReachable : optProperties opt
+               }))
+        "Prove that a terminal marking is reachable"
+
         , Option "i" ["invariant"]
         (NoArg (\opt -> Right opt { optInvariant = True }))
         "Generate an invariant"

src/Property.hs

@@ -94,10 +94,12 @@ data PropertyType = SafetyType
 
 data ConstraintProperty = UniqueTerminalMarkingConstraint
                         | NonConsensusStateConstraint
+                        | TerminalMarkingReachableConstraint
 
 instance Show ConstraintProperty where
         show UniqueTerminalMarkingConstraint = "unique terminal marking"
         show NonConsensusStateConstraint = "non-consensus state"
+        show TerminalMarkingReachableConstraint = "terminal marking reachable"
 
 data PropertyContent = Safety (Formula Place)
                   | Liveness (Formula Transition)

src/Solver/TerminalMarkingReachable.hs

+{-# LANGUAGE FlexibleContexts #-}
+
+module Solver.TerminalMarkingReachable
+    (checkTerminalMarkingReachableSat,
+     TerminalMarkingReachableInvariant)
+where
+
+import Data.SBV
+import Data.List (intercalate)
+import qualified Data.Map as M
+
+import Util
+import PetriNet
+import Property
+import Solver
+import StructuralComputation
+
+type TerminalMarkingReachableInvariant = [BlockInvariant]
+data BlockInvariant =
+            BlockInvariant (Int, [Transition], IVector Place)
+
+instance Invariant BlockInvariant where
+        invariantSize (BlockInvariant (_, _, yi)) = size yi
+
+instance Show BlockInvariant where
+        show (BlockInvariant (i, ti, yi)) =
+                "T_" ++ show i ++ ": " ++ show ti ++ "; " ++ intercalate " + " (map showWeighted (items yi))
+
+nonNegativityConstraints :: (Ord a, Show a) => SIMap a -> SBool
+nonNegativityConstraints m =
+            bAnd $ map checkVal $ vals m
+        where checkVal x = x .>= 0
+
+checkTerminalMarkingReachable :: PetriNet -> [Triplet] -> Int -> [SIMap Place] -> SIMap Transition -> SBool
+checkTerminalMarkingReachable net triplets k ys b =
+        bAnd (map nonNegativityConstraints ys)
+        -- farkas lemma constraints
+        -- triplet constraints
+        -- block constraints
+
+checkTerminalMarkingReachableSat :: PetriNet -> [Triplet] -> Int -> ConstraintProblem Integer TerminalMarkingReachableInvariant
+checkTerminalMarkingReachableSat net triplets k =
+        let makeYName i = (++) (replicate i '\'')
+            ys = [makeVarMapWith (makeYName i) $ places net | i <- [1..k]]
+            b = makeVarMap $ transitions net
+        in  ("terminal marking reachable", "invariant",
+             concat (map getNames ys) ++ getNames b,
+             \fm -> checkTerminalMarkingReachable net triplets k (map (fmap fm) ys) (fmap fm b),
+             \fm -> invariantFromAssignment (map (fmap fm) ys) (fmap fm b))
+
+invariantFromAssignment :: [IMap Place] -> IMap Transition -> TerminalMarkingReachableInvariant
+invariantFromAssignment ys b = [BlockInvariant (1, [], buildVector [])]

src/StructuralComputation.hs

+module StructuralComputation
+    (Triplet
+    ,generateTriplets
+    ,trivialTriplet
+    ,emptyTriplet)
+where
+
+import PetriNet
+import qualified Data.Map as M
+
+type Triplet = (Transition, Transition, [Transition])
+
+generateTriplets :: PetriNet -> [Triplet]
+generateTriplets net =
+        let
+            prePostMultiset t =
+                let
+                    (pre, post) = context net t
+                in
+                    (M.fromList pre, M.fromList post)
+            prePostMultisets = M.fromList $ [(t, prePostMultiset t) | t <- transitions net]
+            multiSetDifference a b = if a > b then Just (a - b) else Nothing
+            findT' s t =
+                let
+                    (sPre, sPost) = prePostMultisets M.! s
+                    (tPre, tPost) = prePostMultisets M.! t
+                    stSet = M.unionWith (+) sPre (M.differenceWith multiSetDifference tPre sPost)
+                in
+                    [t' | t' <- transitions net, t' /= s, checkTriple stSet t']
+            checkTriple stMultiset t' =
+                let
+                    (tPre, _) = prePostMultisets M.! t'
+                    differenceMultiset = M.differenceWith multiSetDifference tPre stMultiset
+                in
+                    M.null differenceMultiset
+        in
+            [(s, t, findT' s t) | s <- transitions net, t <- transitions net, s /= t]
+
+trivialTriplet :: Triplet -> Bool
+trivialTriplet (_, t, ts) = elem t ts
+
+emptyTriplet :: Triplet -> Bool
+emptyTriplet (_, _, ts) = null ts