Main.hs 14.5 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 ((<$>))
Philipp Meyer's avatar
Philipp Meyer committed
11
import Data.List (partition)
Philipp Meyer's avatar
Philipp Meyer committed
12

13
14
import Parser
import qualified Parser.PNET as PNET
Philipp Meyer's avatar
Philipp Meyer committed
15
import qualified Parser.LOLA as LOLA
16
import qualified Parser.TPN as TPN
17
import PetriNet
18
import Printer
19
import Property
20
import Solver
21
22
import Solver.StateEquation
import Solver.TrapConstraints
23
24
import Solver.TransitionInvariant
import Solver.SComponent
25

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

28
29
data NetTransformation = TerminationToReachability

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

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

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

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

71
        , Option "" ["termination-by-reachability"]
72
73
74
        (NoArg (\opt -> Right opt {
            optTransformations = TerminationToReachability : optTransformations opt
          }))
75
        "Prove termination by reducing it to reachability"
76

77
        , Option "" ["terminating"]
78
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
79
                   optProperties = Termination : optProperties opt
80
               }))
81
        "Prove that the net is terminating"
82

Philipp Meyer's avatar
Philipp Meyer committed
83
84
85
86
87
88
        , Option "" ["proper-termination"]
        (NoArg (\opt -> Right opt {
                   optProperties = ProperTermination : optProperties opt
               }))
        "Prove termination in the final marking"

89
        , Option "" ["deadlock-free"]
90
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
91
                   optProperties = NoDeadlock : optProperties opt
92
               }))
93
        "Prove that the net is deadlock-free"
94

95
        , Option "" ["deadlock-free-unless-final"]
Philipp Meyer's avatar
Philipp Meyer committed
96
97
98
        (NoArg (\opt -> Right opt {
                   optProperties = NoDeadlockUnlessFinal : optProperties opt
               }))
99
100
        ("Prove that the net is deadlock-free\n" ++
         "unless it is in the final marking")
Philipp Meyer's avatar
Philipp Meyer committed
101

102
103
        , Option "" ["safe"]
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
104
                   optProperties = Safe : optProperties opt
105
106
107
108
109
110
111
112
113
114
115
116
               }))
        "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"

117
118
119
120
        , Option "n" ["no-refinement"]
        (NoArg (\opt -> Right opt { optRefine = False }))
        "Don't use refinement"

121
122
123
124
125
126
127
        , Option "o" ["output"]
        (ReqArg (\arg opt -> Right opt {
                        optOutput = Just arg
                })
                "FILE")
        "Write net and properties to FILE"

128
        , Option "v" ["verbose"]
129
130
131
132
133
134
        (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)"
135
136
137
138
139
140
141
142
143
144

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

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

145
146
147
148
verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
        when (verbosity >= level) (putStrLn str)

149
150
151
152
153
154
155
156
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

157
158
159
160
161
162
163
164
165
166
167
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)..])

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

189
placeOp :: Op -> (String, Integer) -> Formula
190
placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w)
191

192
193
transformNet :: (PetriNet, [Property]) -> NetTransformation ->
               (PetriNet, [Property])
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
transformNet (net, props) TerminationToReachability =
        let prime = ('\'':)
            primeFst (p,x) = (prime p, x)
            ps = ["'sigma", "'m1", "'m2"] ++
                 places net ++ map prime (places net)
            is = [("'m1", 1)] ++
                 initials net ++ map primeFst (initials net)
            ts = ("'switch", [("'m1",1)], [("'m2",1)]) :
                 concatMap (\t ->
                    let (preT, postT) = context net t
                        pre'  = [("'m1",1)] ++ preT  ++ map primeFst preT
                        post' = [("'m1",1)] ++ postT ++ map primeFst postT
                        pre''  = ("'m2",1) : map primeFst preT
                        post'' = [("'m2",1), ("'sigma",1)] ++ map primeFst postT
                    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))
        in  (makePetriNetWithTrans (name net) ps ts is, prop : props)
216

217
makeImplicitProperty :: PetriNet -> ImplicitProperty -> Property
218
makeImplicitProperty _ Termination =
219
220
        Property "termination" Liveness FTrue
makeImplicitProperty net ProperTermination =
Philipp Meyer's avatar
Philipp Meyer committed
221
        let (finals, nonfinals) = partition (null . lpost net) (places net)
222
        in  Property "proper termination" Safety
Philipp Meyer's avatar
Philipp Meyer committed
223
224
            (foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) finals) :&:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals))
