Commit 9cd19661 authored by Philipp J. Meyer's avatar Philipp J. Meyer
Browse files

Added minimization for unique terminal marking and minimization method messages

parent e2f7a104
......@@ -470,10 +470,10 @@ refineUniqueTerminalMarkingProperty :: PetriNet ->
[Trap] -> [Siphon] -> UniqueTerminalMarkingCounterExample ->
OptIO (Maybe UniqueTerminalMarkingCounterExample, [Trap], [Siphon])
refineUniqueTerminalMarkingProperty net traps siphons m@(m0, m1, m2, x1, x2) = do
r1 <- checkSat $ checkUnmarkedTrapSat net m0 m1 m2 x1 x2
r1 <- checkSatMin $ checkUnmarkedTrapSat net m0 m1 m2 x1 x2
case r1 of
Nothing -> do
r2 <- checkSat $ checkUnmarkedSiphonSat net m0 m1 m2 x1 x2
r2 <- checkSatMin $ checkUnmarkedSiphonSat net m0 m1 m2 x1 x2
case r2 of
Nothing ->
return (Just m, traps, siphons)
......
......@@ -2,8 +2,7 @@
module Solver
(prime,checkSat,checkSatMin,val,vals,positiveVal,zeroVal,
getNames,
ConstraintProblem)
getNames,ConstraintProblem,MinConstraintProblem)
where
import Data.SBV
......@@ -16,6 +15,8 @@ import Control.Applicative
type ConstraintProblem a b =
(String, String, [String], (String -> SBV a) -> SBool, (String -> a) -> b)
type MinConstraintProblem a b c =
(Int -> c -> String, Maybe (Int, c) -> ConstraintProblem a (b, c))
rebuildModel :: SymWord a => [String] -> Either String (Bool, [a]) ->
Maybe (Model a)
......@@ -48,8 +49,8 @@ checkSat (problemName, resultName, vars, constraint, interpretation) = do
return $ Just model
checkSatMin :: (SatModel a, SymWord a, Show a, Show b, Show c) =>
(Maybe (Int, c) -> ConstraintProblem a (b, c)) -> OptIO (Maybe b)
checkSatMin minProblem = do
MinConstraintProblem a b c -> OptIO (Maybe b)
checkSatMin (minMethod, minProblem) = do
optMin <- opt optMinimizeRefinement
r0 <- checkSat $ minProblem Nothing
case r0 of
......@@ -60,7 +61,7 @@ checkSatMin minProblem = do
else
return $ Just result
where findSmaller optMin result curSize = do
verbosePut 2 $ "Checking for size smaller than " ++ show curSize
verbosePut 2 $ "Checking for " ++ minMethod optMin curSize
r1 <- checkSat $ minProblem (Just (optMin, curSize))
case r1 of
Nothing -> return result
......
......@@ -69,6 +69,9 @@ checkSizeLimit :: SIMap Place -> SIMap Transition -> Maybe (Int, Integer) -> SBo
checkSizeLimit _ _ Nothing = true
checkSizeLimit p' _ (Just (_, curSize)) = (.< literal curSize) $ sumVal p'
minimizeMethod :: Int -> Integer -> String
minimizeMethod _ curSize = "size smaller than" ++ show curSize
checkSComponent :: PetriNet -> FiringVector -> Maybe (Int, Integer) -> SIMap Place ->
SIMap Transition -> SIMap Transition -> SBool
checkSComponent net x sizeLimit p' t' y =
......@@ -81,17 +84,17 @@ checkSComponent net x sizeLimit p' t' y =
checkTokens net p' &&&
checkBinary p' t' y
checkSComponentSat :: PetriNet -> FiringVector -> Maybe (Int, Integer) ->
ConstraintProblem Integer (Cut, Integer)
checkSComponentSat net x sizeLimit =
checkSComponentSat :: PetriNet -> FiringVector -> MinConstraintProblem Integer Cut Integer
checkSComponentSat net x =
let fired = elems x
p' = makeVarMap $ places net
t' = makeVarMap $ transitions net
y = makeVarMapWith prime fired
in ("S-component constraints", "cut",
in (minimizeMethod, \sizeLimit ->
("S-component constraints", "cut",
getNames p' ++ getNames t' ++ getNames y,
\fm -> checkSComponent net x sizeLimit (fmap fm p') (fmap fm t') (fmap fm y),
\fm -> cutFromAssignment net x (fmap fm p') (fmap fm t') (fmap fm y))
\fm -> cutFromAssignment net x (fmap fm p') (fmap fm t') (fmap fm y)))
cutFromAssignment :: PetriNet -> FiringVector -> IMap Place ->
IMap Transition -> IMap Transition -> (Cut, Integer)
......
......@@ -108,6 +108,28 @@ checkSizeLimit p1 p2 t0 t1 t2 (Just (minMethod, (p1Size, p2Size, t0Size, t1Size,
9 -> (t1SizeNext + t2SizeNext .> t1SizeNow + t2SizeNow)
_ -> error $ "minimization method " ++ show minMethod ++ " not supported"
minimizeMethod :: Int -> SizeIndicator -> String
minimizeMethod minMethod (p1Size, p2Size, t0Size, t1Size, t2Size) =
case minMethod of
1 -> "(|t0| < " ++ show t0Size ++ ") || " ++
"(|t0| = " ++ show t0Size ++ " && " ++ "|t1| > " ++ show t1Size ++ " && |t2| >= " ++ show t2Size ++ ") || " ++
"(|t0| = " ++ show t0Size ++ " && " ++ "|t1| >= " ++ show t1Size ++ " && |t2| > " ++ show t2Size ++ ")"
2 -> "(|t1| > " ++ show t1Size ++ " && " ++ "|t2| >= " ++ show t2Size ++ ") || " ++
"(|t1| >= " ++ show t1Size ++ " && " ++ "|t2| > " ++ show t2Size ++ ") || " ++
"(|t1| = " ++ show t1Size ++ " && " ++ "|t2| = " ++ show t2Size ++ " && t0 < " ++ show t0Size ++ ")"
3 -> "(|p1| + |p2| < " ++ show (p1Size + p2Size) ++ ") || " ++
"(|p1| + |p2| = " ++ show (p1Size + p2Size) ++ " && " ++ "|t0| < " ++ show t0Size ++ ")"
4 -> "(|p1| + |p2| > " ++ show (p1Size + p2Size) ++ ") || " ++
"(|p1| + |p2| = " ++ show (p1Size + p2Size) ++ " && " ++ "|t0| < " ++ show t0Size ++ ")"
5 -> "(|p1| + |p2| < " ++ show (p1Size + p2Size) ++ ")"
6 -> "(|p1| + |p2| > " ++ show (p1Size + p2Size) ++ ")"
7 -> "(|t1| > " ++ show t1Size ++ " && |t2| >= " ++ show t2Size ++ ") || " ++
"(|t1| >= " ++ show t1Size ++ " && |t2| > " ++ show t2Size ++ ")"
8 -> "(|t1| < " ++ show t1Size ++ " && |t2| <= " ++ show t2Size ++ ") || " ++
"(|t1| <= " ++ show t1Size ++ " && |t2| < " ++ show t2Size ++ ")"
9 -> "(|t1| + |t2| > " ++ show (t1Size + t2Size) ++ ")"
_ -> error $ "minimization method " ++ show minMethod ++ " not supported"
checkSComponent :: PetriNet -> FiringVector -> Maybe (Int, SizeIndicator) ->
SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> SIMap Transition ->
SBool
......@@ -121,20 +143,20 @@ checkSComponent net x sizeLimit p1 p2 t0 t1 t2 =
checkBinary p1 p2 t0 t1 t2 &&&
checkDisjunct net p1 p2 t0 t1 t2
checkSComponentWithCutSat :: PetriNet -> FiringVector -> Maybe (Int, SizeIndicator) ->
ConstraintProblem Integer (Cut, SizeIndicator)
checkSComponentWithCutSat net x sizeLimit =
checkSComponentWithCutSat :: PetriNet -> FiringVector -> MinConstraintProblem Integer Cut SizeIndicator
checkSComponentWithCutSat net x =
let p1 = makeVarMapWith ("P1@"++) $ places net
p2 = makeVarMapWith ("P2@"++) $ places net
t0 = makeVarMapWith ("T0@"++) $ transitions net
t1 = makeVarMapWith ("T1@"++) $ transitions net
t2 = makeVarMapWith ("T2@"++) $ transitions net
in ("general S-component constraints", "cut",
in (minimizeMethod, \sizeLimit ->
("general S-component constraints", "cut",
getNames p1 ++ getNames p2 ++ getNames t0 ++ getNames t1 ++ getNames t2,
\fm -> checkSComponent net x sizeLimit
(fmap fm p1) (fmap fm p2) (fmap fm t0) (fmap fm t1) (fmap fm t2),
\fm -> cutFromAssignment
(fmap fm p1) (fmap fm p2) (fmap fm t0) (fmap fm t1) (fmap fm t2))
(fmap fm p1) (fmap fm p2) (fmap fm t0) (fmap fm t1) (fmap fm t2)))
cutFromAssignment ::
IMap Place -> IMap Place -> IMap Transition -> IMap Transition -> IMap Transition ->
......
......@@ -26,6 +26,9 @@ checkSizeLimit :: SIMap Place -> Maybe (Int, Integer) -> SBool
checkSizeLimit _ Nothing = true
checkSizeLimit b (Just (_, curSize)) = (.< literal curSize) $ sumVal b
minimizeMethod :: Int -> Integer -> String
minimizeMethod _ curSize = "size smaller than " ++ show curSize
checkBinary :: SIMap Place -> SBool
checkBinary = bAnd . map (\x -> x .== 0 ||| x .== 1) . vals
......@@ -37,14 +40,14 @@ checkSubnetEmptyTrap net m x b sizeLimit =
checkBinary b &&&
properTrap b
checkSubnetEmptyTrapSat :: PetriNet -> Marking -> FiringVector -> Maybe (Int, Integer) ->
ConstraintProblem Integer (Trap, Integer)
checkSubnetEmptyTrapSat net m x sizeLimit =
checkSubnetEmptyTrapSat :: PetriNet -> Marking -> FiringVector -> MinConstraintProblem Integer Trap Integer
checkSubnetEmptyTrapSat net m x =
let b = makeVarMap $ filter (\p -> val m p == 0) $ mpost net $ elems x
in ("subnet empty trap constraints", "trap",
in (minimizeMethod, \sizeLimit ->
("subnet empty trap constraints", "trap",
getNames b,
\fm -> checkSubnetEmptyTrap net m x (fmap fm b) sizeLimit,
\fm -> trapFromAssignment (fmap fm b))
\fm -> trapFromAssignment (fmap fm b)))
trapFromAssignment :: IMap Place -> (Trap, Integer)
trapFromAssignment b = (M.keys (M.filter (> 0) b), sum (M.elems b))
......
......@@ -101,67 +101,87 @@ markingsFromAssignment m0 m1 m2 x1 x2 =
-- trap and siphon refinement constraints
siphonConstraints :: PetriNet -> SBMap Place -> SBool
siphonConstraints :: PetriNet -> SIMap Place -> SBool
siphonConstraints net b =
bAnd $ map siphonConstraint $ transitions net
where siphonConstraint t =
bOr (mval b (post net t)) ==> bOr (mval b (pre net t))
sum (mval b $ post net t) .> 0 ==> sum (mval b $ pre net t) .> 0
trapConstraints :: PetriNet -> SBMap Place -> SBool
trapConstraints :: PetriNet -> SIMap Place -> SBool
trapConstraints net b =
bAnd $ map trapConstraint $ transitions net
where trapConstraint t =
bOr (mval b (pre net t)) ==> bOr (mval b (post net t))
sum (mval b $ pre net t) .> 0 ==> sum (mval b $ post net t) .> 0
placesMarkedByMarking :: PetriNet -> RMarking -> SBMap Place -> SBool
placesMarkedByMarking net m b = bOr $ mval b $ elems m
placesMarkedByMarking :: PetriNet -> RMarking -> SIMap Place -> SBool
placesMarkedByMarking net m b = sum (mval b $ elems m) .> 0
placesUnmarkedByMarking :: PetriNet -> RMarking -> SBMap Place -> SBool
placesUnmarkedByMarking net m b = bAnd $ map (bnot . val b) $ elems m
placesUnmarkedByMarking :: PetriNet -> RMarking -> SIMap Place -> SBool
placesUnmarkedByMarking net m b = sum (mval b $ elems m) .== 0
placesPostsetOfSequence :: PetriNet -> RFiringVector -> SBMap Place -> SBool
placesPostsetOfSequence net x b = bOr $ mval b $ mpost net $ elems x
placesPostsetOfSequence :: PetriNet -> RFiringVector -> SIMap Place -> SBool
placesPostsetOfSequence net x b = sum (mval b $ mpost net $ elems x) .> 0
placesPresetOfSequence :: PetriNet -> RFiringVector -> SBMap Place -> SBool
placesPresetOfSequence net x b = bOr $ mval b $ mpre net $ elems x
placesPresetOfSequence :: PetriNet -> RFiringVector -> SIMap Place -> SBool
placesPresetOfSequence net x b = sum (mval b $ mpre net $ elems x) .> 0
nonemptySet :: (Ord a, Show a) => SBMap a -> SBool
nonemptySet b = bOr $ vals b
nonemptySet :: (Ord a, Show a) => SIMap a -> SBool
nonemptySet b = sum (vals b) .> 0
checkUnmarkedTrap :: PetriNet -> RMarking -> RMarking -> RMarking -> RFiringVector -> RFiringVector -> SBMap Place -> SBool
checkUnmarkedTrap net m0 m1 m2 x1 x2 b =
checkBinary :: SIMap Place -> SBool
checkBinary = bAnd . map (\x -> x .== 0 ||| x .== 1) . vals
checkSizeLimit :: SIMap Place -> Maybe (Int, Integer) -> SBool
checkSizeLimit _ Nothing = true
checkSizeLimit b (Just (1, curSize)) = (.< literal curSize) $ sumVal b
checkSizeLimit b (Just (2, curSize)) = (.> literal curSize) $ sumVal b
checkSizeLimit _ (Just (_, _)) = error "minimization method not supported"
minimizeMethod :: Int -> Integer -> String
minimizeMethod 1 curSize = "size smaller than " ++ show curSize
minimizeMethod 2 curSize = "size larger than " ++ show curSize
minimizeMethod _ _ = error "minimization method not supported"
checkUnmarkedTrap :: PetriNet -> RMarking -> RMarking -> RMarking -> RFiringVector -> RFiringVector -> SIMap Place -> Maybe (Int, Integer) -> SBool
checkUnmarkedTrap net m0 m1 m2 x1 x2 b sizeLimit =
trapConstraints net b &&&
nonemptySet b &&&
checkSizeLimit b sizeLimit &&&
checkBinary b &&&
(
(placesMarkedByMarking net m0 b &&& (placesUnmarkedByMarking net m1 b ||| placesUnmarkedByMarking net m2 b)) |||
(placesPostsetOfSequence net x1 b &&& placesUnmarkedByMarking net m1 b) |||
(placesPostsetOfSequence net x2 b &&& placesUnmarkedByMarking net m2 b)
)
checkUnmarkedTrapSat :: PetriNet -> RMarking -> RMarking -> RMarking -> RFiringVector -> RFiringVector -> ConstraintProblem Bool Trap
checkUnmarkedTrapSat :: PetriNet -> RMarking -> RMarking -> RMarking -> RFiringVector -> RFiringVector -> MinConstraintProblem Integer Trap Integer
checkUnmarkedTrapSat net m0 m1 m2 x1 x2 =
let b = makeVarMap $ places net
in ("trap marked in m and unmarked in m1 or m2, or marked by x1 and unmarked in m1, or marked by x2 and unmarked in m2", "trap",
in (minimizeMethod, \sizeLimit ->
("trap marked in m and unmarked in m1 or m2, or marked by x1 and unmarked in m1, or marked by x2 and unmarked in m2", "trap",
getNames b,
\fm -> checkUnmarkedTrap net m0 m1 m2 x1 x2 (fmap fm b),
\fm -> placesFromAssignment (fmap fm b))
\fm -> checkUnmarkedTrap net m0 m1 m2 x1 x2 (fmap fm b) sizeLimit,
\fm -> placesFromAssignment (fmap fm b)))
checkUnmarkedSiphon :: PetriNet -> RMarking -> RMarking -> RMarking -> RFiringVector -> RFiringVector -> SBMap Place -> SBool
checkUnmarkedSiphon net m0 m1 m2 x1 x2 b =
checkUnmarkedSiphon :: PetriNet -> RMarking -> RMarking -> RMarking -> RFiringVector -> RFiringVector -> SIMap Place -> Maybe (Int, Integer) -> SBool
checkUnmarkedSiphon net m0 m1 m2 x1 x2 b sizeLimit =
siphonConstraints net b &&&
nonemptySet b &&&
checkSizeLimit b sizeLimit &&&
checkBinary b &&&
(placesUnmarkedByMarking net m0 b &&&
(placesMarkedByMarking net m1 b ||| placesMarkedByMarking net m2 b |||
placesPresetOfSequence net x1 b ||| placesPresetOfSequence net x2 b)
)
checkUnmarkedSiphonSat :: PetriNet -> RMarking -> RMarking -> RMarking -> RFiringVector -> RFiringVector -> ConstraintProblem Bool Siphon
checkUnmarkedSiphonSat :: PetriNet -> RMarking -> RMarking -> RMarking -> RFiringVector -> RFiringVector -> MinConstraintProblem Integer Siphon Integer
checkUnmarkedSiphonSat net m0 m1 m2 x1 x2 =
let b = makeVarMap $ places net
in ("siphon unmarked in m0 and marked in m1 or m2 or used as input in x1 or x2", "siphon",
in (minimizeMethod, \sizeLimit ->
("siphon unmarked in m0 and marked in m1 or m2 or used as input in x1 or x2", "siphon",
getNames b,
\fm -> checkUnmarkedSiphon net m0 m1 m2 x1 x2 (fmap fm b),
\fm -> placesFromAssignment (fmap fm b))
\fm -> checkUnmarkedSiphon net m0 m1 m2 x1 x2 (fmap fm b) sizeLimit,
\fm -> placesFromAssignment (fmap fm b)))
placesFromAssignment :: BMap Place -> Trap
placesFromAssignment b = M.keys $ M.filter id b
placesFromAssignment :: IMap Place -> ([Place], Integer)
placesFromAssignment b = (M.keys (M.filter (> 0) b), sum (M.elems b))
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