Main.hs 22.1 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)
13
import qualified Data.ByteString.Lazy as L
Philipp Meyer's avatar
Philipp Meyer committed
14

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

34
data InputFormat = PNET | LOLA | TPN | MIST deriving (Show,Read)
35
data OutputFormat = OutLOLA | OutSARA | OutSPEC | OutDOT deriving (Show,Read)
36

37
38
data NetTransformation = TerminationByReachability
                       | ValidateIdentifiers
39

40
data ImplicitProperty = Termination
41
                      | DeadlockFree | DeadlockFreeUnlessFinal
Philipp Meyer's avatar
Philipp Meyer committed
42
                      | ProperTermination
43
                      | Safe | Bounded Integer
44
                      | StructFreeChoice
45
46
                      | StructParallel
                      | StructFinalPlace
47
                      | StructCommunicationFree
48
49
                      deriving (Show,Read)

50
data Options = Options { inputFormat :: InputFormat
51
                       , optVerbosity :: Int
52
53
                       , optShowHelp :: Bool
                       , optShowVersion :: Bool
54
                       , optProperties :: [ImplicitProperty]
55
                       , optTransformations :: [NetTransformation]
56
                       , optRefine :: Bool
57
                       , optOutput :: Maybe String
58
                       , outputFormat :: OutputFormat
59
                       , optUseProperties :: Bool
60
                       , optPrintStructure :: Bool
61
62
63
64
                       }

startOptions :: Options
startOptions = Options { inputFormat = PNET
65
                       , optVerbosity = 1
66
67
                       , optShowHelp = False
                       , optShowVersion = False
68
                       , optProperties = []
69
                       , optTransformations = []
70
                       , optRefine = True
71
                       , optOutput = Nothing
72
                       , outputFormat = OutLOLA
73
                       , optUseProperties = True
74
                       , optPrintStructure = False
75
76
77
78
                       }

options :: [ OptDescr (Options -> Either String Options) ]
options =
79
80
81
82
83
84
85
86
87
88
89
        [ 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"
90

91
92
93
94
        , Option "" ["spec"]
        (NoArg (\opt -> Right opt { inputFormat = MIST }))
        "Use the mist input format"

95
96
97
98
        , Option "s" ["structure"]
        (NoArg (\opt -> Right opt { optPrintStructure = True }))
        "Print structural information"

99
100
101
102
103
104
        , Option "" ["validate-identifiers"]
        (NoArg (\opt -> Right opt {
            optTransformations = ValidateIdentifiers : optTransformations opt
          }))
        "Make identifiers valid for lola"

105
        , Option "" ["termination-by-reachability"]
106
        (NoArg (\opt -> Right opt {
107
            optTransformations = TerminationByReachability : optTransformations opt
108
          }))
109
        "Prove termination by reducing it to reachability"
110

111
        , Option "" ["terminating"]
112
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
113
                   optProperties = Termination : optProperties opt
114
               }))
115
        "Prove that the net is terminating"
116

Philipp Meyer's avatar
Philipp Meyer committed
117
118
119
120
121
122
        , Option "" ["proper-termination"]
        (NoArg (\opt -> Right opt {
                   optProperties = ProperTermination : optProperties opt
               }))
        "Prove termination in the final marking"

123
        , Option "" ["deadlock-free"]
124
        (NoArg (\opt -> Right opt {
125
                   optProperties = DeadlockFree : optProperties opt
126
               }))
127
        "Prove that the net is deadlock-free"
128

129
        , Option "" ["deadlock-free-unless-final"]
Philipp Meyer's avatar
Philipp Meyer committed
130
        (NoArg (\opt -> Right opt {
131
                   optProperties = DeadlockFreeUnlessFinal : optProperties opt
Philipp Meyer's avatar
Philipp Meyer committed
132
               }))
133
134
        ("Prove that the net is deadlock-free\n" ++
         "unless it is in the final marking")
