Main.hs 18.1 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
                       , optPrintStructure :: Bool
52
53
54
55
                       }

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

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

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

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

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

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

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

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

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

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

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

141
142
143
144
        , Option "n" ["no-refinement"]
        (NoArg (\opt -> Right opt { optRefine = False }))
        "Don't use refinement"

145
146
147
148
149
150
151
        , Option "o" ["output"]
        (ReqArg (\arg opt -> Right opt {
                        optOutput = Just arg
                })
                "FILE")
        "Write net and properties to FILE"

152
153
154
155
156
157
        , Option "" ["no-given-properties"]
        (NoArg (\opt -> Right opt {
                   optUseProperties = False
               }))
        "Do not use the properties given in the input file"

158
        , Option "v" ["verbose"]
159
160
161
162
163
164
        (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)"
165
166
167
168
169
170
171
172
173
174

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

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

175
176
177
178
verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
        when (verbosity >= level) (putStrLn str)

179
180
181
182
183
184
185
186
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

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

201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
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)
        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)

220
checkFile :: Parser (PetriNet,[Property]) -> Int -> Bool ->
221
            [ImplicitProperty] -> [NetTransformation] ->
222
            Bool -> Maybe String -> Bool -> String -> IO Bool
223
checkFile parser verbosity refine implicitProperties transformations
224
          useProperties output printStruct file = do
225
        verbosePut verbosity 0 $ "Reading \"" ++ file ++ "\""
226
        (net,props) <- parseFile parser file
227
228
229
        let props' = if useProperties then props else []
        let props'' = props' ++ map (makeImplicitProperty net) implicitProperties
        let (net',props''') = foldl transformNet (net,props'') transformations
230
231
232
233
        verbosePut verbosity 1 $ "Analyzing " ++ showNetName net
        verbosePut verbosity 2 $
                "Places: " ++ show (length  $ places net') ++ "; " ++
                "Transitions: " ++ show (length $ transitions net')
234
        when printStruct $ structuralAnalysis net
235
        verbosePut verbosity 3 $ show net'
236
        case output of
237
            Just outputfile -> writeFiles verbosity outputfile net' props'''
238
            Nothing -> return ()
239
        rs <- mapM (checkProperty verbosity net' refine) props'''
240
        verbosePut verbosity 0 ""
241
242
        return $ and rs

243
placeOp :: Op -> (String, Integer) -> Formula
244
placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w)
245

246
247
transformNet :: (PetriNet, [Property]) -> NetTransformation ->
               (PetriNet, [Property])
248
transformNet (net, props) TerminationByReachability =
249
250
251
252
        let prime = ('\'':)
            ps = ["'sigma", "'m1", "'m2"] ++
                 places net ++ map prime (places net)
            is = [("'m1", 1)] ++
253
                 initials net ++ map (first prime) (initials net)
254
255
256
257
258
259
260
261
262
263
            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'')]
264
            ts = ("'switch", [("'m1",1)], [("'m2",1)]) :
265
266
                 concatMap transformTransition (transitions net)
            gs = ghostTransitions net
267
268
            prop = Property "termination by reachability" Safety $
                    foldl (:&:) (Atom (LinIneq (Var "'sigma") Ge (Const 1)))
269
270
                      (map (\p -> Atom (LinIneq
                                (Var (prime p) :-: Var p) Ge (Const 0)))
271
                        (places net))
272
            -- TODO: map existing liveness properties
273
        in  (makePetriNetWithTrans (name net) ps ts is gs, prop : props)
274
transformNet (net, props) ValidateIdentifiers =
275
276
277
278
        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
279
280
            gs = map validateId $ ghostTransitions net
            net' = makePetriNet (name net) ps ts as is gs
281
            props' = map (rename validateId) props
282
        in  (net', props')
283

284
makeImplicitProperty :: PetriNet -> ImplicitProperty -> Property
285
286
287
288
289
makeImplicitProperty net Termination =
        Property "termination" Liveness $
            foldl (:&:) FTrue
                (map (\t -> Atom (LinIneq (Var t) Eq (Const 0)))
                    (ghostTransitions net))
290
makeImplicitProperty net ProperTermination =
Philipp Meyer's avatar
Philipp Meyer committed
291
        let (finals, nonfinals) = partition (null . lpost net) (places net)
292
        in  Property "proper termination" Safety
Philipp Meyer's avatar
Philipp Meyer committed
293
294
            (foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) finals) :&:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals))
295
296
makeImplicitProperty net DeadlockFree =
        Property "deadlock-free" Safety $
297
298
            foldl (:&:) FTrue
                (map (foldl (:|:) FFalse . map (placeOp Lt) . lpre net)
299
                     (filter (`notElem` ghostTransitions net) (transitions net)))
300
301
makeImplicitProperty net DeadlockFreeUnlessFinal =
        let nodeadlock = makeImplicitProperty net DeadlockFree
