Main.hs 20.2 KB
Newer Older
1
2
module Main where

3
import System.Exit
4
5
import System.IO
import Control.Monad
6
import Control.Concurrent.ParallelIO
7
import Control.Arrow (first)
8
9
import Data.List (partition,minimumBy)
import Data.Ord (comparing)
10
import Data.Maybe
11
import qualified Data.ByteString.Lazy as L
Philipp Meyer's avatar
Philipp Meyer committed
12
import Control.Monad.Reader
Philipp Meyer's avatar
Philipp Meyer committed
13

Philipp Meyer's avatar
Philipp Meyer committed
14
import Util
Philipp Meyer's avatar
Philipp Meyer committed
15
import Options
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
import Solver.SubnetEmptyTrap
34
import Solver.LivenessInvariant
35
import Solver.SafetyInvariant
36
import Solver.SComponentWithCut
37
import Solver.SComponent
38
import Solver.Simplifier
39
--import Solver.Interpolant
40
--import Solver.CommFreeReachability
41

Philipp Meyer's avatar
Philipp Meyer committed
42
43
44
45
writeFiles :: String -> PetriNet -> [Property] -> OptIO ()
writeFiles basename net props = do
        format <- opt outputFormat
        verbosePut 1 $ "Writing " ++ showNetName net ++ " to " ++
46
47
48
                                  basename ++ " in format " ++ show format
        case format of
            OutLOLA -> do
Philipp Meyer's avatar
Philipp Meyer committed
49
                liftIO $ L.writeFile basename $ LOLAPrinter.printNet net
50
51
                mapM_ (\(p,i) -> do
                        let file = basename ++ ".task" ++ show i
Philipp Meyer's avatar
Philipp Meyer committed
52
                        verbosePut 1 $ "Writing " ++ showPropertyName p
53
                                                 ++ " to " ++ file
Philipp Meyer's avatar
Philipp Meyer committed
54
                        liftIO $ L.writeFile file $ LOLAPrinter.printProperty p
55
56
                      ) (zip props [(1::Integer)..])
            OutSARA -> do
Philipp Meyer's avatar
Philipp Meyer committed
57
58
                liftIO $ L.writeFile basename $ LOLAPrinter.printNet net
                verbosePut 1 $ "Writing properties to " ++ basename ++
59
                                         ".sara"
Philipp Meyer's avatar
Philipp Meyer committed
60
                liftIO $ L.writeFile (basename ++ ".sara") $
61
62
63
64
                    SARAPrinter.printProperties basename net props
            OutSPEC ->
                mapM_ (\(p,i) -> do
                        let file = basename ++ ".target" ++ show i
Philipp Meyer's avatar
Philipp Meyer committed
65
                        verbosePut 1 $ "Writing " ++ showPropertyName p
66
                                                 ++ " to " ++ file
Philipp Meyer's avatar
Philipp Meyer committed
67
                        liftIO $ L.writeFile file $ SPECPrinter.printProperty p
68
69
                      ) (zip props [(1::Integer)..])
            OutDOT ->
Philipp Meyer's avatar
Philipp Meyer committed
70
                liftIO $ L.writeFile basename $ DOTPrinter.printNet net
71

Philipp Meyer's avatar
Philipp Meyer committed
72
structuralAnalysis :: PetriNet -> OptIO ()
73
74
75
76
77
78
79
80
81
82
83
84
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)
Philipp Meyer's avatar
Philipp Meyer committed
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
        verbosePut 0 $ "Places             : " ++ show (length (places net))
        verbosePut 0 $ "Transitions        : " ++ show (length (transitions net))
        verbosePut 0 $ "Initial places     : " ++ show (length initP)
        verbosePut 0 $ "Initial transitions: " ++ show (length initT)
        verbosePut 0 $ "Isolated places    : " ++ show (length isolP)
        verbosePut 0 $ "Final places       : " ++ show (length finalP)
        verbosePut 0 $ "Final transitions  : " ++ show (length finalT)

checkFile :: String -> OptIO PropResult
checkFile file = do
        verbosePut 0 $ "Reading \"" ++ file ++ "\""
        format <- opt inputFormat
        let parser = case format of
                             PNET -> PNET.parseContent
                             LOLA -> LOLA.parseContent
                             TPN -> TPN.parseContent
                             MIST -> MIST.parseContent
        (net,props) <- liftIO $ parseFile parser file
        useProperties <- opt optUseProperties
104
        let props' = if useProperties then props else []
Philipp Meyer's avatar
Philipp Meyer committed
105
        implicitProperties <- opt optProperties
106
        let props'' = props' ++ map (makeImplicitProperty net) implicitProperties
