Main.hs 19.8 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 Property
26
import Structure
27
import Solver
28
29
import Solver.StateEquation
import Solver.TrapConstraints
30
31
import Solver.TransitionInvariant
import Solver.SComponent
32

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

35
36
data NetTransformation = TerminationByReachability
                       | ValidateIdentifiers
37

38
data ImplicitProperty = Termination
39
                      | DeadlockFree | DeadlockFreeUnlessFinal
Philipp Meyer's avatar
Philipp Meyer committed
40
                      | ProperTermination
41
                      | Safe | Bounded Integer
42
                      | StructFreeChoice
43
44
                      deriving (Show,Read)

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

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

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

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

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

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

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

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

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

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

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

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

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

150
151
152
153
        , Option "n" ["no-refinement"]
        (NoArg (\opt -> Right opt { optRefine = False }))
        "Don't use refinement"

154
155
156
157
158
159
160
        , Option "o" ["output"]
        (ReqArg (\arg opt -> Right opt {
                        optOutput = Just arg
                })
                "FILE")
        "Write net and properties to FILE"

161
162
163
164
165
166
        , Option "" ["no-given-properties"]
        (NoArg (\opt -> Right opt {
                   optUseProperties = False
               }))
        "Do not use the properties given in the input file"

167
        , Option "v" ["verbose"]
168
169
170
171
172
173
        (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)"
174
175
176
177
178
179
180
181
182
183

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

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

184
185
186
187
verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
        when (verbosity >= level) (putStrLn str)

188
189
190
191
192
193
194
195
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

196
197
writeFiles :: Int -> String -> PetriNet -> [Property] -> IO ()
writeFiles verbosity basename net props = do
198
        -- TODO: add options for different outputs
199
        verbosePut verbosity 1 $ "Writing " ++ showNetName net ++ " to " ++ basename
200
        L.writeFile basename $ LOLAPrinter.printNet net
201
202
203
204
        mapM_ (\(p,i) -> do
                let file = basename ++ ".task" ++ show i
                verbosePut verbosity 1 $ "Writing " ++ showPropertyName p ++
                                         " to " ++ file
205
                L.writeFile file $ LOLAPrinter.printProperty p
206
              ) (zip props [(1::Integer)..])
207
        verbosePut verbosity 1 $ "Writing properties to " ++ basename ++ ".sara"
208
209
        L.writeFile (basename ++ ".sara") $
            SARAPrinter.printProperties basename net props
210
211
212
213
214
215
        --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)..])
216

217
218
219
220
221
222
223
224
225
226
227
228
229
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)
230
231
        putStrLn $ "Places             : " ++ show (length (places net))
        putStrLn $ "Transitions        : " ++ show (length (transitions net))
232
233
234
235
236
237
        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)

238
checkFile :: Parser (PetriNet,[Property]) -> Int -> Bool ->
239
            [ImplicitProperty] -> [NetTransformation] ->
240
            Bool -> Maybe String -> Bool -> String -> IO PropResult
241
checkFile parser verbosity refine implicitProperties transformations
242
          useProperties output printStruct file = do
243
        verbosePut verbosity 0 $ "Reading \"" ++ file ++ "\""
244
        (net,props) <- parseFile parser file
245
246
247
        let props' = if useProperties then props else []
        let props'' = props' ++ map (makeImplicitProperty net) implicitProperties
        let (net',props''') = foldl transformNet (net,props'') transformations
248
249
250
251
        verbosePut verbosity 1 $ "Analyzing " ++ showNetName net
        verbosePut verbosity 2 $
                "Places: " ++ show (length  $ places net') ++ "; " ++
                "Transitions: " ++ show (length $ transitions net')
252
        when printStruct $ structuralAnalysis net
253
        verbosePut verbosity 3 $ show net'
254
        case output of
255
            Just outputfile -> writeFiles verbosity outputfile net' props'''
256
            Nothing -> return ()
Philipp Meyer's avatar
Philipp Meyer committed
257
        -- TODO: short-circuit?
258
        rs <- mapM (checkProperty verbosity net' refine) props'''
259
        verbosePut verbosity 0 ""
260
        return $ resultsAnd rs
261

262
placeOp :: Op -> (String, Integer) -> Formula
263
placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w)
264

265
266
transformNet :: (PetriNet, [Property]) -> NetTransformation ->
               (PetriNet, [Property])
267
transformNet (net, props) TerminationByReachability =
268
269
270
271
        let prime = ('\'':)
            ps = ["'sigma", "'m1", "'m2"] ++
                 places net ++ map prime (places net)
            is = [("'m1", 1)] ++
272
                 initials net ++ map (first prime) (initials net)
273
274
275
276
277
278
279
280
281
282
            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'')]
