Main.hs 25.1 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.SComponent
36
--import Solver.CommFreeReachability
37

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

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

47
48
data NetTransformation = TerminationByReachability
                       | ValidateIdentifiers
49

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

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

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

options :: [ OptDescr (Options -> Either String Options) ]
options =
92
93
94
95
96
97
98
99
100
101
102
        [ 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"
103

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

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

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

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

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

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

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

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

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

155
156
        , Option "" ["safe"]
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
157
                   optProperties = Safe : optProperties opt
158
159
160
161
162
163
164
165
166
167
168
169
               }))
        "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"

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

176
177
178
179
180
181
182
183
184
185
186
187
        , 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"

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

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

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

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

209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
        , 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"

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

231
        , Option "v" ["verbose"]
232
233
234
235
236
237
        (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)"
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255

        , 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

256
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
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
284

285
286
287
288
289
290
291
292
293
294
295
296
297
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)
298
299
        putStrLn $ "Places             : " ++ show (length (places net))
        putStrLn $ "Transitions        : " ++ show (length (transitions net))
300
301
302
303
304
305
        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)

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

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

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

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

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

433
checkSafetyProperty :: Int -> PetriNet -> Bool -> Bool ->
434
        Formula Place -> IO PropResult
435
436
checkSafetyProperty verbosity net refine invariant f = do
        r <- checkSafetyProperty' verbosity net refine f []
437
        case r of
438
439
440
441
442
443
444
445
446
447
448
449
            (Nothing, _) ->
                if invariant then
                    -- TODO: add invariant generation
                    error "Invariant generation for safety properties not yet supported"
                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
450
        r <- checkSat verbosity $ checkStateEquationSat net f traps
451
        case r of
452
453
454
455
            Nothing -> return (Nothing, traps)
            Just m ->
                if refine then
                    refineSafetyProperty verbosity net f traps m
456
                else
457
458
459
460
461
462
463
                    return (Just m, traps)

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
464
465
466
            Nothing ->
                return (Just m, traps)
            Just trap ->
467
                checkSafetyProperty' verbosity net True f (trap:traps)
468

469
checkLivenessProperty :: Int -> PetriNet -> Bool -> Bool ->
470
        Formula Transition -> IO PropResult
471
checkLivenessProperty verbosity net refine invariant f = do
472
473
474
475
476
477
478
479
480
481
        r <- checkLivenessProperty' verbosity net refine f []
        case r of
            (Nothing, _) ->
                if invariant then
                    -- TODO: add invariant generation
                    error "Invariant generation for liveness properties not yet supported"
                else
                    return Satisfied
            (Just _, _) ->
                return Unknown
482
{-
483
generateLivenessInvariant :: Int -> PetriNet ->
484
        Formula -> [SCompCut] -> IO PropResult
485
486
generateLivenessInvariant verbosity net f comps = do
        verbosePut verbosity 1 "Generating invariant"
487
488
489
490
491
492
493
494
        let cuts = generateCuts f comps
        r <- checkSat $ checkLivenessInvariantSat net cuts
        case r of
            Nothing -> return Unsatisfied
            Just as -> do
                let inv = getLivenessInvariant net cuts as
                mapM_ print inv
                return Satisfied
495
-}
496
497
498
checkLivenessProperty' :: Int -> PetriNet -> Bool ->
        Formula Transition -> [Cut] -> IO (Maybe FiringVector, [Cut])
checkLivenessProperty' verbosity net refine f cuts = do
499
        r <- checkSat verbosity $ checkTransitionInvariantSat net f cuts
Philipp Meyer's avatar
Philipp Meyer committed
500
        case r of
501
            Nothing -> return (Nothing, cuts)
Philipp Meyer's avatar
Philipp Meyer committed
502
            Just x ->
503
                if refine then do
504
505
506
                    rt <- findLivenessRefinementBySComponent verbosity net x
                    --rt <- findLivenessRefinementByEmptyTraps verbosity net
                    --                            (initialMarking 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
515
                    return (Just x, cuts)

516
517
518
519
520
521
findLivenessRefinementBySComponent :: Int -> PetriNet -> FiringVector ->
        IO (Maybe Cut)
findLivenessRefinementBySComponent verbosity net x =
        checkSat verbosity $ checkSComponentSat net x

findLivenessRefinementByEmptyTraps :: Int -> PetriNet -> Marking -> FiringVector ->
522
        [Trap] -> IO (Maybe Cut)
523
findLivenessRefinementByEmptyTraps verbosity net m x traps = do
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
        r <- checkSat verbosity $ checkSubnetEmptyTrapSat net m x
        case r of
            Nothing -> do
                rm <- refineSafetyProperty verbosity net FTrue traps m
                case rm of
                    (Nothing, _) ->
                        return $ Just $ generateLivenessRefinement
                                            net x traps
                    (Just _, _) ->
                        return Nothing
            Just trap -> do
                rm <- checkSafetyProperty' verbosity net False FTrue (trap:traps)
                case rm of
                    (Nothing, _) ->
                        return $ Just $ generateLivenessRefinement
                                            net x (trap:traps)
                    (Just m', _) ->
541
                        findLivenessRefinementByEmptyTraps verbosity net m' x (trap:traps)
542
543
544
545
546

generateLivenessRefinement :: PetriNet -> FiringVector -> [Trap] -> Cut
generateLivenessRefinement net x traps =
        (map (filter (\t -> value x t > 0) . mpre net) traps,
         nubOrd (concatMap (filter (\t -> value x t == 0) . mpost net) traps))
547

548
checkStructuralProperty :: Int -> PetriNet -> Structure -> IO PropResult
549
checkStructuralProperty _ net struct =
550
551
552
553
        if checkStructure net struct then
            return Satisfied
        else
            return Unsatisfied
554

555
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
556
main = do
557
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
558
559
560
561
562
563
564
565
        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")
566
567
                let verbosity = optVerbosity opts
                    refinement = optRefine opts
568
                    invariant = optInvariant opts
569
570
                let parser = case inputFormat opts of
                                 PNET -> PNET.parseContent
Philipp Meyer's avatar
Philipp Meyer committed
571
                                 LOLA -> LOLA.parseContent
572
                                 TPN -> TPN.parseContent
573
                                 MIST -> MIST.parseContent
574
575
                let properties = reverse $ optProperties opts
                let transformations = reverse $ optTransformations opts
576
577
578
579
                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
580
                -- TODO: short-circuit with Control.Monad.Loops?
581
582
583
584
585
586
587
                case resultsAnd rs of
                    Satisfied ->
                        exitSuccessWith "All properties satisfied."
                    Unsatisfied ->
                        exitFailureWith "Some properties are not satisfied"
                    Unknown ->
                        exitFailureWith "Some properties may not be satisfied."
588

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

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

600
601
602
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
603
        exitWith $ ExitFailure 3