Main.hs 18.9 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
Philipp Meyer's avatar
Philipp Meyer committed
24
import qualified Printer.SPEC as SPECPrinter
25
import Property
26
import Solver
27
28
import Solver.StateEquation
import Solver.TrapConstraints
29
30
import Solver.TransitionInvariant
import Solver.SComponent
31

32
data InputFormat = PNET | LOLA | TPN | MIST deriving (Show,Read)
33

34
35
data NetTransformation = TerminationByReachability
                       | ValidateIdentifiers
36

37
data ImplicitProperty = Termination
38
                      | DeadlockFree | DeadlockFreeUnlessFinal
Philipp Meyer's avatar
Philipp Meyer committed
39
                      | ProperTermination
40
41
42
                      | Safe | Bounded Integer
                      deriving (Show,Read)

43
data Options = Options { inputFormat :: InputFormat
44
                       , optVerbosity :: Int
45
46
                       , optShowHelp :: Bool
                       , optShowVersion :: Bool
47
                       , optProperties :: [ImplicitProperty]
48
                       , optTransformations :: [NetTransformation]
49
                       , optRefine :: Bool
50
                       , optOutput :: Maybe String
51
                       , optUseProperties :: Bool
52
                       , optPrintStructure :: Bool
53
54
55
56
                       }

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

188
189
writeFiles :: Int -> String -> PetriNet -> [Property] -> IO ()
writeFiles verbosity basename net props = do
190
        -- TODO: add options for different outputs
191
        verbosePut verbosity 1 $ "Writing " ++ showNetName net ++ " to " ++ basename
192
        L.writeFile basename $ LOLAPrinter.printNet net
193
194
195
196
        mapM_ (\(p,i) -> do
                let file = basename ++ ".task" ++ show i
                verbosePut verbosity 1 $ "Writing " ++ showPropertyName p ++
                                         " to " ++ file
197
                L.writeFile file $ LOLAPrinter.printProperty p
198
              ) (zip props [(1::Integer)..])
199
        verbosePut verbosity 1 $ "Writing properties to " ++ basename ++ ".sara"
200
201
        L.writeFile (basename ++ ".sara") $
            SARAPrinter.printProperties basename net props
202
203
204
205
206
207
        --mapM_ (\(p,i) -> do
        --        let file = basename ++ ".target" ++ show i
        --        verbosePut verbosity 1 $ "Writing " ++ showPropertyName p ++
        --                                 " to " ++ file
        --        L.writeFile file $ SPECPrinter.printProperty p
        --      ) (zip props [(1::Integer)..])
208

209
210
211
212
213
214
215
216
217
218
219
220
221
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)
222
223
        putStrLn $ "Places             : " ++ show (length (places net))
        putStrLn $ "Transitions        : " ++ show (length (transitions net))
224
225
226
227
228
229
        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)

230
checkFile :: Parser (PetriNet,[Property]) -> Int -> Bool ->
231
            [ImplicitProperty] -> [NetTransformation] ->
232
            Bool -> Maybe String -> Bool -> String -> IO Bool
233
checkFile parser verbosity refine implicitProperties transformations
234
          useProperties output printStruct file = do
235
        verbosePut verbosity 0 $ "Reading \"" ++ file ++ "\""
236
        (net,props) <- parseFile parser file
237
238
239
        let props' = if useProperties then props else []
        let props'' = props' ++ map (makeImplicitProperty net) implicitProperties
        let (net',props''') = foldl transformNet (net,props'') transformations
