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

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

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

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

45
46
data NetTransformation = TerminationByReachability
                       | ValidateIdentifiers
47

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

229
        , Option "v" ["verbose"]
230
231
232
233
234
235
        (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)"
236
237
238
239
240
241
242
243
244
245

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

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

246
247
248
249
verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
        when (verbosity >= level) (putStrLn str)

250
251
252
253
254
255
256
257
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

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
285
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
286

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

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

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

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

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

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

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

generateLivenessInvariant :: Int -> PetriNet ->
497
        Formula -> [SCompCut] -> IO PropResult
498
499
generateLivenessInvariant verbosity net f comps = do
        verbosePut verbosity 1 "Generating invariant"
500
501
502
503
504
505
506
507
        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
508
509
510
511
512

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
513
        case r of
514
            Nothing -> return (Satisfied, comps)
515
516
            Just ax -> do
                let fired = firedTransitionsFromAssignment ax
517
518
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Transitions fired: " ++ show fired
519
                verbosePut verbosity 3 $ "Assignment: " ++ show ax
520
521
522
523
                if refine then do
                    rt <- checkSat $ checkSComponentSat net fired ax
                    case rt of
                        Nothing -> do
524
                            verbosePut verbosity 1 "No S-component found"
525
                            return (Unknown, comps)
526
                        Just as -> do
527
                            let sCompsCut = getSComponentCompsCut net ax as
528
                            verbosePut verbosity 1 "S-component found"
529
                            verbosePut verbosity 2 $ "Comps/Cut: " ++ show sCompsCut
530
531
                            verbosePut verbosity 3 $ "S-Component assignment: " ++
                                                      show as
532
533
                            checkLivenessPropertyByRef verbosity net refine f
                                                  (sCompsCut:comps)
534
                else
535
                    return (Unknown, comps)
536
-}
537
checkStructuralProperty :: Int -> PetriNet -> Structure -> IO PropResult
538
checkStructuralProperty _ net struct =
539
540
541
542
        if checkStructure net struct then
            return Satisfied
        else
            return Unsatisfied
543

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

Philipp Meyer's avatar
Philipp Meyer committed
578
-- TODO: Always exit with exit code 0 unless an error occured
579
580
581
582
583
584
585
586
exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
        exitSuccess

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

589
590
591
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
592
        exitWith $ ExitFailure 3