Philipp Meyer's avatar
Philipp Meyer committed
135

136
137
        , Option "" ["safe"]
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
138
                   optProperties = Safe : optProperties opt
139
140
141
142
143
144
145
146
147
148
149
150
               }))
        "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"

151
152
153
154
155
156
        , Option "" ["free-choice"]
        (NoArg (\opt -> Right opt {
                   optProperties = StructFreeChoice : optProperties opt
               }))
        "Prove that the net is free-choice"

157
158
159
160
161
162
163
164
165
166
167
168
        , Option "" ["parallel"]
        (NoArg (\opt -> Right opt {
                   optProperties = StructParallel : optProperties opt
               }))
        "Prove that the net has non-trivial parallellism"

        , Option "" ["final-place"]
        (NoArg (\opt -> Right opt {
                   optProperties = StructFinalPlace : optProperties opt
               }))
        "Prove that there is only one needed final place"

169
170
171
172
173
174
        , Option "" ["communication-free"]
        (NoArg (\opt -> Right opt {
                   optProperties = StructCommunicationFree : optProperties opt
               }))
        "Prove that the net is communication-free"

175
176
177
178
        , Option "n" ["no-refinement"]
        (NoArg (\opt -> Right opt { optRefine = False }))
        "Don't use refinement"

179
180
181
182
183
184
185
        , Option "o" ["output"]
        (ReqArg (\arg opt -> Right opt {
                        optOutput = Just arg
                })
                "FILE")
        "Write net and properties to FILE"

186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
        , Option "" ["out-lola"]
        (NoArg (\opt -> Right opt { outputFormat = OutLOLA }))
        "Use the lola output format"

        , Option "" ["out-sara"]
        (NoArg (\opt -> Right opt { outputFormat = OutSARA }))
        "Use the sara output format"

        , Option "" ["out-spec"]
        (NoArg (\opt -> Right opt { outputFormat = OutSPEC }))
        "Use the spec output format"

        , Option "" ["out-dot"]
        (NoArg (\opt -> Right opt { outputFormat = OutDOT }))
        "Use the dot output format"

202
203
204
205
206
207
        , Option "" ["no-given-properties"]
        (NoArg (\opt -> Right opt {
                   optUseProperties = False
               }))
        "Do not use the properties given in the input file"

208
        , Option "v" ["verbose"]
209
210
211
212
213
214
        (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)"
215
216
217
218
219
220
221
222
223
224

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

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

225
226
227
228
verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
        when (verbosity >= level) (putStrLn str)

229
230
231
232
233
234
235
236
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

237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
writeFiles :: Int -> String -> OutputFormat -> PetriNet -> [Property] -> IO ()
writeFiles verbosity basename format net props = do
        verbosePut verbosity 1 $ "Writing " ++ showNetName net ++ " to " ++
                                  basename ++ " in format " ++ show format
        case format of
            OutLOLA -> do
                L.writeFile basename $ LOLAPrinter.printNet net
                mapM_ (\(p,i) -> do
                        let file = basename ++ ".task" ++ show i
                        verbosePut verbosity 1 $ "Writing " ++ showPropertyName p
                                                 ++ " to " ++ file
                        L.writeFile file $ LOLAPrinter.printProperty p
                      ) (zip props [(1::Integer)..])
            OutSARA -> do
                L.writeFile basename $ LOLAPrinter.printNet net
                verbosePut verbosity 1 $ "Writing properties to " ++ basename ++
                                         ".sara"
                L.writeFile (basename ++ ".sara") $
                    SARAPrinter.printProperties basename net props
            OutSPEC ->
                mapM_ (\(p,i) -> do
                        let file = basename ++ ".target" ++ show i
                        verbosePut verbosity 1 $ "Writing " ++ showPropertyName p
                                                 ++ " to " ++ file
                        L.writeFile file $ SPECPrinter.printProperty p
                      ) (zip props [(1::Integer)..])
            OutDOT ->
                L.writeFile basename $ DOTPrinter.printNet net
