Main.hs 15.3 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 PetriNet
19
import Printer
20
import Property
21
import Solver
22
23
import Solver.StateEquation
import Solver.TrapConstraints
24
25
import Solver.TransitionInvariant
import Solver.SComponent
26

27
28
data InputFormat = PNET | LOLA | TPN deriving (Show,Read)

29
30
data NetTransformation = TerminationByReachability
                       | ValidateIdentifiers
31

32
data ImplicitProperty = Termination
33
                      | NoDeadlock | NoDeadlockUnlessFinal
Philipp Meyer's avatar
Philipp Meyer committed
34
                      | ProperTermination
35
36
37
                      | Safe | Bounded Integer
                      deriving (Show,Read)

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

startOptions :: Options
startOptions = Options { inputFormat = PNET
50
                       , optVerbosity = 1
51
52
                       , optShowHelp = False
                       , optShowVersion = False
53
                       , optProperties = []
54
                       , optTransformations = []
55
                       , optRefine = True
56
                       , optOutput = Nothing
57
58
59
60
                       }

options :: [ OptDescr (Options -> Either String Options) ]
options =
61
62
63
64
65
66
67
68
69
70
71
        [ 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"
72

73
74
75
76
77
78
        , Option "" ["validate-identifiers"]
        (NoArg (\opt -> Right opt {
            optTransformations = ValidateIdentifiers : optTransformations opt
          }))
        "Make identifiers valid for lola"

79
        , Option "" ["termination-by-reachability"]
80
        (NoArg (\opt -> Right opt {
81
            optTransformations = TerminationByReachability : optTransformations opt
82
          }))
83
        "Prove termination by reducing it to reachability"
84

85
        , Option "" ["terminating"]
86
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
87
                   optProperties = Termination : optProperties opt
88
               }))
89
        "Prove that the net is terminating"
90

Philipp Meyer's avatar
Philipp Meyer committed
91
92
93
94
95
96
        , Option "" ["proper-termination"]
        (NoArg (\opt -> Right opt {
                   optProperties = ProperTermination : optProperties opt
               }))
        "Prove termination in the final marking"

97
        , Option "" ["deadlock-free"]
98
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
99
                   optProperties = NoDeadlock : optProperties opt
100
               }))
101
        "Prove that the net is deadlock-free"
102

103
        , Option "" ["deadlock-free-unless-final"]
Philipp Meyer's avatar
Philipp Meyer committed
104
105
106
        (NoArg (\opt -> Right opt {
                   optProperties = NoDeadlockUnlessFinal : optProperties opt
               }))
107
108
        ("Prove that the net is deadlock-free\n" ++
         "unless it is in the final marking")
Philipp Meyer's avatar
Philipp Meyer committed
109

110
111
        , Option "" ["safe"]
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
112
                   optProperties = Safe : optProperties opt
113
114
115
116
117
118
119
120
121
122
123
124
               }))
        "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"

125
126
127
128
        , Option "n" ["no-refinement"]
        (NoArg (\opt -> Right opt { optRefine = False }))
        "Don't use refinement"

129
130
131
132
133
134
135
        , Option "o" ["output"]
        (ReqArg (\arg opt -> Right opt {
                        optOutput = Just arg
                })
                "FILE")
        "Write net and properties to FILE"

136
        , Option "v" ["verbose"]
137
138
139
140
141
142
        (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)"
143
144
145
146
147
148
149
150
151
152

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

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

153
154
155
156
verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
        when (verbosity >= level) (putStrLn str)

157
158
159
160
161
162
163
164
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

165
166
167
168
169
170
171
172
173
174
175
writeFiles :: Int -> String -> PetriNet -> [Property] -> IO ()
writeFiles verbosity basename net props = do
        verbosePut verbosity 1 $ "Writing " ++ showNetName net ++ " to " ++ basename
        writeFile basename $ printNet net
        mapM_ (\(p,i) -> do
                let file = basename ++ ".task" ++ show i
                verbosePut verbosity 1 $ "Writing " ++ showPropertyName p ++
                                         " to " ++ file
                writeFile file $ printProperty p
              ) (zip props [(1::Integer)..])

