Main.hs 15.8 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
50
51
52
                       }

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

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

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

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

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

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

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

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

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

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

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

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

143
        , Option "v" ["verbose"]
144
145
146
147
148
149
        (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)"
150
151
152
153
154
155
156
157
158
159

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

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

160
161
162
163
verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
        when (verbosity >= level) (putStrLn str)

164
165
166
167
168
169
170
171
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

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

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

207
placeOp :: Op -> (String, Integer) -> Formula
208
placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w)
209

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

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

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

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

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

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

378
379
380
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
381
        exitWith $ ExitFailure 3