Main.hs 16.7 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
24
import Property
25
import Solver
26
27
import Solver.StateEquation
import Solver.TrapConstraints
28
29
import Solver.TransitionInvariant
import Solver.SComponent
30

31
data InputFormat = PNET | LOLA | TPN | MIST deriving (Show,Read)
32

33
34
data NetTransformation = TerminationByReachability
                       | ValidateIdentifiers
35

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

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

startOptions :: Options
startOptions = Options { inputFormat = PNET
55
                       , optVerbosity = 1
56
57
                       , optShowHelp = False
                       , optShowVersion = False
58
                       , optProperties = []
59
                       , optTransformations = []
60
                       , optRefine = True
61
                       , optOutput = Nothing
62
                       , optUseProperties = True
63
64
65
66
                       }

options :: [ OptDescr (Options -> Either String Options) ]
options =
67
68
69
70
71
72
73
74
75
76
77
        [ 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"
78

79
80
81
82
        , Option "" ["spec"]
        (NoArg (\opt -> Right opt { inputFormat = MIST }))
        "Use the mist input format"

83
84
85
86
87
88
        , Option "" ["validate-identifiers"]
        (NoArg (\opt -> Right opt {
            optTransformations = ValidateIdentifiers : optTransformations opt
          }))
        "Make identifiers valid for lola"

89
        , Option "" ["termination-by-reachability"]
90
        (NoArg (\opt -> Right opt {
91
            optTransformations = TerminationByReachability : optTransformations opt
92
          }))
93
        "Prove termination by reducing it to reachability"
94

95
        , Option "" ["terminating"]
96
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
97
                   optProperties = Termination : optProperties opt
98
               }))
99
        "Prove that the net is terminating"
100

Philipp Meyer's avatar
Philipp Meyer committed
101
102
103
104
105
106
        , Option "" ["proper-termination"]
        (NoArg (\opt -> Right opt {
                   optProperties = ProperTermination : optProperties opt
               }))
        "Prove termination in the final marking"

107
        , Option "" ["deadlock-free"]
108
        (NoArg (\opt -> Right opt {
109
                   optProperties = DeadlockFree : optProperties opt
110
               }))
111
        "Prove that the net is deadlock-free"
112

113
        , Option "" ["deadlock-free-unless-final"]
Philipp Meyer's avatar
Philipp Meyer committed
114
        (NoArg (\opt -> Right opt {
115
                   optProperties = DeadlockFreeUnlessFinal : optProperties opt
Philipp Meyer's avatar
Philipp Meyer committed
116
               }))
117
118
        ("Prove that the net is deadlock-free\n" ++
         "unless it is in the final marking")
Philipp Meyer's avatar
Philipp Meyer committed
119

120
121
        , Option "" ["safe"]
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
122
                   optProperties = Safe : optProperties opt
123
124
125
126
127
128
129
130
131
132
133
134
               }))
        "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"

135
136
137
138
        , Option "n" ["no-refinement"]
        (NoArg (\opt -> Right opt { optRefine = False }))
        "Don't use refinement"

139
140
141
142
143
144
145
        , Option "o" ["output"]
        (ReqArg (\arg opt -> Right opt {
                        optOutput = Just arg
                })
                "FILE")
        "Write net and properties to FILE"

146
147
148
149
150
151
        , Option "" ["no-given-properties"]
        (NoArg (\opt -> Right opt {
                   optUseProperties = False
               }))
        "Do not use the properties given in the input file"

152
        , Option "v" ["verbose"]
153
154
155
156
157
158
        (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)"
159
160
161
162
163
164
165
166
167
168

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

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

169
170
171
172
verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
        when (verbosity >= level) (putStrLn str)

173
174
175
176
177
178
179
180
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

181
182
183
writeFiles :: Int -> String -> PetriNet -> [Property] -> IO ()
writeFiles verbosity basename net props = do
        verbosePut verbosity 1 $ "Writing " ++ showNetName net ++ " to " ++ basename
184
        L.writeFile basename $ LOLAPrinter.printNet net
185
186
187
188
        mapM_ (\(p,i) -> do
                let file = basename ++ ".task" ++ show i
                verbosePut verbosity 1 $ "Writing " ++ showPropertyName p ++
                                         " to " ++ file
189
                L.writeFile file $ LOLAPrinter.printProperty p
190
              ) (zip props [(1::Integer)..])
191
        verbosePut verbosity 1 $ "Writing properties to " ++ basename ++ ".sara"
