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
455
        r <- checkTerminalMarkingsUniqueConsensusProperty' net (fixedTraps net) (fixedSiphons net) []
456
        case r of
457
458
            (Nothing, _, _, _) -> return Satisfied
            (Just _, _, _, _) -> return Unknown
459

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

474
refineTerminalMarkingsUniqueConsensusProperty :: PetriNet ->
475
476
477
        [Trap] -> [Siphon] -> [StableInequality] -> TerminalMarkingsUniqueConsensusCounterExample ->
        OptIO (Maybe TerminalMarkingsUniqueConsensusCounterExample, [Trap], [Siphon], [StableInequality])
refineTerminalMarkingsUniqueConsensusProperty net traps siphons inequalities c@(m0, m1, m2, x1, x2) = do
478
        r1 <- checkSatMin $ Solver.TerminalMarkingsUniqueConsensus.checkUnmarkedTrapSat net m0 m1 m2 x1 x2
479
480
        case r1 of
            Nothing -> do
481
482
483
484
485
486
487
488
489
490
491
                return (Just c, traps, siphons, inequalities)
--                r2 <- checkSatMin $ Solver.TerminalMarkingsUniqueConsensus.checkGeneralizedSiphonConstraintsSat net m0 m1 m2 x1 x2
--                case r2 of
--                    Nothing -> do
--                        r3 <- checkSat $ Solver.TerminalMarkingsUniqueConsensus.checkGeneralizedCoTrapSat net m0 m1 m2 x1 x2
--                        case r3 of
--                            Nothing -> return (Just c, traps, siphons, inequalities)
--                            Just inequality ->
--                                checkTerminalMarkingsUniqueConsensusProperty' net traps siphons (inequality:inequalities)
--                    Just siphon ->
--                        checkTerminalMarkingsUniqueConsensusProperty' net traps (siphon:siphons) inequalities
492
            Just trap ->
493
                checkTerminalMarkingsUniqueConsensusProperty' net (trap:traps) siphons inequalities
494

495
496
checkTerminalMarkingReachableProperty :: PetriNet -> OptIO PropResult
checkTerminalMarkingReachableProperty net = do
497
        let nonTrivialTriplets = filter (not . trivialTriplet) $ generateTriplets net
498
499
500
501
502
        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"
503
        r <- checkSatMin $ checkTerminalMarkingReachableSat net triplets k
504
        case r of
505
506
507
508
509
            Nothing ->
                if k < kmax then
                    checkTerminalMarkingReachableProperty' net triplets (k + 1) kmax
                else
                    return Unknown
510
511
512
513
514
515
516
            Just inv -> do
                invariant <- opt optInvariant
                if invariant then
                    printInvariant (Just inv, [])
                else
                    return Satisfied

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

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

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

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

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