Philipp Meyer's avatar
Philipp Meyer committed
107
        transformations <- opt optTransformations
108
        let (net',props''') = foldl transformNet (net,props'') transformations
Philipp Meyer's avatar
Philipp Meyer committed
109
110
        verbosePut 1 $ "Analyzing " ++ showNetName net
        verbosePut 2 $
111
112
113
114
115
116
117
                "Number of places: " ++ show (length (places net'))
        verbosePut 2 $
                "Number of transitions: " ++ show (length (transitions net'))
        let pRowSize p = let (preP, postP) = context net' p in length preP + length postP
        let arcs = sum $ map pRowSize $ places net'
        verbosePut 2 $
                "Number of arcs: " ++ show arcs
Philipp Meyer's avatar
Philipp Meyer committed
118
        printStruct <- opt optPrintStructure
119
        when printStruct $ structuralAnalysis net
Philipp Meyer's avatar
Philipp Meyer committed
120
121
        verbosePut 3 $ show net'
        output <- opt optOutput
122
        case output of
123
            Just outputfile ->
Philipp Meyer's avatar
Philipp Meyer committed
124
                writeFiles outputfile net' props'''
125
            Nothing -> return ()
126
        -- TODO: short-circuit? parallel?
Philipp Meyer's avatar
Philipp Meyer committed
127
128
        rs <- mapM (checkProperty net') props'''
        verbosePut 0 ""
129
        return $ resultsAnd rs
130

131
132
placeOp :: Op -> (Place, Integer) -> Formula Place
placeOp op (p,w) = LinearInequation (Var p) op (Const w)
133

134
135
transformNet :: (PetriNet, [Property]) -> NetTransformation ->
               (PetriNet, [Property])
136
transformNet (net, props) TerminationByReachability =
137
138
139
140
141
142
143
144
145
        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)] ++
146
                 linitials net ++ map (first primePlace) (linitials net)
147
148
            transformTransition t =
                let (preT, postT) = context net t
149
150
151
152
                    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
153
                in  if t `elem` ghostTransitions net then
154
                        [(t, (pre', post'))]
155
                    else
156
157
                        [(t, (pre', post')), (primeTransition t, (pre'', post''))]
            ts = (switch, ([(m1,1)], [(m2,1)])) :
158
159
                 concatMap transformTransition (transitions net)
            gs = ghostTransitions net
160
            prop = Property "termination by reachability" $ Safety $
161
162
163
                    foldl (:&:) (LinearInequation (Var sigma) Ge (Const 1))
                      (map (\p -> LinearInequation
                                (Var (primePlace p) :-: Var p) Ge (Const 0))
164
                        (places net))
165
            -- TODO: map existing liveness properties
Philipp Meyer's avatar
Philipp Meyer committed
166
        in  (makePetriNetWithTrans (name net) ps ts is gs, prop : props)
167
transformNet (net, props) ValidateIdentifiers =
168
169
        (renamePetriNetPlacesAndTransitions validateId net,
         map (renameProperty validateId) props)
170

171
makeImplicitProperty :: PetriNet -> ImplicitProperty -> Property
172
makeImplicitProperty net Termination =
173
        Property "termination" $ Liveness $
174
            foldl (:&:) FTrue
175
                (map (\t -> LinearInequation (Var t) Eq (Const 0))
176
                    (ghostTransitions net))
177
makeImplicitProperty net ProperTermination =
Philipp Meyer's avatar
Philipp Meyer committed
178
        let (finals, nonfinals) = partition (null . lpost net) (places net)
179
        in  Property "proper termination" $ Safety
Philipp Meyer's avatar
Philipp Meyer committed
180
181
            (foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) finals) :&:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals))
182
makeImplicitProperty net DeadlockFree =
183
        Property "deadlock-free" $ Safety $
184
185
            foldl (:&:) FTrue
                (map (foldl (:|:) FFalse . map (placeOp Lt) . lpre net)
186
                     (filter (`notElem` ghostTransitions net) (transitions net)))
187
makeImplicitProperty net DeadlockFreeUnlessFinal =
188
        let (Property _ (Safety pf)) = makeImplicitProperty net DeadlockFree
189
            (finals, nonfinals) = partition (null . lpost net) (places net)
190
        in  Property "deadlock-free unless final" $ Safety $
Philipp Meyer's avatar
Philipp Meyer committed
191
192
            (foldl (:&:) FTrue  (map (\p -> placeOp Eq (p,0)) finals) :|:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals)) :&:
193
            pf
194
195
196
197
198
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)
199
makeImplicitProperty net (Bounded k) =
200
        Property (show k ++ "-bounded") $ Safety $
