Main.hs 11.1 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
data ImplicitProperty = Termination
28
                      | NoDeadlock | NoDeadlockUnlessFinal
Philipp Meyer's avatar
Philipp Meyer committed
29
                      | ProperTermination
30
31
32
                      | Safe | Bounded Integer
                      deriving (Show,Read)

33
data Options = Options { inputFormat :: InputFormat
34
                       , optVerbosity :: Int
35
36
                       , optShowHelp :: Bool
                       , optShowVersion :: Bool
37
                       , optProperties :: [ImplicitProperty]
38
                       , optRefine :: Bool
39
40
41
42
                       }

startOptions :: Options
startOptions = Options { inputFormat = PNET
43
                       , optVerbosity = 1
44
45
                       , optShowHelp = False
                       , optShowVersion = False
46
                       , optProperties = []
47
                       , optRefine = True
48
49
50
51
                       }

options :: [ OptDescr (Options -> Either String Options) ]
options =
52
53
54
55
56
57
58
59
60
61
62
        [ 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"
63

64
        , Option "" ["termination"]
65
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
66
                   optProperties = Termination : optProperties opt
67
               }))
68
69
        "Prove termination"

Philipp Meyer's avatar
Philipp Meyer committed
70
71
72
73
74
75
        , Option "" ["proper-termination"]
        (NoArg (\opt -> Right opt {
                   optProperties = ProperTermination : optProperties opt
               }))
        "Prove termination in the final marking"

76
77
        , Option "" ["no-deadlock"]
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
78
                   optProperties = NoDeadlock : optProperties opt
79
80
81
               }))
        "Prove that there is no deadlock"

Philipp Meyer's avatar
Philipp Meyer committed
82
83
84
85
86
87
88
        , Option "" ["no-deadlock-unless-final"]
        (NoArg (\opt -> Right opt {
                   optProperties = NoDeadlockUnlessFinal : optProperties opt
               }))
        ("Prove that there is no deadlock unless\n" ++
         "only final places are marked")

89
90
        , Option "" ["safe"]
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
91
                   optProperties = Safe : optProperties opt
92
93
94
95
96
97
98
99
100
101
102
103
               }))
        "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"

104
105
106
107
        , Option "n" ["no-refinement"]
        (NoArg (\opt -> Right opt { optRefine = False }))
        "Don't use refinement"

108
        , Option "v" ["verbose"]
109
110
111
112
113
114
        (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)"
115
116
117
118
119
120
121
122
123
124

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

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

125
126
127
128
verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
        when (verbosity >= level) (putStrLn str)

129
130
131
132
133
134
135
136
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

137
138
139
checkFile :: Parser (PetriNet,[Property]) -> Int -> Bool ->
            [ImplicitProperty] -> String -> IO Bool
checkFile parser verbosity refine implicitProperties file = do
140
        verbosePut verbosity 0 $ "Reading \"" ++ file ++ "\""
141
        (net,properties) <- parseFile parser file
142
143
144
145
        verbosePut verbosity 1 $ "Analyzing " ++ showNetName net
        verbosePut verbosity 2 $
                "Places: " ++ show (length  $ places net) ++ "\n" ++
                "Transitions: " ++ show (length $ transitions net)
146
        let addedProperties = map (makeImplicitProperty net) implicitProperties
147
        rs <- mapM (checkProperty verbosity net refine)
148
                  (addedProperties ++ properties)
149
        verbosePut verbosity 0 ""
150
151
        return $ and rs

152
placeOp :: Op -> (String, Integer) -> Formula
153
placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w)
154

155
makeImplicitProperty :: PetriNet -> ImplicitProperty -> Property
156
makeImplicitProperty _ Termination =
157
158
        Property "termination" Liveness FTrue
makeImplicitProperty net ProperTermination =
Philipp Meyer's avatar
Philipp Meyer committed
159
        let (finals, nonfinals) = partition (null . lpost net) (places net)
160
        in  Property "proper termination" Safety
Philipp Meyer's avatar
Philipp Meyer committed
161
162
            (foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) finals) :&:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals))
