Main.hs 23.5 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
import Solver.CommFreeReachability
34

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

38
39
data NetTransformation = TerminationByReachability
                       | ValidateIdentifiers
40

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

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

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

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

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

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

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

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

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

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

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

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

138
139
140
141
142
143
        , Option "" ["final-state-unreachable"]
        (NoArg (\opt -> Right opt {
                   optProperties = FinalStateUnreachable : optProperties opt
               }))
        "Prove that the final state is unreachable"

144
145
        , Option "" ["safe"]
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
146
                   optProperties = Safe : optProperties opt
147
148
149
150
151
152
153
154
155
156
157
158
               }))
        "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"

159
160
161
162
163
164
        , Option "" ["free-choice"]
        (NoArg (\opt -> Right opt {
                   optProperties = StructFreeChoice : optProperties opt
               }))
        "Prove that the net is free-choice"

165
166
167
168
169
170
171
172
173
174
175
176
        , 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"

177
178
179
180
181
182
        , Option "" ["communication-free"]
        (NoArg (\opt -> Right opt {
                   optProperties = StructCommunicationFree : optProperties opt
               }))
        "Prove that the net is communication-free"

183
184
185
186
        , Option "n" ["no-refinement"]
        (NoArg (\opt -> Right opt { optRefine = False }))
        "Don't use refinement"

187
188
189
190
191
192
193
        , Option "o" ["output"]
        (ReqArg (\arg opt -> Right opt {
                        optOutput = Just arg
                })
                "FILE")
        "Write net and properties to FILE"

194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
        , 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"

210
211
212
213
214
215
        , Option "" ["no-given-properties"]
        (NoArg (\opt -> Right opt {
                   optUseProperties = False
               }))
        "Do not use the properties given in the input file"

216
        , Option "v" ["verbose"]
217
218
219
220
221
222
        (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)"
223
224
225
226
227
228
229
230
231
232

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

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

233
234
235
236
verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
        when (verbosity >= level) (putStrLn str)

237
238
239
240
241
242
243
244
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

245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
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
273

274
275
276
277
278
279
280
281
282
283
284
285
286
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)
287
288
        putStrLn $ "Places             : " ++ show (length (places net))
        putStrLn $ "Transitions        : " ++ show (length (transitions net))
289
290
291
292
293
294
        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)

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

321
placeOp :: Op -> (String, Integer) -> Formula
322
placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w)
323

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

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

407
checkProperty :: Int -> PetriNet -> Bool -> Property -> IO PropResult
408
409
checkProperty verbosity net refine p = do
        verbosePut verbosity 1 $ "\nChecking " ++ showPropertyName p
410
        verbosePut verbosity 3 $ show p
411
        r <- case pcont p of
412
            (Safety pf) -> checkSafetyProperty verbosity net refine pf
413
414
415
416
417
418
419
            (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."
420
421
        return r

422
checkSafetyProperty :: Int -> PetriNet -> Bool ->
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
        Formula -> IO PropResult
checkSafetyProperty verbosity net refine f =
        if checkCommunicationFree net then do
            verbosePut verbosity 1 "Net found to be communication-free"
            checkSafetyPropertyByCommFree verbosity net f
        else
            checkSafetyPropertyBySafetyRef verbosity net refine f []

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

checkSafetyPropertyBySafetyRef :: Int -> PetriNet -> Bool ->
442
        Formula -> [[String]] -> IO PropResult
443
checkSafetyPropertyBySafetyRef verbosity net refine f traps = do
444
445
        r <- checkSat $ checkStateEquationSat net f traps
        case r of
446
            Nothing -> return Satisfied
447
448
            Just a -> do
                let assigned = markedPlacesFromAssignment net a
449
450
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Places marked: " ++ show assigned
451
                verbosePut verbosity 3 $ "Assignment: " ++ show a
452
453
454
455
                if refine then do
                    rt <- checkSat $ checkTrapSat net assigned
                    case rt of
                        Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
456
                            verbosePut verbosity 1 "No trap found."
457
                            return Unknown
458
459
                        Just at -> do
                            let trap = trapFromAssignment at
460
461
462
                            verbosePut verbosity 1 "Trap found"
                            verbosePut verbosity 2 $ "Places in trap: " ++
                                                      show trap
463
464
                            verbosePut verbosity 3 $ "Trap assignment: " ++
                                                      show at
465
466
                            checkSafetyPropertyBySafetyRef verbosity net
                                                refine f (trap:traps)
467
                else
468
                    return Unknown
469

470
checkLivenessProperty :: Int -> PetriNet -> Bool ->
471
        Formula -> [([String],[String])] -> IO PropResult
472
checkLivenessProperty verbosity net refine f strans = do
473
        r <- checkSat $ checkTransitionInvariantSat net f strans
Philipp Meyer's avatar
Philipp Meyer committed
474
        case r of
475
            Nothing -> return Satisfied
476
477
            Just ax -> do
                let fired = firedTransitionsFromAssignment ax
478
479
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Transitions fired: " ++ show fired
480
                verbosePut verbosity 3 $ "Assignment: " ++ show ax
481
482
483
484
                if refine then do
                    rt <- checkSat $ checkSComponentSat net fired ax
                    case rt of
                        Nothing -> do
485
                            verbosePut verbosity 1 "No S-component found"
486
                            return Unknown
487
488
                        Just as -> do
                            let sOutIn = getSComponentOutIn net ax as
489
490
                            verbosePut verbosity 1 "S-component found"
                            verbosePut verbosity 2 $ "Out/In: " ++ show sOutIn
491
492
                            verbosePut verbosity 3 $ "S-Component assignment: " ++
                                                      show as
493
                            checkLivenessProperty verbosity net refine f
494
495
                                                  (sOutIn:strans)
                else
496
497
498
                    return Unknown

checkStructuralProperty :: Int -> PetriNet -> Structure -> IO PropResult
499
checkStructuralProperty _ net struct =
500
501
502
503
        if checkStructure net struct then
            return Satisfied
        else
            return Unsatisfied
504

505
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
506
main = do
507
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
508
509
510
511
512
513
514
515
        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")
516
517
                let verbosity = optVerbosity opts
                    refinement = optRefine opts
518
519
                let parser = case inputFormat opts of
                                 PNET -> PNET.parseContent
Philipp Meyer's avatar
Philipp Meyer committed
520
                                 LOLA -> LOLA.parseContent
521
                                 TPN -> TPN.parseContent
522
                                 MIST -> MIST.parseContent
523
524
525
                let properties = reverse $ optProperties opts
                let transformations = reverse $ optTransformations opts
                rs <- mapM (checkFile parser verbosity refinement properties
526
                     transformations (optUseProperties opts) (optOutput opts)
527
                     (outputFormat opts) (optPrintStructure opts)) files
Philipp Meyer's avatar
Philipp Meyer committed
528
                -- TODO: short-circuit with Control.Monad.Loops?
529
530
531
532
533
534
535
                case resultsAnd rs of
                    Satisfied ->
                        exitSuccessWith "All properties satisfied."
                    Unsatisfied ->
                        exitFailureWith "Some properties are not satisfied"
                    Unknown ->
                        exitFailureWith "Some properties may not be satisfied."
536

Philipp Meyer's avatar
Philipp Meyer committed
537
-- TODO: Always exit with exit code 0 unless an error occured
538
539
540
541
542
543
544
545
exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
        exitSuccess

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

548
549
550
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
551
        exitWith $ ExitFailure 3