From 19a50a08891cc4fd2526817503c61e3cf5adfb75 Mon Sep 17 00:00:00 2001
From: Philipp Meyer <philipp.j.meyer@gmail.com>
Date: Tue, 29 Jul 2014 14:22:10 +0200
Subject: [PATCH] Excluded ghost transitions from deadlock and safety
 properties

---
 src/Main.hs | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/Main.hs b/src/Main.hs
index 9323c286..4db8281b 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -270,7 +270,7 @@ makeImplicitProperty net DeadlockFree =
         Property "deadlock-free" Safety $
             foldl (:&:) FTrue
                 (map (foldl (:|:) FFalse . map (placeOp Lt) . lpre net)
-                     (transitions net))
+                     (filter (`notElem` ghostTransitions net) (transitions net)))
 makeImplicitProperty net DeadlockFreeUnlessFinal =
         let nodeadlock = makeImplicitProperty net DeadlockFree
             (finals, nonfinals) = partition (null . lpost net) (places net)
@@ -281,7 +281,9 @@ makeImplicitProperty net DeadlockFreeUnlessFinal =
 makeImplicitProperty net (Bounded k) =
         Property (show k ++ "-bounded") Safety $
             foldl (:|:) FFalse
-                (map (\p -> placeOp Gt (p,k)) (places net))
+                (map (\p -> placeOp Gt (p,k))
+                    (filter (`notElem` concatMap (post net) (ghostTransitions net))
+                        (places net)))
 makeImplicitProperty net Safe =
         let bounded = makeImplicitProperty net (Bounded 1)
         in  Property "safe" Safety $ pformula bounded
-- 
GitLab