265

266
267
268
269
270
271
272
273
274
275
276
277
278
structuralAnalysis :: PetriNet -> IO ()
structuralAnalysis net =  do
        let noGhost t = t `notElem` ghostTransitions net
        let initP  = filter (\x -> (not . any noGhost . pre net) x &&
                             (any noGhost . post net) x) (places net)
        let finalP = filter (\x -> (not . any noGhost . post net) x &&
                             (any noGhost . pre net) x) (places net)
        let isolP  = filter (\x -> (not . any noGhost . post net) x &&
                             (not . any noGhost . pre net) x) (places net)
        let initT  = filter (\t -> noGhost t && null (pre  net t))
                        (transitions net)
        let finalT = filter (\t -> noGhost t && null (post net t))
                        (transitions net)
279
280
        putStrLn $ "Places             : " ++ show (length (places net))
        putStrLn $ "Transitions        : " ++ show (length (transitions net))
281
282
283
284
285
286
        putStrLn $ "Initial places     : " ++ show (length initP)
        putStrLn $ "Initial transitions: " ++ show (length initT)
        putStrLn $ "Isolated places    : " ++ show (length isolP)
        putStrLn $ "Final places       : " ++ show (length finalP)
        putStrLn $ "Final transitions  : " ++ show (length finalT)

287
checkFile :: Parser (PetriNet,[Property]) -> Int -> Bool ->
288
            [ImplicitProperty] -> [NetTransformation] ->
289
290
            Bool -> Maybe String -> OutputFormat -> Bool -> String ->
            IO PropResult
291
checkFile parser verbosity refine implicitProperties transformations
292
          useProperties output format printStruct file = do
293
        verbosePut verbosity 0 $ "Reading \"" ++ file ++ "\""
294
        (net,props) <- parseFile parser file
295
296
297
        let props' = if useProperties then props else []
        let props'' = props' ++ map (makeImplicitProperty net) implicitProperties
        let (net',props''') = foldl transformNet (net,props'') transformations
298
299
300
301
        verbosePut verbosity 1 $ "Analyzing " ++ showNetName net
        verbosePut verbosity 2 $
                "Places: " ++ show (length  $ places net') ++ "; " ++
                "Transitions: " ++ show (length $ transitions net')
302
        when printStruct $ structuralAnalysis net
303
        verbosePut verbosity 3 $ show net'
304
        case output of
305
306
            Just outputfile ->
                writeFiles verbosity outputfile format net' props'''
307
            Nothing -> return ()
Philipp Meyer's avatar
Philipp Meyer committed
308
        -- TODO: short-circuit?
309
        rs <- mapM (checkProperty verbosity net' refine) props'''
310
        verbosePut verbosity 0 ""
311
        return $ resultsAnd rs
312

313
placeOp :: Op -> (String, Integer) -> Formula
314
placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w)
315

316
317
transformNet :: (PetriNet, [Property]) -> NetTransformation ->
               (PetriNet, [Property])
318
transformNet (net, props) TerminationByReachability =
319
320
321
322
        let prime = ('\'':)
            ps = ["'sigma", "'m1", "'m2"] ++
                 places net ++ map prime (places net)
            is = [("'m1", 1)] ++
323
                 initials net ++ map (first prime) (initials net)
324
325
326
327
328
329
330
331
332
333
            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'')]
334
            ts = ("'switch", [("'m1",1)], [("'m2",1)]) :
335
336
                 concatMap transformTransition (transitions net)
            gs = ghostTransitions net
337
            prop = Property "termination by reachability" $ Safety $
338
                    foldl (:&:) (Atom (LinIneq (Var "'sigma") Ge (Const 1)))
339
340
                      (map (\p -> Atom (LinIneq
                                (Var (prime p) :-: Var p) Ge (Const 0)))
341
                        (places net))
342
            -- TODO: map existing liveness properties
