Main.hs 23.9 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

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

37
data InputFormat = PNET | LOLA | TPN | MIST deriving (Show,Read)
38
39
40
41
42
43
44
data OutputFormat = OutLOLA | OutSARA | OutSPEC | OutDOT deriving (Read)

instance Show OutputFormat where
        show OutLOLA = "LOLA"
        show OutSARA = "SARA"
        show OutSPEC = "SPEC"
        show OutDOT = "DOT"
45

46
47
data NetTransformation = TerminationByReachability
                       | ValidateIdentifiers
48

49
data ImplicitProperty = Termination
50
                      | DeadlockFree | DeadlockFreeUnlessFinal
51
                      | FinalStateUnreachable
Philipp Meyer's avatar
Philipp Meyer committed
52
                      | ProperTermination
53
                      | Safe | Bounded Integer
54
                      | StructFreeChoice
55
56
                      | StructParallel
                      | StructFinalPlace
57
                      | StructCommunicationFree
58
59
                      deriving (Show,Read)

60
data Options = Options { inputFormat :: InputFormat
61
                       , optVerbosity :: Int
62
63
                       , optShowHelp :: Bool
                       , optShowVersion :: Bool
64
                       , optProperties :: [ImplicitProperty]
65
                       , optTransformations :: [NetTransformation]
66
                       , optRefine :: Bool
67
                       , optInvariant :: Bool
68
                       , optOutput :: Maybe String
69
                       , outputFormat :: OutputFormat
70
                       , optUseProperties :: Bool
71
                       , optPrintStructure :: Bool
72
73
74
75
                       }

startOptions :: Options
startOptions = Options { inputFormat = PNET
76
                       , optVerbosity = 1
77
78
                       , optShowHelp = False
                       , optShowVersion = False
79
                       , optProperties = []
80
                       , optTransformations = []
81
                       , optRefine = True
82
                       , optInvariant = False
83
                       , optOutput = Nothing
84
                       , outputFormat = OutLOLA
85
                       , optUseProperties = True
86
                       , optPrintStructure = False
87
88
89
90
                       }

options :: [ OptDescr (Options -> Either String Options) ]
options =
91
92
93
94
95
96
97
98
99
100
101
        [ 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"
102

103
104
105
106
        , Option "" ["spec"]
        (NoArg (\opt -> Right opt { inputFormat = MIST }))
        "Use the mist input format"

107
108
109
110
        , Option "s" ["structure"]
        (NoArg (\opt -> Right opt { optPrintStructure = True }))
        "Print structural information"

111
112
113
114
115
116
        , Option "" ["validate-identifiers"]
        (NoArg (\opt -> Right opt {
            optTransformations = ValidateIdentifiers : optTransformations opt
          }))
        "Make identifiers valid for lola"

117
        , Option "" ["termination-by-reachability"]
118
        (NoArg (\opt -> Right opt {
119
            optTransformations = TerminationByReachability : optTransformations opt
120
          }))
121
        "Prove termination by reducing it to reachability"
122

123
        , Option "" ["termination"]
124
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
125
                   optProperties = Termination : optProperties opt
126
               }))
127
        "Prove that the net is terminating"
128

Philipp Meyer's avatar
Philipp Meyer committed
129
130
131
132
133
134
        , Option "" ["proper-termination"]
        (NoArg (\opt -> Right opt {
                   optProperties = ProperTermination : optProperties opt
               }))
        "Prove termination in the final marking"

135
        , Option "" ["deadlock-free"]
136
        (NoArg (\opt -> Right opt {
137
                   optProperties = DeadlockFree : optProperties opt
138
               }))
139
        "Prove that the net is deadlock-free"
140

141
        , Option "" ["deadlock-free-unless-final"]
Philipp Meyer's avatar
Philipp Meyer committed
142
        (NoArg (\opt -> Right opt {
143
                   optProperties = DeadlockFreeUnlessFinal : optProperties opt
Philipp Meyer's avatar
Philipp Meyer committed
144
               }))
145
146
        ("Prove that the net is deadlock-free\n" ++
         "unless it is in the final marking")
Philipp Meyer's avatar
Philipp Meyer committed
147

148
149
150
151
152
153
        , Option "" ["final-state-unreachable"]
        (NoArg (\opt -> Right opt {
                   optProperties = FinalStateUnreachable : optProperties opt
               }))
        "Prove that the final state is unreachable"

154
155
        , Option "" ["safe"]
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
156
                   optProperties = Safe : optProperties opt
157
158
159
160
161
162
163
164
165
166
167
168
               }))
        "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"

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

175
176
177
178
179
180
181
182
183
184
185
186
        , 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"

187
188
189
190
191
192
        , Option "" ["communication-free"]
        (NoArg (\opt -> Right opt {
                   optProperties = StructCommunicationFree : optProperties opt
               }))
        "Prove that the net is communication-free"

