Main.hs 25.3 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
30
import Solver.StateEquation
import Solver.TrapConstraints
31
import Solver.TransitionInvariant
32
import Solver.LivenessInvariant
33
import Solver.SComponent
34
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
placeOp :: Op -> (String, Integer) -> Formula
335
placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w)
336

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

374
makeImplicitProperty :: PetriNet -> ImplicitProperty -> Property
375
makeImplicitProperty net Termination =
376
        Property "termination" $ Liveness $
377
378
379
            foldl (:&:) FTrue
                (map (\t -> Atom (LinIneq (Var t) Eq (Const 0)))
                    (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
426
            (Safety pf) -> checkSafetyProperty verbosity net refine invariant pf
            (Liveness pf) -> checkLivenessProperty verbosity net refine invariant pf
427
428
429
430
431
432
            (Structural ps) -> checkStructuralProperty verbosity net ps
        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 -> IO PropResult
437
checkSafetyProperty verbosity net refine invariant f =
438
439
440
441
442
443
444
445
446
        -- TODO: add flag for this kind of structural check
        if checkCommunicationFree net then do
            verbosePut verbosity 1 "Net found to be communication-free"
            checkSafetyPropertyByCommFree verbosity net f
        else do
            r <- checkSafetyPropertyBySafetyRef verbosity net refine f []
            if r == Satisfied && invariant then
                -- TODO: add invariant generation
                error "Invariant generation for safety properties not yet supported"
447
            else
448
                return r
449
450
451
452
453
454
455
456
457
458
459
460

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

checkSafetyPropertyBySafetyRef :: Int -> PetriNet -> Bool ->
461
        Formula -> [[String]] -> IO PropResult
462
checkSafetyPropertyBySafetyRef verbosity net refine f traps = do
463
464
        r <- checkSat $ checkStateEquationSat net f traps
        case r of
465
            Nothing -> return Satisfied
466
467
            Just a -> do
                let assigned = markedPlacesFromAssignment net a
468
469
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Places marked: " ++ show assigned
470
                verbosePut verbosity 3 $ "Assignment: " ++ show a
471
472
473
474
                if refine then do
                    rt <- checkSat $ checkTrapSat net assigned
                    case rt of
                        Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
475
                            verbosePut verbosity 1 "No trap found."
476
                            return Unknown
477
478
                        Just at -> do
                            let trap = trapFromAssignment at
479
480
481
                            verbosePut verbosity 1 "Trap found"
                            verbosePut verbosity 2 $ "Places in trap: " ++
                                                      show trap
482
483
                            verbosePut verbosity 3 $ "Trap assignment: " ++
                                                      show at
484
485
                            checkSafetyPropertyBySafetyRef verbosity net
                                                refine f (trap:traps)
486
                else
487
                    return Unknown
488

489
490
491
492
checkLivenessProperty :: Int -> PetriNet -> Bool -> Bool ->
        Formula -> IO PropResult
checkLivenessProperty verbosity net refine invariant f = do
        (r, comps) <- checkLivenessPropertyByRef verbosity net refine f []
493
        if r == Satisfied && invariant then
494
495
496
497
498
            generateLivenessInvariant verbosity net f comps
        else
            return r

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

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

checkStructuralProperty :: Int -> PetriNet -> Structure -> IO PropResult
540
checkStructuralProperty _ net struct =
541
542
543
544
        if checkStructure net struct then
            return Satisfied
        else
            return Unsatisfied
545

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

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

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

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