Main.hs 21 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
32
import Solver.TransitionInvariant
import Solver.SComponent
33

34
data InputFormat = PNET | LOLA | TPN | MIST deriving (Show,Read)
35

36
37
data NetTransformation = TerminationByReachability
                       | ValidateIdentifiers
38

39
data ImplicitProperty = Termination
40
                      | DeadlockFree | DeadlockFreeUnlessFinal
Philipp Meyer's avatar
Philipp Meyer committed
41
                      | ProperTermination
42
                      | Safe | Bounded Integer
43
                      | StructFreeChoice
44
45
                      | StructParallel
                      | StructFinalPlace
46
                      | StructCommunicationFree
47
48
                      deriving (Show,Read)

49
data Options = Options { inputFormat :: InputFormat
50
                       , optVerbosity :: Int
51
52
                       , optShowHelp :: Bool
                       , optShowVersion :: Bool
53
                       , optProperties :: [ImplicitProperty]
54
                       , optTransformations :: [NetTransformation]
55
                       , optRefine :: Bool
56
                       , optOutput :: Maybe String
57
                       , optUseProperties :: Bool
58
                       , optPrintStructure :: Bool
59
60
61
62
                       }

startOptions :: Options
startOptions = Options { inputFormat = PNET
63
                       , optVerbosity = 1
64
65
                       , optShowHelp = False
                       , optShowVersion = False
66
                       , optProperties = []
67
                       , optTransformations = []
68
                       , optRefine = True
69
                       , optOutput = Nothing
70
                       , optUseProperties = True
71
                       , optPrintStructure = False
72
73
74
75
                       }

options :: [ OptDescr (Options -> Either String Options) ]
options =
76
77
78
79
80
81
82
83
84
85
86
        [ 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"
87

88
89
90
91
        , Option "" ["spec"]
        (NoArg (\opt -> Right opt { inputFormat = MIST }))
        "Use the mist input format"

92
93
94
95
        , Option "s" ["structure"]
        (NoArg (\opt -> Right opt { optPrintStructure = True }))
        "Print structural information"

96
97
98
99
100
101
        , Option "" ["validate-identifiers"]
        (NoArg (\opt -> Right opt {
            optTransformations = ValidateIdentifiers : optTransformations opt
          }))
        "Make identifiers valid for lola"

102
        , Option "" ["termination-by-reachability"]
103
        (NoArg (\opt -> Right opt {
104
            optTransformations = TerminationByReachability : optTransformations opt
105
          }))
106
        "Prove termination by reducing it to reachability"
107

108
        , Option "" ["terminating"]
109
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
110
                   optProperties = Termination : optProperties opt
111
               }))
112
        "Prove that the net is terminating"
113

Philipp Meyer's avatar
Philipp Meyer committed
114
115
116
117
118
119
        , Option "" ["proper-termination"]
        (NoArg (\opt -> Right opt {
                   optProperties = ProperTermination : optProperties opt
               }))
        "Prove termination in the final marking"

120
        , Option "" ["deadlock-free"]
121
        (NoArg (\opt -> Right opt {
122
                   optProperties = DeadlockFree : optProperties opt
123
               }))
124
        "Prove that the net is deadlock-free"
125

126
        , Option "" ["deadlock-free-unless-final"]
Philipp Meyer's avatar
Philipp Meyer committed
127
        (NoArg (\opt -> Right opt {
128
                   optProperties = DeadlockFreeUnlessFinal : optProperties opt
Philipp Meyer's avatar
Philipp Meyer committed
129
               }))
130
131
        ("Prove that the net is deadlock-free\n" ++
         "unless it is in the final marking")
Philipp Meyer's avatar
Philipp Meyer committed
132

133
134
        , Option "" ["safe"]
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
135
                   optProperties = Safe : optProperties opt
136
137
138
139
140
141
142
143
144
145
146
147
               }))
        "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"

148
149
150
151
152
153
        , Option "" ["free-choice"]
        (NoArg (\opt -> Right opt {
                   optProperties = StructFreeChoice : optProperties opt
               }))
        "Prove that the net is free-choice"