192
193
        L.writeFile (basename ++ ".sara") $
            SARAPrinter.printProperties basename net props
194

195
checkFile :: Parser (PetriNet,[Property]) -> Int -> Bool ->
196
            [ImplicitProperty] -> [NetTransformation] ->
197
            Bool -> Maybe String -> String -> IO Bool
198
checkFile parser verbosity refine implicitProperties transformations
199
          useProperties output file = do
200
        verbosePut verbosity 0 $ "Reading \"" ++ file ++ "\""
201
        (net,props) <- parseFile parser file
202
203
204
        let props' = if useProperties then props else []
        let props'' = props' ++ map (makeImplicitProperty net) implicitProperties
        let (net',props''') = foldl transformNet (net,props'') transformations
205
206
207
208
209
        verbosePut verbosity 1 $ "Analyzing " ++ showNetName net
        verbosePut verbosity 2 $
                "Places: " ++ show (length  $ places net') ++ "; " ++
                "Transitions: " ++ show (length $ transitions net')
        verbosePut verbosity 3 $ show net'
210
        case output of
211
            Just outputfile -> writeFiles verbosity outputfile net' props'''
212
            Nothing -> return ()
213
        rs <- mapM (checkProperty verbosity net' refine) props'''
214
        verbosePut verbosity 0 ""
215
216
        return $ and rs

217
placeOp :: Op -> (String, Integer) -> Formula
218
placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w)
219

220
221
transformNet :: (PetriNet, [Property]) -> NetTransformation ->
               (PetriNet, [Property])
222
transformNet (net, props) TerminationByReachability =
223
224
225
226
        let prime = ('\'':)
            ps = ["'sigma", "'m1", "'m2"] ++
                 places net ++ map prime (places net)
            is = [("'m1", 1)] ++
227
                 initials net ++ map (first prime) (initials net)
228
229
230
231
232
233
234
235
236
237
            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'')]
238
            ts = ("'switch", [("'m1",1)], [("'m2",1)]) :
239
240
                 concatMap transformTransition (transitions net)
            gs = ghostTransitions net
241
242
            prop = Property "termination by reachability" Safety $
                    foldl (:&:) (Atom (LinIneq (Var "'sigma") Ge (Const 1)))
243
244
                      (map (\p -> Atom (LinIneq
                                (Var (prime p) :-: Var p) Ge (Const 0)))
245
                        (places net))
246
            -- TODO: map existing liveness properties
247
        in  (makePetriNetWithTrans (name net) ps ts is gs, prop : props)
248
transformNet (net, props) ValidateIdentifiers =
249
250
251
252
        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
253
254
            gs = map validateId $ ghostTransitions net
            net' = makePetriNet (name net) ps ts as is gs
255
            props' = map (rename validateId) props
256
        in  (net', props')
257

258
makeImplicitProperty :: PetriNet -> ImplicitProperty -> Property
259
260
261
262
263
makeImplicitProperty net Termination =
        Property "termination" Liveness $
            foldl (:&:) FTrue
                (map (\t -> Atom (LinIneq (Var t) Eq (Const 0)))
                    (ghostTransitions net))
264
makeImplicitProperty net ProperTermination =
Philipp Meyer's avatar
Philipp Meyer committed
265
        let (finals, nonfinals) = partition (null . lpost net) (places net)
266
        in  Property "proper termination" Safety
Philipp Meyer's avatar
Philipp Meyer committed
267
268
            (foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) finals) :&:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals))
269
270
makeImplicitProperty net DeadlockFree =
        Property "deadlock-free" Safety $
271
272
            foldl (:&:) FTrue
                (map (foldl (:|:) FFalse . map (placeOp Lt) . lpre net)
273
                     (filter (`notElem` ghostTransitions net) (transitions net)))
274
275
makeImplicitProperty net DeadlockFreeUnlessFinal =
        let nodeadlock = makeImplicitProperty net DeadlockFree
276
            (finals, nonfinals) = partition (null . lpost net) (places net)
277
        in  Property "deadlock-free unless final" Safety $
Philipp Meyer's avatar
Philipp Meyer committed
278
279
280
            (foldl (:&:) FTrue  (map (\p -> placeOp Eq (p,0)) finals) :|:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals)) :&:
            pformula nodeadlock
281
makeImplicitProperty net (Bounded k) =
282
        Property (show k ++ "-bounded") Safety $
283
            foldl (:|:) FFalse
