Main.hs 27.6 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.NonConsensusState
43
import Solver.TerminalMarkingReachable
44
--import Solver.Interpolant
45
--import Solver.CommFreeReachability
46

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

450
checkConstraintProperty :: PetriNet -> ConstraintProperty -> OptIO PropResult
451
452
checkConstraintProperty net cp =
        case cp of
453
            TerminalMarkingsUniqueConsensusConstraint -> checkTerminalMarkingsUniqueConsensusProperty net
454
            NonConsensusStateConstraint -> checkNonConsensusStateProperty net
455
            TerminalMarkingReachableConstraint -> checkTerminalMarkingReachableProperty net
456

457
458
459
checkTerminalMarkingsUniqueConsensusProperty :: PetriNet -> OptIO PropResult
checkTerminalMarkingsUniqueConsensusProperty net = do
        r <- checkTerminalMarkingsUniqueConsensusProperty' net (fixedTraps net) (fixedSiphons net)
460
        case r of
461
462
            (Nothing, _, _) -> return Satisfied
            (Just _, _, _) -> return Unknown
463

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

478
479
480
481
482
refineTerminalMarkingsUniqueConsensusProperty :: PetriNet ->
        [Trap] -> [Siphon] -> TerminalMarkingsUniqueConsensusCounterExample ->
        OptIO (Maybe TerminalMarkingsUniqueConsensusCounterExample, [Trap], [Siphon])
refineTerminalMarkingsUniqueConsensusProperty net traps siphons c@(m0, m1, m2, x1, x2) = do
        r1 <- checkSatMin $ Solver.TerminalMarkingsUniqueConsensus.checkUnmarkedTrapSat net m0 m1 m2 x1 x2
483
484
        case r1 of
            Nothing -> do
485
                r2 <- checkSatMin $ Solver.TerminalMarkingsUniqueConsensus.checkUnmarkedSiphonSat net m0 m1 m2 x1 x2
486
                case r2 of
487
                    Nothing ->
488
                        return (Just c, traps, siphons)
489
                    Just siphon ->
490
                        checkTerminalMarkingsUniqueConsensusProperty' net traps (siphon:siphons)
491
            Just trap ->
492
                checkTerminalMarkingsUniqueConsensusProperty' net (trap:traps) siphons
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
526
527
528
529
530
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

531
532
533
534
535
536
537
checkTerminalMarkingReachableProperty :: PetriNet -> OptIO PropResult
checkTerminalMarkingReachableProperty net = do
        let triplets = generateTriplets net
        let trivialTriplets = filter trivialTriplet triplets
        let nonTrivialTriplets = filter (not . trivialTriplet) triplets
        let emptyTriplets = filter emptyTriplet triplets
        let nonTrivialNonEmptyTriplets = filter (not . emptyTriplet) nonTrivialTriplets
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
--      TODO optimize triplet computation
--        liftIO $ putStrLn $ "All triplets (" ++ show (length triplets) ++ "):"
--        liftIO $ putStrLn $ unlines $ map show triplets
--        liftIO $ putStrLn $ "Trivial triplets (" ++ show (length trivialTriplets) ++ "):"
--        liftIO $ putStrLn $ unlines $ map show trivialTriplets
--        liftIO $ putStrLn $ "Empty triplets (" ++ show (length emptyTriplets) ++ "):"
--        liftIO $ putStrLn $ unlines $ map show emptyTriplets
--        liftIO $ putStrLn $ "Non-trivial, non-empty triplets (" ++ show (length nonTrivialNonEmptyTriplets) ++ "):"
--        liftIO $ putStrLn $ unlines $ map show nonTrivialNonEmptyTriplets
        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"
        r <- checkSat $ checkTerminalMarkingReachableSat net triplets k
553
        case r of
554
555
556
557
558
            Nothing ->
                if k < kmax then
                    checkTerminalMarkingReachableProperty' net triplets (k + 1) kmax
                else
                    return Unknown
559
560
561
562
563
564
565
            Just inv -> do
                invariant <- opt optInvariant
                if invariant then
                    printInvariant (Just inv, [])
                else
                    return Satisfied

566
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
567
main = do
568
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
569
570
571
572
573
        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
574
                when (optShowHelp opts) (exitSuccessWith usageInformation)
575
                when (null files) (exitErrorWith "No input file given")
Philipp Meyer's avatar
Philipp Meyer committed
576
577
578
579
580
                let opts' = opts {
                        optProperties = reverse (optProperties opts),
                        optTransformations= reverse (optTransformations opts)
                    }
                rs <- runReaderT (mapM checkFile files) opts'
581
582
                -- TODO: short-circuit with Control.Monad.Loops? parallel
                -- execution?
583
584
585
586
587
588
589
                case resultsAnd rs of
                    Satisfied ->
                        exitSuccessWith "All properties satisfied."
                    Unsatisfied ->
                        exitFailureWith "Some properties are not satisfied"
                    Unknown ->
                        exitFailureWith "Some properties may not be satisfied."
590

Philipp Meyer's avatar
Philipp Meyer committed
591
-- TODO: Always exit with exit code 0 unless an error occured
592
593
594
exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
595
        cleanupAndExitWith ExitSuccess
596
597
598
599

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

602
603
604
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
605
606
607
608
609
610
        cleanupAndExitWith $ ExitFailure 3

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