154
155
156
157
158
159
160
161
162
163
164
165
        , 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"

166
167
168
169
170
171
        , Option "" ["communication-free"]
        (NoArg (\opt -> Right opt {
                   optProperties = StructCommunicationFree : optProperties opt
               }))
        "Prove that the net is communication-free"

172
173
174
175
        , Option "n" ["no-refinement"]
        (NoArg (\opt -> Right opt { optRefine = False }))
        "Don't use refinement"

176
177
178
179
180
181
182
        , Option "o" ["output"]
        (ReqArg (\arg opt -> Right opt {
                        optOutput = Just arg
                })
                "FILE")
        "Write net and properties to FILE"

183
184
185
186
187
188
        , Option "" ["no-given-properties"]
        (NoArg (\opt -> Right opt {
                   optUseProperties = False
               }))
        "Do not use the properties given in the input file"

189
        , Option "v" ["verbose"]
190
191
192
193
194
195
        (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)"
196
197
198
199
200
201
202
203
204
205

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

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

206
207
208
209
verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
        when (verbosity >= level) (putStrLn str)

210
211
212
213
214
215
216
217
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

218
219
writeFiles :: Int -> String -> PetriNet -> [Property] -> IO ()
writeFiles verbosity basename net props = do
220
        -- TODO: add options for different outputs
221
        verbosePut verbosity 1 $ "Writing " ++ showNetName net ++ " to " ++ basename
222
223
224
225
226
227
228
229
230
231
232
        L.writeFile basename $ DOTPrinter.printNet net
        --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)..])
        --verbosePut verbosity 1 $ "Writing properties to " ++ basename ++ ".sara"
        --L.writeFile (basename ++ ".sara") $
        --    SARAPrinter.printProperties basename net props
233
234
235
236
237
238
        --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)..])
239

240
241
242
243
244
245
246
247
248
249
250
251
252
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)
253
254
        putStrLn $ "Places             : " ++ show (length (places net))
        putStrLn $ "Transitions        : " ++ show (length (transitions net))
255
256
257
258
259
260
        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)

261
checkFile :: Parser (PetriNet,[Property]) -> Int -> Bool ->
262
            [ImplicitProperty] -> [NetTransformation] ->
263
            Bool -> Maybe String -> Bool -> String -> IO PropResult
264
checkFile parser verbosity refine implicitProperties transformations
265
          useProperties output printStruct file = do
266
        verbosePut verbosity 0 $ "Reading \"" ++ file ++ "\""
267
        (net,props) <- parseFile parser file
268
269
270
        let props' = if useProperties then props else []
        let props'' = props' ++ map (makeImplicitProperty net) implicitProperties
        let (net',props''') = foldl transformNet (net,props'') transformations
271
272
273
274
        verbosePut verbosity 1 $ "Analyzing " ++ showNetName net
        verbosePut verbosity 2 $
                "Places: " ++ show (length  $ places net') ++ "; " ++
                "Transitions: " ++ show (length $ transitions net')
275
        when printStruct $ structuralAnalysis net
276
        verbosePut verbosity 3 $ show net'
277
        case output of
278
            Just outputfile -> writeFiles verbosity outputfile net' props'''
279
            Nothing -> return ()
Philipp Meyer's avatar
Philipp Meyer committed
280
        -- TODO: short-circuit?
281
        rs <- mapM (checkProperty verbosity net' refine) props'''
282
        verbosePut verbosity 0 ""
283
        return $ resultsAnd rs
284

285
placeOp :: Op -> (String, Integer) -> Formula
286
placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w)
287

288
289
transformNet :: (PetriNet, [Property]) -> NetTransformation ->
               (PetriNet, [Property])
290
transformNet (net, props) TerminationByReachability =
291
292
293
294
        let prime = ('\'':)
            ps = ["'sigma", "'m1", "'m2"] ++
                 places net ++ map prime (places net)
            is = [("'m1", 1)] ++
295
                 initials net ++ map (first prime) (initials net)
296
297
298
299
300
301
302
303
304
305
            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'')]
