Main.hs 25.6 KB
Newer Older
1
2
{-# LANGUAGE TupleSections #-}

3
4
module Main where

Philipp Meyer's avatar
Philipp Meyer committed
5
import System.Environment (getArgs)
6
import System.Exit
7
8
9
import System.IO
import System.Console.GetOpt
import Control.Monad
10
import Control.Applicative ((<$>))
11
import Control.Arrow (first)
Philipp Meyer's avatar
Philipp Meyer committed
12
import Data.List (partition)
13
import qualified Data.ByteString.Lazy as L
Philipp Meyer's avatar
Philipp Meyer committed
14

Philipp Meyer's avatar
Philipp Meyer committed
15
import Util
16
17
import Parser
import qualified Parser.PNET as PNET
Philipp Meyer's avatar
Philipp Meyer committed
18
import qualified Parser.LOLA as LOLA
19
import qualified Parser.TPN as TPN
20
import qualified Parser.MIST as MIST
21
import PetriNet
22
import Printer
23
24
import qualified Printer.LOLA as LOLAPrinter
import qualified Printer.SARA as SARAPrinter
Philipp Meyer's avatar
Philipp Meyer committed
25
import qualified Printer.SPEC as SPECPrinter
26
import qualified Printer.DOT as DOTPrinter
27
import Property
28
import Structure
29
import Solver
30
import Solver.StateEquation
Philipp Meyer's avatar
Philipp Meyer committed
31
import Solver.TrapConstraints
32
import Solver.TransitionInvariant
33
import Solver.SubnetEmptyTrap
34
import Solver.LivenessInvariant
35
import Solver.SafetyInvariant
36
import Solver.SComponent
37
--import Solver.CommFreeReachability
38

39
data InputFormat = PNET | LOLA | TPN | MIST deriving (Show,Read)
40
41
42
43
44
45
46
data OutputFormat = OutLOLA | OutSARA | OutSPEC | OutDOT deriving (Read)

instance Show OutputFormat where
        show OutLOLA = "LOLA"
        show OutSARA = "SARA"
        show OutSPEC = "SPEC"
        show OutDOT = "DOT"
47

48
49
data NetTransformation = TerminationByReachability
                       | ValidateIdentifiers
50

51
data ImplicitProperty = Termination
52
                      | DeadlockFree | DeadlockFreeUnlessFinal
53
                      | FinalStateUnreachable
Philipp Meyer's avatar
Philipp Meyer committed
54
                      | ProperTermination
55
                      | Safe | Bounded Integer
56
                      | StructFreeChoice
57
58
                      | StructParallel
                      | StructFinalPlace
59
                      | StructCommunicationFree
60
61
                      deriving (Show,Read)

62
data Options = Options { inputFormat :: InputFormat
63
                       , optVerbosity :: Int
64
65
                       , optShowHelp :: Bool
                       , optShowVersion :: Bool
66
                       , optProperties :: [ImplicitProperty]
67
                       , optTransformations :: [NetTransformation]
68
                       , optRefine :: Bool
69
                       , optInvariant :: Bool
70
                       , optOutput :: Maybe String
71
                       , outputFormat :: OutputFormat
72
                       , optUseProperties :: Bool
73
                       , optPrintStructure :: Bool
74
75
76
77
                       }

startOptions :: Options
startOptions = Options { inputFormat = PNET
78
                       , optVerbosity = 1
79
80
                       , optShowHelp = False
                       , optShowVersion = False
81
                       , optProperties = []
82
                       , optTransformations = []
83
                       , optRefine = True
84
                       , optInvariant = False
85
                       , optOutput = Nothing
86
                       , outputFormat = OutLOLA
87
                       , optUseProperties = True
88
                       , optPrintStructure = False
89
90
91
92
                       }

options :: [ OptDescr (Options -> Either String Options) ]
options =
93
94
95
96
97
98
99
100
101
102
103
        [ Option "" ["pnet"]
        (NoArg (\opt -> Right opt { inputFormat = PNET }))
        "Use the pnet input format"

        , Option "" ["lola"]
        (NoArg (\opt -> Right opt { inputFormat = LOLA }))
        "Use the lola input format"

        , Option "" ["tpn"]
        (NoArg (\opt -> Right opt { inputFormat = TPN }))
        "Use the tpn input format"
104

105
106
107
108
        , Option "" ["spec"]
        (NoArg (\opt -> Right opt { inputFormat = MIST }))
        "Use the mist input format"

109
110
111
112
        , Option "s" ["structure"]
        (NoArg (\opt -> Right opt { optPrintStructure = True }))
        "Print structural information"

113
114
115
116
117
118
        , Option "" ["validate-identifiers"]
        (NoArg (\opt -> Right opt {
            optTransformations = ValidateIdentifiers : optTransformations opt
          }))
        "Make identifiers valid for lola"

119
        , Option "" ["termination-by-reachability"]
120
        (NoArg (\opt -> Right opt {
121
            optTransformations = TerminationByReachability : optTransformations opt
122
          }))
123
        "Prove termination by reducing it to reachability"
124

125
        , Option "" ["termination"]
126
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
127
                   optProperties = Termination : optProperties opt
128
               }))
