Commit 490fe966 authored by Philipp Meyer's avatar Philipp Meyer

Added exit code and changed some formatting

parent 93e8965f
module Main where
import System.Environment (getArgs)
import System.Exit
import Parser (parseFile)
import PetriNet
......@@ -52,21 +53,6 @@ checkProperty net p = do
else "Property may not be satisfied."
return r
--checkPropertyWithTrapRefinement :: PetriNet -> Property -> [[String]] -> IO ()
--checkPropertyWithTrapRefinement net p traps = do
-- r <- checkPropertyConstraintsSat net p traps
-- case r of
-- Nothing -> putStrLn "Property is satisfied"
-- Just m -> do
-- putStrLn "Property may not satisfied, model:" >> print m
-- r2 <- checkTrapConstraintsSat net m
-- case r2 of
-- Nothing -> putStrLn "No trap found"
-- Just m2 -> do
-- let trap = map fst $ filter snd m2
-- putStrLn "Trap found:" >> print trap
-- checkPropertyWithTrapRefinement net p (trap:traps)
main :: IO ()
main = do
args <- getArgs
......@@ -74,9 +60,13 @@ main = do
putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
putStrLn $ "Reading \"" ++ file ++ "\""
(net,properties) <- parseFile file
putStrLn $ "Analyzing " ++ showName net
mapM_ (\p -> do
putStrLn $ "\nChecking " ++ show p
checkProperty net p
) properties
putStrLn $ "Analyzing " ++ showNetName net
rs <- mapM (\p -> do
putStrLn $ "\nChecking " ++ showPropertyName p
checkProperty net p
) properties
if and rs then
exitSuccess
else
exitWith $ ExitFailure 2
{-# OPTIONS_GHC -fno-warn-name-shadowing #-}
module PetriNet
(PetriNet,showName,places,transitions,initial,
(PetriNet,showNetName,places,transitions,initial,
pre,lpre,post,lpost,initials,
makePetriNet)
where
......@@ -37,12 +37,12 @@ lpost net = snd . context net
initials :: PetriNet -> [(String,Integer)]
initials net = M.toList (initMap net)
showName :: PetriNet -> String
showName net = "Petri net" ++
showNetName :: PetriNet -> String
showNetName net = "Petri net" ++
(if null (name net) then "" else " " ++ show (name net))
instance Show PetriNet where
show net = showName net ++
show net = showNetName net ++
"\nPlaces: " ++ unwords (places net) ++
"\nTransitions: " ++ unwords (transitions net) ++
"\nArcs:\n" ++ unlines
......
......@@ -2,6 +2,7 @@
module Property
(Property(..),
showPropertyName,
PropertyType(..),
Formula(..),
LinearInequation(..),
......@@ -71,3 +72,6 @@ instance Show Property where
(if null (pname p) then "" else show (pname p) ++ " ") ++
"{ " ++ show (pformula p) ++ " }"
showPropertyName :: Property -> String
showPropertyName p = "property" ++
(if null (pname p) then "" else " " ++ show (pname p))
......@@ -9,8 +9,6 @@ type ModelSI = M.Map String SInteger
type ModelSB = M.Map String SBool
type ModelI = M.Map String Integer
type ModelB = M.Map String Bool
--type ModelLI = [(String, Integer)]
--type ModelLB = [(String, Bool)]
symConstraints :: SymWord a => [String] -> (M.Map String (SBV a) -> SBool) ->
Symbolic SBool
......@@ -30,17 +28,3 @@ checkSat :: (SatModel a, SymWord a) =>
checkSat (vars, constraint) = do
result <- sat $ symConstraints vars constraint
return $ rebuildModel vars $ getModel result
-- TODO: separate place and transition variables
--checkPropertyConstraintsSat :: PetriNet -> Property -> [[String]] -> IO (Maybe ModelLI)
--checkPropertyConstraintsSat net p traps =
-- let vars = places net ++ transitions net
-- cons m = checkPropertyPlusTrapConstraints (M.fromList m) net p traps
-- in checkSat vars cons
--checkTrapConstraintsSat :: PetriNet -> ModelLI -> IO (Maybe ModelLB)
--checkTrapConstraintsSat net ma =
-- let vars = places net
-- cons m = checkAllTrapConstraints (M.fromList m) (M.fromList ma) net
-- in checkSat vars cons
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