176
checkFile :: Parser (PetriNet,[Property]) -> Int -> Bool ->
177
178
179
180
            [ImplicitProperty] -> [NetTransformation] ->
            Maybe String -> String -> IO Bool
checkFile parser verbosity refine implicitProperties transformations
          output file = do
181
        verbosePut verbosity 0 $ "Reading \"" ++ file ++ "\""
182
183
184
        (net,props) <- parseFile parser file
        let props' = props ++ map (makeImplicitProperty net) implicitProperties
        let (net',props'') = foldl transformNet (net,props') transformations
185
186
187
188
189
        verbosePut verbosity 1 $ "Analyzing " ++ showNetName net
        verbosePut verbosity 2 $
                "Places: " ++ show (length  $ places net') ++ "; " ++
                "Transitions: " ++ show (length $ transitions net')
        verbosePut verbosity 3 $ show net'
190
        rs <- mapM (checkProperty verbosity net' refine) props''
191
192
193
        case output of
            Just outputfile -> writeFiles verbosity outputfile net' props''
            Nothing -> return ()
194
        verbosePut verbosity 0 ""
195
196
        return $ and rs

197
placeOp :: Op -> (String, Integer) -> Formula
198
placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w)
199

200
201
transformNet :: (PetriNet, [Property]) -> NetTransformation ->
               (PetriNet, [Property])
202
transformNet (net, props) TerminationByReachability =
203
204
205
206
        let prime = ('\'':)
            ps = ["'sigma", "'m1", "'m2"] ++
                 places net ++ map prime (places net)
            is = [("'m1", 1)] ++
207
                 initials net ++ map (first prime) (initials net)
208
209
210
            ts = ("'switch", [("'m1",1)], [("'m2",1)]) :
                 concatMap (\t ->
                    let (preT, postT) = context net t
211
212
213
214
                        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
215
216
217
218
219
220
221
                    in  [(t, pre', post'), (prime t, pre'', post'')]
                 )
                 (transitions net)
            prop = Property "termination by reachability" Safety $
                    foldl (:&:) (Atom (LinIneq (Var "'sigma") Ge (Const 1)))
                      (map (\p -> Atom (LinIneq (Var (prime p)) Ge (Var p)))
                        (places net))
222
            -- TODO: map existing liveness properties
223
        in  (makePetriNetWithTrans (name net) ps ts is, prop : props)
224
225
226
227
228
229
230
231
232
transformNet (net, props) ValidateIdentifiers =
        let validate = map (\c -> if c `elem` ",;:(){}\t \n\r" then '_' else c)
            ps = map validate $ places net
            ts = map validate $ transitions net
            is = map (first validate) $ initials net
            as = map (\(a,b,x) -> (validate a, validate b, x)) $ arcs net
            net' = makePetriNet (name net) ps ts as is
            props' = map (rename validate) props
        in  (net', props')
233

234
makeImplicitProperty :: PetriNet -> ImplicitProperty -> Property
235
makeImplicitProperty _ Termination =
236
237
        Property "termination" Liveness FTrue
makeImplicitProperty net ProperTermination =
Philipp Meyer's avatar
Philipp Meyer committed
238
        let (finals, nonfinals) = partition (null . lpost net) (places net)
239
        in  Property "proper termination" Safety
Philipp Meyer's avatar
Philipp Meyer committed
240
241
            (foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) finals) :&:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals))
242
makeImplicitProperty net NoDeadlock =
243
        Property "no deadlock" Safety $
244
245
246
            foldl (:&:) FTrue
                (map (foldl (:|:) FFalse . map (placeOp Lt) . lpre net)
                     (transitions net))
247
248
249
250
makeImplicitProperty net NoDeadlockUnlessFinal =
        let nodeadlock = makeImplicitProperty net NoDeadlock
            (finals, nonfinals) = partition (null . lpost net) (places net)
        in  Property "no deadlock unless final" Safety $
Philipp Meyer's avatar
Philipp Meyer committed
251
252
253
            (foldl (:&:) FTrue  (map (\p -> placeOp Eq (p,0)) finals) :|:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals)) :&:
            pformula nodeadlock
254
makeImplicitProperty net (Bounded k) =
255
        Property (show k ++ "-bounded") Safety $