129
        "Prove that the net is terminating"
130

Philipp Meyer's avatar
Philipp Meyer committed
131
132
133
134
135
136
        , Option "" ["proper-termination"]
        (NoArg (\opt -> Right opt {
                   optProperties = ProperTermination : optProperties opt
               }))
        "Prove termination in the final marking"

137
        , Option "" ["deadlock-free"]
138
        (NoArg (\opt -> Right opt {
139
                   optProperties = DeadlockFree : optProperties opt
140
               }))
141
        "Prove that the net is deadlock-free"
142

143
        , Option "" ["deadlock-free-unless-final"]
Philipp Meyer's avatar
Philipp Meyer committed
144
        (NoArg (\opt -> Right opt {
145
                   optProperties = DeadlockFreeUnlessFinal : optProperties opt
Philipp Meyer's avatar
Philipp Meyer committed
146
               }))
147
148
        ("Prove that the net is deadlock-free\n" ++
         "unless it is in the final marking")
Philipp Meyer's avatar
Philipp Meyer committed
149

150
151
152
153
154
155
        , Option "" ["final-state-unreachable"]
        (NoArg (\opt -> Right opt {
                   optProperties = FinalStateUnreachable : optProperties opt
               }))
        "Prove that the final state is unreachable"

156
157
        , Option "" ["safe"]
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
158
                   optProperties = Safe : optProperties opt
159
160
161
162
163
164
165
166
167
168
169
170
               }))
        "Prove that the net is safe, i.e. 1-bounded"

        , Option "" ["bounded"]
        (ReqArg (\arg opt -> case reads arg of
                    [(k, "")] -> Right opt {
                           optProperties = Bounded k : optProperties opt }
                    _ -> Left ("invalid argument for k-bounded option: " ++ arg)
                )
                "K")
        "Prove that the net is K-bounded"

171
172
173
174
175
176
        , Option "" ["free-choice"]
        (NoArg (\opt -> Right opt {
                   optProperties = StructFreeChoice : optProperties opt
               }))
        "Prove that the net is free-choice"

177
178
179
180
181
182
183
184
185
186
187
188
        , Option "" ["parallel"]
        (NoArg (\opt -> Right opt {
                   optProperties = StructParallel : optProperties opt
               }))
        "Prove that the net has non-trivial parallellism"

        , Option "" ["final-place"]
        (NoArg (\opt -> Right opt {
                   optProperties = StructFinalPlace : optProperties opt
               }))
        "Prove that there is only one needed final place"

189
190
191
192
193
194
        , Option "" ["communication-free"]
        (NoArg (\opt -> Right opt {
                   optProperties = StructCommunicationFree : optProperties opt
               }))
        "Prove that the net is communication-free"

195
196
197
198
        , Option "n" ["no-refinement"]
        (NoArg (\opt -> Right opt { optRefine = False }))
        "Don't use refinement"

199
200
201
202
        , Option "i" ["invariant"]
        (NoArg (\opt -> Right opt { optInvariant = True }))
        "Try to generate an invariant"

203
204
205
206
207
208
209
        , Option "o" ["output"]
        (ReqArg (\arg opt -> Right opt {
                        optOutput = Just arg
                })
                "FILE")
        "Write net and properties to FILE"

210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
        , Option "" ["out-lola"]
        (NoArg (\opt -> Right opt { outputFormat = OutLOLA }))
        "Use the lola output format"

        , Option "" ["out-sara"]
        (NoArg (\opt -> Right opt { outputFormat = OutSARA }))
        "Use the sara output format"

        , Option "" ["out-spec"]
        (NoArg (\opt -> Right opt { outputFormat = OutSPEC }))
        "Use the spec output format"

        , Option "" ["out-dot"]
        (NoArg (\opt -> Right opt { outputFormat = OutDOT }))
        "Use the dot output format"