306
            ts = ("'switch", [("'m1",1)], [("'m2",1)]) :
307
308
                 concatMap transformTransition (transitions net)
            gs = ghostTransitions net
309
            prop = Property "termination by reachability" $ Safety $
310
                    foldl (:&:) (Atom (LinIneq (Var "'sigma") Ge (Const 1)))
311
312
                      (map (\p -> Atom (LinIneq
                                (Var (prime p) :-: Var p) Ge (Const 0)))
313
                        (places net))
314
            -- TODO: map existing liveness properties
315
        in  (makePetriNetWithTrans (name net) ps ts is gs, prop : props)
316
transformNet (net, props) ValidateIdentifiers =
317
318
319
320
        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
321
322
            gs = map validateId $ ghostTransitions net
            net' = makePetriNet (name net) ps ts as is gs
323
            props' = map (rename validateId) props
324
        in  (net', props')
325

326
makeImplicitProperty :: PetriNet -> ImplicitProperty -> Property
327
makeImplicitProperty net Termination =
328
        Property "termination" $ Liveness $
329
330
331
            foldl (:&:) FTrue
                (map (\t -> Atom (LinIneq (Var t) Eq (Const 0)))
                    (ghostTransitions net))
332
makeImplicitProperty net ProperTermination =
Philipp Meyer's avatar
Philipp Meyer committed
333
        let (finals, nonfinals) = partition (null . lpost net) (places net)
334
        in  Property "proper termination" $ Safety
Philipp Meyer's avatar
Philipp Meyer committed
335
336
            (foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) finals) :&:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals))
337
makeImplicitProperty net DeadlockFree =
338
        Property "deadlock-free" $ Safety $
339
340
            foldl (:&:) FTrue
                (map (foldl (:|:) FFalse . map (placeOp Lt) . lpre net)
341
                     (filter (`notElem` ghostTransitions net) (transitions net)))
342
makeImplicitProperty net DeadlockFreeUnlessFinal =
343
        let (Property _ (Safety pf)) = makeImplicitProperty net DeadlockFree
344
            (finals, nonfinals) = partition (null . lpost net) (places net)
345
        in  Property "deadlock-free unless final" $ Safety $
Philipp Meyer's avatar
Philipp Meyer committed
346
347
            (foldl (:&:) FTrue  (map (\p -> placeOp Eq (p,0)) finals) :|:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals)) :&:
348
            pf
349
makeImplicitProperty net (Bounded k) =
350
        Property (show k ++ "-bounded") $ Safety $
351
            foldl (:|:) FFalse
Philipp Meyer's avatar
Philipp Meyer committed
352
                (map (\p -> placeOp Ge (p,k+1))
353
354
                    (filter (`notElem` concatMap (post net) (ghostTransitions net))
                        (places net)))
355
356
makeImplicitProperty net Safe =
        let bounded = makeImplicitProperty net (Bounded 1)
357
358
359
        in  Property "safe" $ pcont bounded
makeImplicitProperty _ StructFreeChoice =
        Property "free choice" $ Structural FreeChoice
360
361
362
363
makeImplicitProperty _ StructParallel =
        Property "parallel" $ Structural Parallel
makeImplicitProperty _ StructFinalPlace =
        Property "final place" $ Structural FinalPlace
364
365
makeImplicitProperty _ StructCommunicationFree =
        Property "communication free" $ Structural CommunicationFree
366

367
checkProperty :: Int -> PetriNet -> Bool -> Property -> IO PropResult
368
369
checkProperty verbosity net refine p = do
        verbosePut verbosity 1 $ "\nChecking " ++ showPropertyName p
370
        verbosePut verbosity 3 $ show p
