Main.hs 25.4 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
Philipp Meyer's avatar
Philipp Meyer committed
368
        in  (makePetriNetWithTrans (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
            (Nothing, traps) ->
                if invariant then do
                    r' <- checkSat verbosity $ checkSafetyInvariantSat net f traps
Philipp Meyer's avatar
Philipp Meyer committed
442
                    printInvariant verbosity r'
443
444
445
446
447
                else
                    return Satisfied
            (Just _, _) ->
                return Unknown

Philipp Meyer's avatar
Philipp Meyer committed
448
449
450
451
452
453
454
455
456
457
458
printInvariant :: (Show a) => Int -> Maybe [a] -> IO PropResult
printInvariant verbosity invResult =
        case invResult of
            Nothing -> do
                verbosePut verbosity 0 "No invariant found"
                return Unknown
            Just inv -> do
                verbosePut verbosity 0 "Invariant found"
                mapM_ print inv
                return Satisfied

459
460
461
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
462
        r <- checkSat verbosity $ checkStateEquationSat net f traps
463
        case r of
464
465
466
            Nothing -> return (Nothing, traps)
            Just m ->
                if refine then
Philipp Meyer's avatar
Philipp Meyer committed
467
                    refineSafetyProperty verbosity net f traps m
468
                else
469
                    return (Just m, traps)
Philipp Meyer's avatar
Philipp Meyer committed
470

471
472
473
474
475
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
476
477
478
            Nothing ->
                return (Just m, traps)
            Just trap ->
479
                checkSafetyProperty' verbosity net True f (trap:traps)
480

481
checkLivenessProperty :: Int -> PetriNet -> Bool -> Bool ->
482
        Formula Transition -> IO PropResult
483
checkLivenessProperty verbosity net refine invariant f = do
484
485
        r <- checkLivenessProperty' verbosity net refine f []
        case r of
486
487
488
            (Nothing, cuts) ->
                if invariant then do
                    r' <- checkSat verbosity $ checkLivenessInvariantSat net f cuts
Philipp Meyer's avatar
Philipp Meyer committed
489
                    printInvariant verbosity r'
490
491
492
493
                else
                    return Satisfied
            (Just _, _) ->
                return Unknown
494

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

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

524
525
526
527
528
529
findLivenessRefinementBySComponent :: Int -> PetriNet -> FiringVector ->
        IO (Maybe Cut)
findLivenessRefinementBySComponent verbosity net x =
        checkSat verbosity $ checkSComponentSat net x

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

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

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

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

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

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

610
611
612
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
613
        exitWith $ ExitFailure 3