Main.hs 8.01 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
import System.IO
import System.Console.GetOpt
import Control.Monad
import Control.Applicative
Philipp Meyer's avatar
Philipp Meyer committed
11

12
13
import Parser
import qualified Parser.PNET as PNET
Philipp Meyer's avatar
Philipp Meyer committed
14
import qualified Parser.LOLA as LOLA
15
import qualified Parser.TPN as TPN
16
17
import PetriNet
import Property
18
import Solver
19
20
import Solver.StateEquation
import Solver.TrapConstraints
21
22
import Solver.TransitionInvariant
import Solver.SComponent
23

24
25
26
data InputFormat = PNET | LOLA | TPN deriving (Show,Read)

data Options = Options { inputFormat :: InputFormat
27
                       , optVerbosity :: Int
28
29
                       , optShowHelp :: Bool
                       , optShowVersion :: Bool
30
                       , proveTermination :: Bool
31
                       , optRefine :: Bool
32
33
34
35
                       }

startOptions :: Options
startOptions = Options { inputFormat = PNET
36
                       , optVerbosity = 1
37
38
                       , optShowHelp = False
                       , optShowVersion = False
39
                       , proveTermination = False
40
                       , optRefine = True
41
42
43
44
                       }

options :: [ OptDescr (Options -> Either String Options) ]
options =
45
46
47
48
49
50
51
52
53
54
55
        [ Option "" ["pnet"]
        (NoArg (\opt -> Right opt { inputFormat = PNET }))
        "Use the pnet input format"

        , Option "" ["lola"]
        (NoArg (\opt -> Right opt { inputFormat = LOLA }))
        "Use the lola input format"

        , Option "" ["tpn"]
        (NoArg (\opt -> Right opt { inputFormat = TPN }))
        "Use the tpn input format"
56

57
58
59
60
        , Option "" ["termination"]
        (NoArg (\opt -> Right opt { proveTermination = True }))
        "Prove termination"

61
62
63
64
        , Option "n" ["no-refinement"]
        (NoArg (\opt -> Right opt { optRefine = False }))
        "Don't use refinement"

65
        , Option "v" ["verbose"]
66
67
68
69
70
71
        (NoArg (\opt -> Right opt { optVerbosity = optVerbosity opt + 1 }))
        "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)"
72
73
74
75
76
77
78
79
80
81

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

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

82
83
84
85
verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
        when (verbosity >= level) (putStrLn str)

86
87
88
89
90
91
92
93
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

94
checkFile :: Parser (PetriNet,[Property]) -> Int -> Bool -> [Property] ->
95
            String -> IO Bool
96
97
checkFile parser verbosity refine addedProperties file = do
        verbosePut verbosity 0 $ "Reading \"" ++ file ++ "\""
98
        (net,properties) <- parseFile parser file
99
100
101
102
103
        verbosePut verbosity 1 $ "Analyzing " ++ showNetName net
        verbosePut verbosity 2 $
                "Places: " ++ show (length  $ places net) ++ "\n" ++
                "Transitions: " ++ show (length $ transitions net)
        rs <- mapM (checkProperty verbosity net refine)
104
                  (addedProperties ++ properties)
105
        verbosePut verbosity 0 ""
106
107
        return $ and rs

108
109
110
checkProperty :: Int -> PetriNet -> Bool -> Property -> IO Bool
checkProperty verbosity net refine p = do
        verbosePut verbosity 1 $ "\nChecking " ++ showPropertyName p
111
        r <- case ptype p of
112
113
114
115
116
            Safety -> checkSafetyProperty verbosity net refine (pformula p) []
            Liveness -> checkLivenessProperty verbosity net refine (pformula p) []
        verbosePut verbosity 0 $ showPropertyName p ++
                                    if r then "is satisfied."
                                    else " may not be satisfied."
117
118
        return r

119
checkSafetyProperty :: Int -> PetriNet -> Bool ->
120
        Formula -> [[String]] -> IO Bool
121
checkSafetyProperty verbosity net refine f traps = do
122
123
124
125
126
        r <- checkSat $ checkStateEquationSat net f traps
        case r of
            Nothing -> return True
            Just a -> do
                let assigned = markedPlacesFromAssignment net a
127
128
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Places marked: " ++ show assigned
129
130
131
132
133
134
135
136
                if refine then do
                    rt <- checkSat $ checkTrapSat net assigned
                    case rt of
                        Nothing -> do
                            putStrLn "No trap found."
                            return False
                        Just at -> do
                            let trap = trapFromAssignment at
137
138
139
140
                            verbosePut verbosity 1 "Trap found"
                            verbosePut verbosity 2 $ "Places in trap: " ++
                                                      show trap
                            checkSafetyProperty verbosity net refine f
141
142
143
144
                                                (trap:traps)
                else
                    return False

145
checkLivenessProperty :: Int -> PetriNet -> Bool ->
146
        Formula -> [([String],[String])] -> IO Bool
147
checkLivenessProperty verbosity net refine f strans = do
148
        r <- checkSat $ checkTransitionInvariantSat net f strans
Philipp Meyer's avatar
Philipp Meyer committed
149
        case r of
150
            Nothing -> return True
151
152
            Just ax -> do
                let fired = firedTransitionsFromAssignment ax
153
154
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Transitions fired: " ++ show fired
155
156
157
158
                if refine then do
                    rt <- checkSat $ checkSComponentSat net fired ax
                    case rt of
                        Nothing -> do
159
                            verbosePut verbosity 1 "No S-component found"
160
161
162
                            return False
                        Just as -> do
                            let sOutIn = getSComponentOutIn net ax as
163
164
165
                            verbosePut verbosity 1 "S-component found"
                            verbosePut verbosity 2 $ "Out/In: " ++ show sOutIn
                            checkLivenessProperty verbosity net refine f
166
167
168
                                                  (sOutIn:strans)
                else
                    return False
169

170
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
171
main = do
172
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
173
174
175
176
177
178
179
180
        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")
181
182
                let verbosity = optVerbosity opts
                    refinement = optRefine opts
183
184
                let parser = case inputFormat opts of
                                 PNET -> PNET.parseContent
Philipp Meyer's avatar
Philipp Meyer committed
185
                                 LOLA -> LOLA.parseContent
186
                                 TPN -> TPN.parseContent
187
188
                let properties = [ Property "termination" Liveness FTrue
                                 | proveTermination opts ]
189
190
                rs <- mapM (checkFile parser verbosity refinement properties)
                          files
191
192
193
194
195
196
197
198
199
200
201
202
203
204
                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
205

206
207
208
209
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
        exitWith $ ExitFailure 2