Main.hs 25.4 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
import Data.List (partition,minimumBy,genericLength)
9
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 StructuralComputation
30
import Solver
31
import Solver.StateEquation
Philipp Meyer's avatar
Philipp Meyer committed
32
import Solver.TrapConstraints
33
import Solver.TransitionInvariant
34
import Solver.BooleanTransitionInvariant
35
import Solver.SubnetEmptyTrap
36
import Solver.LivenessInvariant
37
import Solver.SafetyInvariant
38
import Solver.SComponentWithCut
39
import Solver.SComponent
40
import Solver.Simplifier
41
import Solver.TerminalMarkingsUniqueConsensus
42
import Solver.TerminalMarkingReachable
43
--import Solver.Interpolant
44
--import Solver.CommFreeReachability
45

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

447
checkConstraintProperty :: PetriNet -> ConstraintProperty -> OptIO PropResult
448
449
checkConstraintProperty net cp =
        case cp of
450
            TerminalMarkingsUniqueConsensusConstraint -> checkTerminalMarkingsUniqueConsensusProperty net
451
            TerminalMarkingReachableConstraint -> checkTerminalMarkingReachableProperty net
452

453
454
checkTerminalMarkingsUniqueConsensusProperty :: PetriNet -> OptIO PropResult
checkTerminalMarkingsUniqueConsensusProperty net = do
Philipp J. Meyer's avatar
Philipp J. Meyer committed
455
        r <- checkTerminalMarkingsUniqueConsensusProperty' net (fixedTraps net) [] (fixedSiphons net) []
456
        case r of
Philipp J. Meyer's avatar
Philipp J. Meyer committed
457
458
            (Nothing, _, _, _, _) -> return Satisfied
            (Just _, _, _, _, _) -> return Unknown
459

460
checkTerminalMarkingsUniqueConsensusProperty' :: PetriNet ->
Philipp J. Meyer's avatar
Philipp J. Meyer committed
461
462
463
464
        [Trap] -> [Trap] -> [Siphon] -> [StableInequality] ->
        OptIO (Maybe TerminalMarkingsUniqueConsensusCounterExample, [Trap], [Trap], [Siphon], [StableInequality])
checkTerminalMarkingsUniqueConsensusProperty' net traps utraps usiphons inequalities = do
        r <- checkSat $ checkTerminalMarkingsUniqueConsensusSat net traps utraps usiphons inequalities
465
        case r of
Philipp J. Meyer's avatar
Philipp J. Meyer committed
466
            Nothing -> return (Nothing, traps, utraps, usiphons, inequalities)
467
            Just c -> do
468
469
                refine <- opt optRefinementType
                if isJust refine then
Philipp J. Meyer's avatar
Philipp J. Meyer committed
470
                    refineTerminalMarkingsUniqueConsensusProperty net traps utraps usiphons inequalities c
471
                else
Philipp J. Meyer's avatar
Philipp J. Meyer committed
472
                    return (Just c, traps, utraps, usiphons, inequalities)
473

474
refineTerminalMarkingsUniqueConsensusProperty :: PetriNet ->
Philipp J. Meyer's avatar
Philipp J. Meyer committed
475
476
477
478
        [Trap] -> [Trap] -> [Siphon] -> [StableInequality] -> TerminalMarkingsUniqueConsensusCounterExample ->
        OptIO (Maybe TerminalMarkingsUniqueConsensusCounterExample, [Trap], [Trap], [Siphon], [StableInequality])
refineTerminalMarkingsUniqueConsensusProperty net traps utraps usiphons inequalities c@(m0, m1, m2, x1, x2) = do
        r1 <- checkSatMin $ Solver.TerminalMarkingsUniqueConsensus.findTrapConstraintsSat net m0 m1 m2
479
480
        case r1 of
            Nothing -> do
Philipp J. Meyer's avatar
Philipp J. Meyer committed
481
                r2 <- checkSatMin $ Solver.TerminalMarkingsUniqueConsensus.findUSiphonConstraintsSat net m0 m1 m2 x1 x2
482
483
                case r2 of
                    Nothing -> do
Philipp J. Meyer's avatar
Philipp J. Meyer committed
484
485
486
487
488
489
490
                        r3 <- checkSatMin $ Solver.TerminalMarkingsUniqueConsensus.findUTrapConstraintsSat net m0 m1 m2 x1 x2
                        case r3 of
                            Nothing -> return (Just c, traps, utraps, usiphons, inequalities)
                            Just utrap ->
                                checkTerminalMarkingsUniqueConsensusProperty' net traps (utrap:utraps) usiphons inequalities
                    Just usiphon ->
                        checkTerminalMarkingsUniqueConsensusProperty' net traps utraps (usiphon:usiphons) inequalities
491
            Just trap ->
Philipp J. Meyer's avatar
Philipp J. Meyer committed
492
                checkTerminalMarkingsUniqueConsensusProperty' net (trap:traps) utraps usiphons inequalities
493

494
495
checkTerminalMarkingReachableProperty :: PetriNet -> OptIO PropResult
checkTerminalMarkingReachableProperty net = do
496
        let nonTrivialTriplets = filter (not . trivialTriplet) $ generateTriplets net
497
498
499
500
501
        checkTerminalMarkingReachableProperty' net nonTrivialTriplets 1 $ genericLength $ transitions net

checkTerminalMarkingReachableProperty' :: PetriNet -> [Triplet] -> Integer -> Integer -> OptIO PropResult
checkTerminalMarkingReachableProperty' net triplets k kmax = do
        verbosePut 1 $ "Checking terminal marking reachable with at most " ++ show k ++ " partitions"
502
        r <- checkSatMin $ checkTerminalMarkingReachableSat net triplets k
503
        case r of
504
505
506
507
508
            Nothing ->
                if k < kmax then
                    checkTerminalMarkingReachableProperty' net triplets (k + 1) kmax
                else
                    return Unknown
509
510
511
512
513
514
515
            Just inv -> do
                invariant <- opt optInvariant
                if invariant then
                    printInvariant (Just inv, [])
                else
                    return Satisfied

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

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

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

552
553
554
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
555
556
557
558
559
560
        cleanupAndExitWith $ ExitFailure 3

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