Main.hs 20.9 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.BooleanTransitionInvariant
34
import Solver.SubnetEmptyTrap
35
import Solver.LivenessInvariant
36
import Solver.SafetyInvariant
37
import Solver.SComponentWithCut
38
import Solver.SComponent
39
import Solver.Simplifier
40
--import Solver.Interpolant
41
--import Solver.CommFreeReachability
42

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

Philipp Meyer's avatar
Philipp Meyer committed
73
structuralAnalysis :: PetriNet -> OptIO ()
74
75
76
77
78
79
80
81
82
83
84
85
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
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
        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
105
        let props' = if useProperties then props else []
Philipp Meyer's avatar
Philipp Meyer committed
106
        implicitProperties <- opt optProperties
107
        let props'' = props' ++ map (makeImplicitProperty net) implicitProperties
Philipp Meyer's avatar
Philipp Meyer committed
108
        transformations <- opt optTransformations
109
        let (net',props''') = foldl transformNet (net,props'') transformations
Philipp Meyer's avatar
Philipp Meyer committed
110
111
        verbosePut 1 $ "Analyzing " ++ showNetName net
        verbosePut 2 $
112
113
114
115
116
117
118
                "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
119
        printStruct <- opt optPrintStructure
120
        when printStruct $ structuralAnalysis net
Philipp Meyer's avatar
Philipp Meyer committed
121
122
        verbosePut 3 $ show net'
        output <- opt optOutput
123
        case output of
124
            Just outputfile ->
Philipp Meyer's avatar
Philipp Meyer committed
125
                writeFiles outputfile net' props'''
126
            Nothing -> return ()
127
        -- TODO: short-circuit? parallel?