302
            (finals, nonfinals) = partition (null . lpost net) (places net)
303
        in  Property "deadlock-free unless final" Safety $
Philipp Meyer's avatar
Philipp Meyer committed
304
305
306
            (foldl (:&:) FTrue  (map (\p -> placeOp Eq (p,0)) finals) :|:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals)) :&:
            pformula nodeadlock
307
makeImplicitProperty net (Bounded k) =
308
        Property (show k ++ "-bounded") Safety $
309
            foldl (:|:) FFalse
310
311
312
                (map (\p -> placeOp Gt (p,k))
                    (filter (`notElem` concatMap (post net) (ghostTransitions net))
                        (places net)))
313
314
315
makeImplicitProperty net Safe =
        let bounded = makeImplicitProperty net (Bounded 1)
        in  Property "safe" Safety $ pformula bounded
316

317
318
319
checkProperty :: Int -> PetriNet -> Bool -> Property -> IO Bool
checkProperty verbosity net refine p = do
        verbosePut verbosity 1 $ "\nChecking " ++ showPropertyName p
320
        verbosePut verbosity 3 $ show p
321
        r <- case ptype p of
322
323
324
            Safety -> checkSafetyProperty verbosity net refine (pformula p) []
            Liveness -> checkLivenessProperty verbosity net refine (pformula p) []
        verbosePut verbosity 0 $ showPropertyName p ++
325
                                    if r then " is satisfied."
326
                                    else " may not be satisfied."
327
328
        return r

329
checkSafetyProperty :: Int -> PetriNet -> Bool ->
330
        Formula -> [[String]] -> IO Bool
331
checkSafetyProperty verbosity net refine f traps = do
332
333
334
335
336
        r <- checkSat $ checkStateEquationSat net f traps
        case r of
            Nothing -> return True
            Just a -> do
                let assigned = markedPlacesFromAssignment net a
337
338
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Places marked: " ++ show assigned
339
                verbosePut verbosity 3 $ "Assignment: " ++ show a
340
341
342
343
                if refine then do
                    rt <- checkSat $ checkTrapSat net assigned
                    case rt of
                        Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
344
                            verbosePut verbosity 1 "No trap found."
345
346
347
                            return False
                        Just at -> do
                            let trap = trapFromAssignment at
348
349
350
                            verbosePut verbosity 1 "Trap found"
                            verbosePut verbosity 2 $ "Places in trap: " ++
                                                      show trap
351
352
                            verbosePut verbosity 3 $ "Trap assignment: " ++
                                                      show at
353
                            checkSafetyProperty verbosity net refine f
354
355
356
357
                                                (trap:traps)
                else
                    return False

358
checkLivenessProperty :: Int -> PetriNet -> Bool ->
359
        Formula -> [([String],[String])] -> IO Bool
360
checkLivenessProperty verbosity net refine f strans = do
361
        r <- checkSat $ checkTransitionInvariantSat net f strans
Philipp Meyer's avatar
Philipp Meyer committed
362
        case r of
363
            Nothing -> return True
364
365
            Just ax -> do
                let fired = firedTransitionsFromAssignment ax
366
367
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Transitions fired: " ++ show fired
368
                verbosePut verbosity 3 $ "Assignment: " ++ show ax
369
370
371
372
                if refine then do
                    rt <- checkSat $ checkSComponentSat net fired ax
                    case rt of
                        Nothing -> do
373
                            verbosePut verbosity 1 "No S-component found"
374
375
376
                            return False
                        Just as -> do
                            let sOutIn = getSComponentOutIn net ax as
377
378
                            verbosePut verbosity 1 "S-component found"
                            verbosePut verbosity 2 $ "Out/In: " ++ show sOutIn
379
380
                            verbosePut verbosity 3 $ "S-Component assignment: " ++
                                                      show as
381
                            checkLivenessProperty verbosity net refine f
382
383
384
                                                  (sOutIn:strans)
                else
                    return False
385

386
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
387
main = do
388
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
389
390
391
392
393
394
395
396
        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")
397
398
                let verbosity = optVerbosity opts
                    refinement = optRefine opts
399
400
                let parser = case inputFormat opts of
                                 PNET -> PNET.parseContent
Philipp Meyer's avatar
Philipp Meyer committed
401
                                 LOLA -> LOLA.parseContent
402
                                 TPN -> TPN.parseContent
403
                                 MIST -> MIST.parseContent
404
405
406
                let properties = reverse $ optProperties opts
                let transformations = reverse $ optTransformations opts
                rs <- mapM (checkFile parser verbosity refinement properties
407
408
                     transformations (optUseProperties opts) (optOutput opts)
                     (optPrintStructure opts)) files
409
410
411
412
413
414
415
416
417
418
419
420
421
                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
422
        exitWith $ ExitFailure 2
Philipp Meyer's avatar
Philipp Meyer committed
423

424
425
426
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
427
        exitWith $ ExitFailure 3