226
227
228
229
230
231
        , Option "" ["no-given-properties"]
        (NoArg (\opt -> Right opt {
                   optUseProperties = False
               }))
        "Do not use the properties given in the input file"

232
        , Option "v" ["verbose"]
233
234
235
236
237
238
        (NoArg (\opt -> Right opt { optVerbosity = optVerbosity opt + 1 }))
        "Increase verbosity (may be specified more than once)"

        , Option "q" ["quiet"]
        (NoArg (\opt -> Right opt { optVerbosity = optVerbosity opt - 1 }))
        "Decrease verbosity (may be specified more than once)"
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256

        , Option "V" ["version"]
        (NoArg (\opt -> Right opt { optShowVersion = True }))
        "Show version"

        , Option "h" ["help"]
        (NoArg (\opt -> Right opt { optShowHelp = True }))
        "Show help"
        ]

parseArgs :: IO (Either String (Options, [String]))
parseArgs = do
        args <- getArgs
        case getOpt Permute options args of
            (actions, files, []) ->
                return $ (,files) <$> foldl (>>=) (return startOptions) actions
            (_, _, errs) -> return $ Left $ concat errs

257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
writeFiles :: Int -> String -> OutputFormat -> PetriNet -> [Property] -> IO ()
writeFiles verbosity basename format net props = do
        verbosePut verbosity 1 $ "Writing " ++ showNetName net ++ " to " ++
                                  basename ++ " in format " ++ show format
        case format of
            OutLOLA -> do
                L.writeFile basename $ LOLAPrinter.printNet net
                mapM_ (\(p,i) -> do
                        let file = basename ++ ".task" ++ show i
                        verbosePut verbosity 1 $ "Writing " ++ showPropertyName p
                                                 ++ " to " ++ file
                        L.writeFile file $ LOLAPrinter.printProperty p
                      ) (zip props [(1::Integer)..])
            OutSARA -> do
                L.writeFile basename $ LOLAPrinter.printNet net
                verbosePut verbosity 1 $ "Writing properties to " ++ basename ++
                                         ".sara"
                L.writeFile (basename ++ ".sara") $
                    SARAPrinter.printProperties basename net props
            OutSPEC ->
                mapM_ (\(p,i) -> do
                        let file = basename ++ ".target" ++ show i
                        verbosePut verbosity 1 $ "Writing " ++ showPropertyName p
                                                 ++ " to " ++ file
                        L.writeFile file $ SPECPrinter.printProperty p
                      ) (zip props [(1::Integer)..])
            OutDOT ->
                L.writeFile basename $ DOTPrinter.printNet net
285

286
287
288
289
290
291
292
293
294
295
296
297
298
structuralAnalysis :: PetriNet -> IO ()
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)
299
300
        putStrLn $ "Places             : " ++ show (length (places net))
        putStrLn $ "Transitions        : " ++ show (length (transitions net))
301
302
303
304
305
306
        putStrLn $ "Initial places     : " ++ show (length initP)
        putStrLn $ "Initial transitions: " ++ show (length initT)
        putStrLn $ "Isolated places    : " ++ show (length isolP)
        putStrLn $ "Final places       : " ++ show (length finalP)
        putStrLn $ "Final transitions  : " ++ show (length finalT)

307
checkFile :: Parser (PetriNet,[Property]) -> Int -> Bool -> Bool ->
308
            [ImplicitProperty] -> [NetTransformation] ->
309
310
            Bool -> Maybe String -> OutputFormat -> Bool -> String ->
            IO PropResult
311
checkFile parser verbosity refine invariant implicitProperties transformations
312
          useProperties output format printStruct file = do
313
        verbosePut verbosity 0 $ "Reading \"" ++ file ++ "\""
314
        (net,props) <- parseFile parser file
315
316
317
        let props' = if useProperties then props else []
        let props'' = props' ++ map (makeImplicitProperty net) implicitProperties
        let (net',props''') = foldl transformNet (net,props'') transformations
