Main.hs 23.7 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
37
38
39
40
41
42
data OutputFormat = OutLOLA | OutSARA | OutSPEC | OutDOT deriving (Read)

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

44
45
data NetTransformation = TerminationByReachability
                       | ValidateIdentifiers
46

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

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

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

options :: [ OptDescr (Options -> Either String Options) ]
options =
87
88
89
90
91
92
93
94
95
96
97
        [ 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"
98

99
100
101
102
        , Option "" ["spec"]
        (NoArg (\opt -> Right opt { inputFormat = MIST }))
        "Use the mist input format"

103
104
105
106
        , Option "s" ["structure"]
        (NoArg (\opt -> Right opt { optPrintStructure = True }))
        "Print structural information"

107
108
109
110
111
112
        , Option "" ["validate-identifiers"]
        (NoArg (\opt -> Right opt {
            optTransformations = ValidateIdentifiers : optTransformations opt
          }))
        "Make identifiers valid for lola"

113
        , Option "" ["termination-by-reachability"]
114
        (NoArg (\opt -> Right opt {
115
            optTransformations = TerminationByReachability : optTransformations opt
116
          }))
117
        "Prove termination by reducing it to reachability"
118

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

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

131
        , Option "" ["deadlock-free"]
132
        (NoArg (\opt -> Right opt {
133
                   optProperties = DeadlockFree : optProperties opt
134
               }))
135
        "Prove that the net is deadlock-free"
136

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

144
145
146
147
148
149
        , Option "" ["final-state-unreachable"]
        (NoArg (\opt -> Right opt {
                   optProperties = FinalStateUnreachable : optProperties opt
               }))
        "Prove that the final state is unreachable"

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

165
166
167
168
169
170
        , Option "" ["free-choice"]
        (NoArg (\opt -> Right opt {
                   optProperties = StructFreeChoice : optProperties opt
               }))
        "Prove that the net is free-choice"

171
172
173
174
175
176
177
178
179
180
181
182
        , 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"

183
184
185
186
187
188
        , Option "" ["communication-free"]
        (NoArg (\opt -> Right opt {
                   optProperties = StructCommunicationFree : optProperties opt
               }))
        "Prove that the net is communication-free"

189
190
191
192
        , Option "n" ["no-refinement"]
        (NoArg (\opt -> Right opt { optRefine = False }))
        "Don't use refinement"

193
194
195
196
197
198
199
        , Option "o" ["output"]
        (ReqArg (\arg opt -> Right opt {
                        optOutput = Just arg
                })
                "FILE")
        "Write net and properties to FILE"

200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
        , 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"

216
217
218
219
220
221
        , Option "" ["no-given-properties"]
        (NoArg (\opt -> Right opt {
                   optUseProperties = False
               }))
        "Do not use the properties given in the input file"

222
        , Option "v" ["verbose"]
223
224
225
226
227
228
        (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)"
229
230
231
232
233
234
235
236
237
238

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

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

239
240
241
242
verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
        when (verbosity >= level) (putStrLn str)

243
244
245
246
247
248
249
250
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

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

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

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

327
placeOp :: Op -> (String, Integer) -> Formula
328
placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w)
329

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

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

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

428
checkSafetyProperty :: Int -> PetriNet -> Bool ->
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
        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 ->
448
        Formula -> [[String]] -> IO PropResult
449
checkSafetyPropertyBySafetyRef verbosity net refine f traps = do
450
451
        r <- checkSat $ checkStateEquationSat net f traps
        case r of
452
            Nothing -> return Satisfied
453
454
            Just a -> do
                let assigned = markedPlacesFromAssignment net a
455
456
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Places marked: " ++ show assigned
457
                verbosePut verbosity 3 $ "Assignment: " ++ show a
458
459
460
461
                if refine then do
                    rt <- checkSat $ checkTrapSat net assigned
                    case rt of
                        Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
462
                            verbosePut verbosity 1 "No trap found."
463
                            return Unknown
464
465
                        Just at -> do
                            let trap = trapFromAssignment at
466
467
468
                            verbosePut verbosity 1 "Trap found"
                            verbosePut verbosity 2 $ "Places in trap: " ++
                                                      show trap
469
470
                            verbosePut verbosity 3 $ "Trap assignment: " ++
                                                      show at
471
472
                            checkSafetyPropertyBySafetyRef verbosity net
                                                refine f (trap:traps)
473
                else
474
                    return Unknown
475

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

checkStructuralProperty :: Int -> PetriNet -> Structure -> IO PropResult
505
checkStructuralProperty _ net struct =
506
507
508
509
        if checkStructure net struct then
            return Satisfied
        else
            return Unsatisfied
510

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

Philipp Meyer's avatar
Philipp Meyer committed
543
-- TODO: Always exit with exit code 0 unless an error occured
544
545
546
547
548
549
550
551
exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
        exitSuccess

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

554
555
556
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
557
        exitWith $ ExitFailure 3