201
            foldl (:|:) FFalse
Philipp Meyer's avatar
Philipp Meyer committed
202
                (map (\p -> placeOp Ge (p,k+1))
203
204
                    (filter (`notElem` concatMap (post net) (ghostTransitions net))
                        (places net)))
205
206
makeImplicitProperty net Safe =
        let bounded = makeImplicitProperty net (Bounded 1)
207
208
209
        in  Property "safe" $ pcont bounded
makeImplicitProperty _ StructFreeChoice =
        Property "free choice" $ Structural FreeChoice
210
211
212
213
makeImplicitProperty _ StructParallel =
        Property "parallel" $ Structural Parallel
makeImplicitProperty _ StructFinalPlace =
        Property "final place" $ Structural FinalPlace
214
215
makeImplicitProperty _ StructCommunicationFree =
        Property "communication free" $ Structural CommunicationFree
216

Philipp Meyer's avatar
Philipp Meyer committed
217
218
219
220
checkProperty :: PetriNet -> Property -> OptIO PropResult
checkProperty net p = do
        verbosePut 1 $ "\nChecking " ++ showPropertyName p
        verbosePut 3 $ show p
221
        r <- case pcont p of
Philipp Meyer's avatar
Philipp Meyer committed
222
223
224
225
            (Safety pf) -> checkSafetyProperty net pf
            (Liveness pf) -> checkLivenessProperty net pf
            (Structural ps) -> checkStructuralProperty net ps
        verbosePut 0 $ showPropertyName p ++ " " ++
226
227
228
229
            case r of
                Satisfied -> "is satisfied."
                Unsatisfied -> "is not satisfied."
                Unknown-> "may not be satisfied."
230
231
        return r

Philipp Meyer's avatar
Philipp Meyer committed
232
233
234
235
checkSafetyProperty :: PetriNet ->
        Formula Place -> OptIO PropResult
checkSafetyProperty net f = do
        r <- checkSafetyProperty' net f []
236
        case r of
Philipp Meyer's avatar
Philipp Meyer committed
237
238
            (Nothing, traps) -> do
                invariant <- opt optInvariant
239
                if invariant then
240
                    getSafetyInvariant net f traps >>= printInvariant
241
242
243
244
245
                else
                    return Satisfied
            (Just _, _) ->
                return Unknown

246
247
248
249
250
251
252
253
254
255
getSafetyInvariant :: PetriNet -> Formula Place -> [Trap] ->
        OptIO (Maybe [SafetyInvariant], [SafetyInvariant])
getSafetyInvariant net f traps = do
        r <- checkSat $ checkSafetyInvariantSat net f traps
        let trapInvs = map trapToSafetyInvariant traps
        return (sequence [r], trapInvs)

printInvariant :: (Show a, Invariant a) => (Maybe [a], [a]) -> OptIO PropResult
printInvariant (baseInvResult, addedInv) =
        case baseInvResult of
Philipp Meyer's avatar
Philipp Meyer committed
256
            Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
257
                verbosePut 0 "No invariant found"
Philipp Meyer's avatar
Philipp Meyer committed
258
                return Unknown
259
            Just baseInv -> do
Philipp Meyer's avatar
Philipp Meyer committed
260
                verbosePut 0 "Invariant found"
261
262
263
                let baseSize = map invariantSize baseInv
                let addedSize = map invariantSize addedInv
                verbosePut 2 $ "Number of atoms in base invariants: " ++ show baseSize ++
264
                        " (total of " ++ show (sum baseSize) ++ ")"
265
                verbosePut 2 $ "Number of atoms in added invariants: " ++ show addedSize ++
266
                        " (total of " ++ show (sum addedSize) ++ ")"
267
268
                mapM_ (putLine . show) baseInv
                mapM_ (putLine . show) addedInv
Philipp Meyer's avatar
Philipp Meyer committed
269
270
                return Satisfied

Philipp Meyer's avatar
Philipp Meyer committed
271
272
273
274
checkSafetyProperty' :: PetriNet ->
        Formula Place -> [Trap] -> OptIO (Maybe Marking, [Trap])
checkSafetyProperty' net f traps = do
        r <- checkSat $ checkStateEquationSat net f traps
275
        case r of
276
            Nothing -> return (Nothing, traps)
Philipp Meyer's avatar
Philipp Meyer committed
277
            Just m -> do
278
279
                refine <- opt optRefinementType
                if isJust refine then
Philipp Meyer's avatar
Philipp Meyer committed
280
                    refineSafetyProperty net f traps m
281
                else
282
                    return (Just m, traps)