163
makeImplicitProperty net NoDeadlock =
164
        Property "no deadlock" Safety $
165
166
167
            foldl (:&:) FTrue
                (map (foldl (:|:) FFalse . map (placeOp Lt) . lpre net)
                     (transitions net))
168
169
170
171
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
172
173
174
            (foldl (:&:) FTrue  (map (\p -> placeOp Eq (p,0)) finals) :|:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals)) :&:
            pformula nodeadlock
175
makeImplicitProperty net (Bounded k) =
176
        Property (show k ++ "-bounded") Safety $
177
178
            foldl (:|:) FFalse
                (map (\p -> placeOp Gt (p,k)) (places net))
179
180
181
makeImplicitProperty net Safe =
        let bounded = makeImplicitProperty net (Bounded 1)
        in  Property "safe" Safety $ pformula bounded
182

183
184
185
checkProperty :: Int -> PetriNet -> Bool -> Property -> IO Bool
checkProperty verbosity net refine p = do
        verbosePut verbosity 1 $ "\nChecking " ++ showPropertyName p
186
        r <- case ptype p of
187
188
189
            Safety -> checkSafetyProperty verbosity net refine (pformula p) []
            Liveness -> checkLivenessProperty verbosity net refine (pformula p) []
        verbosePut verbosity 0 $ showPropertyName p ++
190
                                    if r then " is satisfied."
191
                                    else " may not be satisfied."
192
193
        return r

194
checkSafetyProperty :: Int -> PetriNet -> Bool ->
195
        Formula -> [[String]] -> IO Bool
196
checkSafetyProperty verbosity net refine f traps = do
197
198
199
200
201
        r <- checkSat $ checkStateEquationSat net f traps
        case r of
            Nothing -> return True
            Just a -> do
                let assigned = markedPlacesFromAssignment net a
202
203
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Places marked: " ++ show assigned
204
205
206
207
208
209
210
211
                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
212
213
214
215
                            verbosePut verbosity 1 "Trap found"
                            verbosePut verbosity 2 $ "Places in trap: " ++
                                                      show trap
                            checkSafetyProperty verbosity net refine f
216
217
218
219
                                                (trap:traps)
                else
                    return False

220
checkLivenessProperty :: Int -> PetriNet -> Bool ->
221
        Formula -> [([String],[String])] -> IO Bool
222
checkLivenessProperty verbosity net refine f strans = do
223
        r <- checkSat $ checkTransitionInvariantSat net f strans
Philipp Meyer's avatar
Philipp Meyer committed
224
        case r of
225
            Nothing -> return True
226
227
            Just ax -> do
                let fired = firedTransitionsFromAssignment ax
228
229
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Transitions fired: " ++ show fired
230
231
232
233
                if refine then do
                    rt <- checkSat $ checkSComponentSat net fired ax
                    case rt of
                        Nothing -> do
234
                            verbosePut verbosity 1 "No S-component found"
235
236
237
                            return False
                        Just as -> do
                            let sOutIn = getSComponentOutIn net ax as
238
239
240
                            verbosePut verbosity 1 "S-component found"
                            verbosePut verbosity 2 $ "Out/In: " ++ show sOutIn
                            checkLivenessProperty verbosity net refine f
241
242
243
                                                  (sOutIn:strans)
                else
                    return False
244

245
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
246
main = do
247
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
248
249
250
251
252
253
254
255
        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")
256
257
                let verbosity = optVerbosity opts
                    refinement = optRefine opts
258
259
                let parser = case inputFormat opts of
                                 PNET -> PNET.parseContent
Philipp Meyer's avatar
Philipp Meyer committed
260
                                 LOLA -> LOLA.parseContent
261
                                 TPN -> TPN.parseContent
262
                let properties = optProperties opts
263
264
                rs <- mapM (checkFile parser verbosity refinement properties)
                          files
265
266
267
268
269
270
271
272
273
274
275
276
277
                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
278
        exitWith $ ExitFailure 2
Philipp Meyer's avatar
Philipp Meyer committed
279

280
281
282
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
283
        exitWith $ ExitFailure 3