284
285
286
                (map (\p -> placeOp Gt (p,k))
                    (filter (`notElem` concatMap (post net) (ghostTransitions net))
                        (places net)))
287
288
289
makeImplicitProperty net Safe =
        let bounded = makeImplicitProperty net (Bounded 1)
        in  Property "safe" Safety $ pformula bounded
290

291
292
293
checkProperty :: Int -> PetriNet -> Bool -> Property -> IO Bool
checkProperty verbosity net refine p = do
        verbosePut verbosity 1 $ "\nChecking " ++ showPropertyName p
294
        verbosePut verbosity 3 $ show p
295
        r <- case ptype p of
296
297
298
            Safety -> checkSafetyProperty verbosity net refine (pformula p) []
            Liveness -> checkLivenessProperty verbosity net refine (pformula p) []
        verbosePut verbosity 0 $ showPropertyName p ++
299
                                    if r then " is satisfied."
300
                                    else " may not be satisfied."
301
302
        return r

303
checkSafetyProperty :: Int -> PetriNet -> Bool ->
304
        Formula -> [[String]] -> IO Bool
305
checkSafetyProperty verbosity net refine f traps = do
306
307
308
309
310
        r <- checkSat $ checkStateEquationSat net f traps
        case r of
            Nothing -> return True
            Just a -> do
                let assigned = markedPlacesFromAssignment net a
311
312
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Places marked: " ++ show assigned
313
                verbosePut verbosity 3 $ "Assignment: " ++ show a
314
315
316
317
                if refine then do
                    rt <- checkSat $ checkTrapSat net assigned
                    case rt of
                        Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
318
                            verbosePut verbosity 1 "No trap found."
319
320
321
                            return False
                        Just at -> do
                            let trap = trapFromAssignment at
322
323
324
                            verbosePut verbosity 1 "Trap found"
                            verbosePut verbosity 2 $ "Places in trap: " ++
                                                      show trap
325
326
                            verbosePut verbosity 3 $ "Trap assignment: " ++
                                                      show at
327
                            checkSafetyProperty verbosity net refine f
328
329
330
331
                                                (trap:traps)
                else
                    return False

332
checkLivenessProperty :: Int -> PetriNet -> Bool ->
333
        Formula -> [([String],[String])] -> IO Bool
334
checkLivenessProperty verbosity net refine f strans = do
335
        r <- checkSat $ checkTransitionInvariantSat net f strans
Philipp Meyer's avatar
Philipp Meyer committed
336
        case r of
337
            Nothing -> return True
338
339
            Just ax -> do
                let fired = firedTransitionsFromAssignment ax
340
341
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Transitions fired: " ++ show fired
342
                verbosePut verbosity 3 $ "Assignment: " ++ show ax
343
344
345
346
                if refine then do
                    rt <- checkSat $ checkSComponentSat net fired ax
                    case rt of
                        Nothing -> do
347
                            verbosePut verbosity 1 "No S-component found"
348
349
350
                            return False
                        Just as -> do
                            let sOutIn = getSComponentOutIn net ax as
351
352
                            verbosePut verbosity 1 "S-component found"
                            verbosePut verbosity 2 $ "Out/In: " ++ show sOutIn
353
354
                            verbosePut verbosity 3 $ "S-Component assignment: " ++
                                                      show as
355
                            checkLivenessProperty verbosity net refine f
356
357
358
                                                  (sOutIn:strans)
                else
                    return False
359

360
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
361
main = do
362
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
363
364
365
366
367
368
369
370
        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")
371
372
                let verbosity = optVerbosity opts
                    refinement = optRefine opts
373
374
                let parser = case inputFormat opts of
                                 PNET -> PNET.parseContent
Philipp Meyer's avatar
Philipp Meyer committed
375
                                 LOLA -> LOLA.parseContent
376
                                 TPN -> TPN.parseContent
377
                                 MIST -> MIST.parseContent
378
379
380
                let properties = reverse $ optProperties opts
                let transformations = reverse $ optTransformations opts
                rs <- mapM (checkFile parser verbosity refinement properties
381
382
                     transformations (optUseProperties opts) (optOutput opts))
                     files
383
384
385
386
387
388
389
390
391
392
393
394
395
                if and rs then
                    exitSuccessWith "All properties satisfied."
                else
                    exitFailureWith "Some properties may not be satisfied."

exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
        exitSuccess

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

398
399
400
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
401
        exitWith $ ExitFailure 3