Philipp Meyer's avatar
Philipp Meyer committed
128
129
        rs <- mapM (checkProperty net') props'''
        verbosePut 0 ""
130
        return $ resultsAnd rs
131

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

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

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

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

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

247
248
249
250
251
252
253
254
255
256
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
257
            Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
258
                verbosePut 0 "No invariant found"
Philipp Meyer's avatar
Philipp Meyer committed
259
                return Unknown
260
            Just baseInv -> do
Philipp Meyer's avatar
Philipp Meyer committed
261
                verbosePut 0 "Invariant found"
262
263
264
                let baseSize = map invariantSize baseInv
                let addedSize = map invariantSize addedInv
                verbosePut 2 $ "Number of atoms in base invariants: " ++ show baseSize ++
265
                        " (total of " ++ show (sum baseSize) ++ ")"
266
                verbosePut 2 $ "Number of atoms in added invariants: " ++ show addedSize ++
267
                        " (total of " ++ show (sum addedSize) ++ ")"
268
269
                mapM_ (putLine . show) baseInv
                mapM_ (putLine . show) addedInv
Philipp Meyer's avatar
Philipp Meyer committed
270
271
                return Satisfied

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

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

295
296
297
298
299
300
301
302
303
304
305
306
307
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
308
309
310
checkLivenessProperty :: PetriNet ->
        Formula Transition -> OptIO PropResult
checkLivenessProperty net f = do
311
312
313
314
        let methods = map (local . applyRefinementMethod) refinementMethods
        auto <- opt optAuto
        r <-
            if auto then do
315
                rAll <- parallelIO $ map ($ checkLivenessProperty' net f []) methods
316
317
318
319
320
321
322
323
324
                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 []
325
        case r of
326
327
            (Nothing, cuts) -> do
                verbosePut 2 $ "Number of refinements: " ++ show (length cuts)
328
329
330
                let cutSizes= map (invariantSize . cutToLivenessInvariant) cuts
                verbosePut 2 $ "Number of atoms in refinements: " ++ show cutSizes ++
                        " (total of " ++ show (sum cutSizes) ++ ")"
Philipp Meyer's avatar
Philipp Meyer committed
331
                invariant <- opt optInvariant
332
333
                if invariant then
                    getLivenessInvariant net f cuts >>= printInvariant
334
335
                else
                    return Satisfied
336
            (Just _, _) ->
337
                return Unknown
338

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

Philipp Meyer's avatar
Philipp Meyer committed
348
349
350
checkLivenessProperty' :: PetriNet ->
        Formula Transition -> [Cut] -> OptIO (Maybe FiringVector, [Cut])
checkLivenessProperty' net f cuts = do
351
352
353
354
        boolConst <- opt optBoolConst
        r <- if boolConst
                then checkSat $ checkBooleanTransitionInvariantSat net f cuts
                else checkSat $ checkTransitionInvariantSat net f cuts
Philipp Meyer's avatar
Philipp Meyer committed
355
        case r of
356
            Nothing -> return (Nothing, cuts)
Philipp Meyer's avatar
Philipp Meyer committed
357
            Just x -> do
358
359
360
361
362
363
                rt <- findLivenessRefinement net x
                case rt of
                    Nothing ->
                        return (Just x, cuts)
                    Just cut ->
                        checkLivenessProperty' net f (cut:cuts)
364

Philipp Meyer's avatar
Philipp Meyer committed
365
366
367
findLivenessRefinement :: PetriNet -> FiringVector ->
        OptIO (Maybe Cut)
findLivenessRefinement net x = do
368
369
        refinementType <- opt optRefinementType
        case refinementType of
370
            Just TrapRefinement ->
371
                findLivenessRefinementByEmptyTraps net x
372
            Just SComponentRefinement -> do
373
374
                r1 <- findLivenessRefinementBySComponent net x
                case r1 of
375
                    Nothing -> findLivenessRefinementByEmptyTraps net x
376
                    Just _ -> return r1
377
378
379
            Just SComponentWithCutRefinement -> do
                r1 <- findLivenessRefinementBySComponentWithCut net x
                case r1 of
380
                    Nothing -> findLivenessRefinementByEmptyTraps net x
381
382
                    Just _ -> return r1
            Nothing -> return Nothing
383

Philipp Meyer's avatar
Philipp Meyer committed
384
385
findLivenessRefinementBySComponent :: PetriNet -> FiringVector ->
        OptIO (Maybe Cut)
386
findLivenessRefinementBySComponent net x =
387
388
389
390
391
        checkSatMin $ checkSComponentSat net x

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

394
395
396
397
398
399
400
findLivenessRefinementByEmptyTraps :: PetriNet -> FiringVector -> OptIO (Maybe Cut)
findLivenessRefinementByEmptyTraps net x =
        findLivenessRefinementByEmptyTraps' net (initialMarking net) x [] True

findLivenessRefinementByEmptyTraps' :: PetriNet -> Marking -> FiringVector ->
        [Trap] -> Bool -> OptIO (Maybe Cut)
findLivenessRefinementByEmptyTraps' net m x traps cont = do
401
        r <- checkSatMin $ checkSubnetEmptyTrapSat net m x
402
403
        case r of
            Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
404
                rm <- refineSafetyProperty net FTrue traps m
405
406
                case (rm, cont) of
                    ((Nothing, _), _) -> do
Philipp Meyer's avatar
Philipp Meyer committed
407
                        -- TODO: include traps needed for proving safety
408
                        cut <- generateLivenessRefinement net x traps
409
                        return $ Just cut
410
411
412
                    ((Just m', _), True) ->
                        findLivenessRefinementByEmptyTraps' net m' x traps False
                    ((Just _, _), False) ->
413
414
                        return Nothing
            Just trap -> do
415
                let traps' = trap:traps
416
                rm <- local (\opts -> opts { optRefinementType = Nothing }) $
Philipp Meyer's avatar
Philipp Meyer committed
417
                            checkSafetyProperty' net FTrue traps'
418
                case rm of
419
                    (Nothing, _) -> do
420
                        cut <- generateLivenessRefinement net x traps'
421
                        return $ Just cut
422
                    (Just m', _) ->
423
                        findLivenessRefinementByEmptyTraps' net m' x traps' True
424

425
426
generateLivenessRefinement :: PetriNet -> FiringVector -> [Trap] -> OptIO Cut
generateLivenessRefinement net x traps = do
427
        -- TODO: also use better cuts for traps
428
        let cut = constructCut net x traps
Philipp Meyer's avatar
Philipp Meyer committed
429
        verbosePut 3 $ "- cut: " ++ show cut
430
        return cut
431

Philipp Meyer's avatar
Philipp Meyer committed
432
433
checkStructuralProperty :: PetriNet -> Structure -> OptIO PropResult
checkStructuralProperty net struct =
434
435
436
437
        if checkStructure net struct then
            return Satisfied
        else
            return Unsatisfied
438

439
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
440
main = do
441
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
442
443
444
445
446
        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
447
                when (optShowHelp opts) (exitSuccessWith usageInformation)
448
                when (null files) (exitErrorWith "No input file given")
Philipp Meyer's avatar
Philipp Meyer committed
449
450
451
452
453
                let opts' = opts {
                        optProperties = reverse (optProperties opts),
                        optTransformations= reverse (optTransformations opts)
                    }
                rs <- runReaderT (mapM checkFile files) opts'
454
455
                -- TODO: short-circuit with Control.Monad.Loops? parallel
                -- execution?
456
457
458
459
460
461
462
                case resultsAnd rs of
                    Satisfied ->
                        exitSuccessWith "All properties satisfied."
                    Unsatisfied ->
                        exitFailureWith "Some properties are not satisfied"
                    Unknown ->
                        exitFailureWith "Some properties may not be satisfied."
463

Philipp Meyer's avatar
Philipp Meyer committed
464
-- TODO: Always exit with exit code 0 unless an error occured
465
466
467
exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
468
        cleanupAndExitWith ExitSuccess
469
470
471
472

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

475
476
477
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
478
479
480
481
482
483
        cleanupAndExitWith $ ExitFailure 3

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