Main.hs 10.6 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

12
13
import Parser
import qualified Parser.PNET as PNET
Philipp Meyer's avatar
Philipp Meyer committed
14
import qualified Parser.LOLA as LOLA
15
import qualified Parser.TPN as TPN
16
17
import PetriNet
import Property
18
import Solver
19
20
import Solver.StateEquation
import Solver.TrapConstraints
21
22
import Solver.TransitionInvariant
import Solver.SComponent
23

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

26
data ImplicitProperty = Termination
27
                      | NoDeadlock | NoDeadlockUnlessFinal
28
29
30
                      | Safe | Bounded Integer
                      deriving (Show,Read)

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

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

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

62
        , Option "" ["termination"]
63
64
65
        (NoArg (\opt -> Right opt {
                           optProperties = Termination : optProperties opt
               }))
66
67
        "Prove termination"

68
69
70
71
72
73
        , Option "" ["no-deadlock"]
        (NoArg (\opt -> Right opt {
                           optProperties = NoDeadlock : optProperties opt
               }))
        "Prove that there is no deadlock"

74
75
76
77
78
        , Option "" ["no-deadlock-unless-final"]
        (NoArg (\opt -> Right opt {
                           optProperties = NoDeadlockUnlessFinal : optProperties opt
               }))
        "Prove that there is no deadlock unless a final place is marked"
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94

        , Option "" ["safe"]
        (NoArg (\opt -> Right opt {
                           optProperties = Safe : optProperties opt
               }))
        "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"

95
96
97
98
        , Option "n" ["no-refinement"]
        (NoArg (\opt -> Right opt { optRefine = False }))
        "Don't use refinement"

99
        , Option "v" ["verbose"]
100
101
102
103
104
105
        (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)"
106
107
108
109
110
111
112
113
114
115

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

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

116
117
118
119
verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
        when (verbosity >= level) (putStrLn str)

120
121
122
123
124
125
126
127
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

128
129
130
checkFile :: Parser (PetriNet,[Property]) -> Int -> Bool ->
            [ImplicitProperty] -> String -> IO Bool
checkFile parser verbosity refine implicitProperties file = do
131
        verbosePut verbosity 0 $ "Reading \"" ++ file ++ "\""
132
        (net,properties) <- parseFile parser file
133
134
135
136
        verbosePut verbosity 1 $ "Analyzing " ++ showNetName net
        verbosePut verbosity 2 $
                "Places: " ++ show (length  $ places net) ++ "\n" ++
                "Transitions: " ++ show (length $ transitions net)
137
        let addedProperties = map (makeImplicitProperty net) implicitProperties
138
        print addedProperties
139
        rs <- mapM (checkProperty verbosity net refine)
140
                  (addedProperties ++ properties)
141
        verbosePut verbosity 0 ""
142
143
        return $ and rs

144
145
146
147
148
149
150
151
152
153
placeOp :: Op -> (String, Integer) -> Formula
placeOp op (p,w) = Atom $ LinIneq (Term [Var 1 p]) op (Term [Const w])

makeImplicitProperty :: PetriNet -> ImplicitProperty -> Property
makeImplicitProperty _ Termination = Property "termination" Liveness FTrue
makeImplicitProperty net NoDeadlock =
        Property "no deadlock" Safety $
            foldl (:&:) FTrue
                (map (foldl (:|:) FFalse . map (placeOp Lt) . lpre net)
                     (transitions net))
154
155
156
157
158
159
160
161
makeImplicitProperty net NoDeadlockUnlessFinal =
        let finals = [ p | p <- places net, null (lpost net p) ]
        in  if null finals then error "no final place!"
            else if length finals > 1 then error ("more than one final place: " ++ show finals)
            else
                Property "no deadlock unless final" Safety $
                    foldl (:&:) FTrue (map (\p -> placeOp Lt (p,1)) finals) :&:
                    pformula (makeImplicitProperty net NoDeadlock)
162
163
164
165
166
167
168
makeImplicitProperty net (Bounded k) =
        Property (show k ++ "-bounded") Safety $
            foldl (:|:) FFalse
                (map (\p -> placeOp Gt (p,k)) (places net))
makeImplicitProperty net Safe =
        Property "safe" Safety $ pformula (makeImplicitProperty net (Bounded 1))

169
170
171
checkProperty :: Int -> PetriNet -> Bool -> Property -> IO Bool
checkProperty verbosity net refine p = do
        verbosePut verbosity 1 $ "\nChecking " ++ showPropertyName p
172
        r <- case ptype p of
173
174
175
            Safety -> checkSafetyProperty verbosity net refine (pformula p) []
            Liveness -> checkLivenessProperty verbosity net refine (pformula p) []
        verbosePut verbosity 0 $ showPropertyName p ++
176
                                    if r then " is satisfied."
177
                                    else " may not be satisfied."
178
179
        return r

180
checkSafetyProperty :: Int -> PetriNet -> Bool ->
181
        Formula -> [[String]] -> IO Bool
182
checkSafetyProperty verbosity net refine f traps = do
183
184
185
186
187
        r <- checkSat $ checkStateEquationSat net f traps
        case r of
            Nothing -> return True
            Just a -> do
                let assigned = markedPlacesFromAssignment net a
188
189
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Places marked: " ++ show assigned
190
191
192
193
194
195
196
197
                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
198
199
200
201
                            verbosePut verbosity 1 "Trap found"
                            verbosePut verbosity 2 $ "Places in trap: " ++
                                                      show trap
                            checkSafetyProperty verbosity net refine f
202
203
204
205
                                                (trap:traps)
                else
                    return False

206
checkLivenessProperty :: Int -> PetriNet -> Bool ->
207
        Formula -> [([String],[String])] -> IO Bool
208
checkLivenessProperty verbosity net refine f strans = do
209
        r <- checkSat $ checkTransitionInvariantSat net f strans
Philipp Meyer's avatar
Philipp Meyer committed
210
        case r of
211
            Nothing -> return True
212
213
            Just ax -> do
                let fired = firedTransitionsFromAssignment ax
214
215
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Transitions fired: " ++ show fired
216
217
218
219
                if refine then do
                    rt <- checkSat $ checkSComponentSat net fired ax
                    case rt of
                        Nothing -> do
220
                            verbosePut verbosity 1 "No S-component found"
221
222
223
                            return False
                        Just as -> do
                            let sOutIn = getSComponentOutIn net ax as
224
225
226
                            verbosePut verbosity 1 "S-component found"
                            verbosePut verbosity 2 $ "Out/In: " ++ show sOutIn
                            checkLivenessProperty verbosity net refine f
227
228
229
                                                  (sOutIn:strans)
                else
                    return False
230

231
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
232
main = do
233
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
234
235
236
237
238
239
240
241
        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")
242
243
                let verbosity = optVerbosity opts
                    refinement = optRefine opts
244
245
                let parser = case inputFormat opts of
                                 PNET -> PNET.parseContent
Philipp Meyer's avatar
Philipp Meyer committed
246
                                 LOLA -> LOLA.parseContent
247
                                 TPN -> TPN.parseContent
248
                let properties = optProperties opts
249
250
                rs <- mapM (checkFile parser verbosity refinement properties)
                          files
251
252
253
254
255
256
257
258
259
260
261
262
263
                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
264
        exitWith $ ExitFailure 2
Philipp Meyer's avatar
Philipp Meyer committed
265

266
267
268
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
269
        exitWith $ ExitFailure r