Philipp Meyer's avatar
Philipp Meyer committed
283

Philipp Meyer's avatar
Philipp Meyer committed
284
285
286
287
refineSafetyProperty :: PetriNet ->
        Formula Place -> [Trap] -> Marking -> OptIO (Maybe Marking, [Trap])
refineSafetyProperty net f traps m = do
        r <- checkSat $ checkTrapSat net m
288
        case r of
Philipp Meyer's avatar
Philipp Meyer committed
289
290
291
            Nothing ->
                return (Just m, traps)
            Just trap ->
Philipp Meyer's avatar
Philipp Meyer committed
292
                checkSafetyProperty' net f (trap:traps)
293

294
295
296
297
298
299
300
301
302
303
304
305
306
applyRefinementMethod :: RefinementMethod -> Options -> Options
applyRefinementMethod (rtype, mtype) opts =
        opts { optRefinementType = rtype, optMinimizeRefinement = mtype }

type RefinementMethod = (Maybe RefinementType, Int)

refinementMethods :: [RefinementMethod]
refinementMethods =
        [(Just SComponentRefinement, 0)
        ,(Just SComponentWithCutRefinement, 1)
        ,(Just SComponentWithCutRefinement, 2)
        ]

Philipp Meyer's avatar
Philipp Meyer committed
307
308
309
checkLivenessProperty :: PetriNet ->
        Formula Transition -> OptIO PropResult
checkLivenessProperty net f = do
310
311
312
313
        let methods = map (local . applyRefinementMethod) refinementMethods
        auto <- opt optAuto
        r <-
            if auto then do
