Main.hs 16.6 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 ((<$>))
11
import Control.Arrow (first)
Philipp Meyer's avatar
Philipp Meyer committed
12
import Data.List (partition)
Philipp Meyer's avatar
Philipp Meyer committed
13

14
15
import Parser
import qualified Parser.PNET as PNET
Philipp Meyer's avatar
Philipp Meyer committed
16
import qualified Parser.LOLA as LOLA
17
import qualified Parser.TPN as TPN
18
import qualified Parser.MIST as MIST
19
import PetriNet
20
import Printer
21
22
import qualified Printer.LOLA as LOLAPrinter
import qualified Printer.SARA as SARAPrinter
23
import Property
24
import Solver
25
26
import Solver.StateEquation
import Solver.TrapConstraints
27
28
import Solver.TransitionInvariant
import Solver.SComponent
29

30
data InputFormat = PNET | LOLA | TPN | MIST deriving (Show,Read)
31

32
33
data NetTransformation = TerminationByReachability
                       | ValidateIdentifiers
34

35
data ImplicitProperty = Termination
36
                      | DeadlockFree | DeadlockFreeUnlessFinal
Philipp Meyer's avatar
Philipp Meyer committed
37
                      | ProperTermination
38
39
40
                      | Safe | Bounded Integer
                      deriving (Show,Read)

41
data Options = Options { inputFormat :: InputFormat
42
                       , optVerbosity :: Int
43
44
                       , optShowHelp :: Bool
                       , optShowVersion :: Bool
45
                       , optProperties :: [ImplicitProperty]
46
                       , optTransformations :: [NetTransformation]
47
                       , optRefine :: Bool
48
                       , optOutput :: Maybe String
49
                       , optUseProperties :: Bool
50
51
52
53
                       }

startOptions :: Options
startOptions = Options { inputFormat = PNET
54
                       , optVerbosity = 1
55
56
                       , optShowHelp = False
                       , optShowVersion = False
57
                       , optProperties = []
58
                       , optTransformations = []
59
                       , optRefine = True
60
                       , optOutput = Nothing
61
                       , optUseProperties = True
62
63
64
65
                       }

options :: [ OptDescr (Options -> Either String Options) ]
options =
66
67
68
69
70
71
72
73
74
75
76
        [ 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"
77

78
79
80
81
        , Option "" ["spec"]
        (NoArg (\opt -> Right opt { inputFormat = MIST }))
        "Use the mist input format"

82
83
84
85
86
87
        , Option "" ["validate-identifiers"]
        (NoArg (\opt -> Right opt {
            optTransformations = ValidateIdentifiers : optTransformations opt
          }))
        "Make identifiers valid for lola"

88
        , Option "" ["termination-by-reachability"]
89
        (NoArg (\opt -> Right opt {
90
            optTransformations = TerminationByReachability : optTransformations opt
91
          }))
92
        "Prove termination by reducing it to reachability"
93

94
        , Option "" ["terminating"]
95
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
96
                   optProperties = Termination : optProperties opt
97
               }))
98
        "Prove that the net is terminating"
99

Philipp Meyer's avatar
Philipp Meyer committed
100
101
102
103
104
105
        , Option "" ["proper-termination"]
        (NoArg (\opt -> Right opt {
                   optProperties = ProperTermination : optProperties opt
               }))
        "Prove termination in the final marking"

106
        , Option "" ["deadlock-free"]
107
        (NoArg (\opt -> Right opt {
108
                   optProperties = DeadlockFree : optProperties opt
109
               }))
110
        "Prove that the net is deadlock-free"
111

112
        , Option "" ["deadlock-free-unless-final"]
Philipp Meyer's avatar
Philipp Meyer committed
113
        (NoArg (\opt -> Right opt {
114
                   optProperties = DeadlockFreeUnlessFinal : optProperties opt
Philipp Meyer's avatar
Philipp Meyer committed
115
               }))
116
117
        ("Prove that the net is deadlock-free\n" ++
         "unless it is in the final marking")
Philipp Meyer's avatar
Philipp Meyer committed
118

119
120
        , Option "" ["safe"]
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
121
                   optProperties = Safe : optProperties opt
122
123
124
125
126
127
128
129
130
131
132
133
               }))
        "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"

134
135
136
137
        , Option "n" ["no-refinement"]
        (NoArg (\opt -> Right opt { optRefine = False }))
        "Don't use refinement"

138
139
140
141
142
143
144
        , Option "o" ["output"]
        (ReqArg (\arg opt -> Right opt {
                        optOutput = Just arg
                })
                "FILE")
        "Write net and properties to FILE"

145
146
147
148
149
150
        , Option "" ["no-given-properties"]
        (NoArg (\opt -> Right opt {
                   optUseProperties = False
               }))
        "Do not use the properties given in the input file"

151
        , Option "v" ["verbose"]
152
153
154
155
156
157
        (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)"
158
159
160
161
162
163
164
165
166
167

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

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

168
169
170
171
verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
        when (verbosity >= level) (putStrLn str)

172
173
174
175
176
177
178
179
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

