Added possibility to specify fixed traps and siphons

src/Main.hs

@@ -158,14 +158,14 @@ transformNet (net, props) TerminationByReachability =
                         [(t, (pre', post')), (primeTransition t, (pre'', post''))]
             ts = (switch, ([(m1,1)], [(m2,1)])) :
                  concatMap transformTransition (transitions net)
-            gs = ghostTransitions net
             prop = Property "termination by reachability" $ Safety $
                     foldl (:&:) (LinearInequation (Var sigma) Ge (Const 1))
                       (map (\p -> LinearInequation
                                 (Var (primePlace p) :-: Var p) Ge (Const 0))
                         (places net))
             -- TODO: map existing liveness properties
-        in  (makePetriNetWithTrans (name net) ps ts is gs, prop : props)
+        in  (makePetriNetWithTrans (name net) ps ts is
+                (ghostTransitions net) (fixedTraps net) (fixedSiphons net), prop : props)
 transformNet (net, props) ValidateIdentifiers =
         (renamePetriNetPlacesAndTransitions validateId net,
          map (renameProperty validateId) props)
@@ -237,7 +237,7 @@ checkProperty net p = do
 checkSafetyProperty :: PetriNet ->
         Formula Place -> OptIO PropResult
 checkSafetyProperty net f = do
-        r <- checkSafetyProperty' net f []
+        r <- checkSafetyProperty' net f (fixedTraps net)
         case r of
             (Nothing, traps) -> do
                 invariant <- opt optInvariant
@@ -447,7 +447,7 @@ checkConstraintProperty net cp =
 
 checkUniqueTerminalMarkingProperty :: PetriNet -> OptIO PropResult
 checkUniqueTerminalMarkingProperty net = do
-        r <- checkUniqueTerminalMarkingProperty' net [] []
+        r <- checkUniqueTerminalMarkingProperty' net (fixedTraps net) (fixedSiphons net)
         case r of
             (Nothing, _, _) -> return Satisfied
             (Just _, _, _) -> return Unknown

src/Parser/LOLA.hs

@@ -57,7 +57,7 @@ net = do
         initial <- option [] markingList
         _ <- semi
         ts <- many1 transition
-        return $ makePetriNetWithTransFromStrings "" ps ts initial []
+        return $ makePetriNetWithTransFromStrings "" ps ts initial [] [] []
 
 placeLists :: Parser [String]
 placeLists =

src/Parser/MIST.hs

@@ -58,7 +58,7 @@ net = do
         reserved "init"
         (is,initTrans) <- initial
         return $ makePetriNetWithTransFromStrings "" ps (initTrans ++ ts) is
-                 (map fst initTrans)
+                 (map fst initTrans) [] []
 
 prop :: Parser Property
 prop = do

src/Parser/PNET.hs

@@ -81,6 +81,12 @@ initial = reserved "initial" *> singleOrList (do
             return (n,i)
           )
 
+trap :: Parser [String]
+trap = reserved "trap" *> identList
+
+siphon :: Parser [String]
+siphon = reserved "siphon" *> identList
+
 arc :: Parser [(String,String,Integer)]
 arc = do
         lhs <- identList
@@ -101,13 +107,16 @@ arcs = do
         return $ concat as
 
 data Statement = Places [String] | Transitions [String] |
-                 Arcs [(String,String,Integer)] | Initial [(String,Integer)]
+                 Arcs [(String,String,Integer)] | Initial [(String,Integer)] |
+                 TrapStatement [String] | SiphonStatement [String]
 
 statement :: Parser Statement
 statement = Places <$> places <|>
             Transitions <$> transitions <|>
             Arcs <$> arcs <|>
-            Initial <$> initial
+            Initial <$> initial <|>
+            TrapStatement <$> trap <|>
+            SiphonStatement <$> siphon
 
 petriNet :: Parser PetriNet
 petriNet = do
@@ -115,14 +124,16 @@ petriNet = do
             reserved "net"
             name <- option "" ident
             statements <- braces (many statement)
