Main.hs 12.3 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
import System.IO
import System.Console.GetOpt
import Control.Monad
10
import Control.Applicative ((<$>))
Philipp Meyer's avatar
Philipp Meyer committed
11
import Data.List (partition)
Philipp Meyer's avatar
Philipp Meyer committed
12

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

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

27
data ImplicitProperty = Termination
28
                      | NoDeadlock | NoDeadlockUnless String
Philipp Meyer's avatar
Philipp Meyer committed
29
30
31
                      | NoDeadlockUnlessFinal
                      | ProperTermination
                      | Workflow
32
33
34
                      | Safe | Bounded Integer
                      deriving (Show,Read)

35
data Options = Options { inputFormat :: InputFormat
36
                       , optVerbosity :: Int
37
38
                       , optShowHelp :: Bool
                       , optShowVersion :: Bool
39
                       , optProperties :: [ImplicitProperty]
40
                       , optRefine :: Bool
41
42
43
44
                       }

startOptions :: Options
startOptions = Options { inputFormat = PNET
45
                       , optVerbosity = 1
46
47
                       , optShowHelp = False
                       , optShowVersion = False
48
                       , optProperties = []
49
                       , optRefine = True
50
51
52
53
                       }

options :: [ OptDescr (Options -> Either String Options) ]
options =
54
55
56
57
58
59
60
61
62
63
64
        [ 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"
65

Philipp Meyer's avatar
Philipp Meyer committed
66
67
68
69
70
71
        , Option "" ["workflow"]
        (NoArg (\opt -> Right opt {
                   optProperties = Workflow : optProperties opt
               }))
        "Check that the net is a workflow net"

72
        , Option "" ["termination"]
73
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
74
                   optProperties = Termination : optProperties opt
75
               }))
76
77
        "Prove termination"

Philipp Meyer's avatar
Philipp Meyer committed
78
79
80
81
82
83
        , Option "" ["proper-termination"]
        (NoArg (\opt -> Right opt {
                   optProperties = ProperTermination : optProperties opt
               }))
        "Prove termination in the final marking"

84
85
        , Option "" ["no-deadlock"]
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
86
                   optProperties = NoDeadlock : optProperties opt
87
88
89
               }))
        "Prove that there is no deadlock"

Philipp Meyer's avatar
Philipp Meyer committed
90
91
92
93
94
95
96
        , Option "" ["no-deadlock-unless-final"]
        (NoArg (\opt -> Right opt {
                   optProperties = NoDeadlockUnlessFinal : optProperties opt
               }))
        ("Prove that there is no deadlock unless\n" ++
         "only final places are marked")

97
        , Option "" ["no-deadlock-unless"]
98
        (ReqArg (\arg opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
99
                   optProperties = NoDeadlockUnless arg : optProperties opt
100
                })
101
                "FILE")
Philipp Meyer's avatar
Philipp Meyer committed
102
103
        ("Prove that there is no deadlock unless\n" ++
         "the formula given in FILE is satisfied")
104
105
106

        , Option "" ["safe"]
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
107
                   optProperties = Safe : optProperties opt
108
109
110
111
112
113
114
115
116
117
118
119
               }))
        "Prove that the net is safe, i.e. 1-bounded"

        , Option "" ["bounded"]
        (ReqArg (\arg opt -> case reads arg of
                    [(k, "")] -> Right opt {
                           optProperties = Bounded k : optProperties opt }
                    _ -> Left ("invalid argument for k-bounded option: " ++ arg)
                )
                "K")
        "Prove that the net is K-bounded"

120
121
122
123
        , Option "n" ["no-refinement"]
        (NoArg (\opt -> Right opt { optRefine = False }))
        "Don't use refinement"

124
        , Option "v" ["verbose"]
125
126
127
128
129
130
        (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)"
131
132
133
134
135
136
137
138
139
140

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

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

141
142
143
144
verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
        when (verbosity >= level) (putStrLn str)

145
146
147
148
149
150
151
152
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

153
154
155
checkFile :: Parser (PetriNet,[Property]) -> Int -> Bool ->
            [ImplicitProperty] -> String -> IO Bool
checkFile parser verbosity refine implicitProperties file = do
156
        verbosePut verbosity 0 $ "Reading \"" ++ file ++ "\""
157
        (net,properties) <- parseFile parser file
158
159
160
161
        verbosePut verbosity 1 $ "Analyzing " ++ showNetName net
        verbosePut verbosity 2 $
                "Places: " ++ show (length  $ places net) ++ "\n" ++
                "Transitions: " ++ show (length $ transitions net)
162
        addedProperties <- mapM (makeImplicitProperty net) implicitProperties
163
        rs <- mapM (checkProperty verbosity net refine)
164
                  (addedProperties ++ properties)
165
        verbosePut verbosity 0 ""
166
167
        return $ and rs

168
placeOp :: Op -> (String, Integer) -> Formula
169
placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w)
170

171
makeImplicitProperty :: PetriNet -> ImplicitProperty -> IO Property
Philipp Meyer's avatar
Philipp Meyer committed
172
173
174
175
176
177
178
179
180
makeImplicitProperty net Workflow = do
        let sources = filter (null . lpre net) (places net)
        let sinks = filter (null . lpost net) (places net)
        putStrLn "Sources:"
        print sources
        putStrLn "Sinks:"
        print sinks
        return $ Property "workflow" Safety $
            if length sources == 1 && length sinks == 1 then FFalse else FTrue