314
                rAll <- parallelIO $ map ($ checkLivenessProperty' net f []) methods
315
316
317
318
319
320
321
322
323
                verbosePut 2 $
                    "Number of refinements in tested methods: " ++ show (map (length . snd) rAll)
                let rSucc = filter (isNothing . fst) rAll
                if null rSucc then
                    return (Nothing, [])
                else
                    return $ minimumBy (comparing (length . snd)) rSucc
            else
                checkLivenessProperty' net f []
324
        case r of
325
326
            (Nothing, cuts) -> do
                verbosePut 2 $ "Number of refinements: " ++ show (length cuts)
Philipp Meyer's avatar
Philipp Meyer committed
327
                invariant <- opt optInvariant
328
329
                if invariant then
                    getLivenessInvariant net f cuts >>= printInvariant
330
331
                else
                    return Satisfied
332
            (Just _, _) ->
333
                return Unknown
334

335
336
getLivenessInvariant :: PetriNet -> Formula Transition -> [Cut] ->
        OptIO (Maybe [LivenessInvariant], [LivenessInvariant])
337
getLivenessInvariant net f cuts = do
338
        dnfCuts <- generateCuts net f cuts
339
        verbosePut 2 $ "Number of disjuncts: " ++ show (length dnfCuts)
340
        invs <- parallelIO (map (checkSat . checkLivenessInvariantSat net f) dnfCuts)
341
342
        let cutInvs = map cutToLivenessInvariant cuts
        return (sequence invs, cutInvs)
343

Philipp Meyer's avatar
Philipp Meyer committed
344
345
346
347
checkLivenessProperty' :: PetriNet ->
        Formula Transition -> [Cut] -> OptIO (Maybe FiringVector, [Cut])
checkLivenessProperty' net f cuts = do
        r <- checkSat $ checkTransitionInvariantSat net f cuts
Philipp Meyer's avatar
Philipp Meyer committed
348
        case r of
349
            Nothing -> return (Nothing, cuts)
Philipp Meyer's avatar
Philipp Meyer committed
350
            Just x -> do
351
352
353
354
355
356
                rt <- findLivenessRefinement net x
                case rt of
                    Nothing ->
                        return (Just x, cuts)
                    Just cut ->
                        checkLivenessProperty' net f (cut:cuts)
357

Philipp Meyer's avatar
Philipp Meyer committed
358
359
360
findLivenessRefinement :: PetriNet -> FiringVector ->
        OptIO (Maybe Cut)
findLivenessRefinement net x = do
361
362
        refinementType <- opt optRefinementType
        case refinementType of
363
            Just TrapRefinement ->
364
                findLivenessRefinementByEmptyTraps net (initialMarking net) x []
365
            Just SComponentRefinement -> do
366
367
368
369
370
                r1 <- findLivenessRefinementBySComponent net x
                case r1 of
                    Nothing -> findLivenessRefinementByEmptyTraps net
                                                      (initialMarking net) x []
                    Just _ -> return r1
371
372
373
374
375
376
377
            Just SComponentWithCutRefinement -> do
                r1 <- findLivenessRefinementBySComponentWithCut net x
                case r1 of
                    Nothing -> findLivenessRefinementByEmptyTraps net
                                                      (initialMarking net) x []
                    Just _ -> return r1
            Nothing -> return Nothing
378

Philipp Meyer's avatar
Philipp Meyer committed
379
380
findLivenessRefinementBySComponent :: PetriNet -> FiringVector ->
        OptIO (Maybe Cut)
381
findLivenessRefinementBySComponent net x =
382
383
384
385
386
        checkSatMin $ checkSComponentSat net x

findLivenessRefinementBySComponentWithCut :: PetriNet -> FiringVector ->
        OptIO (Maybe Cut)
findLivenessRefinementBySComponentWithCut net x =
387
        checkSatMin $ checkSComponentWithCutSat net x
388

Philipp Meyer's avatar
Philipp Meyer committed
389
390
391
findLivenessRefinementByEmptyTraps :: PetriNet -> Marking -> FiringVector ->
        [Trap] -> OptIO (Maybe Cut)
findLivenessRefinementByEmptyTraps net m x traps = do
392
        r <- checkSatMin $ checkSubnetEmptyTrapSat net m x
393
394
        case r of
            Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
395
                rm <- refineSafetyProperty net FTrue traps m
396
                case rm of
397
                    (Nothing, _) -> do
398
                        cut <- generateLivenessRefinement net x traps
399
                        return $ Just cut
400
401
402
                    (Just _, _) ->
                        return Nothing
            Just trap -> do
403
                let traps' = trap:traps
404
                rm <- local (\opts -> opts { optRefinementType = Nothing }) $
Philipp Meyer's avatar
Philipp Meyer committed
405
                            checkSafetyProperty' net FTrue traps'
406
                case rm of
407
                    (Nothing, _) -> do
408
                        cut <- generateLivenessRefinement net x traps'
409
                        return $ Just cut
410
                    (Just m', _) ->
Philipp Meyer's avatar
Philipp Meyer committed
411
                        findLivenessRefinementByEmptyTraps net m' x traps'
412

413
414
generateLivenessRefinement :: PetriNet -> FiringVector -> [Trap] -> OptIO Cut
generateLivenessRefinement net x traps = do
415
        -- TODO: also use better cuts for traps
416
        let cut = constructCut net x traps
Philipp Meyer's avatar
Philipp Meyer committed
417
        verbosePut 3 $ "- cut: " ++ show cut
418
        return cut
419

Philipp Meyer's avatar
Philipp Meyer committed
420
421
checkStructuralProperty :: PetriNet -> Structure -> OptIO PropResult
checkStructuralProperty net struct =
422
423
424
425
        if checkStructure net struct then
            return Satisfied
        else
            return Unsatisfied
426

427
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
428
main = do
429
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
430
431
432
433
434
        args <- parseArgs
        case args of
            Left err -> exitErrorWith err
            Right (opts, files) -> do
                when (optShowVersion opts) (exitSuccessWith "Version 0.01")
Philipp Meyer's avatar
Philipp Meyer committed
435
                when (optShowHelp opts) (exitSuccessWith usageInformation)
436
                when (null files) (exitErrorWith "No input file given")
Philipp Meyer's avatar
Philipp Meyer committed
437
438
439
440
441
                let opts' = opts {
                        optProperties = reverse (optProperties opts),
                        optTransformations= reverse (optTransformations opts)
                    }
                rs <- runReaderT (mapM checkFile files) opts'
442
443
                -- TODO: short-circuit with Control.Monad.Loops? parallel
                -- execution?
444
445
446
447
448
449
450
                case resultsAnd rs of
                    Satisfied ->
                        exitSuccessWith "All properties satisfied."
                    Unsatisfied ->
                        exitFailureWith "Some properties are not satisfied"
                    Unknown ->
                        exitFailureWith "Some properties may not be satisfied."
451

Philipp Meyer's avatar
Philipp Meyer committed
452
-- TODO: Always exit with exit code 0 unless an error occured
453
454
455
exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
456
        cleanupAndExitWith ExitSuccess
457
458
459
460

exitFailureWith :: String -> IO ()
exitFailureWith msg = do
        putStrLn msg
461
        cleanupAndExitWith $ ExitFailure 2
Philipp Meyer's avatar
Philipp Meyer committed
462

463
464
465
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
466
467
468
469
470
471
        cleanupAndExitWith $ ExitFailure 3

cleanupAndExitWith :: ExitCode -> IO ()
cleanupAndExitWith code = do
        stopGlobalPool
        exitWith code