Main.hs 16.2 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)
Philipp Meyer's avatar
Philipp Meyer committed
13

14
15
import Parser
import qualified Parser.PNET as PNET
Philipp Meyer's avatar
Philipp Meyer committed
16
import qualified Parser.LOLA as LOLA
17
import qualified Parser.TPN as TPN
18
import qualified Parser.MIST as MIST
19
import PetriNet
20
import Printer
21
22
import qualified Printer.LOLA as LOLAPrinter
import qualified Printer.SARA as SARAPrinter
23
import Property
24
import Solver
25
26
import Solver.StateEquation
import Solver.TrapConstraints
27
28
import Solver.TransitionInvariant
import Solver.SComponent
29

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

32
33
data NetTransformation = TerminationByReachability
                       | ValidateIdentifiers
34

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

253
makeImplicitProperty :: PetriNet -> ImplicitProperty -> Property
254
makeImplicitProperty _ Termination =
255
256
        Property "termination" Liveness FTrue
makeImplicitProperty net ProperTermination =
Philipp Meyer's avatar
Philipp Meyer committed
257
        let (finals, nonfinals) = partition (null . lpost net) (places net)
258
        in  Property "proper termination" Safety
Philipp Meyer's avatar
Philipp Meyer committed
259
260
            (foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) finals) :&:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals))
261
262
makeImplicitProperty net DeadlockFree =
        Property "deadlock-free" Safety $
263
264
265
            foldl (:&:) FTrue
                (map (foldl (:|:) FFalse . map (placeOp Lt) . lpre net)
                     (transitions net))
266
267
makeImplicitProperty net DeadlockFreeUnlessFinal =
        let nodeadlock = makeImplicitProperty net DeadlockFree
268
            (finals, nonfinals) = partition (null . lpost net) (places net)
269
        in  Property "deadlock-free unless final" Safety $
Philipp Meyer's avatar
Philipp Meyer committed
270
271
272
            (foldl (:&:) FTrue  (map (\p -> placeOp Eq (p,0)) finals) :|:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals)) :&:
            pformula nodeadlock
273
makeImplicitProperty net (Bounded k) =
274
        Property (show k ++ "-bounded") Safety $
275
276
            foldl (:|:) FFalse
                (map (\p -> placeOp Gt (p,k)) (places net))
277
278
279
makeImplicitProperty net Safe =
        let bounded = makeImplicitProperty net (Bounded 1)
        in  Property "safe" Safety $ pformula bounded
280

281
282
283
checkProperty :: Int -> PetriNet -> Bool -> Property -> IO Bool
checkProperty verbosity net refine p = do
        verbosePut verbosity 1 $ "\nChecking " ++ showPropertyName p
284
        verbosePut verbosity 3 $ show p
285
        r <- case ptype p of
286
287
288
            Safety -> checkSafetyProperty verbosity net refine (pformula p) []
            Liveness -> checkLivenessProperty verbosity net refine (pformula p) []
        verbosePut verbosity 0 $ showPropertyName p ++
289
                                    if r then " is satisfied."
290
                                    else " may not be satisfied."
291
292
        return r

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

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

350
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
351
main = do
352
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
353
354
355
356
357
358
359
360
        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")
361
362
                let verbosity = optVerbosity opts
                    refinement = optRefine opts
363
364
                let parser = case inputFormat opts of
                                 PNET -> PNET.parseContent
Philipp Meyer's avatar
Philipp Meyer committed
365
                                 LOLA -> LOLA.parseContent
366
                                 TPN -> TPN.parseContent
367
                                 MIST -> MIST.parseContent
368
369
370
                let properties = reverse $ optProperties opts
                let transformations = reverse $ optTransformations opts
                rs <- mapM (checkFile parser verbosity refinement properties
371
372
                     transformations (optUseProperties opts) (optOutput opts))
                     files
373
374
375
376
377
378
379
380
381
382
383
384
385
                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
386
        exitWith $ ExitFailure 2
Philipp Meyer's avatar
Philipp Meyer committed
387

388
389
390
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
391
        exitWith $ ExitFailure 3