318
319
320
321
        verbosePut verbosity 1 $ "Analyzing " ++ showNetName net
        verbosePut verbosity 2 $
                "Places: " ++ show (length  $ places net') ++ "; " ++
                "Transitions: " ++ show (length $ transitions net')
322
        when printStruct $ structuralAnalysis net
323
        verbosePut verbosity 3 $ show net'
324
        case output of
325
326
            Just outputfile ->
                writeFiles verbosity outputfile format net' props'''
327
            Nothing -> return ()
Philipp Meyer's avatar
Philipp Meyer committed
328
        -- TODO: short-circuit?
329
        rs <- mapM (checkProperty verbosity net' refine invariant) props'''
330
        verbosePut verbosity 0 ""
331
        return $ resultsAnd rs
332

333
334
placeOp :: Op -> (Place, Integer) -> Formula Place
placeOp op (p,w) = LinearInequation (Var p) op (Const w)
335

336
337
transformNet :: (PetriNet, [Property]) -> NetTransformation ->
               (PetriNet, [Property])
338
transformNet (net, props) TerminationByReachability =
339
340
341
342
343
344
345
346
347
        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)] ++
348
                 linitials net ++ map (first primePlace) (linitials net)
349
350
            transformTransition t =
                let (preT, postT) = context net t
351
352
353
354
                    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
355
                in  if t `elem` ghostTransitions net then
356
                        [(t, (pre', post'))]
357
                    else
358
359
                        [(t, (pre', post')), (primeTransition t, (pre'', post''))]
            ts = (switch, ([(m1,1)], [(m2,1)])) :
360
361
                 concatMap transformTransition (transitions net)
            gs = ghostTransitions net
362
            prop = Property "termination by reachability" $ Safety $
363
364
365
                    foldl (:&:) (LinearInequation (Var sigma) Ge (Const 1))
                      (map (\p -> LinearInequation
                                (Var (primePlace p) :-: Var p) Ge (Const 0))
366
                        (places net))
367
            -- TODO: map existing liveness properties
368
        in  (makePetriNetWith (name net) ps ts is gs, prop : props)
369
transformNet (net, props) ValidateIdentifiers =
370
371
        (renamePetriNetPlacesAndTransitions validateId net,
         map (renameProperty validateId) props)
372

373
makeImplicitProperty :: PetriNet -> ImplicitProperty -> Property
374
makeImplicitProperty net Termination =
375
        Property "termination" $ Liveness $
376
            foldl (:&:) FTrue
377
                (map (\t -> LinearInequation (Var t) Eq (Const 0))
378
                    (ghostTransitions net))
379
makeImplicitProperty net ProperTermination =
Philipp Meyer's avatar
Philipp Meyer committed
380
        let (finals, nonfinals) = partition (null . lpost net) (places net)
381
        in  Property "proper termination" $ Safety
Philipp Meyer's avatar
Philipp Meyer committed
382
383
            (foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) finals) :&:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals))
384
makeImplicitProperty net DeadlockFree =
385
        Property "deadlock-free" $ Safety $
386
387
            foldl (:&:) FTrue
                (map (foldl (:|:) FFalse . map (placeOp Lt) . lpre net)
388
                     (filter (`notElem` ghostTransitions net) (transitions net)))
389
makeImplicitProperty net DeadlockFreeUnlessFinal =
390
        let (Property _ (Safety pf)) = makeImplicitProperty net DeadlockFree
391
            (finals, nonfinals) = partition (null . lpost net) (places net)
392
        in  Property "deadlock-free unless final" $ Safety $
Philipp Meyer's avatar
Philipp Meyer committed
393
394
            (foldl (:&:) FTrue  (map (\p -> placeOp Eq (p,0)) finals) :|:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals)) :&:
395
            pf
396
397
398
399
400
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)
401
makeImplicitProperty net (Bounded k) =
402
        Property (show k ++ "-bounded") $ Safety $
403
            foldl (:|:) FFalse
Philipp Meyer's avatar
Philipp Meyer committed
404
                (map (\p -> placeOp Ge (p,k+1))
405
406
                    (filter (`notElem` concatMap (post net) (ghostTransitions net))
                        (places net)))
407
408
makeImplicitProperty net Safe =
        let bounded = makeImplicitProperty net (Bounded 1)
409
410
411
        in  Property "safe" $ pcont bounded
makeImplicitProperty _ StructFreeChoice =
        Property "free choice" $ Structural FreeChoice
412
413
414
415
makeImplicitProperty _ StructParallel =
        Property "parallel" $ Structural Parallel
makeImplicitProperty _ StructFinalPlace =
        Property "final place" $ Structural FinalPlace
416
417
makeImplicitProperty _ StructCommunicationFree =
        Property "communication free" $ Structural CommunicationFree
418

419
420
checkProperty :: Int -> PetriNet -> Bool -> Bool -> Property -> IO PropResult
checkProperty verbosity net refine invariant p = do
421
        verbosePut verbosity 1 $ "\nChecking " ++ showPropertyName p
422
        verbosePut verbosity 3 $ show p