180
181
182
writeFiles :: Int -> String -> PetriNet -> [Property] -> IO ()
writeFiles verbosity basename net props = do
        verbosePut verbosity 1 $ "Writing " ++ showNetName net ++ " to " ++ basename
183
        writeFile basename $ LOLAPrinter.printNet net
184
185
186
187
        mapM_ (\(p,i) -> do
                let file = basename ++ ".task" ++ show i
                verbosePut verbosity 1 $ "Writing " ++ showPropertyName p ++
                                         " to " ++ file
188
                writeFile file $ LOLAPrinter.printProperty p
189
              ) (zip props [(1::Integer)..])
190
191
192
        verbosePut verbosity 1 $ "Writing properties to " ++ basename ++ ".sara"
        writeFile (basename ++ ".sara") $ unlines $
                map (SARAPrinter.printProperty basename net) props
193

194
checkFile :: Parser (PetriNet,[Property]) -> Int -> Bool ->
195
            [ImplicitProperty] -> [NetTransformation] ->
196
            Bool -> Maybe String -> String -> IO Bool
197
checkFile parser verbosity refine implicitProperties transformations
198
          useProperties output file = do
199
        verbosePut verbosity 0 $ "Reading \"" ++ file ++ "\""
200
        (net,props) <- parseFile parser file
201
202
203
        let props' = if useProperties then props else []
        let props'' = props' ++ map (makeImplicitProperty net) implicitProperties
        let (net',props''') = foldl transformNet (net,props'') transformations
204
205
206
207
208
        verbosePut verbosity 1 $ "Analyzing " ++ showNetName net
        verbosePut verbosity 2 $
                "Places: " ++ show (length  $ places net') ++ "; " ++
                "Transitions: " ++ show (length $ transitions net')
        verbosePut verbosity 3 $ show net'
209
        rs <- mapM (checkProperty verbosity net' refine) props'''
210
        case output of
211
            Just outputfile -> writeFiles verbosity outputfile net' props'''
212
            Nothing -> return ()
213
        verbosePut verbosity 0 ""
214
215
        return $ and rs

216
placeOp :: Op -> (String, Integer) -> Formula
217
placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w)
218

219
220
transformNet :: (PetriNet, [Property]) -> NetTransformation ->
               (PetriNet, [Property])
221
transformNet (net, props) TerminationByReachability =
222
223
224
225
        let prime = ('\'':)
            ps = ["'sigma", "'m1", "'m2"] ++
                 places net ++ map prime (places net)
            is = [("'m1", 1)] ++
226
                 initials net ++ map (first prime) (initials net)
227
228
229
230
231
232
233
234
235
236
            transformTransition t =
                let (preT, postT) = context net t
                    pre'  = [("'m1",1)] ++ preT  ++ map (first prime) preT
                    post' = [("'m1",1)] ++ postT ++ map (first prime) postT
                    pre''  = ("'m2",1) : map (first prime) preT
                    post'' = [("'m2",1), ("'sigma",1)] ++ map (first prime) postT
                in  if t `elem` ghostTransitions net then
                        [(t, pre', post')]
                    else
                        [(t, pre', post'), (prime t, pre'', post'')]
237
            ts = ("'switch", [("'m1",1)], [("'m2",1)]) :
238
239
                 concatMap transformTransition (transitions net)
            gs = ghostTransitions net
240
241
            prop = Property "termination by reachability" Safety $
                    foldl (:&:) (Atom (LinIneq (Var "'sigma") Ge (Const 1)))
242
243
                      (map (\p -> Atom (LinIneq
                                (Var (prime p) :-: Var p) Ge (Const 0)))
244
                        (places net))
245
            -- TODO: map existing liveness properties
246
        in  (makePetriNetWithTrans (name net) ps ts is gs, prop : props)
247
transformNet (net, props) ValidateIdentifiers =
248
249
250
251
        let ps = map validateId $ places net
            ts = map validateId $ transitions net
            is = map (first validateId) $ initials net
            as = map (\(a,b,x) -> (validateId a, validateId b, x)) $ arcs net
252
253
            gs = map validateId $ ghostTransitions net
            net' = makePetriNet (name net) ps ts as is gs
254
            props' = map (rename validateId) props
255
        in  (net', props')
256

257
makeImplicitProperty :: PetriNet -> ImplicitProperty -> Property
258
259
260
261
262
makeImplicitProperty net Termination =
        Property "termination" Liveness $
            foldl (:&:) FTrue
                (map (\t -> Atom (LinIneq (Var t) Eq (Const 0)))
                    (ghostTransitions net))
263
makeImplicitProperty net ProperTermination =
Philipp Meyer's avatar
Philipp Meyer committed
264
        let (finals, nonfinals) = partition (null . lpost net) (places net)
265
        in  Property "proper termination" Safety
Philipp Meyer's avatar
Philipp Meyer committed
266
267
            (foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) finals) :&:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals))
268
269
makeImplicitProperty net DeadlockFree =
        Property "deadlock-free" Safety $
