Main.hs 22.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.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
checkConstraintProperty :: PetriNet -> ConstraintProperty -> OptIO PropResult
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
checkConstraintProperty net cp =
        case cp of
            UniqueTerminalMarkingConstraint -> checkUniqueTerminalMarkingProperty net

checkUniqueTerminalMarkingProperty :: PetriNet -> OptIO PropResult
checkUniqueTerminalMarkingProperty net = do
        r <- checkUniqueTerminalMarkingProperty' net []
        case r of
            (Nothing, _) -> return Satisfied
            (Just _, _) -> return Unknown

checkUniqueTerminalMarkingProperty' :: PetriNet ->
        [Trap] -> OptIO (Maybe (Marking, Marking, Marking, FiringVector, FiringVector), [Trap])
checkUniqueTerminalMarkingProperty' net traps = do
        r <- checkSat $ checkUniqueTerminalMarkingSat net traps
459
        case r of
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
            Nothing -> return (Nothing, traps)
            Just m -> do
                refine <- opt optRefinementType
                if isJust refine then
                    refineUniqueTerminalMarkingProperty net traps m
                else
                    return (Just m, traps)

refineUniqueTerminalMarkingProperty :: PetriNet ->
        [Trap] -> (Marking, Marking, Marking, FiringVector, FiringVector) -> OptIO (Maybe (Marking, Marking, Marking, FiringVector, FiringVector), [Trap])
refineUniqueTerminalMarkingProperty net traps m@(m0, m1, m2, x1, x2) = do
        r1 <- checkSat $ checkUnmarkedTrapSat net m0 m1 x1
        case r1 of
            Nothing -> do
                r2 <- checkSat $ checkUnmarkedTrapSat net m0 m2 x2
                case r2 of
                    Nothing -> return (Just m, traps)
                    Just trap ->
                        checkUniqueTerminalMarkingProperty' net (trap:traps)
            Just trap ->
                checkUniqueTerminalMarkingProperty' net (trap:traps)
481

482
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
483
main = do
484
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
485
486
487
488
489
        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
490
                when (optShowHelp opts) (exitSuccessWith usageInformation)
491
                when (null files) (exitErrorWith "No input file given")
Philipp Meyer's avatar
Philipp Meyer committed
492
493
494
495
496
                let opts' = opts {
                        optProperties = reverse (optProperties opts),
                        optTransformations= reverse (optTransformations opts)
                    }
                rs <- runReaderT (mapM checkFile files) opts'
497
498
                -- TODO: short-circuit with Control.Monad.Loops? parallel
                -- execution?
499
500
501
502
503
504
505
                case resultsAnd rs of
                    Satisfied ->
                        exitSuccessWith "All properties satisfied."
                    Unsatisfied ->
                        exitFailureWith "Some properties are not satisfied"
                    Unknown ->
                        exitFailureWith "Some properties may not be satisfied."
506

Philipp Meyer's avatar
Philipp Meyer committed
507
-- TODO: Always exit with exit code 0 unless an error occured
508
509
510
exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
511
        cleanupAndExitWith ExitSuccess
512
513
514
515

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

518
519
520
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
521
522
523
524
525
526
        cleanupAndExitWith $ ExitFailure 3

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