Main.hs 20.6 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
47
                      deriving (Show,Read)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

165
166
167
168
        , Option "n" ["no-refinement"]
        (NoArg (\opt -> Right opt { optRefine = False }))
        "Don't use refinement"

169
170
171
172
173
174
175
        , Option "o" ["output"]
        (ReqArg (\arg opt -> Right opt {
                        optOutput = Just arg
                })
                "FILE")
        "Write net and properties to FILE"

176
177
178
179
180
181
        , Option "" ["no-given-properties"]
        (NoArg (\opt -> Right opt {
                   optUseProperties = False
               }))
        "Do not use the properties given in the input file"

182
        , Option "v" ["verbose"]
183
184
185
186
187
188
        (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)"
189
190
191
192
193
194
195
196
197
198

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

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

199
200
201
202
verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
        when (verbosity >= level) (putStrLn str)

203
204
205
206
207
208
209
210
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

211
212
writeFiles :: Int -> String -> PetriNet -> [Property] -> IO ()
writeFiles verbosity basename net props = do
213
        -- TODO: add options for different outputs
214
        verbosePut verbosity 1 $ "Writing " ++ showNetName net ++ " to " ++ basename
215
216
217
218
219
220
221
222
223
224
225
        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
226
227
228
229
230
231
        --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)..])
232

233
234
235
236
237
238
239
240
241
242
243
244
245
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)
246
247
        putStrLn $ "Places             : " ++ show (length (places net))
        putStrLn $ "Transitions        : " ++ show (length (transitions net))
248
249
250
251
252
253
        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)

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

278
placeOp :: Op -> (String, Integer) -> Formula
279
placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w)
280

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

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

358
checkProperty :: Int -> PetriNet -> Bool -> Property -> IO PropResult
359
360
checkProperty verbosity net refine p = do
        verbosePut verbosity 1 $ "\nChecking " ++ showPropertyName p
361
        verbosePut verbosity 3 $ show p
362
363
364
365
366
367
368
369
370
        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."
371
372
        return r

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

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

checkStructuralProperty :: Int -> PetriNet -> Structure -> IO PropResult
431
checkStructuralProperty _ net struct =
432
433
434
435
        if checkStructure net struct then
            return Satisfied
        else
            return Unsatisfied
436

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

Philipp Meyer's avatar
Philipp Meyer committed
469
-- TODO: Always exit with exit code 0 unless an error occured
470
471
472
473
474
475
476
477
exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
        exitSuccess

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

480
481
482
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
483
        exitWith $ ExitFailure 3