423
        r <- case pcont p of
424
            (Safety pf) -> checkSafetyProperty verbosity net refine invariant pf
425
            (Liveness pf) -> checkLivenessProperty verbosity net refine invariant pf
Philipp Meyer's avatar
Philipp Meyer committed
426
            (Structural ps) -> checkStructuralProperty verbosity net ps
427
428
429
430
431
        verbosePut verbosity 0 $ showPropertyName p ++ " " ++
            case r of
                Satisfied -> "is satisfied."
                Unsatisfied -> "is not satisfied."
                Unknown-> "may not be satisfied."
432
433
        return r

434
checkSafetyProperty :: Int -> PetriNet -> Bool -> Bool ->
435
        Formula Place -> IO PropResult
436
437
checkSafetyProperty verbosity net refine invariant f = do
        r <- checkSafetyProperty' verbosity net refine f []
438
        case r of
439
440
441
442
443
444
445
446
447
448
449
            (Nothing, traps) ->
                if invariant then do
                    r' <- checkSat verbosity $ checkSafetyInvariantSat net f traps
                    case r' of
                        Nothing -> do
                            verbosePut verbosity 0 "No invariant found"
                            return Unknown
                        Just inv -> do
                            verbosePut verbosity 0 "Invariant found"
                            mapM_ print inv
                            return Satisfied
450
451
452
453
454
455
456
457
                else
                    return Satisfied
            (Just _, _) ->
                return Unknown

checkSafetyProperty' :: Int -> PetriNet -> Bool ->
        Formula Place -> [Trap] -> IO (Maybe Marking, [Trap])
checkSafetyProperty' verbosity net refine f traps = do
Philipp Meyer's avatar
Philipp Meyer committed
458
        r <- checkSat verbosity $ checkStateEquationSat net f traps
459
        case r of
460
461
462
            Nothing -> return (Nothing, traps)
            Just m ->
                if refine then
Philipp Meyer's avatar
Philipp Meyer committed
463
                    refineSafetyProperty verbosity net f traps m
464
                else
465
                    return (Just m, traps)
Philipp Meyer's avatar
Philipp Meyer committed
466

467
468
469
470
471
refineSafetyProperty :: Int -> PetriNet ->
        Formula Place -> [Trap] -> Marking -> IO (Maybe Marking, [Trap])
refineSafetyProperty verbosity net f traps m = do
        r <- checkSat verbosity $ checkTrapSat net m
        case r of
Philipp Meyer's avatar
Philipp Meyer committed
472
473
474
            Nothing ->
                return (Just m, traps)
            Just trap ->
475
                checkSafetyProperty' verbosity net True f (trap:traps)
476

477
checkLivenessProperty :: Int -> PetriNet -> Bool -> Bool ->
478
        Formula Transition -> IO PropResult
479
checkLivenessProperty verbosity net refine invariant f = do
480
481
        r <- checkLivenessProperty' verbosity net refine f []
        case r of
482
483
484
485
486
487
488
489
490
491
492
            (Nothing, cuts) ->
                if invariant then do
                    r' <- checkSat verbosity $ checkLivenessInvariantSat net f cuts
                    case r' of
                        Nothing -> do
                            verbosePut verbosity 0 "No invariant found"
                            return Unknown
                        Just inv -> do
                            verbosePut verbosity 0 "Invariant found"
                            mapM_ print inv
                            return Satisfied
493
494
495
496
                else
                    return Satisfied
            (Just _, _) ->
                return Unknown
497

498
499
500
checkLivenessProperty' :: Int -> PetriNet -> Bool ->
        Formula Transition -> [Cut] -> IO (Maybe FiringVector, [Cut])
checkLivenessProperty' verbosity net refine f cuts = do
501
        r <- checkSat verbosity $ checkTransitionInvariantSat net f cuts
Philipp Meyer's avatar
Philipp Meyer committed
502
        case r of
503
            Nothing -> return (Nothing, cuts)
Philipp Meyer's avatar
Philipp Meyer committed
504
            Just x ->
505
                if refine then do
506
                    rt <- findLivenessRefinement verbosity net x
507
                    case rt of
Philipp Meyer's avatar
Philipp Meyer committed
508
                        Nothing ->
509
                            return (Just x, cuts)
Philipp Meyer's avatar
Philipp Meyer committed
510
                        Just cut ->
511
512
                            checkLivenessProperty' verbosity net refine f
                                                   (cut:cuts)
513
                else
514
                    return (Just x, cuts)
515