371
372
373
374
375
376
377
378
379
        r <- case pcont p of
            (Safety pf) -> checkSafetyProperty verbosity net refine pf []
            (Liveness pf) -> checkLivenessProperty verbosity net refine pf []
            (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."
380
381
        return r

382
checkSafetyProperty :: Int -> PetriNet -> Bool ->
383
        Formula -> [[String]] -> IO PropResult
384
checkSafetyProperty verbosity net refine f traps = do
385
386
        r <- checkSat $ checkStateEquationSat net f traps
        case r of
387
            Nothing -> return Satisfied
388
389
            Just a -> do
                let assigned = markedPlacesFromAssignment net a
390
391
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Places marked: " ++ show assigned
392
                verbosePut verbosity 3 $ "Assignment: " ++ show a
393
394
395
396
                if refine then do
                    rt <- checkSat $ checkTrapSat net assigned
                    case rt of
                        Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
397
                            verbosePut verbosity 1 "No trap found."
398
                            return Unknown
399
400
                        Just at -> do
                            let trap = trapFromAssignment at
401
402
403
                            verbosePut verbosity 1 "Trap found"
                            verbosePut verbosity 2 $ "Places in trap: " ++
                                                      show trap
404
405
                            verbosePut verbosity 3 $ "Trap assignment: " ++
                                                      show at
406
                            checkSafetyProperty verbosity net refine f
407
408
                                                (trap:traps)
                else
409
                    return Unknown
410

411
checkLivenessProperty :: Int -> PetriNet -> Bool ->
412
        Formula -> [([String],[String])] -> IO PropResult
413
checkLivenessProperty verbosity net refine f strans = do
414
        r <- checkSat $ checkTransitionInvariantSat net f strans
Philipp Meyer's avatar
Philipp Meyer committed
415
        case r of
416
            Nothing -> return Satisfied
417
418
            Just ax -> do
                let fired = firedTransitionsFromAssignment ax
419
420
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Transitions fired: " ++ show fired
421
                verbosePut verbosity 3 $ "Assignment: " ++ show ax
422
423
424
425
                if refine then do
                    rt <- checkSat $ checkSComponentSat net fired ax
                    case rt of
                        Nothing -> do
426
                            verbosePut verbosity 1 "No S-component found"
427
                            return Unknown
428
429
                        Just as -> do
                            let sOutIn = getSComponentOutIn net ax as
430
431
                            verbosePut verbosity 1 "S-component found"
                            verbosePut verbosity 2 $ "Out/In: " ++ show sOutIn
432
433
                            verbosePut verbosity 3 $ "S-Component assignment: " ++
                                                      show as
434
                            checkLivenessProperty verbosity net refine f
435
436
                                                  (sOutIn:strans)
                else
437
438
439
                    return Unknown

checkStructuralProperty :: Int -> PetriNet -> Structure -> IO PropResult
440
checkStructuralProperty _ net struct =
441
442
443
444
        if checkStructure net struct then
            return Satisfied
        else
            return Unsatisfied
445

446
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
447
main = do
448
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
449
450
451
452
453
454
455
456
        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")
457
458
                let verbosity = optVerbosity opts
                    refinement = optRefine opts
459
460
                let parser = case inputFormat opts of
                                 PNET -> PNET.parseContent
Philipp Meyer's avatar
Philipp Meyer committed
461
                                 LOLA -> LOLA.parseContent
462
                                 TPN -> TPN.parseContent
463
                                 MIST -> MIST.parseContent
464
465
466
                let properties = reverse $ optProperties opts
                let transformations = reverse $ optTransformations opts
                rs <- mapM (checkFile parser verbosity refinement properties
467
468
                     transformations (optUseProperties opts) (optOutput opts)
                     (optPrintStructure opts)) files
Philipp Meyer's avatar
Philipp Meyer committed
469
                -- TODO: short-circuit with Control.Monad.Loops?
470
471
472
473
474
475
476
                case resultsAnd rs of
                    Satisfied ->
                        exitSuccessWith "All properties satisfied."
                    Unsatisfied ->
                        exitFailureWith "Some properties are not satisfied"
                    Unknown ->
                        exitFailureWith "Some properties may not be satisfied."
477

Philipp Meyer's avatar
Philipp Meyer committed
478
-- TODO: Always exit with exit code 0 unless an error occured
479
480
481
482
483
484
485
486
exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
        exitSuccess

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

489
490
491
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
492
        exitWith $ ExitFailure 3