Commit f822e68f authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Re-added structural check

parent ac5befda
...@@ -422,7 +422,7 @@ checkProperty verbosity net refine invariant p = do ...@@ -422,7 +422,7 @@ checkProperty verbosity net refine invariant p = do
r <- case pcont p of r <- case pcont p of
(Safety pf) -> checkSafetyProperty verbosity net refine invariant pf (Safety pf) -> checkSafetyProperty verbosity net refine invariant pf
(Liveness pf) -> checkLivenessProperty verbosity net refine invariant pf (Liveness pf) -> checkLivenessProperty verbosity net refine invariant pf
--(Structural ps) -> checkStructuralProperty verbosity net ps (Structural ps) -> checkStructuralProperty verbosity net ps
verbosePut verbosity 0 $ showPropertyName p ++ " " ++ verbosePut verbosity 0 $ showPropertyName p ++ " " ++
case r of case r of
Satisfied -> "is satisfied." Satisfied -> "is satisfied."
...@@ -461,9 +461,9 @@ refineSafetyProperty :: Int -> PetriNet -> ...@@ -461,9 +461,9 @@ refineSafetyProperty :: Int -> PetriNet ->
refineSafetyProperty verbosity net f traps m = do refineSafetyProperty verbosity net f traps m = do
r <- checkSat verbosity $ checkTrapSat net m r <- checkSat verbosity $ checkTrapSat net m
case r of case r of
Nothing -> do Nothing ->
return $ (Just m, traps) return (Just m, traps)
Just trap -> do Just trap ->
checkSafetyProperty' verbosity net True f (trap:traps) checkSafetyProperty' verbosity net True f (trap:traps)
checkLivenessProperty :: Int -> PetriNet -> Bool -> Bool -> checkLivenessProperty :: Int -> PetriNet -> Bool -> Bool ->
...@@ -499,14 +499,14 @@ checkLivenessProperty' verbosity net refine f cuts = do ...@@ -499,14 +499,14 @@ checkLivenessProperty' verbosity net refine f cuts = do
r <- checkSat verbosity $ checkTransitionInvariantSat net f cuts r <- checkSat verbosity $ checkTransitionInvariantSat net f cuts
case r of case r of
Nothing -> return (Nothing, cuts) Nothing -> return (Nothing, cuts)
Just x -> do Just x ->
if refine then do if refine then do
rt <- findLivenessRefinement verbosity net rt <- findLivenessRefinement verbosity net
(initialMarking net) x [] (initialMarking net) x []
case rt of case rt of
Nothing -> do Nothing ->
return (Just x, cuts) return (Just x, cuts)
Just cut -> do Just cut ->
checkLivenessProperty' verbosity net refine f checkLivenessProperty' verbosity net refine f
(cut:cuts) (cut:cuts)
else else
......
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