193
194
195
196
        , Option "n" ["no-refinement"]
        (NoArg (\opt -> Right opt { optRefine = False }))
        "Don't use refinement"

197
198
199
200
        , Option "i" ["invariant"]
        (NoArg (\opt -> Right opt { optInvariant = True }))
        "Try to generate an invariant"

201
202
203
204
205
206
207
        , Option "o" ["output"]
        (ReqArg (\arg opt -> Right opt {
                        optOutput = Just arg
                })
                "FILE")
        "Write net and properties to FILE"

208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
        , 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"

224
225
226
227
228
229
        , Option "" ["no-given-properties"]
        (NoArg (\opt -> Right opt {
                   optUseProperties = False
               }))
        "Do not use the properties given in the input file"

230
        , Option "v" ["verbose"]
231
232
233
234
235
236
        (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)"
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254

        , 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

255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
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
283

284
285
286
287
288
289
290
291
292
293
294
295
296
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)
297
298
        putStrLn $ "Places             : " ++ show (length (places net))
        putStrLn $ "Transitions        : " ++ show (length (transitions net))
299
300
301
302
303
304
        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)

305
checkFile :: Parser (PetriNet,[Property]) -> Int -> Bool -> Bool ->
306
            [ImplicitProperty] -> [NetTransformation] ->
307
308
            Bool -> Maybe String -> OutputFormat -> Bool -> String ->
            IO PropResult
309
checkFile parser verbosity refine invariant implicitProperties transformations
310
          useProperties output format printStruct file = do
311
        verbosePut verbosity 0 $ "Reading \"" ++ file ++ "\""
312
        (net,props) <- parseFile parser file
313
314
315
        let props' = if useProperties then props else []
        let props'' = props' ++ map (makeImplicitProperty net) implicitProperties
        let (net',props''') = foldl transformNet (net,props'') transformations
316
317
318
319
        verbosePut verbosity 1 $ "Analyzing " ++ showNetName net
        verbosePut verbosity 2 $
                "Places: " ++ show (length  $ places net') ++ "; " ++
                "Transitions: " ++ show (length $ transitions net')
320
        when printStruct $ structuralAnalysis net
321
        verbosePut verbosity 3 $ show net'
322
        case output of
323
324
            Just outputfile ->
                writeFiles verbosity outputfile format net' props'''
325
            Nothing -> return ()
Philipp Meyer's avatar
Philipp Meyer committed
326
        -- TODO: short-circuit?
327
        rs <- mapM (checkProperty verbosity net' refine invariant) props'''
328
        verbosePut verbosity 0 ""
329
        return $ resultsAnd rs
330

331
332
placeOp :: Op -> (Place, Integer) -> Formula Place
placeOp op (p,w) = LinearInequation (Var p) op (Const w)
333

334
335
transformNet :: (PetriNet, [Property]) -> NetTransformation ->
               (PetriNet, [Property])
336
transformNet (net, props) TerminationByReachability =
337
338
339
340
341
342
343
344
345
        let m1 = Place "'m1"
            m2 = Place "'m1"
            sigma = Place "'sigma"
            switch = Transition "'switch"
            primePlace = renamePlace prime
            primeTransition = renameTransition prime
            ps = [sigma, m1, m2] ++
                 places net ++ map primePlace (places net)
            is = [(Place "'m1", 1)] ++
346
                 linitials net ++ map (first primePlace) (linitials net)
347
348
            transformTransition t =
                let (preT, postT) = context net t
349
350
351
352
                    pre'  = [(m1,1)] ++ preT  ++ map (first primePlace) preT
                    post' = [(m1,1)] ++ postT ++ map (first primePlace) postT
                    pre''  = (m2,1) : map (first primePlace) preT
                    post'' = [(m2,1), (sigma,1)] ++ map (first primePlace) postT
353
                in  if t `elem` ghostTransitions net then
354
                        [(t, (pre', post'))]
355
                    else
356
357
                        [(t, (pre', post')), (primeTransition t, (pre'', post''))]
            ts = (switch, ([(m1,1)], [(m2,1)])) :
358
359
                 concatMap transformTransition (transitions net)
            gs = ghostTransitions net
360
            prop = Property "termination by reachability" $ Safety $
361
362
363
                    foldl (:&:) (LinearInequation (Var sigma) Ge (Const 1))
                      (map (\p -> LinearInequation
                                (Var (primePlace p) :-: Var p) Ge (Const 0))
364
                        (places net))
365
            -- TODO: map existing liveness properties
366
        in  (makePetriNetWith (name net) ps ts is gs, prop : props)
367
transformNet (net, props) ValidateIdentifiers =
368
369
        (renamePetriNetPlacesAndTransitions validateId net,
         map (renameProperty validateId) props)
370

371
makeImplicitProperty :: PetriNet -> ImplicitProperty -> Property
372
makeImplicitProperty net Termination =
373
        Property "termination" $ Liveness $
374
            foldl (:&:) FTrue
375
                (map (\t -> LinearInequation (Var t) Eq (Const 0))
376
                    (ghostTransitions net))
377
makeImplicitProperty net ProperTermination =
Philipp Meyer's avatar
Philipp Meyer committed
378
        let (finals, nonfinals) = partition (null . lpost net) (places net)
379
        in  Property "proper termination" $ Safety
Philipp Meyer's avatar
Philipp Meyer committed
380
381
            (foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) finals) :&:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals))
