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
31
32
33
--import Solver.TrapConstraints
--import Solver.TransitionInvariant
--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
450
        r <- checkSat2 verbosity $ checkStateEquationSat net f traps
451
        case r of
452
453
454
            Nothing -> return (Nothing, traps)
            Just m ->
                if refine then
455
456
                    return (Just m, traps)
                    --refineSafetyProperty verbosity net f traps m
457
                else
458
                    return (Just m, traps)
459
{-
460
461
462
463
464
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
465
466
467
            Nothing ->
                return (Just m, traps)
            Just trap ->
468
                checkSafetyProperty' verbosity net True f (trap:traps)
469

470
checkLivenessProperty :: Int -> PetriNet -> Bool -> Bool ->
471
        Formula Transition -> IO PropResult
472
checkLivenessProperty verbosity net refine invariant f = do
473
474
475
476
477
478
479
480
481
482
        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
483
-}
484
{-
485
generateLivenessInvariant :: Int -> PetriNet ->
486
        Formula -> [SCompCut] -> IO PropResult
487
488
generateLivenessInvariant verbosity net f comps = do
        verbosePut verbosity 1 "Generating invariant"
489
490
491
492
493
494
495
496
        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
497
-}
498
{-
499
500
501
checkLivenessProperty' :: Int -> PetriNet -> Bool ->
        Formula Transition -> [Cut] -> IO (Maybe FiringVector, [Cut])
checkLivenessProperty' verbosity net refine f cuts = do
502
        r <- checkSat verbosity $ checkTransitionInvariantSat net f cuts
Philipp Meyer's avatar
Philipp Meyer committed
503
        case r of
504
            Nothing -> return (Nothing, cuts)
Philipp Meyer's avatar
Philipp Meyer committed
505
            Just x ->
506
                if refine then do
507
                    rt <- findLivenessRefinement verbosity net x
508
                    case rt of
Philipp Meyer's avatar
Philipp Meyer committed
509
                        Nothing ->
510
                            return (Just x, cuts)
Philipp Meyer's avatar
Philipp Meyer committed
511
                        Just cut ->
512
513
                            checkLivenessProperty' verbosity net refine f
                                                   (cut:cuts)
514
                else
515
516
                    return (Just x, cuts)

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

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

findLivenessRefinementByEmptyTraps :: Int -> PetriNet -> Marking -> FiringVector ->
532
        [Trap] -> IO (Maybe Cut)
533
findLivenessRefinementByEmptyTraps verbosity net m x traps = do
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
        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', _) ->
551
                        findLivenessRefinementByEmptyTraps verbosity net m' x (trap:traps)
552
553
554
555
556

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))
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