Main.hs 24.5 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
33
34
35
--import Solver.TransitionInvariant
--import Solver.LivenessInvariant
--import Solver.SComponent
--import Solver.CommFreeReachability
36

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

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

46
47
data NetTransformation = TerminationByReachability
                       | ValidateIdentifiers
48

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        , 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

255
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
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
283

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

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

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

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

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

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

432
checkSafetyProperty :: Int -> PetriNet -> Bool -> Bool ->
433
        Formula Place -> IO PropResult
434
checkSafetyProperty verbosity net refine invariant f =
435
        -- TODO: add flag for this kind of structural check
436
437
438
439
440
        --if checkCommunicationFree net then do
        --    verbosePut verbosity 1 "Net found to be communication-free"
        --    checkSafetyPropertyByCommFree verbosity net f
        --else
        do
441
442
443
444
            r <- checkSafetyPropertyBySafetyRef verbosity net refine f []
            if r == Satisfied && invariant then
                -- TODO: add invariant generation
                error "Invariant generation for safety properties not yet supported"
445
            else
446
                return r
447
{-
448
449
450
451
452
453
454
455
456
checkSafetyPropertyByCommFree :: Int -> PetriNet -> Formula -> IO PropResult
checkSafetyPropertyByCommFree verbosity net f = do
        r <- checkSat $ checkCommFreeReachabilitySat net f
        case r of
            Nothing -> return Satisfied
            Just a -> do
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 3 $ "Assignment: " ++ show a
                return Unsatisfied
457
-}
458
checkSafetyPropertyBySafetyRef :: Int -> PetriNet -> Bool ->
459
        Formula Place -> [Trap] -> IO PropResult
460
checkSafetyPropertyBySafetyRef verbosity net refine f traps = do
Philipp Meyer's avatar
Philipp Meyer committed
461
        r <- checkSat verbosity $ checkStateEquationSat net f traps
462
        case r of
463
            Nothing -> return Satisfied
Philipp Meyer's avatar
Philipp Meyer committed
464
            Just marking -> do
465
                if refine then do
Philipp Meyer's avatar
Philipp Meyer committed
466
                    rt <- checkSat verbosity $ checkTrapSat net marking
467
468
                    case rt of
                        Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
469
                            verbosePut verbosity 1 "No trap found."
470
                            return Unknown
471
                        Just trap -> do
Philipp Meyer's avatar
Philipp Meyer committed
472
473
                            checkSafetyPropertyBySafetyRef verbosity net
                                                refine f (trap:traps)
474
                else
475
                    return Unknown
476
{-
477
478
479
480
checkLivenessProperty :: Int -> PetriNet -> Bool -> Bool ->
        Formula -> IO PropResult
checkLivenessProperty verbosity net refine invariant f = do
        (r, comps) <- checkLivenessPropertyByRef verbosity net refine f []
481
        if r == Satisfied && invariant then
482
483
484
485
486
            generateLivenessInvariant verbosity net f comps
        else
            return r

generateLivenessInvariant :: Int -> PetriNet ->
487
        Formula -> [SCompCut] -> IO PropResult
488
489
generateLivenessInvariant verbosity net f comps = do
        verbosePut verbosity 1 "Generating invariant"
490
491
492
493
494
495
496
497
        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
498
499
500
501
502

checkLivenessPropertyByRef :: Int -> PetriNet -> Bool ->
        Formula -> [SCompCut] -> IO (PropResult, [SCompCut])
checkLivenessPropertyByRef verbosity net refine f comps = do
        r <- checkSat $ checkTransitionInvariantSat net f comps
Philipp Meyer's avatar
Philipp Meyer committed
503
        case r of
504
            Nothing -> return (Satisfied, comps)
505
506
            Just ax -> do
                let fired = firedTransitionsFromAssignment ax
507
508
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Transitions fired: " ++ show fired
509
                verbosePut verbosity 3 $ "Assignment: " ++ show ax
510
511
512
513
                if refine then do
                    rt <- checkSat $ checkSComponentSat net fired ax
                    case rt of
                        Nothing -> do
514
                            verbosePut verbosity 1 "No S-component found"
515
                            return (Unknown, comps)
516
                        Just as -> do
517
                            let sCompsCut = getSComponentCompsCut net ax as
518
                            verbosePut verbosity 1 "S-component found"
519
                            verbosePut verbosity 2 $ "Comps/Cut: " ++ show sCompsCut
520
521
                            verbosePut verbosity 3 $ "S-Component assignment: " ++
                                                      show as
522
523
                            checkLivenessPropertyByRef verbosity net refine f
                                                  (sCompsCut:comps)
524
                else
525
                    return (Unknown, comps)
526
-}
527
checkStructuralProperty :: Int -> PetriNet -> Structure -> IO PropResult
528
checkStructuralProperty _ net struct =
529
530
531
532
        if checkStructure net struct then
            return Satisfied
        else
            return Unsatisfied
533

534
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
535
main = do
536
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
537
538
539
540
541
542
543
544
        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")
545
546
                let verbosity = optVerbosity opts
                    refinement = optRefine opts
547
                    invariant = optInvariant opts
548
549
                let parser = case inputFormat opts of
                                 PNET -> PNET.parseContent
Philipp Meyer's avatar
Philipp Meyer committed
550
                                 LOLA -> LOLA.parseContent
551
                                 TPN -> TPN.parseContent
552
                                 MIST -> MIST.parseContent
553
554
                let properties = reverse $ optProperties opts
                let transformations = reverse $ optTransformations opts
555
556
557
558
                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
559
                -- TODO: short-circuit with Control.Monad.Loops?
560
561
562
563
564
565
566
                case resultsAnd rs of
                    Satisfied ->
                        exitSuccessWith "All properties satisfied."
                    Unsatisfied ->
                        exitFailureWith "Some properties are not satisfied"
                    Unknown ->
                        exitFailureWith "Some properties may not be satisfied."
567

Philipp Meyer's avatar
Philipp Meyer committed
568
-- TODO: Always exit with exit code 0 unless an error occured
569
570
571
572
573
574
575
576
exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
        exitSuccess

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

579
580
581
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
582
        exitWith $ ExitFailure 3