382
makeImplicitProperty net DeadlockFree =
383
        Property "deadlock-free" $ Safety $
384
385
            foldl (:&:) FTrue
                (map (foldl (:|:) FFalse . map (placeOp Lt) . lpre net)
386
                     (filter (`notElem` ghostTransitions net) (transitions net)))
387
makeImplicitProperty net DeadlockFreeUnlessFinal =
388
        let (Property _ (Safety pf)) = makeImplicitProperty net DeadlockFree
389
            (finals, nonfinals) = partition (null . lpost net) (places net)
390
        in  Property "deadlock-free unless final" $ Safety $
Philipp Meyer's avatar
Philipp Meyer committed
391
392
            (foldl (:&:) FTrue  (map (\p -> placeOp Eq (p,0)) finals) :|:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals)) :&:
393
            pf
394
395
396
397
398
makeImplicitProperty net FinalStateUnreachable =
        let (finals, nonfinals) = partition (null . lpost net) (places net)
        in  Property "final state unreachable" $ Safety $
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) finals) :&:
             foldl (:&:) FTrue (map (\p -> placeOp Eq (p,0)) nonfinals)
399
makeImplicitProperty net (Bounded k) =
400
        Property (show k ++ "-bounded") $ Safety $
401
            foldl (:|:) FFalse
Philipp Meyer's avatar
Philipp Meyer committed
402
                (map (\p -> placeOp Ge (p,k+1))
403
404
                    (filter (`notElem` concatMap (post net) (ghostTransitions net))
                        (places net)))
405
406
makeImplicitProperty net Safe =
        let bounded = makeImplicitProperty net (Bounded 1)
407
408
409
        in  Property "safe" $ pcont bounded
makeImplicitProperty _ StructFreeChoice =
        Property "free choice" $ Structural FreeChoice
410
411
412
413
makeImplicitProperty _ StructParallel =
        Property "parallel" $ Structural Parallel
makeImplicitProperty _ StructFinalPlace =
        Property "final place" $ Structural FinalPlace
414
415
makeImplicitProperty _ StructCommunicationFree =
        Property "communication free" $ Structural CommunicationFree
416

417
418
checkProperty :: Int -> PetriNet -> Bool -> Bool -> Property -> IO PropResult
checkProperty verbosity net refine invariant p = do
419
        verbosePut verbosity 1 $ "\nChecking " ++ showPropertyName p
420
        verbosePut verbosity 3 $ show p
421
        r <- case pcont p of
422
            (Safety pf) -> checkSafetyProperty verbosity net refine invariant pf
423
            (Liveness pf) -> checkLivenessProperty verbosity net refine invariant pf
424
            --(Structural ps) -> checkStructuralProperty verbosity net ps
425
426
427
428
429
        verbosePut verbosity 0 $ showPropertyName p ++ " " ++
            case r of
                Satisfied -> "is satisfied."
                Unsatisfied -> "is not satisfied."
                Unknown-> "may not be satisfied."
430
431
        return r

432
checkSafetyProperty :: Int -> PetriNet -> Bool -> Bool ->
433
        Formula Place -> IO PropResult
434
checkSafetyProperty verbosity net refine invariant f =
435
        -- TODO: add flag for this kind of structural check
436
437
438
439
440
        --if checkCommunicationFree net then do
        --    verbosePut verbosity 1 "Net found to be communication-free"
        --    checkSafetyPropertyByCommFree verbosity net f
        --else
        do
441
442
443
444
            r <- checkSafetyPropertyBySafetyRef verbosity net refine f []
            if r == Satisfied && invariant then
                -- TODO: add invariant generation
                error "Invariant generation for safety properties not yet supported"
445
            else
446
                return r
447
{-
448
449
450
451
452
453
454
455
456
checkSafetyPropertyByCommFree :: Int -> PetriNet -> Formula -> IO PropResult
checkSafetyPropertyByCommFree verbosity net f = do
        r <- checkSat $ checkCommFreeReachabilitySat net f
        case r of
            Nothing -> return Satisfied
            Just a -> do
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 3 $ "Assignment: " ++ show a
                return Unsatisfied
457
-}
458
checkSafetyPropertyBySafetyRef :: Int -> PetriNet -> Bool ->
459
        Formula Place -> [Trap] -> IO PropResult
