Main.hs 25.1 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.NonConsensusState
42
--import Solver.Interpolant
43
--import Solver.CommFreeReachability
44

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

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

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

137
138
transformNet :: (PetriNet, [Property]) -> NetTransformation ->
               (PetriNet, [Property])
139
transformNet (net, props) TerminationByReachability =
140
141
142
143
144
145
146
147
148
        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)] ++
149
                 linitials net ++ map (first primePlace) (linitials net)
150
151
            transformTransition t =
                let (preT, postT) = context net t
152
153
154
155
                    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
156
                in  if t `elem` ghostTransitions net then
157
                        [(t, (pre', post'))]
158
                    else
159
160
                        [(t, (pre', post')), (primeTransition t, (pre'', post''))]
            ts = (switch, ([(m1,1)], [(m2,1)])) :
161
                 concatMap transformTransition (transitions 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
168
        in  (makePetriNetWithTrans (name net) ps ts is
169
                (ghostTransitions net) (fixedTraps net) (fixedSiphons net) (yesStates net) (noStates net), prop : props)
170
transformNet (net, props) ValidateIdentifiers =
171
172
        (renamePetriNetPlacesAndTransitions validateId net,
         map (renameProperty validateId) props)
173

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

446
checkConstraintProperty :: PetriNet -> ConstraintProperty -> OptIO PropResult
447
448
449
checkConstraintProperty net cp =
        case cp of
            UniqueTerminalMarkingConstraint -> checkUniqueTerminalMarkingProperty net
450
            NonConsensusStateConstraint -> checkNonConsensusStateProperty net
451
452
453

checkUniqueTerminalMarkingProperty :: PetriNet -> OptIO PropResult
checkUniqueTerminalMarkingProperty net = do
454
        r <- checkUniqueTerminalMarkingProperty' net (fixedTraps net) (fixedSiphons net)
455
        case r of
456
457
            (Nothing, _, _) -> return Satisfied
            (Just _, _, _) -> return Unknown
458
459

checkUniqueTerminalMarkingProperty' :: PetriNet ->
460
        [Trap] -> [Siphon] ->
461
        OptIO (Maybe UniqueTerminalMarkingCounterExample, [Trap], [Siphon])
462
463
checkUniqueTerminalMarkingProperty' net traps siphons = do
        r <- checkSat $ checkUniqueTerminalMarkingSat net traps siphons
464
        case r of
465
            Nothing -> return (Nothing, traps, siphons)
466
            Just c -> do
467
468
                refine <- opt optRefinementType
                if isJust refine then
469
                    refineUniqueTerminalMarkingProperty net traps siphons c
470
                else
471
                    return (Just c, traps, siphons)
472
473

refineUniqueTerminalMarkingProperty :: PetriNet ->
474
475
        [Trap] -> [Siphon] -> UniqueTerminalMarkingCounterExample ->
        OptIO (Maybe UniqueTerminalMarkingCounterExample, [Trap], [Siphon])
476
477
refineUniqueTerminalMarkingProperty net traps siphons c@(m0, m1, m2, x1, x2) = do
        r1 <- checkSatMin $ Solver.UniqueTerminalMarking.checkUnmarkedTrapSat net m0 m1 m2 x1 x2
478
479
        case r1 of
            Nothing -> do
480
                r2 <- checkSatMin $ Solver.UniqueTerminalMarking.checkUnmarkedSiphonSat net m0 m1 m2 x1 x2
481
                case r2 of
482
                    Nothing ->
483
                        return (Just c, traps, siphons)
484
485
                    Just siphon ->
                        checkUniqueTerminalMarkingProperty' net traps (siphon:siphons)
486
            Just trap ->
487
                checkUniqueTerminalMarkingProperty' net (trap:traps) siphons
488

489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
checkNonConsensusStateProperty :: PetriNet -> OptIO PropResult
checkNonConsensusStateProperty net = do
        r <- checkNonConsensusStateProperty' net (fixedTraps net) (fixedSiphons net)
        case r of
            (Nothing, _, _) -> return Satisfied
            (Just _, _, _) -> return Unknown

checkNonConsensusStateProperty' :: PetriNet ->
        [Trap] -> [Siphon] ->
        OptIO (Maybe NonConsensusStateCounterExample, [Trap], [Siphon])
checkNonConsensusStateProperty' net traps siphons = do
        r <- checkSat $ checkNonConsensusStateSat net traps siphons
        case r of
            Nothing -> return (Nothing, traps, siphons)
            Just c -> do
                refine <- opt optRefinementType
                if isJust refine then
                    refineNonConsensusStateProperty net traps siphons c
                else
                    return (Just c, traps, siphons)

refineNonConsensusStateProperty :: PetriNet ->
        [Trap] -> [Siphon] -> NonConsensusStateCounterExample ->
        OptIO (Maybe NonConsensusStateCounterExample, [Trap], [Siphon])
refineNonConsensusStateProperty net traps siphons c@(m0, m, x) = do
        r1 <- checkSatMin $ Solver.NonConsensusState.checkUnmarkedTrapSat net m0 m x
        case r1 of
            Nothing -> do
                r2 <- checkSatMin $ Solver.NonConsensusState.checkUnmarkedSiphonSat net m0 m x
                case r2 of
                    Nothing ->
                        return (Just c, traps, siphons)
                    Just siphon ->
                        checkNonConsensusStateProperty' net traps (siphon:siphons)
            Just trap ->
                checkNonConsensusStateProperty' net (trap:traps) siphons

526
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
527
main = do
528
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
529
530
531
532
533
        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
534
                when (optShowHelp opts) (exitSuccessWith usageInformation)
535
                when (null files) (exitErrorWith "No input file given")
Philipp Meyer's avatar
Philipp Meyer committed
536
537
538
539
540
                let opts' = opts {
                        optProperties = reverse (optProperties opts),
                        optTransformations= reverse (optTransformations opts)
                    }
                rs <- runReaderT (mapM checkFile files) opts'
541
542
                -- TODO: short-circuit with Control.Monad.Loops? parallel
                -- execution?
543
544
545
546
547
548
549
                case resultsAnd rs of
                    Satisfied ->
                        exitSuccessWith "All properties satisfied."
                    Unsatisfied ->
                        exitFailureWith "Some properties are not satisfied"
                    Unknown ->
                        exitFailureWith "Some properties may not be satisfied."
550

Philipp Meyer's avatar
Philipp Meyer committed
551
-- TODO: Always exit with exit code 0 unless an error occured
552
553
554
exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
555
        cleanupAndExitWith ExitSuccess
556
557
558
559

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

562
563
564
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
565
566
567
568
569
570
        cleanupAndExitWith $ ExitFailure 3

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