343
        in  (makePetriNetWithTrans (name net) ps ts is gs, prop : props)
344
transformNet (net, props) ValidateIdentifiers =
345
346
347
348
        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
349
350
            gs = map validateId $ ghostTransitions net
            net' = makePetriNet (name net) ps ts as is gs
351
            props' = map (rename validateId) props
352
        in  (net', props')
353

354
makeImplicitProperty :: PetriNet -> ImplicitProperty -> Property
355
makeImplicitProperty net Termination =
356
        Property "termination" $ Liveness $
357
358
359
            foldl (:&:) FTrue
                (map (\t -> Atom (LinIneq (Var t) Eq (Const 0)))
                    (ghostTransitions net))
360
makeImplicitProperty net ProperTermination =
Philipp Meyer's avatar
Philipp Meyer committed
361
        let (finals, nonfinals) = partition (null . lpost net) (places net)
362
        in  Property "proper termination" $ Safety
Philipp Meyer's avatar
Philipp Meyer committed
363
364
            (foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) finals) :&:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals))
365
makeImplicitProperty net DeadlockFree =
366
        Property "deadlock-free" $ Safety $
367
368
            foldl (:&:) FTrue
                (map (foldl (:|:) FFalse . map (placeOp Lt) . lpre net)
369
                     (filter (`notElem` ghostTransitions net) (transitions net)))
370
makeImplicitProperty net DeadlockFreeUnlessFinal =
371
        let (Property _ (Safety pf)) = makeImplicitProperty net DeadlockFree
372
            (finals, nonfinals) = partition (null . lpost net) (places net)
373
        in  Property "deadlock-free unless final" $ Safety $
Philipp Meyer's avatar
Philipp Meyer committed
374
375
            (foldl (:&:) FTrue  (map (\p -> placeOp Eq (p,0)) finals) :|:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals)) :&:
376
            pf
377
makeImplicitProperty net (Bounded k) =
378
        Property (show k ++ "-bounded") $ Safety $
379
            foldl (:|:) FFalse
Philipp Meyer's avatar
Philipp Meyer committed
380
                (map (\p -> placeOp Ge (p,k+1))
381
382
                    (filter (`notElem` concatMap (post net) (ghostTransitions net))
                        (places net)))
383
384
makeImplicitProperty net Safe =
        let bounded = makeImplicitProperty net (Bounded 1)
385
386
387
        in  Property "safe" $ pcont bounded
makeImplicitProperty _ StructFreeChoice =
        Property "free choice" $ Structural FreeChoice
388
389
390
391
makeImplicitProperty _ StructParallel =
        Property "parallel" $ Structural Parallel
makeImplicitProperty _ StructFinalPlace =
        Property "final place" $ Structural FinalPlace
392
393
makeImplicitProperty _ StructCommunicationFree =
        Property "communication free" $ Structural CommunicationFree
394

395
checkProperty :: Int -> PetriNet -> Bool -> Property -> IO PropResult
396
397
checkProperty verbosity net refine p = do
        verbosePut verbosity 1 $ "\nChecking " ++ showPropertyName p
398
        verbosePut verbosity 3 $ show p
399
400
401
402
403
404
405
406
407
        r <- case pcont p of
            (Safety pf) -> checkSafetyProperty verbosity net refine pf []
            (Liveness pf) -> checkLivenessProperty verbosity net refine pf []
            (Structural ps) -> checkStructuralProperty verbosity net ps
        verbosePut verbosity 0 $ showPropertyName p ++ " " ++
            case r of
                Satisfied -> "is satisfied."
                Unsatisfied -> "is not satisfied."
                Unknown-> "may not be satisfied."
408
409
        return r

410
checkSafetyProperty :: Int -> PetriNet -> Bool ->
411
        Formula -> [[String]] -> IO PropResult
412
checkSafetyProperty verbosity net refine f traps = do
413
414
        r <- checkSat $ checkStateEquationSat net f traps
        case r of
415
            Nothing -> return Satisfied
