In January 2021 we will introduce a 10 GB quota for project repositories. Higher limits for individual projects will be available on request. Please see https://doku.lrz.de/display/PUBLIC/GitLab for more information.

Main.hs 21.5 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.UniqueTerminalMarking
41
--import Solver.Interpolant
42
--import Solver.CommFreeReachability
43

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

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

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

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

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

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

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

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

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

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

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

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

Philipp Meyer's avatar
Philipp Meyer committed
352 353 354
checkLivenessProperty' :: PetriNet ->
        Formula Transition -> [Cut] -> OptIO (Maybe FiringVector, [Cut])
checkLivenessProperty' net f cuts = do
355 356 357 358
        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
359
        case r of
360
            Nothing -> return (Nothing, cuts)
Philipp Meyer's avatar
Philipp Meyer committed
361
            Just x -> do
362 363 364 365 366 367
                rt <- findLivenessRefinement net x
                case rt of
                    Nothing ->
                        return (Just x, cuts)
                    Just cut ->
                        checkLivenessProperty' net f (cut:cuts)
368

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

Philipp Meyer's avatar
Philipp Meyer committed
388 389
findLivenessRefinementBySComponent :: PetriNet -> FiringVector ->
        OptIO (Maybe Cut)
390
findLivenessRefinementBySComponent net x =
391 392 393 394 395
        checkSatMin $ checkSComponentSat net x

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

398 399 400 401 402 403 404
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
405
        r <- checkSatMin $ checkSubnetEmptyTrapSat net m x
406 407
        case r of
            Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
408
                rm <- refineSafetyProperty net FTrue traps m
409 410
                case (rm, cont) of
                    ((Nothing, _), _) -> do
Philipp Meyer's avatar
Philipp Meyer committed
411
                        -- TODO: include traps needed for proving safety
412
                        cut <- generateLivenessRefinement net x traps
413
                        return $ Just cut
414 415 416
                    ((Just m', _), True) ->
                        findLivenessRefinementByEmptyTraps' net m' x traps False
                    ((Just _, _), False) ->
417 418
                        return Nothing
            Just trap -> do
419
                let traps' = trap:traps
420
                rm <- local (\opts -> opts { optRefinementType = Nothing }) $
Philipp Meyer's avatar
Philipp Meyer committed
421
                            checkSafetyProperty' net FTrue traps'
422
                case rm of
423
                    (Nothing, _) -> do
424
                        cut <- generateLivenessRefinement net x traps'
425
                        return $ Just cut
426
                    (Just m', _) ->
427
                        findLivenessRefinementByEmptyTraps' net m' x traps' True
428

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

Philipp Meyer's avatar
Philipp Meyer committed
436 437
checkStructuralProperty :: PetriNet -> Structure -> OptIO PropResult
checkStructuralProperty net struct =
438 439 440 441
        if checkStructure net struct then
            return Satisfied
        else
            return Unsatisfied
442

443 444 445 446 447 448 449 450 451
checkConstraintProperty :: PetriNet -> ConstraintProperty -> OptIO PropResult
checkConstraintProperty net cp = do
        let c = case cp of
                 UniqueTerminalMarkingConstraint -> checkUniqueTerminalMarkingSat
        r <- checkSat $ c net
        case r of
            Nothing -> return Satisfied
            Just _ -> return Unknown

452
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
453
main = do
454
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
455 456 457 458 459
        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
460
                when (optShowHelp opts) (exitSuccessWith usageInformation)
461
                when (null files) (exitErrorWith "No input file given")
Philipp Meyer's avatar
Philipp Meyer committed
462 463 464 465 466
                let opts' = opts {
                        optProperties = reverse (optProperties opts),
                        optTransformations= reverse (optTransformations opts)
                    }
                rs <- runReaderT (mapM checkFile files) opts'
467 468
                -- TODO: short-circuit with Control.Monad.Loops? parallel
                -- execution?
469 470 471 472 473 474 475
                case resultsAnd rs of
                    Satisfied ->
                        exitSuccessWith "All properties satisfied."
                    Unsatisfied ->
                        exitFailureWith "Some properties are not satisfied"
                    Unknown ->
                        exitFailureWith "Some properties may not be satisfied."
476

Philipp Meyer's avatar
Philipp Meyer committed
477
-- TODO: Always exit with exit code 0 unless an error occured
478 479 480
exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
481
        cleanupAndExitWith ExitSuccess
482 483 484 485

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

488 489 490
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
491 492 493 494 495 496
        cleanupAndExitWith $ ExitFailure 3

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