Commit 32a95c75 authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Need to add traps to proof

parent fe442856
......@@ -404,6 +404,7 @@ findLivenessRefinementByEmptyTraps' net m x traps cont = do
rm <- refineSafetyProperty net FTrue traps m
case (rm, cont) of
((Nothing, _), _) -> do
-- TODO: include traps needed for proving safety
cut <- generateLivenessRefinement net x traps
return $ Just cut
((Just m', _), True) ->
......
......@@ -19,7 +19,7 @@ import PetriNet
data LivenessInvariant =
RankingFunction (SimpleCut, Vector Place)
| ComponentCut (SimpleCut, [Trap])
| ComponentCut (SimpleCut, [Trap]) -- TODO: add proof why
instance Invariant LivenessInvariant where
invariantSize (RankingFunction ((c0, cs), ps)) =
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment