Added ghost transitions and added filter for zero entries

src/Main.hs

@@ -224,35 +224,42 @@ transformNet (net, props) TerminationByReachability =
                  places net ++ map prime (places net)
             is = [("'m1", 1)] ++
                  initials net ++ map (first prime) (initials net)
+            transformTransition t =
+                let (preT, postT) = context net t
+                    pre'  = [("'m1",1)] ++ preT  ++ map (first prime) preT
+                    post' = [("'m1",1)] ++ postT ++ map (first prime) postT
+                    pre''  = ("'m2",1) : map (first prime) preT
+                    post'' = [("'m2",1), ("'sigma",1)] ++ map (first prime) postT
+                in  if t `elem` ghostTransitions net then
+                        [(t, pre', post')]
+                    else
+                        [(t, pre', post'), (prime t, pre'', post'')]
             ts = ("'switch", [("'m1",1)], [("'m2",1)]) :
-                 concatMap (\t ->
-                    let (preT, postT) = context net t
-                        pre'  = [("'m1",1)] ++ preT  ++ map (first prime) preT
-                        post' = [("'m1",1)] ++ postT ++ map (first prime) postT
-                        pre''  = ("'m2",1) : map (first prime) preT
-                        post'' = [("'m2",1), ("'sigma",1)] ++ map (first prime) postT
-                    in  [(t, pre', post'), (prime t, pre'', post'')]
-                 )
-                 (transitions net)
+                 concatMap transformTransition (transitions net)
+            gs = ghostTransitions net
             prop = Property "termination by reachability" Safety $
                     foldl (:&:) (Atom (LinIneq (Var "'sigma") Ge (Const 1)))
                       (map (\p -> Atom (LinIneq
                                 (Var (prime p) :-: Var p) Ge (Const 0)))
                         (places net))
             -- TODO: map existing liveness properties
-        in  (makePetriNetWithTrans (name net) ps ts is, prop : props)
+        in  (makePetriNetWithTrans (name net) ps ts is gs, prop : props)
 transformNet (net, props) ValidateIdentifiers =
         let ps = map validateId $ places net
             ts = map validateId $ transitions net
             is = map (first validateId) $ initials net
             as = map (\(a,b,x) -> (validateId a, validateId b, x)) $ arcs net
-            net' = makePetriNet (name net) ps ts as is
+            gs = map validateId $ ghostTransitions net
+            net' = makePetriNet (name net) ps ts as is gs
             props' = map (rename validateId) props
         in  (net', props')
 
 makeImplicitProperty :: PetriNet -> ImplicitProperty -> Property
-makeImplicitProperty _ Termination =
-        Property "termination" Liveness FTrue
+makeImplicitProperty net Termination =
+        Property "termination" Liveness $
+            foldl (:&:) FTrue
+                (map (\t -> Atom (LinIneq (Var t) Eq (Const 0)))
+                    (ghostTransitions net))
 makeImplicitProperty net ProperTermination =
         let (finals, nonfinals) = partition (null . lpost net) (places net)
         in  Property "proper termination" Safety

src/Parser/LOLA.hs

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

src/Parser/MIST.hs

@@ -58,6 +58,7 @@ net = do
         reserved "init"
         (is,initTrans) <- initial
         return $ makePetriNetWithTrans "" ps (initTrans ++ ts) is
+                 [t | (t,_,_) <- initTrans]
 
 prop :: Parser Property
 prop = do
@@ -85,8 +86,7 @@ transition = do
         lhs <- commaSep ((,) <$> identifier <* reservedOp ">=" <*> integer)
         reservedOp "->"
         rhs <- commaSep transitionAssignment
-        let rhs' = filter ((/=0) . snd) $
-                   map (\xs -> (fst (head xs), sum (map snd xs))) $
+        let rhs' = map (\xs -> (fst (head xs), sum (map snd xs))) $
                    groupBy ((==) `on` fst) $
                    sortBy (comparing fst) $
                    lhs ++ rhs
@@ -112,7 +112,7 @@ initial = do
         let covered = [x | (x,_,True) <- xs]
         let initTrans = map (\(i,x) -> ("'init" ++ show i, [], [(x,1)]))
                             ([(1::Integer)..] `zip` covered)
