Main.hs 10.3 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
-- TODO: Change NoDeadlockOutOf to NoDeadlockUnless=FILE
27
data ImplicitProperty = Termination
28
                      | NoDeadlock | NoDeadlockOutOf String
29
30
31
                      | Safe | Bounded Integer
                      deriving (Show,Read)

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

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

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

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

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

75
76
77
78
79
80
        , Option "" ["no-deadlock-out-of"]
        (ReqArg (\arg opt -> Right opt {
                           optProperties = NoDeadlockOutOf arg : optProperties opt
                })
                "PLACE")
        "Prove that there is no deadlock unless PLACE is marked"
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96

        , 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"

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

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

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

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

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

122
123
124
125
126
127
128
129
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

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

146
placeOp :: Op -> (String, Integer) -> Formula
147
placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w)
148
149
150
151
152
153
154
155

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))
156
157
158
makeImplicitProperty net (NoDeadlockOutOf pl) =
        Property ("no deadlock out of " ++ pl) Safety $
            placeOp Lt (pl,1) :&: pformula (makeImplicitProperty net NoDeadlock)
159
160
161
162
163
164
165
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))

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

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

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

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

263
264
265
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
266
        exitWith $ ExitFailure 3