240
241
242
243
        verbosePut verbosity 1 $ "Analyzing " ++ showNetName net
        verbosePut verbosity 2 $
                "Places: " ++ show (length  $ places net') ++ "; " ++
                "Transitions: " ++ show (length $ transitions net')
244
        when printStruct $ structuralAnalysis net
245
        verbosePut verbosity 3 $ show net'
246
        case output of
247
            Just outputfile -> writeFiles verbosity outputfile net' props'''
248
            Nothing -> return ()
Philipp Meyer's avatar
Philipp Meyer committed
249
        -- TODO: short-circuit?
250
        rs <- mapM (checkProperty verbosity net' refine) props'''
251
        verbosePut verbosity 0 ""
252
253
        return $ and rs

254
placeOp :: Op -> (String, Integer) -> Formula
255
placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w)
256

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

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

328
329
330
checkProperty :: Int -> PetriNet -> Bool -> Property -> IO Bool
checkProperty verbosity net refine p = do
        verbosePut verbosity 1 $ "\nChecking " ++ showPropertyName p
331
        verbosePut verbosity 3 $ show p
332
        r <- case ptype p of
333
334
335
            Safety -> checkSafetyProperty verbosity net refine (pformula p) []
            Liveness -> checkLivenessProperty verbosity net refine (pformula p) []
        verbosePut verbosity 0 $ showPropertyName p ++
336
                                    if r then " is satisfied."
337
                                    else " may not be satisfied."
338
339
        return r

340
checkSafetyProperty :: Int -> PetriNet -> Bool ->
341
        Formula -> [[String]] -> IO Bool
342
checkSafetyProperty verbosity net refine f traps = do
343
344
345
346
347
        r <- checkSat $ checkStateEquationSat net f traps
        case r of
            Nothing -> return True
            Just a -> do
                let assigned = markedPlacesFromAssignment net a
348
349
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Places marked: " ++ show assigned
350
                verbosePut verbosity 3 $ "Assignment: " ++ show a
351
352
353
354
                if refine then do
                    rt <- checkSat $ checkTrapSat net assigned
                    case rt of
                        Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
355
                            verbosePut verbosity 1 "No trap found."
356
357
358
                            return False
                        Just at -> do
                            let trap = trapFromAssignment at
359
360
361
                            verbosePut verbosity 1 "Trap found"
                            verbosePut verbosity 2 $ "Places in trap: " ++
                                                      show trap
362
363
                            verbosePut verbosity 3 $ "Trap assignment: " ++
                                                      show at
364
                            checkSafetyProperty verbosity net refine f
365
366
367
368
                                                (trap:traps)
                else
                    return False

369
checkLivenessProperty :: Int -> PetriNet -> Bool ->
370
        Formula -> [([String],[String])] -> IO Bool
371
checkLivenessProperty verbosity net refine f strans = do
372
        r <- checkSat $ checkTransitionInvariantSat net f strans
Philipp Meyer's avatar
Philipp Meyer committed
373
        case r of
374
            Nothing -> return True
375
376
            Just ax -> do
                let fired = firedTransitionsFromAssignment ax
377
378
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Transitions fired: " ++ show fired
379
                verbosePut verbosity 3 $ "Assignment: " ++ show ax
380
381
382
383
                if refine then do
                    rt <- checkSat $ checkSComponentSat net fired ax
                    case rt of
                        Nothing -> do
384
                            verbosePut verbosity 1 "No S-component found"
385
386
387
                            return False
                        Just as -> do
                            let sOutIn = getSComponentOutIn net ax as
388
389
                            verbosePut verbosity 1 "S-component found"
                            verbosePut verbosity 2 $ "Out/In: " ++ show sOutIn
390
391
                            verbosePut verbosity 3 $ "S-Component assignment: " ++
                                                      show as
392
                            checkLivenessProperty verbosity net refine f
393
394
395
                                                  (sOutIn:strans)
                else
                    return False
396

397
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
398
main = do
399
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
400
401
402
403
404
405
406
407
        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")
408
409
                let verbosity = optVerbosity opts
                    refinement = optRefine opts
410
411
                let parser = case inputFormat opts of
                                 PNET -> PNET.parseContent
Philipp Meyer's avatar
Philipp Meyer committed
412
                                 LOLA -> LOLA.parseContent
413
                                 TPN -> TPN.parseContent
414
                                 MIST -> MIST.parseContent
415
416
417
                let properties = reverse $ optProperties opts
                let transformations = reverse $ optTransformations opts
                rs <- mapM (checkFile parser verbosity refinement properties
418
419
                     transformations (optUseProperties opts) (optOutput opts)
                     (optPrintStructure opts)) files
Philipp Meyer's avatar
Philipp Meyer committed
420
                -- TODO: short-circuit with Control.Monad.Loops?
421
422
423
424
425
                if and rs then
                    exitSuccessWith "All properties satisfied."
                else
                    exitFailureWith "Some properties may not be satisfied."

Philipp Meyer's avatar
Philipp Meyer committed
426
-- TODO: Always exit with exit code 0 unless an error occured
427
428
429
430
431
432
433
434
exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
        exitSuccess

exitFailureWith :: String -> IO ()
exitFailureWith msg = do
        putStrLn msg
435
        exitWith $ ExitFailure 2
Philipp Meyer's avatar
Philipp Meyer committed
436

437
438
439
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
440
        exitWith $ ExitFailure 3