283
            ts = ("'switch", [("'m1",1)], [("'m2",1)]) :
284
285
                 concatMap transformTransition (transitions net)
            gs = ghostTransitions net
286
            prop = Property "termination by reachability" $ Safety $
287
                    foldl (:&:) (Atom (LinIneq (Var "'sigma") Ge (Const 1)))
288
289
                      (map (\p -> Atom (LinIneq
                                (Var (prime p) :-: Var p) Ge (Const 0)))
290
                        (places net))
291
            -- TODO: map existing liveness properties
292
        in  (makePetriNetWithTrans (name net) ps ts is gs, prop : props)
293
transformNet (net, props) ValidateIdentifiers =
294
295
296
297
        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
298
299
            gs = map validateId $ ghostTransitions net
            net' = makePetriNet (name net) ps ts as is gs
300
            props' = map (rename validateId) props
301
        in  (net', props')
302

303
makeImplicitProperty :: PetriNet -> ImplicitProperty -> Property
304
makeImplicitProperty net Termination =
305
        Property "termination" $ Liveness $
306
307
308
            foldl (:&:) FTrue
                (map (\t -> Atom (LinIneq (Var t) Eq (Const 0)))
                    (ghostTransitions net))
309
makeImplicitProperty net ProperTermination =
Philipp Meyer's avatar
Philipp Meyer committed
310
        let (finals, nonfinals) = partition (null . lpost net) (places net)
311
        in  Property "proper termination" $ Safety
Philipp Meyer's avatar
Philipp Meyer committed
312
313
            (foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) finals) :&:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals))
314
makeImplicitProperty net DeadlockFree =
315
        Property "deadlock-free" $ Safety $
316
317
            foldl (:&:) FTrue
                (map (foldl (:|:) FFalse . map (placeOp Lt) . lpre net)
318
                     (filter (`notElem` ghostTransitions net) (transitions net)))
319
makeImplicitProperty net DeadlockFreeUnlessFinal =
320
        let (Property _ (Safety pf)) = makeImplicitProperty net DeadlockFree
321
            (finals, nonfinals) = partition (null . lpost net) (places net)
322
        in  Property "deadlock-free unless final" $ Safety $
Philipp Meyer's avatar
Philipp Meyer committed
323
324
            (foldl (:&:) FTrue  (map (\p -> placeOp Eq (p,0)) finals) :|:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals)) :&:
325
            pf
326
makeImplicitProperty net (Bounded k) =
327
        Property (show k ++ "-bounded") $ Safety $
328
            foldl (:|:) FFalse
Philipp Meyer's avatar
Philipp Meyer committed
329
                (map (\p -> placeOp Ge (p,k+1))
330
331
                    (filter (`notElem` concatMap (post net) (ghostTransitions net))
                        (places net)))
332
333
makeImplicitProperty net Safe =
        let bounded = makeImplicitProperty net (Bounded 1)
334
335
336
        in  Property "safe" $ pcont bounded
makeImplicitProperty _ StructFreeChoice =
        Property "free choice" $ Structural FreeChoice
337

338
checkProperty :: Int -> PetriNet -> Bool -> Property -> IO PropResult
339
340
checkProperty verbosity net refine p = do
        verbosePut verbosity 1 $ "\nChecking " ++ showPropertyName p
341
        verbosePut verbosity 3 $ show p
342
343
344
345
346
347
348
349
350
        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."
351
352
        return r

353
checkSafetyProperty :: Int -> PetriNet -> Bool ->
354
        Formula -> [[String]] -> IO PropResult
