Excluded ghost transitions from deadlock and safety properties

19a50a08 · Philipp Meyer · a1fd605d · 19a50a08
Commit 19a50a08 authored Jul 29, 2014 by Philipp Meyer
Hide whitespace changes
Inline Side-by-side

Showing with 4 additions and 2 deletions

src/Main.hs src/Main.hs +4 -2

No files found.
--- 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