Skip to content

GitLab

peregrine
peregrine
Commit 41902d45 authored by Philipp Meyer's avatar Philipp Meyer
Browse files
Options

Added option to choose minimization method

parent f5b89345
Hide whitespace changes
Inline Side-by-side
Showing with 56 additions and 34 deletions
src/Main.hs
View file @ 41902d45
......@@ -31,8 +31,9 @@ import Solver.SubnetEmptyTrap
import Solver.LivenessInvariant
import Solver.SafetyInvariant
import Solver.SComponentWithCut
import Solver.SComponent
import Solver.Simplifier
import Solver.Interpolant
--import Solver.Interpolant
--import Solver.CommFreeReachability
writeFiles :: String -> PetriNet -> [Property] -> OptIO ()
......
src/Options.hs
View file @ 41902d45
......@@ -45,7 +45,7 @@ data Options = Options { inputFormat :: InputFormat
, optRefine :: Bool
, optSimpFormula :: Int
, optRefinementType :: RefinementType
, optMinimizeRefinement :: Bool
, optMinimizeRefinement :: Int
, optInvariant :: Bool
, optOutput :: Maybe String
, outputFormat :: OutputFormat
......@@ -63,7 +63,7 @@ startOptions = Options { inputFormat = PNET
, optRefine = True
, optSimpFormula = 2
, optRefinementType = SComponentRefinement
, optMinimizeRefinement = False
, optMinimizeRefinement = 0
, optInvariant = False
, optOutput = Nothing
, outputFormat = OutLOLA
......@@ -238,11 +238,15 @@ options =
}))
"Use simplification level 2 for invariant generation"
, Option "" ["minimize-refinement"]
(NoArg (\opt -> Right opt {
optMinimizeRefinement = True
}))
"Minimize size of refinement structure (trap/s-component)"
, Option "m" ["minimize"]
(OptArg (\arg opt -> case arg of
Nothing -> Right opt { optMinimizeRefinement = 1 }
Just is -> case reads is of
[(i, "")] | i >= 1 -> Right opt { optMinimizeRefinement = i }
_ -> Left ("invalid argument for minimization method: " ++ is)
)
"METHOD")
"Minimize size of refinement structure by method METHOD"
, Option "v" ["verbose"]
(NoArg (\opt -> Right opt { optVerbosity = optVerbosity opt + 1 }))
......
src/Solver.hs
View file @ 41902d45
......@@ -48,21 +48,21 @@ checkSat (problemName, resultName, vars, constraint, interpretation) = do
return $ Just model
checkSatMin :: (SatModel a, SymWord a, Show a, Show b, Show c) =>
(Maybe c -> ConstraintProblem a (b, c)) -> OptIO (Maybe b)
(Maybe (Int, c) -> ConstraintProblem a (b, c)) -> OptIO (Maybe b)
checkSatMin minProblem = do
optMin <- opt optMinimizeRefinement
r0 <- checkSat $ minProblem Nothing
case r0 of
Nothing -> return Nothing
Just (result, size) ->
if optMin then
Just <$> findSmaller result size
if optMin > 0 then
Just <$> findSmaller optMin result size
else
return $ Just result
where findSmaller result size = do
where findSmaller optMin result size = do
verbosePut 2 $ "Checking for size smaller than " ++ show size
r1 <- checkSat $ minProblem (Just size)
r1 <- checkSat $ minProblem (Just (optMin, size))
case r1 of
Nothing -> return result
Just (result', size') -> findSmaller result' size'
Just (result', size') -> findSmaller optMin result' size'
src/Solver/SComponent.hs
View file @ 41902d45
......@@ -65,11 +65,11 @@ checkBinary p' t' y =
checkBins y
where checkBins xs = bAnd $ map (\x -> x .== 0 ||| x .== 1) $ vals xs
checkSizeLimit :: SIMap Place -> SIMap Transition -> Maybe Integer -> SBool
checkSizeLimit :: SIMap Place -> SIMap Transition -> Maybe (Int, Integer) -> SBool
checkSizeLimit _ _ Nothing = true
checkSizeLimit p' _ (Just size) = (.< literal size) $ sumVal p'
checkSizeLimit p' _ (Just (_, size)) = (.< literal size) $ sumVal p'
checkSComponent :: PetriNet -> FiringVector -> Maybe Integer -> SIMap Place ->
checkSComponent :: PetriNet -> FiringVector -> Maybe (Int, Integer) -> SIMap Place ->
SIMap Transition -> SIMap Transition -> SBool
checkSComponent net x sizeLimit p' t' y =
checkPrePostPlaces net p' t' &&&
......@@ -81,7 +81,7 @@ checkSComponent net x sizeLimit p' t' y =
checkTokens net p' &&&
checkBinary p' t' y
checkSComponentSat :: PetriNet -> FiringVector -> Maybe Integer ->
checkSComponentSat :: PetriNet -> FiringVector -> Maybe (Int, Integer) ->
ConstraintProblem Integer (Cut, Integer)
checkSComponentSat net x sizeLimit =
let fired = elems x
......
src/Solver/SComponentWithCut.hs
View file @ 41902d45
......@@ -68,9 +68,9 @@ checkBinary p1 p2 t0 t1 t2 =
checkSizeLimit ::
SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> SIMap Transition ->
Maybe SizeIndicator -> SBool
Maybe (Int, SizeIndicator) -> SBool
checkSizeLimit _ _ _ _ _ Nothing = true
checkSizeLimit p1 p2 t0 t1 t2 (Just (p1Size, p2Size, t0Size, t1Size, t2Size)) =
checkSizeLimit p1 p2 t0 t1 t2 (Just (minMethod, (p1Size, p2Size, t0Size, t1Size, t2Size))) =
let p1SizeNext = sumVal p1
p2SizeNext = sumVal p2
t0SizeNext = sumVal t0
......@@ -81,16 +81,33 @@ checkSizeLimit p1 p2 t0 t1 t2 (Just (p1Size, p2Size, t0Size, t1Size, t2Size)) =
t0SizeNow = literal t0Size
t1SizeNow = literal t1Size
t2SizeNow = literal t2Size
in (p1SizeNext + p2SizeNext .< p1SizeNow + p2SizeNow) |||
(p1SizeNext + p2SizeNext .== p1SizeNow + p2SizeNow &&& t0SizeNext .< t0SizeNow) |||
(p1SizeNext + p2SizeNext .== p1SizeNow + p2SizeNow &&& t0SizeNext .== t0SizeNow &&&
((t1SizeNext .> t1SizeNow &&& t2SizeNext .>= t2SizeNow) |||
(t1SizeNext .>= t1SizeNow &&& t2SizeNext .> t2SizeNow)))
-- in (t0SizeNext .< t0SizeNow) |||
-- (t0SizeNext .== t0SizeNow &&& t1SizeNext .> t1SizeNow &&& t2SizeNext .>= t2SizeNow) |||
-- (t0SizeNext .== t0SizeNow &&& t1SizeNext .>= t1SizeNow &&& t2SizeNext .> t2SizeNow)
in case minMethod of
1 -> (p1SizeNext + p2SizeNext .< p1SizeNow + p2SizeNow) |||
(p1SizeNext + p2SizeNext .== p1SizeNow + p2SizeNow &&&
t0SizeNext .< t0SizeNow) |||
(p1SizeNext + p2SizeNext .== p1SizeNow + p2SizeNow &&&
t0SizeNext .== t0SizeNow &&&
t1SizeNext .> t1SizeNow &&& t2SizeNext .>= t2SizeNow) |||
(p1SizeNext + p2SizeNext .== p1SizeNow + p2SizeNow &&&
t0SizeNext .== t0SizeNow &&&
t1SizeNext .>= t1SizeNow &&& t2SizeNext .> t2SizeNow)
2 -> (t0SizeNext .< t0SizeNow) |||
(t0SizeNext .== t0SizeNow &&&
t1SizeNext .> t1SizeNow &&& t2SizeNext .>= t2SizeNow) |||
(t0SizeNext .== t0SizeNow &&&
t1SizeNext .>= t1SizeNow &&& t2SizeNext .> t2SizeNow)
3 -> (t1SizeNext .> t1SizeNow &&& t2SizeNext .>= t2SizeNow) |||
(t1SizeNext .>= t1SizeNow &&& t2SizeNext .> t2SizeNow) |||
(t1SizeNext .== t1SizeNow &&& t2SizeNext .== t2SizeNow &&&
t0SizeNext .< t0SizeNow)
4 -> (t0SizeNext .< t0SizeNow) |||
(t0SizeNext .== t0SizeNow &&&
t1SizeNext .> t1SizeNow &&& t2SizeNext .>= t2SizeNow) |||
(t0SizeNext .== t0SizeNow &&&
t1SizeNext .>= t1SizeNow &&& t2SizeNext .> t2SizeNow)
_ -> error $ "minimization method " ++ show minMethod ++ " not supported"
checkSComponent :: PetriNet -> FiringVector -> Maybe SizeIndicator ->
checkSComponent :: PetriNet -> FiringVector -> Maybe (Int, SizeIndicator) ->
SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> SIMap Transition ->
SBool
checkSComponent net x sizeLimit p1 p2 t0 t1 t2 =
......@@ -103,7 +120,7 @@ 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 SizeIndicator ->
checkSComponentWithCutSat :: PetriNet -> FiringVector -> Maybe (Int, SizeIndicator) ->
ConstraintProblem Integer (Cut, SizeIndicator)
checkSComponentWithCutSat net x sizeLimit =
let p1 = makeVarMapWith ("P1@"++) $ places net
......
src/Solver/SubnetEmptyTrap.hs
View file @ 41902d45
......@@ -20,22 +20,22 @@ subnetTrapConstraints net m x b =
properTrap :: SIMap Place -> SBool
properTrap b = sum (vals b) .> 0
checkSizeLimit :: SIMap Place -> Maybe Integer -> SBool
checkSizeLimit :: SIMap Place -> Maybe (Int, Integer) -> SBool
checkSizeLimit _ Nothing = true
checkSizeLimit b (Just size) = (.< literal size) $ sumVal b
checkSizeLimit b (Just (_, size)) = (.< literal size) $ sumVal b
checkBinary :: SIMap Place -> SBool
checkBinary = bAnd . map (\x -> x .== 0 ||| x .== 1) . vals
checkSubnetEmptyTrap :: PetriNet -> Marking -> FiringVector ->
SIMap Place -> Maybe Integer -> SBool
SIMap Place -> Maybe (Int, Integer) -> SBool
checkSubnetEmptyTrap net m x b sizeLimit =
subnetTrapConstraints net m x b &&&
checkSizeLimit b sizeLimit &&&
checkBinary b &&&
properTrap b
checkSubnetEmptyTrapSat :: PetriNet -> Marking -> FiringVector -> Maybe Integer ->
checkSubnetEmptyTrapSat :: PetriNet -> Marking -> FiringVector -> Maybe (Int, Integer) ->
ConstraintProblem Integer (Trap, Integer)
checkSubnetEmptyTrapSat net m x sizeLimit =
let b = makeVarMap $ filter (\p -> val m p == 0) $ mpost net $ elems x
......
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