Main.hs 15.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 ((<$>))
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
21
import qualified Printer.LOLA as LOLAPrinter
import qualified Printer.SARA as SARAPrinter
22
import Property
23
import Solver
24
25
import Solver.StateEquation
import Solver.TrapConstraints
26
27
import Solver.TransitionInvariant
import Solver.SComponent
28

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

31
32
data NetTransformation = TerminationByReachability
                       | ValidateIdentifiers
33

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

159
160
161
162
163
164
165
166
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

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

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

202
placeOp :: Op -> (String, Integer) -> Formula
203
placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w)
204

205
206
transformNet :: (PetriNet, [Property]) -> NetTransformation ->
               (PetriNet, [Property])
207
transformNet (net, props) TerminationByReachability =
208
209
210
211
        let prime = ('\'':)
            ps = ["'sigma", "'m1", "'m2"] ++
                 places net ++ map prime (places net)
            is = [("'m1", 1)] ++
212
                 initials net ++ map (first prime) (initials net)
213
214
215
            ts = ("'switch", [("'m1",1)], [("'m2",1)]) :
                 concatMap (\t ->
                    let (preT, postT) = context net t
216
217
218
219
                        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
220
221
222
223
224
225
226
                    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))
227
            -- TODO: map existing liveness properties
228
        in  (makePetriNetWithTrans (name net) ps ts is, prop : props)
229
transformNet (net, props) ValidateIdentifiers =
230
231
232
233
        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
234
            net' = makePetriNet (name net) ps ts as is
235
            props' = map (rename validateId) props
236
        in  (net', props')
237

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

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

278
checkSafetyProperty :: Int -> PetriNet -> Bool ->
279
        Formula -> [[String]] -> IO Bool
280
checkSafetyProperty verbosity net refine f traps = do
281
282
283
284
285
        r <- checkSat $ checkStateEquationSat net f traps
        case r of
            Nothing -> return True
            Just a -> do
                let assigned = markedPlacesFromAssignment net a
286
287
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Places marked: " ++ show assigned
288
                verbosePut verbosity 3 $ "Assignment: " ++ show a
289
290
291
292
293
294
295
296
                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
297
298
299
                            verbosePut verbosity 1 "Trap found"
                            verbosePut verbosity 2 $ "Places in trap: " ++
                                                      show trap
300
301
                            verbosePut verbosity 3 $ "Trap assignment: " ++
                                                      show at
302
                            checkSafetyProperty verbosity net refine f
303
304
305
306
                                                (trap:traps)
                else
                    return False

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

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

371
372
373
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
374
        exitWith $ ExitFailure 3