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

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

27
28
data NetTransformation = TerminationToReachability

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

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

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

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

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

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

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

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

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

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

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

118
        , Option "v" ["verbose"]
119
120
121
122
123
124
        (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)"
125
126
127
128
129
130
131
132
133
134

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

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

135
136
137
138
verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
        when (verbosity >= level) (putStrLn str)

139
140
141
142
143
144
145
146
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

147
checkFile :: Parser (PetriNet,[Property]) -> Int -> Bool ->
148
149
            [ImplicitProperty] -> [NetTransformation] -> String -> IO Bool
checkFile parser verbosity refine implicitProperties transformations file = do
150
        verbosePut verbosity 0 $ "Reading \"" ++ file ++ "\""
151
152
153
        (net,props) <- parseFile parser file
        let props' = props ++ map (makeImplicitProperty net) implicitProperties
        let (net',props'') = foldl transformNet (net,props') transformations
154
155
156
157
158
        verbosePut verbosity 1 $ "Analyzing " ++ showNetName net
        verbosePut verbosity 2 $
                "Places: " ++ show (length  $ places net') ++ "; " ++
                "Transitions: " ++ show (length $ transitions net')
        verbosePut verbosity 3 $ show net'
159
        rs <- mapM (checkProperty verbosity net' refine) props''
160
        verbosePut verbosity 0 ""
161
162
        return $ and rs

163
placeOp :: Op -> (String, Integer) -> Formula
164
placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w)
165

166
167
transformNet :: (PetriNet, [Property]) -> NetTransformation ->
               (PetriNet, [Property])
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
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)
190

191
makeImplicitProperty :: PetriNet -> ImplicitProperty -> Property
192
makeImplicitProperty _ Termination =
193
194
        Property "termination" Liveness FTrue
makeImplicitProperty net ProperTermination =
Philipp Meyer's avatar
Philipp Meyer committed
195
        let (finals, nonfinals) = partition (null . lpost net) (places net)
196
        in  Property "proper termination" Safety
Philipp Meyer's avatar
Philipp Meyer committed
197
198
            (foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) finals) :&:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals))
199
makeImplicitProperty net NoDeadlock =
200
        Property "no deadlock" Safety $
201
202
203
            foldl (:&:) FTrue
                (map (foldl (:|:) FFalse . map (placeOp Lt) . lpre net)
                     (transitions net))
204
205
206
207
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
208
209
210
            (foldl (:&:) FTrue  (map (\p -> placeOp Eq (p,0)) finals) :|:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals)) :&:
            pformula nodeadlock
211
makeImplicitProperty net (Bounded k) =
212
        Property (show k ++ "-bounded") Safety $
213
214
            foldl (:|:) FFalse
                (map (\p -> placeOp Gt (p,k)) (places net))
215
216
217
makeImplicitProperty net Safe =
        let bounded = makeImplicitProperty net (Bounded 1)
        in  Property "safe" Safety $ pformula bounded
218

219
220
221
checkProperty :: Int -> PetriNet -> Bool -> Property -> IO Bool
checkProperty verbosity net refine p = do
        verbosePut verbosity 1 $ "\nChecking " ++ showPropertyName p
222
        verbosePut verbosity 3 $ show p
223
        r <- case ptype p of
224
225
226
            Safety -> checkSafetyProperty verbosity net refine (pformula p) []
            Liveness -> checkLivenessProperty verbosity net refine (pformula p) []
        verbosePut verbosity 0 $ showPropertyName p ++
227
                                    if r then " is satisfied."
228
                                    else " may not be satisfied."
229
230
        return r

231
checkSafetyProperty :: Int -> PetriNet -> Bool ->
232
        Formula -> [[String]] -> IO Bool
233
checkSafetyProperty verbosity net refine f traps = do
234
235
236
237
238
        r <- checkSat $ checkStateEquationSat net f traps
        case r of
            Nothing -> return True
            Just a -> do
                let assigned = markedPlacesFromAssignment net a
239
240
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Places marked: " ++ show assigned
241
                verbosePut verbosity 3 $ "Assignment: " ++ show a
242
243
244
245
246
247
248
249
                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
250
251
252
                            verbosePut verbosity 1 "Trap found"
                            verbosePut verbosity 2 $ "Places in trap: " ++
                                                      show trap
253
254
                            verbosePut verbosity 3 $ "Trap assignment: " ++
                                                      show at
255
                            checkSafetyProperty verbosity net refine f
256
257
258
259
                                                (trap:traps)
                else
                    return False

260
checkLivenessProperty :: Int -> PetriNet -> Bool ->
261
        Formula -> [([String],[String])] -> IO Bool
262
checkLivenessProperty verbosity net refine f strans = do
263
        r <- checkSat $ checkTransitionInvariantSat net f strans
Philipp Meyer's avatar
Philipp Meyer committed
264
        case r of
265
            Nothing -> return True
266
267
            Just ax -> do
                let fired = firedTransitionsFromAssignment ax
268
269
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Transitions fired: " ++ show fired
270
                verbosePut verbosity 3 $ "Assignment: " ++ show ax
271
272
273
274
                if refine then do
                    rt <- checkSat $ checkSComponentSat net fired ax
                    case rt of
                        Nothing -> do
275
                            verbosePut verbosity 1 "No S-component found"
276
277
278
                            return False
                        Just as -> do
                            let sOutIn = getSComponentOutIn net ax as
279
280
                            verbosePut verbosity 1 "S-component found"
                            verbosePut verbosity 2 $ "Out/In: " ++ show sOutIn
281
282
                            verbosePut verbosity 3 $ "S-Component assignment: " ++
                                                      show as
283
                            checkLivenessProperty verbosity net refine f
284
285
286
                                                  (sOutIn:strans)
                else
                    return False
287

288
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
289
main = do
290
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
291
292
293
294
295
296
297
298
        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")
299
300
                let verbosity = optVerbosity opts
                    refinement = optRefine opts
301
302
                let parser = case inputFormat opts of
                                 PNET -> PNET.parseContent
Philipp Meyer's avatar
Philipp Meyer committed
303
                                 LOLA -> LOLA.parseContent
304
                                 TPN -> TPN.parseContent
305
306
307
308
                let properties = reverse $ optProperties opts
                let transformations = reverse $ optTransformations opts
                rs <- mapM (checkFile parser verbosity refinement properties
                                transformations) files
309
310
311
312
313
314
315
316
317
318
319
320
321
                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
322
        exitWith $ ExitFailure 2
Philipp Meyer's avatar
Philipp Meyer committed
323

324
325
326
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
327
        exitWith $ ExitFailure 3