516
517
518
findLivenessRefinement :: Int -> PetriNet -> FiringVector ->
        IO (Maybe Cut)
findLivenessRefinement verbosity net x = do
519
520
521
        r1 <- findLivenessRefinementByEmptyTraps verbosity net
                                              (initialMarking net) x []
        --r1 <- findLivenessRefinementBySComponent verbosity net x
522
523
524
525
526
        case r1 of
            Nothing -> findLivenessRefinementByEmptyTraps verbosity net
                                              (initialMarking net) x []
            Just _ -> return r1

527
528
529
530
531
532
findLivenessRefinementBySComponent :: Int -> PetriNet -> FiringVector ->
        IO (Maybe Cut)
findLivenessRefinementBySComponent verbosity net x =
        checkSat verbosity $ checkSComponentSat net x

findLivenessRefinementByEmptyTraps :: Int -> PetriNet -> Marking -> FiringVector ->
533
        [Trap] -> IO (Maybe Cut)
534
findLivenessRefinementByEmptyTraps verbosity net m x traps = do
535
536
537
538
539
        r <- checkSat verbosity $ checkSubnetEmptyTrapSat net m x
        case r of
            Nothing -> do
                rm <- refineSafetyProperty verbosity net FTrue traps m
                case rm of
540
541
542
                    (Nothing, _) -> do
                        cut <- generateLivenessRefinement verbosity net x traps
                        return $ Just cut
543
544
545
                    (Just _, _) ->
                        return Nothing
            Just trap -> do
546
547
                let traps' = trap:traps
                rm <- checkSafetyProperty' verbosity net False FTrue traps'
548
                case rm of
549
                    (Nothing, _) -> do
550
                        cut <- generateLivenessRefinement verbosity net x traps'
551
                        return $ Just cut
552
                    (Just m', _) ->
553
                        findLivenessRefinementByEmptyTraps verbosity net m' x traps'
554

555
556
generateLivenessRefinement :: Int -> PetriNet -> FiringVector -> [Trap] -> IO Cut
generateLivenessRefinement verbosity net x traps = do
557
        let cut = constructCut net x traps
558
559
        verbosePut verbosity 3 $ "- cut: " ++ show cut
        return cut
560

561
checkStructuralProperty :: Int -> PetriNet -> Structure -> IO PropResult
562
checkStructuralProperty _ net struct =
563
564
565
566
        if checkStructure net struct then
            return Satisfied
        else
            return Unsatisfied
567

568
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
569
main = do
570
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
571
572
573
574
575
576
577
578
        args <- parseArgs
        case args of
            Left err -> exitErrorWith err
            Right (opts, files) -> do
                when (optShowVersion opts) (exitSuccessWith "Version 0.01")
                when (optShowHelp opts) (exitSuccessWith
                     (usageInfo "SLAPnet" options))
                when (null files) (exitErrorWith "No input file given")
579
580
                let verbosity = optVerbosity opts
                    refinement = optRefine opts
581
                    invariant = optInvariant opts
582
583
                let parser = case inputFormat opts of
                                 PNET -> PNET.parseContent
Philipp Meyer's avatar
Philipp Meyer committed
584
                                 LOLA -> LOLA.parseContent
585
                                 TPN -> TPN.parseContent
586
                                 MIST -> MIST.parseContent
587
588
                let properties = reverse $ optProperties opts
                let transformations = reverse $ optTransformations opts
589
590
591
592
                rs <- mapM (checkFile parser verbosity refinement invariant
                     properties transformations (optUseProperties opts)
                     (optOutput opts) (outputFormat opts) (optPrintStructure opts))
                     files
Philipp Meyer's avatar
Philipp Meyer committed
593
                -- TODO: short-circuit with Control.Monad.Loops?
594
595
596
597
598
599
600
                case resultsAnd rs of
                    Satisfied ->
                        exitSuccessWith "All properties satisfied."
                    Unsatisfied ->
                        exitFailureWith "Some properties are not satisfied"
                    Unknown ->
                        exitFailureWith "Some properties may not be satisfied."
601

Philipp Meyer's avatar
Philipp Meyer committed
602
-- TODO: Always exit with exit code 0 unless an error occured
603
604
605
606
607
608
609
610
exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
        exitSuccess

exitFailureWith :: String -> IO ()
exitFailureWith msg = do
        putStrLn msg
611
        exitWith $ ExitFailure 2
Philipp Meyer's avatar
Philipp Meyer committed
612

613
614
615
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
616
        exitWith $ ExitFailure 3