Main.hs 5.88 KB
Newer Older
1
2
{-# LANGUAGE TupleSections #-}

3
4
module Main where

Philipp Meyer's avatar
Philipp Meyer committed
5
import System.Environment (getArgs)
6
import System.Exit
7
8
9
10
11
import System.IO
import System.Console.GetOpt
import Control.Monad
import Control.Applicative
import Data.Char (toUpper)
Philipp Meyer's avatar
Philipp Meyer committed
12
13

import Parser (parseFile)
14
15
import PetriNet
import Property
16
import Solver
17
18
import Solver.StateEquation
import Solver.TrapConstraints
19
20
import Solver.TransitionInvariant
import Solver.SComponent
21

22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
data InputFormat = PNET | LOLA | TPN deriving (Show,Read)

data Options = Options { inputFormat :: InputFormat
                       , optVerbose :: Bool
                       , optShowHelp :: Bool
                       , optShowVersion :: Bool
                       }

startOptions :: Options
startOptions = Options { inputFormat = PNET
                       , optVerbose = False
                       , optShowHelp = False
                       , optShowVersion = False
                       }

options :: [ OptDescr (Options -> Either String Options) ]
options =
        [ Option "f" ["format"]
        (ReqArg (\arg opt ->
            case reads (map toUpper arg) of
                [(format, "")] -> Right opt { inputFormat = format }
                _ -> Left ("invalid input format `" ++ arg ++ "'\n"))
        "FORMAT")
        ("Input format (possible values=\"pnet\", \"lola\", \"tpn\"\n" ++
         "              default=\"pnet\")")

        , Option "v" ["verbose"]
        (NoArg (\opt -> Right opt { optVerbose = True }))
        "Enable verbose messages"

        , Option "V" ["version"]
        (NoArg (\opt -> Right opt { optShowVersion = True }))
        "Show version"

        , Option "h" ["help"]
        (NoArg (\opt -> Right opt { optShowHelp = True }))
        "Show help"
        ]

parseArgs :: IO (Either String (Options, [String]))
parseArgs = do
        args <- getArgs
        case getOpt Permute options args of
            (actions, files, []) ->
                return $ (,files) <$> foldl (>>=) (return startOptions) actions
            (_, _, errs) -> return $ Left $ concat errs

checkFile :: Options -> String -> IO Bool
checkFile opts file = do
        putStrLn $ "Reading \"" ++ file ++ "\""
        (net,properties) <- parseFile file
        putStrLn $ "Analyzing " ++ showNetName net
        when (optVerbose opts) (do
                putStrLn $ "Places: " ++ show (length  $ places net)
                putStrLn $ "Transitions: " ++ show (length $ transitions net)
            )
        rs <- mapM (checkProperty (optVerbose opts) net) properties
        putStrLn ""
        return $ and rs

checkProperty :: Bool -> PetriNet -> Property -> IO Bool
checkProperty verbose net p = do
        putStrLn $ "\nChecking " ++ showPropertyName p
        r <- case ptype p of
            Safety -> checkSafetyProperty verbose net (pformula p) []
            Liveness -> checkLivenessProperty verbose net (pformula p) []
        putStrLn $ if r then "Property is satisfied."
                        else "Property may not be satisfied."
        return r

checkSafetyProperty :: Bool -> PetriNet -> Formula -> [[String]] -> IO Bool
checkSafetyProperty verbose net f traps = do
94
95
96
97
98
        r <- checkSat $ checkStateEquationSat net f traps
        case r of
            Nothing -> return True
            Just a -> do
                let assigned = markedPlacesFromAssignment net a
99
100
                putStrLn "Assignment found"
                when verbose (putStrLn $ "Places marked: " ++ show assigned)
101
102
103
104
105
106
107
                rt <- checkSat $ checkTrapSat net assigned
                case rt of
                    Nothing -> do
                        putStrLn "No trap found."
                        return False
                    Just at -> do
                        let trap = trapFromAssignment at
108
109
110
                        putStrLn "Trap found"
                        when verbose (putStrLn $ "Places in trap: " ++ show trap)
                        checkSafetyProperty verbose net f (trap:traps)
111

112
113
checkLivenessProperty :: Bool -> PetriNet -> Formula -> [([String],[String])] -> IO Bool
checkLivenessProperty verbose net f strans = do
114
        r <- checkSat $ checkTransitionInvariantSat net f strans
Philipp Meyer's avatar
Philipp Meyer committed
115
        case r of
116
            Nothing -> return True
117
118
            Just ax -> do
                let fired = firedTransitionsFromAssignment ax
119
120
                putStrLn "Assignment found"
                when verbose (putStrLn $ "Transitions fired: " ++ show fired)
121
                rt <- checkSat $ checkSComponentSat net fired ax
122
123
124
125
                case rt of
                    Nothing -> do
                        putStrLn "No S-component found"
                        return False
126
                    Just as -> do
127
                        let sOutIn = getSComponentOutIn net ax as
128
129
130
                        putStrLn "S-component found"
                        when verbose (putStrLn $ "Out/In: " ++ show sOutIn)
                        checkLivenessProperty verbose net f (sOutIn:strans)
131

132
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
133
main = do
134
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
        args <- parseArgs
        case args of
            Left err -> exitErrorWith err
            Right (opts, files) -> do

                when (optShowVersion opts) (exitSuccessWith "Version 0.01")
                when (optShowHelp opts) (exitSuccessWith
                     (usageInfo "SLAPnet" options))
                when (null files) (exitErrorWith "No input file given")
                rs <- mapM (checkFile opts) files
                if and rs then
                    exitSuccessWith "All properties satisfied."
                else
                    exitFailureWith "Some properties may not be satisfied."

exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
        exitSuccess

exitFailureWith :: String -> IO ()
exitFailureWith msg = do
        putStrLn msg
        exitWith $ ExitFailure 1
Philipp Meyer's avatar
Philipp Meyer committed
159

160
161
162
163
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
        exitWith $ ExitFailure 2