225
makeImplicitProperty net NoDeadlock =
226
        Property "no deadlock" Safety $
227
228
229
            foldl (:&:) FTrue
                (map (foldl (:|:) FFalse . map (placeOp Lt) . lpre net)
                     (transitions net))
230
231
232
233
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
234
235
236
            (foldl (:&:) FTrue  (map (\p -> placeOp Eq (p,0)) finals) :|:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals)) :&:
            pformula nodeadlock
237
makeImplicitProperty net (Bounded k) =
238
        Property (show k ++ "-bounded") Safety $
239
240
            foldl (:|:) FFalse
                (map (\p -> placeOp Gt (p,k)) (places net))
241
242
243
makeImplicitProperty net Safe =
        let bounded = makeImplicitProperty net (Bounded 1)
        in  Property "safe" Safety $ pformula bounded
244

245
246
247
checkProperty :: Int -> PetriNet -> Bool -> Property -> IO Bool
checkProperty verbosity net refine p = do
        verbosePut verbosity 1 $ "\nChecking " ++ showPropertyName p
248
        verbosePut verbosity 3 $ show p
249
        r <- case ptype p of
250
251
252
            Safety -> checkSafetyProperty verbosity net refine (pformula p) []
            Liveness -> checkLivenessProperty verbosity net refine (pformula p) []
        verbosePut verbosity 0 $ showPropertyName p ++
253
                                    if r then " is satisfied."
254
                                    else " may not be satisfied."
255
256
        return r

257
checkSafetyProperty :: Int -> PetriNet -> Bool ->
258
        Formula -> [[String]] -> IO Bool
259
checkSafetyProperty verbosity net refine f traps = do
260
261
262
263
264
        r <- checkSat $ checkStateEquationSat net f traps
        case r of
            Nothing -> return True
            Just a -> do
                let assigned = markedPlacesFromAssignment net a
265
266
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Places marked: " ++ show assigned
267
                verbosePut verbosity 3 $ "Assignment: " ++ show a
268
269
270
271
272
273
274
275
                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
276
277
278
                            verbosePut verbosity 1 "Trap found"
                            verbosePut verbosity 2 $ "Places in trap: " ++
                                                      show trap
279
280
                            verbosePut verbosity 3 $ "Trap assignment: " ++
                                                      show at
281
                            checkSafetyProperty verbosity net refine f
282
283
284
285
                                                (trap:traps)
                else
                    return False

286
checkLivenessProperty :: Int -> PetriNet -> Bool ->
287
        Formula -> [([String],[String])] -> IO Bool
288
checkLivenessProperty verbosity net refine f strans = do
289
        r <- checkSat $ checkTransitionInvariantSat net f strans
Philipp Meyer's avatar
Philipp Meyer committed
290
        case r of
291
            Nothing -> return True
292
293
            Just ax -> do
                let fired = firedTransitionsFromAssignment ax
294
295
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Transitions fired: " ++ show fired
296
                verbosePut verbosity 3 $ "Assignment: " ++ show ax
297
298
299
300
                if refine then do
                    rt <- checkSat $ checkSComponentSat net fired ax
                    case rt of
                        Nothing -> do
301
                            verbosePut verbosity 1 "No S-component found"
302
303
304
                            return False
                        Just as -> do
                            let sOutIn = getSComponentOutIn net ax as
305
306
                            verbosePut verbosity 1 "S-component found"
                            verbosePut verbosity 2 $ "Out/In: " ++ show sOutIn
307
308
                            verbosePut verbosity 3 $ "S-Component assignment: " ++
                                                      show as
309
                            checkLivenessProperty verbosity net refine f
310
311
312
                                                  (sOutIn:strans)
                else
                    return False
313

314
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
315
main = do
316
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
317
318
319
320
321
322
323
324
        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")
325
326
                let verbosity = optVerbosity opts
                    refinement = optRefine opts
327
328
                let parser = case inputFormat opts of
                                 PNET -> PNET.parseContent
Philipp Meyer's avatar
Philipp Meyer committed
329
                                 LOLA -> LOLA.parseContent
330
                                 TPN -> TPN.parseContent
331
332
333
                let properties = reverse $ optProperties opts
                let transformations = reverse $ optTransformations opts
                rs <- mapM (checkFile parser verbosity refinement properties
334
                                transformations (optOutput opts)) files
335
336
337
338
339
340
341
342
343
344
345
346
347
                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
348
        exitWith $ ExitFailure 2
Philipp Meyer's avatar
Philipp Meyer committed
349

350
351
352
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
353
        exitWith $ ExitFailure 3