-            let (p,t,a,i) = foldl splitStatement ([],[],[],[]) statements
-            return $ makePetriNetFromStrings name p t a i []
+            let (p,t,a,i,traps,siphons) = foldl splitStatement ([],[],[],[],[],[]) statements
+            return $ makePetriNetFromStrings name p t a i [] traps siphons
         where
-            splitStatement (ps,ts,as,is) stmnt = case stmnt of
-                  Places p -> (p ++ ps,ts,as,is)
-                  Transitions t -> (ps,t ++ ts,as,is)
-                  Arcs a -> (ps,ts,a ++ as,is)
-                  Initial i -> (ps,ts,as,i ++ is)
+            splitStatement (ps,ts,as,is,traps,siphons) stmnt = case stmnt of
+                  Places p -> (p ++ ps,ts,as,is,traps,siphons)
+                  Transitions t -> (ps,t ++ ts,as,is,traps,siphons)
+                  Arcs a -> (ps,ts,a ++ as,is,traps,siphons)
+                  Initial i -> (ps,ts,as,i ++ is,traps,siphons)
+                  TrapStatement trap -> (ps,ts,as,is,trap:traps,siphons)
+                  SiphonStatement siphon -> (ps,ts,as,is,traps,siphon:siphons)
 
 binary :: String -> (a -> a -> a) -> Assoc -> Operator String () Identity a
 binary name fun = Infix  ( reservedOp name *> return fun )

src/Parser/TPN.hs

@@ -77,7 +77,7 @@ petriNet = do
         ts <- many transition
         let places = [ p | (p,_) <- ps ]
             initial = [ (p,i) | (p,Just i) <- ps ]
-        return $ makePetriNetWithTransFromStrings "" places ts initial []
+        return $ makePetriNetWithTransFromStrings "" places ts initial [] [] []
 
 parseContent :: Parser (PetriNet,[Property])
 parseContent = do

src/PetriNet.hs

@@ -7,7 +7,7 @@ module PetriNet
      renamePlace,renameTransition,renamePetriNetPlacesAndTransitions,
      name,showNetName,places,transitions,
      initialMarking,initial,initials,linitials,
-     pre,lpre,post,lpost,mpre,mpost,context,ghostTransitions,
+     pre,lpre,post,lpost,mpre,mpost,context,ghostTransitions,fixedTraps,fixedSiphons,
      makePetriNet,makePetriNetWithTrans,
      makePetriNetFromStrings,makePetriNetWithTransFromStrings,Trap,Siphon,Cut,
      constructCut,SimpleCut,Invariant(..))
@@ -79,7 +79,9 @@ data PetriNet = PetriNet {
         adjacencyP :: M.Map Place ([(Transition,Integer)], [(Transition,Integer)]),
         adjacencyT :: M.Map Transition ([(Place,Integer)], [(Place,Integer)]),
         initialMarking :: Marking,
-        ghostTransitions :: [Transition]
+        ghostTransitions :: [Transition],
+        fixedTraps :: [Trap],
+        fixedSiphons :: [Siphon]
 }
 
 initial :: PetriNet -> Place -> Integer
@@ -104,7 +106,9 @@ instance Show PetriNet where
                    "\nTransition arcs:\n" ++ unlines
                         (map showContext (M.toList (adjacencyT net))) ++
                    "\nInitial: " ++ show (initialMarking net) ++
-                   "\nGhost transitions: " ++ show (ghostTransitions net)
+                   "\nGhost transitions: " ++ show (ghostTransitions net) ++
+                   "\nFixed traps: " ++ show (fixedTraps net) ++
+                   "\nFixed siphons: " ++ show (fixedSiphons net)
                 where showContext (s,(l,r)) =
                           show l ++ " -> " ++ show s ++ " -> " ++ show r
 
@@ -143,7 +147,9 @@ renamePetriNetPlacesAndTransitions f net =
                     adjacencyT net,
                 initialMarking = emap (renamePlace f) $ initialMarking net,
                 ghostTransitions =