416
417
            Just a -> do
                let assigned = markedPlacesFromAssignment net a
418
419
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Places marked: " ++ show assigned
420
                verbosePut verbosity 3 $ "Assignment: " ++ show a
421
422
423
424
                if refine then do
                    rt <- checkSat $ checkTrapSat net assigned
                    case rt of
                        Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
425
                            verbosePut verbosity 1 "No trap found."
426
                            return Unknown
427
428
                        Just at -> do
                            let trap = trapFromAssignment at
429
430
431
                            verbosePut verbosity 1 "Trap found"
                            verbosePut verbosity 2 $ "Places in trap: " ++
                                                      show trap
432
433
                            verbosePut verbosity 3 $ "Trap assignment: " ++
                                                      show at
434
                            checkSafetyProperty verbosity net refine f
435
436
                                                (trap:traps)
                else
437
                    return Unknown
438

439
checkLivenessProperty :: Int -> PetriNet -> Bool ->
440
        Formula -> [([String],[String])] -> IO PropResult
441
checkLivenessProperty verbosity net refine f strans = do
442
        r <- checkSat $ checkTransitionInvariantSat net f strans
Philipp Meyer's avatar
Philipp Meyer committed
443
        case r of
444
            Nothing -> return Satisfied
445
446
            Just ax -> do
                let fired = firedTransitionsFromAssignment ax
447
448
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Transitions fired: " ++ show fired
449
                verbosePut verbosity 3 $ "Assignment: " ++ show ax
450
451
452
453
                if refine then do
                    rt <- checkSat $ checkSComponentSat net fired ax
                    case rt of
                        Nothing -> do
454
                            verbosePut verbosity 1 "No S-component found"
455
                            return Unknown
456
457
                        Just as -> do
                            let sOutIn = getSComponentOutIn net ax as
458
459
                            verbosePut verbosity 1 "S-component found"
                            verbosePut verbosity 2 $ "Out/In: " ++ show sOutIn
460
461
                            verbosePut verbosity 3 $ "S-Component assignment: " ++
                                                      show as
462
                            checkLivenessProperty verbosity net refine f
463
464
                                                  (sOutIn:strans)
                else
465
466
467
                    return Unknown

checkStructuralProperty :: Int -> PetriNet -> Structure -> IO PropResult
468
checkStructuralProperty _ net struct =
469
470
471
472
        if checkStructure net struct then
            return Satisfied
        else
            return Unsatisfied
473

474
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
475
main = do
476
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
477
478
479
480
481
482
483
484
        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")
485
486
                let verbosity = optVerbosity opts
                    refinement = optRefine opts
487
488
                let parser = case inputFormat opts of
                                 PNET -> PNET.parseContent
Philipp Meyer's avatar
Philipp Meyer committed
489
                                 LOLA -> LOLA.parseContent
490
                                 TPN -> TPN.parseContent
491
                                 MIST -> MIST.parseContent
492
493
494
                let properties = reverse $ optProperties opts
                let transformations = reverse $ optTransformations opts
                rs <- mapM (checkFile parser verbosity refinement properties
495
                     transformations (optUseProperties opts) (optOutput opts)
496
                     (outputFormat opts) (optPrintStructure opts)) files
Philipp Meyer's avatar
Philipp Meyer committed
497
                -- TODO: short-circuit with Control.Monad.Loops?
498
499
500
501
502
503
504
                case resultsAnd rs of
                    Satisfied ->
                        exitSuccessWith "All properties satisfied."
                    Unsatisfied ->
                        exitFailureWith "Some properties are not satisfied"
                    Unknown ->
                        exitFailureWith "Some properties may not be satisfied."
505

Philipp Meyer's avatar
Philipp Meyer committed
506
-- TODO: Always exit with exit code 0 unless an error occured
507
508
509
510
511
512
513
514
exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
        exitSuccess

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

517
518
519
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
520
        exitWith $ ExitFailure 3