460
checkSafetyPropertyBySafetyRef verbosity net refine f traps = do
Philipp Meyer's avatar
Philipp Meyer committed
461
        r <- checkSat verbosity $ checkStateEquationSat net f traps
462
        case r of
463
            Nothing -> return Satisfied
Philipp Meyer's avatar
Philipp Meyer committed
464
            Just marking -> do
465
                if refine then do
Philipp Meyer's avatar
Philipp Meyer committed
466
                    rt <- checkSat verbosity $ checkTrapSat net marking
467
468
                    case rt of
                        Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
469
                            verbosePut verbosity 1 "No trap found."
470
                            return Unknown
471
                        Just trap -> do
Philipp Meyer's avatar
Philipp Meyer committed
472
473
                            checkSafetyPropertyBySafetyRef verbosity net
                                                refine f (trap:traps)
474
                else
475
                    return Unknown
476

477
checkLivenessProperty :: Int -> PetriNet -> Bool -> Bool ->
478
        Formula Transition -> IO PropResult
479
480
checkLivenessProperty verbosity net refine invariant f = do
        (r, comps) <- checkLivenessPropertyByRef verbosity net refine f []
481
482
483
484
485
486
        return r
        --if r == Satisfied && invariant then
        --    generateLivenessInvariant verbosity net f comps
        --else
        --    return r
{-
487
generateLivenessInvariant :: Int -> PetriNet ->
488
        Formula -> [SCompCut] -> IO PropResult
489
490
generateLivenessInvariant verbosity net f comps = do
        verbosePut verbosity 1 "Generating invariant"
491
492
493
494
495
496
497
498
        let cuts = generateCuts f comps
        r <- checkSat $ checkLivenessInvariantSat net cuts
        case r of
            Nothing -> return Unsatisfied
            Just as -> do
                let inv = getLivenessInvariant net cuts as
                mapM_ print inv
                return Satisfied
499
-}
500
checkLivenessPropertyByRef :: Int -> PetriNet -> Bool ->
501
502
503
        Formula Transition -> [Cut] -> IO (PropResult, [Cut])
checkLivenessPropertyByRef verbosity net refine f cuts = do
        r <- checkSat verbosity $ checkTransitionInvariantSat net f cuts
Philipp Meyer's avatar
Philipp Meyer committed
504
        case r of
505
506
            Nothing -> return (Satisfied, cuts)
            Just x -> do
507
                if refine then do
508
                    rt <- return Nothing -- checkSat $ checkSComponentSat net x
509
510
                    case rt of
                        Nothing -> do
511
512
                            return (Unknown, cuts)
                        Just cut -> do
513
                            checkLivenessPropertyByRef verbosity net refine f
514
                                                  (cut:cuts)
515
                else
516
517
                    return (Unknown, cuts)

518
checkStructuralProperty :: Int -> PetriNet -> Structure -> IO PropResult
519
checkStructuralProperty _ net struct =
520
521
522
523
        if checkStructure net struct then
            return Satisfied
        else
            return Unsatisfied
524

525
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
526
main = do
527
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
528
529
530
531
532
533
534
535
        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")
536
537
                let verbosity = optVerbosity opts
                    refinement = optRefine opts
538
                    invariant = optInvariant opts
539
540
                let parser = case inputFormat opts of
                                 PNET -> PNET.parseContent
Philipp Meyer's avatar
Philipp Meyer committed
541
                                 LOLA -> LOLA.parseContent
542
                                 TPN -> TPN.parseContent
543
                                 MIST -> MIST.parseContent
544
545
                let properties = reverse $ optProperties opts
                let transformations = reverse $ optTransformations opts
546
547
548
549
                rs <- mapM (checkFile parser verbosity refinement invariant
                     properties transformations (optUseProperties opts)
                     (optOutput opts) (outputFormat opts) (optPrintStructure opts))
                     files
Philipp Meyer's avatar
Philipp Meyer committed
550
                -- TODO: short-circuit with Control.Monad.Loops?
551
552
553
554
555
556
557
                case resultsAnd rs of
                    Satisfied ->
                        exitSuccessWith "All properties satisfied."
                    Unsatisfied ->
                        exitFailureWith "Some properties are not satisfied"
                    Unknown ->
                        exitFailureWith "Some properties may not be satisfied."
558

Philipp Meyer's avatar
Philipp Meyer committed
559
-- TODO: Always exit with exit code 0 unless an error occured
560
561
562
563
564
565
566
567
exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
        exitSuccess

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

570
571
572
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
573
        exitWith $ ExitFailure 3