256
257
            foldl (:|:) FFalse
                (map (\p -> placeOp Gt (p,k)) (places net))
258
259
260
makeImplicitProperty net Safe =
        let bounded = makeImplicitProperty net (Bounded 1)
        in  Property "safe" Safety $ pformula bounded
261

262
263
264
checkProperty :: Int -> PetriNet -> Bool -> Property -> IO Bool
checkProperty verbosity net refine p = do
        verbosePut verbosity 1 $ "\nChecking " ++ showPropertyName p
265
        verbosePut verbosity 3 $ show p
266
        r <- case ptype p of
267
268
269
            Safety -> checkSafetyProperty verbosity net refine (pformula p) []
            Liveness -> checkLivenessProperty verbosity net refine (pformula p) []
        verbosePut verbosity 0 $ showPropertyName p ++
270
                                    if r then " is satisfied."
271
                                    else " may not be satisfied."
272
273
        return r

274
checkSafetyProperty :: Int -> PetriNet -> Bool ->
275
        Formula -> [[String]] -> IO Bool
276
checkSafetyProperty verbosity net refine f traps = do
277
278
279
280
281
        r <- checkSat $ checkStateEquationSat net f traps
        case r of
            Nothing -> return True
            Just a -> do
                let assigned = markedPlacesFromAssignment net a
282
283
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Places marked: " ++ show assigned
284
                verbosePut verbosity 3 $ "Assignment: " ++ show a
285
286
287
288
289
290
291
292
                if refine then do
                    rt <- checkSat $ checkTrapSat net assigned
                    case rt of
                        Nothing -> do
                            putStrLn "No trap found."
                            return False
                        Just at -> do
                            let trap = trapFromAssignment at
293
294
295
                            verbosePut verbosity 1 "Trap found"
                            verbosePut verbosity 2 $ "Places in trap: " ++
                                                      show trap
296
297
                            verbosePut verbosity 3 $ "Trap assignment: " ++
                                                      show at
298
                            checkSafetyProperty verbosity net refine f
299
300
301
302
                                                (trap:traps)
                else
                    return False

303
checkLivenessProperty :: Int -> PetriNet -> Bool ->
304
        Formula -> [([String],[String])] -> IO Bool
305
checkLivenessProperty verbosity net refine f strans = do
306
        r <- checkSat $ checkTransitionInvariantSat net f strans
Philipp Meyer's avatar
Philipp Meyer committed
307
        case r of
308
            Nothing -> return True
309
310
            Just ax -> do
                let fired = firedTransitionsFromAssignment ax
311
312
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Transitions fired: " ++ show fired
313
                verbosePut verbosity 3 $ "Assignment: " ++ show ax
314
315
316
317
                if refine then do
                    rt <- checkSat $ checkSComponentSat net fired ax
                    case rt of
                        Nothing -> do
318
                            verbosePut verbosity 1 "No S-component found"
319
320
321
                            return False
                        Just as -> do
                            let sOutIn = getSComponentOutIn net ax as
322
323
                            verbosePut verbosity 1 "S-component found"
                            verbosePut verbosity 2 $ "Out/In: " ++ show sOutIn
324
325
                            verbosePut verbosity 3 $ "S-Component assignment: " ++
                                                      show as
326
                            checkLivenessProperty verbosity net refine f
327
328
329
                                                  (sOutIn:strans)
                else
                    return False
330

331
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
332
main = do
333
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
334
335
336
337
338
339
340
341
        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")
342
343
                let verbosity = optVerbosity opts
                    refinement = optRefine opts
344
345
                let parser = case inputFormat opts of
                                 PNET -> PNET.parseContent
Philipp Meyer's avatar
Philipp Meyer committed
346
                                 LOLA -> LOLA.parseContent
347
                                 TPN -> TPN.parseContent
348
349
350
                let properties = reverse $ optProperties opts
                let transformations = reverse $ optTransformations opts
                rs <- mapM (checkFile parser verbosity refinement properties
351
                                transformations (optOutput opts)) files
352
353
354
355
356
357
358
359
360
361
362
363
364
                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
365
        exitWith $ ExitFailure 2
Philipp Meyer's avatar
Philipp Meyer committed
366

367
368
369
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
370
        exitWith $ ExitFailure 3