270
271
272
            foldl (:&:) FTrue
                (map (foldl (:|:) FFalse . map (placeOp Lt) . lpre net)
                     (transitions net))
273
274
makeImplicitProperty net DeadlockFreeUnlessFinal =
        let nodeadlock = makeImplicitProperty net DeadlockFree
275
            (finals, nonfinals) = partition (null . lpost net) (places net)
276
        in  Property "deadlock-free unless final" Safety $
Philipp Meyer's avatar
Philipp Meyer committed
277
278
279
            (foldl (:&:) FTrue  (map (\p -> placeOp Eq (p,0)) finals) :|:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals)) :&:
            pformula nodeadlock
280
makeImplicitProperty net (Bounded k) =
281
        Property (show k ++ "-bounded") Safety $
282
283
            foldl (:|:) FFalse
                (map (\p -> placeOp Gt (p,k)) (places net))
284
285
286
makeImplicitProperty net Safe =
        let bounded = makeImplicitProperty net (Bounded 1)
        in  Property "safe" Safety $ pformula bounded
287

288
289
290
checkProperty :: Int -> PetriNet -> Bool -> Property -> IO Bool
checkProperty verbosity net refine p = do
        verbosePut verbosity 1 $ "\nChecking " ++ showPropertyName p
291
        verbosePut verbosity 3 $ show p
292
        r <- case ptype p of
293
294
295
            Safety -> checkSafetyProperty verbosity net refine (pformula p) []
            Liveness -> checkLivenessProperty verbosity net refine (pformula p) []
        verbosePut verbosity 0 $ showPropertyName p ++
296
                                    if r then " is satisfied."
297
                                    else " may not be satisfied."
298
299
        return r

300
checkSafetyProperty :: Int -> PetriNet -> Bool ->
301
        Formula -> [[String]] -> IO Bool
302
checkSafetyProperty verbosity net refine f traps = do
303
304
305
306
307
        r <- checkSat $ checkStateEquationSat net f traps
        case r of
            Nothing -> return True
            Just a -> do
                let assigned = markedPlacesFromAssignment net a
308
309
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Places marked: " ++ show assigned
310
                verbosePut verbosity 3 $ "Assignment: " ++ show a
311
312
313
314
                if refine then do
                    rt <- checkSat $ checkTrapSat net assigned
                    case rt of
                        Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
315
                            verbosePut verbosity 1 "No trap found."
316
317
318
                            return False
                        Just at -> do
                            let trap = trapFromAssignment at
319
320
321
                            verbosePut verbosity 1 "Trap found"
                            verbosePut verbosity 2 $ "Places in trap: " ++
                                                      show trap
322
323
                            verbosePut verbosity 3 $ "Trap assignment: " ++
                                                      show at
324
                            checkSafetyProperty verbosity net refine f
325
326
327
328
                                                (trap:traps)
                else
                    return False

329
checkLivenessProperty :: Int -> PetriNet -> Bool ->
330
        Formula -> [([String],[String])] -> IO Bool
331
checkLivenessProperty verbosity net refine f strans = do
332
        r <- checkSat $ checkTransitionInvariantSat net f strans
Philipp Meyer's avatar
Philipp Meyer committed
333
        case r of
334
            Nothing -> return True
335
336
            Just ax -> do
                let fired = firedTransitionsFromAssignment ax
337
338
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Transitions fired: " ++ show fired
339
                verbosePut verbosity 3 $ "Assignment: " ++ show ax
340
341
342
343
                if refine then do
                    rt <- checkSat $ checkSComponentSat net fired ax
                    case rt of
                        Nothing -> do
344
                            verbosePut verbosity 1 "No S-component found"
345
346
347
                            return False
                        Just as -> do
                            let sOutIn = getSComponentOutIn net ax as
348
349
                            verbosePut verbosity 1 "S-component found"
                            verbosePut verbosity 2 $ "Out/In: " ++ show sOutIn
350
351
                            verbosePut verbosity 3 $ "S-Component assignment: " ++
                                                      show as
352
                            checkLivenessProperty verbosity net refine f
353
354
355
                                                  (sOutIn:strans)
                else
                    return False
356

357
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
358
main = do
359
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
360
361
362
363
364
365
366
367
        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")
368
369
                let verbosity = optVerbosity opts
                    refinement = optRefine opts
370
371
                let parser = case inputFormat opts of
                                 PNET -> PNET.parseContent
Philipp Meyer's avatar
Philipp Meyer committed
372
                                 LOLA -> LOLA.parseContent
373
                                 TPN -> TPN.parseContent
374
                                 MIST -> MIST.parseContent
375
376
377
                let properties = reverse $ optProperties opts
                let transformations = reverse $ optTransformations opts
                rs <- mapM (checkFile parser verbosity refinement properties
378
379
                     transformations (optUseProperties opts) (optOutput opts))
                     files
380
381
382
383
384
385
386
387
388
389
390
391
392
                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
393
        exitWith $ ExitFailure 2
Philipp Meyer's avatar
Philipp Meyer committed
394

395
396
397
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
398
        exitWith $ ExitFailure 3