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

Added more options to control output verbosity

parent 2829680d
...@@ -24,7 +24,7 @@ import Solver.SComponent ...@@ -24,7 +24,7 @@ import Solver.SComponent
data InputFormat = PNET | LOLA | TPN deriving (Show,Read) data InputFormat = PNET | LOLA | TPN deriving (Show,Read)
data Options = Options { inputFormat :: InputFormat data Options = Options { inputFormat :: InputFormat
, optVerbose :: Bool , optVerbosity :: Int
, optShowHelp :: Bool , optShowHelp :: Bool
, optShowVersion :: Bool , optShowVersion :: Bool
, proveTermination :: Bool , proveTermination :: Bool
...@@ -33,7 +33,7 @@ data Options = Options { inputFormat :: InputFormat ...@@ -33,7 +33,7 @@ data Options = Options { inputFormat :: InputFormat
startOptions :: Options startOptions :: Options
startOptions = Options { inputFormat = PNET startOptions = Options { inputFormat = PNET
, optVerbose = False , optVerbosity = 1
, optShowHelp = False , optShowHelp = False
, optShowVersion = False , optShowVersion = False
, proveTermination = False , proveTermination = False
...@@ -63,8 +63,12 @@ options = ...@@ -63,8 +63,12 @@ options =
"Don't use refinement" "Don't use refinement"
, Option "v" ["verbose"] , Option "v" ["verbose"]
(NoArg (\opt -> Right opt { optVerbose = True })) (NoArg (\opt -> Right opt { optVerbosity = optVerbosity opt + 1 }))
"Enable verbose messages" "Increase verbosity (may be specified more than once)"
, Option "q" ["quiet"]
(NoArg (\opt -> Right opt { optVerbosity = optVerbosity opt - 1 }))
"Decrease verbosity (may be specified more than once)"
, Option "V" ["version"] , Option "V" ["version"]
(NoArg (\opt -> Right opt { optShowVersion = True })) (NoArg (\opt -> Right opt { optShowVersion = True }))
...@@ -75,6 +79,10 @@ options = ...@@ -75,6 +79,10 @@ options =
"Show help" "Show help"
] ]
verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
when (verbosity >= level) (putStrLn str)
parseArgs :: IO (Either String (Options, [String])) parseArgs :: IO (Either String (Options, [String]))
parseArgs = do parseArgs = do
args <- getArgs args <- getArgs
...@@ -83,41 +91,41 @@ parseArgs = do ...@@ -83,41 +91,41 @@ parseArgs = do
return $ (,files) <$> foldl (>>=) (return startOptions) actions return $ (,files) <$> foldl (>>=) (return startOptions) actions
(_, _, errs) -> return $ Left $ concat errs (_, _, errs) -> return $ Left $ concat errs
checkFile :: Parser (PetriNet,[Property]) -> Bool -> Bool -> [Property] -> checkFile :: Parser (PetriNet,[Property]) -> Int -> Bool -> [Property] ->
String -> IO Bool String -> IO Bool
checkFile parser verbose refine addedProperties file = do checkFile parser verbosity refine addedProperties file = do
putStrLn $ "Reading \"" ++ file ++ "\"" verbosePut verbosity 0 $ "Reading \"" ++ file ++ "\""
(net,properties) <- parseFile parser file (net,properties) <- parseFile parser file
putStrLn $ "Analyzing " ++ showNetName net verbosePut verbosity 1 $ "Analyzing " ++ showNetName net
when verbose (do verbosePut verbosity 2 $
putStrLn $ "Places: " ++ show (length $ places net) "Places: " ++ show (length $ places net) ++ "\n" ++
putStrLn $ "Transitions: " ++ show (length $ transitions net) "Transitions: " ++ show (length $ transitions net)
) rs <- mapM (checkProperty verbosity net refine)
rs <- mapM (checkProperty verbose net refine)
(addedProperties ++ properties) (addedProperties ++ properties)
putStrLn "" verbosePut verbosity 0 ""
return $ and rs return $ and rs
checkProperty :: Bool -> PetriNet -> Bool -> Property -> IO Bool checkProperty :: Int -> PetriNet -> Bool -> Property -> IO Bool
checkProperty verbose net refine p = do checkProperty verbosity net refine p = do
putStrLn $ "\nChecking " ++ showPropertyName p verbosePut verbosity 1 $ "\nChecking " ++ showPropertyName p
r <- case ptype p of r <- case ptype p of
Safety -> checkSafetyProperty verbose net refine (pformula p) [] Safety -> checkSafetyProperty verbosity net refine (pformula p) []
Liveness -> checkLivenessProperty verbose net refine (pformula p) [] Liveness -> checkLivenessProperty verbosity net refine (pformula p) []
putStrLn $ if r then "Property is satisfied." verbosePut verbosity 0 $ showPropertyName p ++
else "Property may not be satisfied." if r then "is satisfied."
else " may not be satisfied."
return r return r
checkSafetyProperty :: Bool -> PetriNet -> Bool -> checkSafetyProperty :: Int -> PetriNet -> Bool ->
Formula -> [[String]] -> IO Bool Formula -> [[String]] -> IO Bool
checkSafetyProperty verbose net refine f traps = do checkSafetyProperty verbosity net refine f traps = do
r <- checkSat $ checkStateEquationSat net f traps r <- checkSat $ checkStateEquationSat net f traps
case r of case r of
Nothing -> return True Nothing -> return True
Just a -> do Just a -> do
let assigned = markedPlacesFromAssignment net a let assigned = markedPlacesFromAssignment net a
putStrLn "Assignment found" verbosePut verbosity 1 "Assignment found"
when verbose (putStrLn $ "Places marked: " ++ show assigned) verbosePut verbosity 2 $ "Places marked: " ++ show assigned
if refine then do if refine then do
rt <- checkSat $ checkTrapSat net assigned rt <- checkSat $ checkTrapSat net assigned
case rt of case rt of
...@@ -126,35 +134,35 @@ checkSafetyProperty verbose net refine f traps = do ...@@ -126,35 +134,35 @@ checkSafetyProperty verbose net refine f traps = do
return False return False
Just at -> do Just at -> do
let trap = trapFromAssignment at let trap = trapFromAssignment at
putStrLn "Trap found" verbosePut verbosity 1 "Trap found"
when verbose (putStrLn $ "Places in trap: " ++ verbosePut verbosity 2 $ "Places in trap: " ++
show trap) show trap
checkSafetyProperty verbose net refine f checkSafetyProperty verbosity net refine f
(trap:traps) (trap:traps)
else else
return False return False
checkLivenessProperty :: Bool -> PetriNet -> Bool -> checkLivenessProperty :: Int -> PetriNet -> Bool ->
Formula -> [([String],[String])] -> IO Bool Formula -> [([String],[String])] -> IO Bool
checkLivenessProperty verbose net refine f strans = do checkLivenessProperty verbosity net refine f strans = do
r <- checkSat $ checkTransitionInvariantSat net f strans r <- checkSat $ checkTransitionInvariantSat net f strans
case r of case r of
Nothing -> return True Nothing -> return True
Just ax -> do Just ax -> do
let fired = firedTransitionsFromAssignment ax let fired = firedTransitionsFromAssignment ax
putStrLn "Assignment found" verbosePut verbosity 1 "Assignment found"
when verbose (putStrLn $ "Transitions fired: " ++ show fired) verbosePut verbosity 2 $ "Transitions fired: " ++ show fired
if refine then do if refine then do
rt <- checkSat $ checkSComponentSat net fired ax rt <- checkSat $ checkSComponentSat net fired ax
case rt of case rt of
Nothing -> do Nothing -> do
putStrLn "No S-component found" verbosePut verbosity 1 "No S-component found"
return False return False
Just as -> do Just as -> do
let sOutIn = getSComponentOutIn net ax as let sOutIn = getSComponentOutIn net ax as
putStrLn "S-component found" verbosePut verbosity 1 "S-component found"
when verbose (putStrLn $ "Out/In: " ++ show sOutIn) verbosePut verbosity 2 $ "Out/In: " ++ show sOutIn
checkLivenessProperty verbose net refine f checkLivenessProperty verbosity net refine f
(sOutIn:strans) (sOutIn:strans)
else else
return False return False
...@@ -166,19 +174,20 @@ main = do ...@@ -166,19 +174,20 @@ main = do
case args of case args of
Left err -> exitErrorWith err Left err -> exitErrorWith err
Right (opts, files) -> do Right (opts, files) -> do
when (optShowVersion opts) (exitSuccessWith "Version 0.01") when (optShowVersion opts) (exitSuccessWith "Version 0.01")
when (optShowHelp opts) (exitSuccessWith when (optShowHelp opts) (exitSuccessWith
(usageInfo "SLAPnet" options)) (usageInfo "SLAPnet" options))
when (null files) (exitErrorWith "No input file given") when (null files) (exitErrorWith "No input file given")
let verbosity = optVerbosity opts
refinement = optRefine opts
let parser = case inputFormat opts of let parser = case inputFormat opts of
PNET -> PNET.parseContent PNET -> PNET.parseContent
LOLA -> LOLA.parseContent LOLA -> LOLA.parseContent
TPN -> TPN.parseContent TPN -> TPN.parseContent
let properties = [ Property "termination" Liveness FTrue let properties = [ Property "termination" Liveness FTrue
| proveTermination opts ] | proveTermination opts ]
rs <- mapM (checkFile parser (optVerbose opts) (optRefine opts) rs <- mapM (checkFile parser verbosity refinement properties)
properties) files files
if and rs then if and rs then
exitSuccessWith "All properties satisfied." exitSuccessWith "All properties satisfied."
else else
......
Supports Markdown
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