181
182
makeImplicitProperty _ Termination =
        return $ Property "termination" Liveness FTrue
Philipp Meyer's avatar
Philipp Meyer committed
183
184
185
186
187
makeImplicitProperty net ProperTermination = do
        let (finals, nonfinals) = partition (null . lpost net) (places net)
        return $ Property "proper termination" Safety
            (foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) finals) :&:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals))
188
makeImplicitProperty net NoDeadlock =
189
        return $ Property "no deadlock" Safety $
190
191
192
            foldl (:&:) FTrue
                (map (foldl (:|:) FFalse . map (placeOp Lt) . lpre net)
                     (transitions net))
Philipp Meyer's avatar
Philipp Meyer committed
193
194
195
196
197
198
199
makeImplicitProperty net NoDeadlockUnlessFinal = do
        nodeadlock <- makeImplicitProperty net NoDeadlock
        let (finals, nonfinals) = partition (null . lpost net) (places net)
        return $ Property "no deadlock unless final" Safety $
            (foldl (:&:) FTrue  (map (\p -> placeOp Eq (p,0)) finals) :|:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals)) :&:
            pformula nodeadlock
200
201
202
203
204
makeImplicitProperty net (NoDeadlockUnless file) = do
        nodeadlock <- makeImplicitProperty net NoDeadlock
        property <- parseFile LOLA.parseFormula file
        return $ Property "no deadlock unless" Safety $
            Neg property :&: pformula nodeadlock
205
makeImplicitProperty net (Bounded k) =
206
        return $ Property (show k ++ "-bounded") Safety $
207
208
            foldl (:|:) FFalse
                (map (\p -> placeOp Gt (p,k)) (places net))
209
210
211
makeImplicitProperty net Safe = do
        bounded <- makeImplicitProperty net (Bounded 1)
        return $ Property "safe" Safety $ pformula bounded
212

213
214
215
checkProperty :: Int -> PetriNet -> Bool -> Property -> IO Bool
checkProperty verbosity net refine p = do
        verbosePut verbosity 1 $ "\nChecking " ++ showPropertyName p
216
        r <- case ptype p of
217
218
219
            Safety -> checkSafetyProperty verbosity net refine (pformula p) []
            Liveness -> checkLivenessProperty verbosity net refine (pformula p) []
        verbosePut verbosity 0 $ showPropertyName p ++
220
                                    if r then " is satisfied."
221
                                    else " may not be satisfied."
222
223
        return r

224
checkSafetyProperty :: Int -> PetriNet -> Bool ->
225
        Formula -> [[String]] -> IO Bool
226
checkSafetyProperty verbosity net refine f traps = do
227
228
229
230
231
        r <- checkSat $ checkStateEquationSat net f traps
        case r of
            Nothing -> return True
            Just a -> do
                let assigned = markedPlacesFromAssignment net a
232
233
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Places marked: " ++ show assigned
234
235
236
237
238
239
240
241
                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
242
243
244
245
                            verbosePut verbosity 1 "Trap found"
                            verbosePut verbosity 2 $ "Places in trap: " ++
                                                      show trap
                            checkSafetyProperty verbosity net refine f
246
247
248
249
                                                (trap:traps)
                else
                    return False

250
checkLivenessProperty :: Int -> PetriNet -> Bool ->
251
        Formula -> [([String],[String])] -> IO Bool
252
checkLivenessProperty verbosity net refine f strans = do
253
        r <- checkSat $ checkTransitionInvariantSat net f strans
Philipp Meyer's avatar
Philipp Meyer committed
254
        case r of
255
            Nothing -> return True
256
257
            Just ax -> do
                let fired = firedTransitionsFromAssignment ax
258
259
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Transitions fired: " ++ show fired
260
261
262
263
                if refine then do
                    rt <- checkSat $ checkSComponentSat net fired ax
                    case rt of
                        Nothing -> do
264
                            verbosePut verbosity 1 "No S-component found"
265
266
267
                            return False
                        Just as -> do
                            let sOutIn = getSComponentOutIn net ax as
268
269
270
                            verbosePut verbosity 1 "S-component found"
                            verbosePut verbosity 2 $ "Out/In: " ++ show sOutIn
                            checkLivenessProperty verbosity net refine f
271
272
273
                                                  (sOutIn:strans)
                else
                    return False
274

275
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
276
main = do
277
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
278
279
280
281
282
283
284
285
        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")
286
287
                let verbosity = optVerbosity opts
                    refinement = optRefine opts
288
289
                let parser = case inputFormat opts of
                                 PNET -> PNET.parseContent
Philipp Meyer's avatar
Philipp Meyer committed
290
                                 LOLA -> LOLA.parseContent
291
                                 TPN -> TPN.parseContent
292
                let properties = optProperties opts
293
294
                rs <- mapM (checkFile parser verbosity refinement properties)
                          files
295
296
297
298
299
300
301
302
303
304
305
306
307
                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
308
        exitWith $ ExitFailure 2
Philipp Meyer's avatar
Philipp Meyer committed
309

310
311
312
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
313
        exitWith $ ExitFailure 3