-        return (filter ((/=0) . snd) inits, initTrans)
+        return (inits, initTrans)
 
 initState :: Parser (String, Integer, Bool)
 initState = do

src/Parser/PNET.hs

@@ -116,7 +116,7 @@ petriNet = do
             name <- option "" ident
             statements <- braces (many statement)
             let (p,t,a,i) = foldl splitStatement ([],[],[],[]) statements
-            return $ makePetriNet name p t a i
+            return $ makePetriNet name p t a i []
         where
             splitStatement (ps,ts,as,is) stmnt = case stmnt of
                   Places p -> (p ++ ps,ts,as,is)

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 $ makePetriNetWithTrans "" places ts initial
+        return $ makePetriNetWithTrans "" places ts initial []
 
 parseContent :: Parser (PetriNet,[Property])
 parseContent = do

src/PetriNet.hs

@@ -2,7 +2,7 @@
 
 module PetriNet
     (PetriNet,name,showNetName,places,transitions,initial,
-     pre,lpre,post,lpost,initials,context,arcs,
+     pre,lpre,post,lpost,initials,context,arcs,ghostTransitions,
      makePetriNet,makePetriNetWithTrans)
 where
 
@@ -13,7 +13,8 @@ data PetriNet = PetriNet {
         places :: [String],
         transitions :: [String],
         adjacency :: M.Map String ([(String,Integer)], [(String,Integer)]),
-        initMap :: M.Map String Integer
+        initMap :: M.Map String Integer,
+        ghostTransitions :: [String]
 }
 
 initial :: PetriNet -> String -> Integer
@@ -56,15 +57,17 @@ instance Show PetriNet where
                    "Initial: " ++ unwords
                         (map (\(n,i) -> n ++
                             (if i /= 1 then "[" ++ show i ++ "]" else []))
-                        (M.toList (initMap net)))
+                        (M.toList (initMap net))) ++
+                   "\nGhost transitions: " ++ unwords (ghostTransitions net)
 
 makePetriNet :: String -> [String] -> [String] ->
-        [(String, String, Integer)] -> [(String, Integer)] -> PetriNet
-makePetriNet name places transitions arcs initial =
-        let adjacency = foldl buildMap M.empty arcs
-            initMap = M.fromList initial
+        [(String, String, Integer)] -> [(String, Integer)] -> [String] -> PetriNet
+makePetriNet name places transitions arcs initial gs =
+        let adjacency = foldl buildMap M.empty $ filter (\(_,_,w) -> w /= 0) arcs
+            initMap = M.fromList $ filter ((/=0) . snd) initial
         in  PetriNet { name=name, places=places, transitions=transitions,
-                   adjacency=adjacency, initMap=initMap }
+                       adjacency=adjacency, initMap=initMap,
+                       ghostTransitions=gs }
         where
             buildMap m (l,r,w) =
               let m'  = M.insertWith addArc l ([],[(r,w)]) m
@@ -74,9 +77,9 @@ makePetriNet name places transitions arcs initial =
 
 makePetriNetWithTrans :: String -> [String] ->
         [(String, [(String, Integer)], [(String, Integer)])] ->
-        [(String, Integer)] -> PetriNet
-makePetriNetWithTrans name places ts initial =
+        [(String, Integer)] -> [String] -> PetriNet
+makePetriNetWithTrans name places ts initial gs =
         let transitions = [ t | (t,_,_) <- ts ]
             arcs = [ (i,t,w) | (t,is,_) <- ts, (i,w) <- is ] ++
                    [ (t,o,w) | (t,_,os) <- ts, (o,w) <- os ]
-        in  makePetriNet name places transitions arcs initial
+        in  makePetriNet name places transitions arcs initial gs

src/Printer.hs

@@ -5,6 +5,6 @@ where
 import Data.Char
 
 validateId :: String -> String
-validateId "" = ""
+validateId "" = "_"
 validateId (x:xs) = (if isAlpha x then x else '_') :
         map (\c -> if isAlphaNum c then c else '_') xs