-                    listSet $ map (renameTransition f) $ ghostTransitions net
+                    listSet $ map (renameTransition f) $ ghostTransitions net,
+                fixedTraps = map (map $ renamePlace f) $ fixedTraps net,
+                fixedSiphons = map (map $ renamePlace f) $ fixedSiphons net
             }
         where mapAdjacency f g m = M.mapKeys f (M.map (mapContext g) m)
               mapContext f (pre, post) =
@@ -151,8 +157,8 @@ renamePetriNetPlacesAndTransitions f net =
 
 makePetriNet :: String -> [Place] -> [Transition] ->
         [Either (Transition, Place, Integer) (Place, Transition, Integer)] ->
-        [(Place, Integer)] -> [Transition] -> PetriNet
-makePetriNet name places transitions arcs initial gs =
+        [(Place, Integer)] -> [Transition] -> [Trap] -> [Siphon] -> PetriNet
+makePetriNet name places transitions arcs initial gs fixedTraps fixedSiphons =
             PetriNet {
                 name = name,
                 places = listSet places,
@@ -160,7 +166,9 @@ makePetriNet name places transitions arcs initial gs =
                 adjacencyP = M.map (listMap *** listMap) adP,
                 adjacencyT = M.map (listMap *** listMap)adT,
                 initialMarking = buildVector initial,
-                ghostTransitions = listSet gs
+                ghostTransitions = listSet gs,
+                fixedTraps = map listSet fixedTraps,
+                fixedSiphons = map listSet fixedSiphons
             }
         where
             (adP, adT) = foldl buildMaps (M.empty, M.empty) arcs
@@ -182,8 +190,8 @@ makePetriNet name places transitions arcs initial gs =
 
 makePetriNetFromStrings :: String -> [String] -> [String] ->
         [(String, String, Integer)] ->
-        [(String, Integer)] -> [String] -> PetriNet
-makePetriNetFromStrings name places transitions arcs initial gs =
+        [(String, Integer)] -> [String] -> [[String]] -> [[String]] -> PetriNet
+makePetriNetFromStrings name places transitions arcs initial gs fixedTraps fixedSiphons =
             makePetriNet
                 name
                 (map Place (S.toAscList placeSet))
@@ -191,6 +199,8 @@ makePetriNetFromStrings name places transitions arcs initial gs =
                 (map toEitherArc arcs)
                 (map (first Place) initial)
                 (map Transition gs)
+                (map (map Place) fixedTraps)
+                (map (map Place) fixedSiphons)
         where
             placeSet = S.fromList places
             transitionSet = S.fromList transitions
@@ -215,23 +225,25 @@ makePetriNetFromStrings name places transitions arcs initial gs =
 
 makePetriNetWithTrans :: String -> [Place] ->
         [(Transition, ([(Place, Integer)], [(Place, Integer)]))] ->
-        [(Place, Integer)] -> [Transition] -> PetriNet
-makePetriNetWithTrans name places ts =
-            makePetriNet name places (map fst ts) arcs
+        [(Place, Integer)] -> [Transition] -> [Trap] -> [Siphon] ->PetriNet
+makePetriNetWithTrans name places ts fixedTraps fixedSiphons =
+            makePetriNet name places (map fst ts) arcs fixedTraps fixedSiphons
         where
             arcs = [ Right (p,t,w) | (t,(is,_)) <- ts, (p,w) <- is ] ++
                    [ Left  (t,p,w) | (t,(_,os)) <- ts, (p,w) <- os ]
 
 makePetriNetWithTransFromStrings :: String -> [String] ->
         [(String, ([(String, Integer)], [(String, Integer)]))] ->
-        [(String, Integer)] -> [String] -> PetriNet
-makePetriNetWithTransFromStrings name places arcs initial gs =
+        [(String, Integer)] -> [String] -> [[String]] -> [[String]] -> PetriNet
+makePetriNetWithTransFromStrings name places arcs initial gs fixedTraps fixedSiphons =
             makePetriNetWithTrans
                 name
                 (map Place places)
                 (map toTArc arcs)
                 (map (first Place) initial)
                 (map Transition gs)
+                (map (map Place) fixedTraps)
+                (map (map Place) fixedSiphons)
         where
             toTArc (t, (is, os)) =
                 (Transition t, (map (first Place) is, map (first Place) os))