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

Fixed bug in generation liveness refinement cuts

parent e74bd43d
......@@ -516,9 +516,9 @@ checkLivenessProperty' verbosity net refine f cuts = do
findLivenessRefinement :: Int -> PetriNet -> FiringVector ->
IO (Maybe Cut)
findLivenessRefinement verbosity net x = do
r1 <- findLivenessRefinementByEmptyTraps verbosity net
(initialMarking net) x []
--r1 <- findLivenessRefinementBySComponent verbosity net x
--r1 <- findLivenessRefinementByEmptyTraps verbosity net
-- (initialMarking net) x []
r1 <- findLivenessRefinementBySComponent verbosity net x
case r1 of
Nothing -> findLivenessRefinementByEmptyTraps verbosity net
(initialMarking net) x []
......@@ -543,19 +543,18 @@ findLivenessRefinementByEmptyTraps verbosity net m x traps = do
(Just _, _) ->
return Nothing
Just trap -> do
rm <- checkSafetyProperty' verbosity net False FTrue (trap:traps)
let traps' = trap:traps
rm <- checkSafetyProperty' verbosity net False FTrue traps'
case rm of
(Nothing, _) -> do
cut <- generateLivenessRefinement verbosity net x traps
cut <- generateLivenessRefinement verbosity net x traps'
return $ Just cut
(Just m', _) ->
findLivenessRefinementByEmptyTraps verbosity net m' x (trap:traps)
findLivenessRefinementByEmptyTraps verbosity net m' x traps'
generateLivenessRefinement :: Int -> PetriNet -> FiringVector -> [Trap] -> IO Cut
generateLivenessRefinement verbosity net x traps = do
let ts = map (filter (\t -> val x t > 0) . mpre net) traps
let u = nubOrd (concatMap (filter (\t -> val x t == 0) . mpost net) traps)
let cut = (ts,u)
let cut = constructCut net x traps
verbosePut verbosity 3 $ "- cut: " ++ show cut
return cut
......
......@@ -4,13 +4,15 @@
module PetriNet
(PetriNet,Place(..),Transition(..),Marking,FiringVector,
renamePlace,renameTransition,renamePetriNetPlacesAndTransitions,
name,showNetName,places,transitions,initialMarking,initial,initials,linitials,
name,showNetName,places,transitions,
initialMarking,initial,initials,linitials,
pre,lpre,post,lpost,mpre,mpost,context,ghostTransitions,
makePetriNet,makePetriNetWithTrans,makePetriNetWith,Trap,Cut)
makePetriNet,makePetriNetWithTrans,makePetriNetWith,Trap,Cut,constructCut)
where
import qualified Data.Map as M
import Control.Arrow (first)
import Data.List (sort)
import Util
......@@ -114,6 +116,12 @@ renamePetriNetPlacesAndTransitions f net =
where mapAdjacency f g m = M.mapKeys f (M.map (mapContext g) m)
mapContext f (pre, post) = (map (first f) pre, map (first f) post)
-- TODO: use strongly connected components and min cuts
constructCut :: PetriNet -> FiringVector -> [Trap] -> Cut
constructCut net x traps =
(nubOrd (map (sort . filter (\t -> val x t > 0) . mpre net) traps),
nubOrd (concatMap (filter (\t -> val x t == 0) . mpost net) traps))
-- TODO: better constructors, only one main constructor
-- TODO: enforce sorted lists
makePetriNet :: String -> [String] -> [String] ->
......
......@@ -43,5 +43,6 @@ checkSat verbosity (problemName, resultName, vars, constraint, interpretation) =
let fm x = rawModel M.! x
let model = interpretation fm
verbosePut verbosity 3 $ "- " ++ resultName ++ ": " ++ show model
verbosePut verbosity 4 $ "- raw model: " ++ show rawModel
return $ Just model
......@@ -86,12 +86,15 @@ checkSComponentSat net x =
in ("S-component constraints", "cut",
getNames p' ++ getNames t' ++ getNames y,
\fm -> checkSComponent net x (fmap fm p') (fmap fm t') (fmap fm y),
\fm -> cutFromAssignment x (fmap fm t') (fmap fm y))
\fm -> cutFromAssignment net x (fmap fm p') (fmap fm t') (fmap fm y))
-- TODO: use strongly connected components and min cuts
cutFromAssignment :: FiringVector -> IMap Transition -> IMap Transition -> Cut
cutFromAssignment x t' y =
let (ts, u) = partition (\t -> val x t > 0) $ M.keys $ M.filter (> 0) t'
cutFromAssignment :: PetriNet -> FiringVector -> IMap Place ->
IMap Transition -> IMap Transition -> Cut
cutFromAssignment net x p' t' y =
let ts = filter (\t -> val x t > 0) $ elems $ M.filter (> 0) t'
(t1, t2) = partition (\t -> val y t > 0) ts
in ([t1,t2], u)
--let (ts, u) = partition (\t -> val x t > 0) $ elems $ M.filter (> 0) t'
s1 = filter (\p -> val p' p > 0) $ mpre net t1
s2 = filter (\p -> val p' p > 0) $ mpre net t2
in constructCut net x [s1,s2]
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