355
checkSafetyProperty verbosity net refine f traps = do
356
357
        r <- checkSat $ checkStateEquationSat net f traps
        case r of
358
            Nothing -> return Satisfied
359
360
            Just a -> do
                let assigned = markedPlacesFromAssignment net a
361
362
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Places marked: " ++ show assigned
363
                verbosePut verbosity 3 $ "Assignment: " ++ show a
364
365
366
367
                if refine then do
                    rt <- checkSat $ checkTrapSat net assigned
                    case rt of
                        Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
368
                            verbosePut verbosity 1 "No trap found."
369
                            return Unknown
370
371
                        Just at -> do
                            let trap = trapFromAssignment at
372
373
374
                            verbosePut verbosity 1 "Trap found"
                            verbosePut verbosity 2 $ "Places in trap: " ++
                                                      show trap
375
376
                            verbosePut verbosity 3 $ "Trap assignment: " ++
                                                      show at
377
                            checkSafetyProperty verbosity net refine f
378
379
                                                (trap:traps)
                else
380
                    return Unknown
381

382
checkLivenessProperty :: Int -> PetriNet -> Bool ->
383
        Formula -> [([String],[String])] -> IO PropResult
384
checkLivenessProperty verbosity net refine f strans = do
385
        r <- checkSat $ checkTransitionInvariantSat net f strans
Philipp Meyer's avatar
Philipp Meyer committed
386
        case r of
387
            Nothing -> return Satisfied
388
389
            Just ax -> do
                let fired = firedTransitionsFromAssignment ax
390
391
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Transitions fired: " ++ show fired
392
                verbosePut verbosity 3 $ "Assignment: " ++ show ax
393
394
395
396
                if refine then do
                    rt <- checkSat $ checkSComponentSat net fired ax
                    case rt of
                        Nothing -> do
397
                            verbosePut verbosity 1 "No S-component found"
398
                            return Unknown
399
400
                        Just as -> do
                            let sOutIn = getSComponentOutIn net ax as
401
402
                            verbosePut verbosity 1 "S-component found"
                            verbosePut verbosity 2 $ "Out/In: " ++ show sOutIn
403
404
                            verbosePut verbosity 3 $ "S-Component assignment: " ++
                                                      show as
405
                            checkLivenessProperty verbosity net refine f
406
407
                                                  (sOutIn:strans)
                else
408
409
410
411
412
413
414
415
                    return Unknown

checkStructuralProperty :: Int -> PetriNet -> Structure -> IO PropResult
checkStructuralProperty _ net struct = do
        if checkStructure net struct then
            return Satisfied
        else
            return Unsatisfied
416

417
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
418
main = do
419
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
420
421
422
423
424
425
426
427
        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")
428
429
                let verbosity = optVerbosity opts
                    refinement = optRefine opts
430
431
                let parser = case inputFormat opts of
                                 PNET -> PNET.parseContent
Philipp Meyer's avatar
Philipp Meyer committed
432
                                 LOLA -> LOLA.parseContent
433
                                 TPN -> TPN.parseContent
434
                                 MIST -> MIST.parseContent
435
436
437
                let properties = reverse $ optProperties opts
                let transformations = reverse $ optTransformations opts
                rs <- mapM (checkFile parser verbosity refinement properties
438
439
                     transformations (optUseProperties opts) (optOutput opts)
                     (optPrintStructure opts)) files
Philipp Meyer's avatar
Philipp Meyer committed
440
                -- TODO: short-circuit with Control.Monad.Loops?
441
442
443
444
445
446
447
                case resultsAnd rs of
                    Satisfied ->
                        exitSuccessWith "All properties satisfied."
                    Unsatisfied ->
                        exitFailureWith "Some properties are not satisfied"
                    Unknown ->
                        exitFailureWith "Some properties may not be satisfied."
448

Philipp Meyer's avatar
Philipp Meyer committed
449
-- TODO: Always exit with exit code 0 unless an error occured
450
451
452
453
454
455
456
457
exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
        exitSuccess

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

460
461
462
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
463
        exitWith $ ExitFailure 3