Main.hs 16.7 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
24
import Property
25
import Solver
26 27
import Solver.StateEquation
import Solver.TrapConstraints
28 29
import Solver.TransitionInvariant
import Solver.SComponent
30

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

33 34
data NetTransformation = TerminationByReachability
                       | ValidateIdentifiers
35

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

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

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

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

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

83 84 85 86 87 88
        , Option "" ["validate-identifiers"]
        (NoArg (\opt -> Right opt {
            optTransformations = ValidateIdentifiers : optTransformations opt
          }))
        "Make identifiers valid for lola"

89
        , Option "" ["termination-by-reachability"]
90
        (NoArg (\opt -> Right opt {
91
            optTransformations = TerminationByReachability : optTransformations opt
92
          }))
93
        "Prove termination by reducing it to reachability"
94

95
        , Option "" ["terminating"]
96
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
97
                   optProperties = Termination : optProperties opt
98
               }))
99
        "Prove that the net is terminating"
100

Philipp Meyer's avatar
Philipp Meyer committed
101 102 103 104 105 106
        , Option "" ["proper-termination"]
        (NoArg (\opt -> Right opt {
                   optProperties = ProperTermination : optProperties opt
               }))
        "Prove termination in the final marking"

107
        , Option "" ["deadlock-free"]
108
        (NoArg (\opt -> Right opt {
109
                   optProperties = DeadlockFree : optProperties opt
110
               }))
111
        "Prove that the net is deadlock-free"
112

113
        , Option "" ["deadlock-free-unless-final"]
Philipp Meyer's avatar
Philipp Meyer committed
114
        (NoArg (\opt -> Right opt {
115
                   optProperties = DeadlockFreeUnlessFinal : optProperties opt
Philipp Meyer's avatar
Philipp Meyer committed
116
               }))
117 118
        ("Prove that the net is deadlock-free\n" ++
         "unless it is in the final marking")
Philipp Meyer's avatar
Philipp Meyer committed
119

120 121
        , Option "" ["safe"]
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
122
                   optProperties = Safe : optProperties opt
123 124 125 126 127 128 129 130 131 132 133 134
               }))
        "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"

135 136 137 138
        , Option "n" ["no-refinement"]
        (NoArg (\opt -> Right opt { optRefine = False }))
        "Don't use refinement"

139 140 141 142 143 144 145
        , Option "o" ["output"]
        (ReqArg (\arg opt -> Right opt {
                        optOutput = Just arg
                })
                "FILE")
        "Write net and properties to FILE"

146 147 148 149 150 151
        , Option "" ["no-given-properties"]
        (NoArg (\opt -> Right opt {
                   optUseProperties = False
               }))
        "Do not use the properties given in the input file"

152
        , Option "v" ["verbose"]
153 154 155 156 157 158
        (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)"
159 160 161 162 163 164 165 166 167 168

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

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

169 170 171 172
verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
        when (verbosity >= level) (putStrLn str)

173 174 175 176 177 178 179 180
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

181 182 183
writeFiles :: Int -> String -> PetriNet -> [Property] -> IO ()
writeFiles verbosity basename net props = do
        verbosePut verbosity 1 $ "Writing " ++ showNetName net ++ " to " ++ basename
184
        L.writeFile basename $ LOLAPrinter.printNet net
185 186 187 188
        mapM_ (\(p,i) -> do
                let file = basename ++ ".task" ++ show i
                verbosePut verbosity 1 $ "Writing " ++ showPropertyName p ++
                                         " to " ++ file
189
                L.writeFile file $ LOLAPrinter.printProperty p
190
              ) (zip props [(1::Integer)..])
191
        verbosePut verbosity 1 $ "Writing properties to " ++ basename ++ ".sara"
192 193
        L.writeFile (basename ++ ".sara") $
            SARAPrinter.printProperties basename net props
194

195
checkFile :: Parser (PetriNet,[Property]) -> Int -> Bool ->
196
            [ImplicitProperty] -> [NetTransformation] ->
197
            Bool -> Maybe String -> String -> IO Bool
198
checkFile parser verbosity refine implicitProperties transformations
199
          useProperties output file = do
200
        verbosePut verbosity 0 $ "Reading \"" ++ file ++ "\""
201
        (net,props) <- parseFile parser file
202 203 204
        let props' = if useProperties then props else []
        let props'' = props' ++ map (makeImplicitProperty net) implicitProperties
        let (net',props''') = foldl transformNet (net,props'') transformations
205 206 207 208 209
        verbosePut verbosity 1 $ "Analyzing " ++ showNetName net
        verbosePut verbosity 2 $
                "Places: " ++ show (length  $ places net') ++ "; " ++
                "Transitions: " ++ show (length $ transitions net')
        verbosePut verbosity 3 $ show net'
210
        case output of
211
            Just outputfile -> writeFiles verbosity outputfile net' props'''
212
            Nothing -> return ()
213
        rs <- mapM (checkProperty verbosity net' refine) props'''
214
        verbosePut verbosity 0 ""
215 216
        return $ and rs

217
placeOp :: Op -> (String, Integer) -> Formula
218
placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w)
219

220 221
transformNet :: (PetriNet, [Property]) -> NetTransformation ->
               (PetriNet, [Property])
222
transformNet (net, props) TerminationByReachability =
223 224 225 226
        let prime = ('\'':)
            ps = ["'sigma", "'m1", "'m2"] ++
                 places net ++ map prime (places net)
            is = [("'m1", 1)] ++
227
                 initials net ++ map (first prime) (initials net)
228 229 230 231 232 233 234 235 236 237
            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'')]
238
            ts = ("'switch", [("'m1",1)], [("'m2",1)]) :
239 240
                 concatMap transformTransition (transitions net)
            gs = ghostTransitions net
241 242
            prop = Property "termination by reachability" Safety $
                    foldl (:&:) (Atom (LinIneq (Var "'sigma") Ge (Const 1)))
243 244
                      (map (\p -> Atom (LinIneq
                                (Var (prime p) :-: Var p) Ge (Const 0)))
245
                        (places net))
246
            -- TODO: map existing liveness properties
247
        in  (makePetriNetWithTrans (name net) ps ts is gs, prop : props)
248
transformNet (net, props) ValidateIdentifiers =
249 250 251 252
        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
253 254
            gs = map validateId $ ghostTransitions net
            net' = makePetriNet (name net) ps ts as is gs
255
            props' = map (rename validateId) props
256
        in  (net', props')
257

258
makeImplicitProperty :: PetriNet -> ImplicitProperty -> Property
259 260 261 262 263
makeImplicitProperty net Termination =
        Property "termination" Liveness $
            foldl (:&:) FTrue
                (map (\t -> Atom (LinIneq (Var t) Eq (Const 0)))
                    (ghostTransitions net))
264
makeImplicitProperty net ProperTermination =
Philipp Meyer's avatar
Philipp Meyer committed
265
        let (finals, nonfinals) = partition (null . lpost net) (places net)
266
        in  Property "proper termination" Safety
Philipp Meyer's avatar
Philipp Meyer committed
267 268
            (foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) finals) :&:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals))
269 270
makeImplicitProperty net DeadlockFree =
        Property "deadlock-free" Safety $
271 272
            foldl (:&:) FTrue
                (map (foldl (:|:) FFalse . map (placeOp Lt) . lpre net)
273
                     (filter (`notElem` ghostTransitions net) (transitions net)))
274 275
makeImplicitProperty net DeadlockFreeUnlessFinal =
        let nodeadlock = makeImplicitProperty net DeadlockFree
276
            (finals, nonfinals) = partition (null . lpost net) (places net)
277
        in  Property "deadlock-free unless final" Safety $
Philipp Meyer's avatar
Philipp Meyer committed
278 279 280
            (foldl (:&:) FTrue  (map (\p -> placeOp Eq (p,0)) finals) :|:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals)) :&:
            pformula nodeadlock
281
makeImplicitProperty net (Bounded k) =
282
        Property (show k ++ "-bounded") Safety $
283
            foldl (:|:) FFalse
284 285 286
                (map (\p -> placeOp Gt (p,k))
                    (filter (`notElem` concatMap (post net) (ghostTransitions net))
                        (places net)))
287 288 289
makeImplicitProperty net Safe =
        let bounded = makeImplicitProperty net (Bounded 1)
        in  Property "safe" Safety $ pformula bounded
290

291 292 293
checkProperty :: Int -> PetriNet -> Bool -> Property -> IO Bool
checkProperty verbosity net refine p = do
        verbosePut verbosity 1 $ "\nChecking " ++ showPropertyName p
294
        verbosePut verbosity 3 $ show p
295
        r <- case ptype p of
296 297 298
            Safety -> checkSafetyProperty verbosity net refine (pformula p) []
            Liveness -> checkLivenessProperty verbosity net refine (pformula p) []
        verbosePut verbosity 0 $ showPropertyName p ++
299
                                    if r then " is satisfied."
300
                                    else " may not be satisfied."
301 302
        return r

303
checkSafetyProperty :: Int -> PetriNet -> Bool ->
304
        Formula -> [[String]] -> IO Bool
305
checkSafetyProperty verbosity net refine f traps = do
306 307 308 309 310
        r <- checkSat $ checkStateEquationSat net f traps
        case r of
            Nothing -> return True
            Just a -> do
                let assigned = markedPlacesFromAssignment net a
311 312
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Places marked: " ++ show assigned
313
                verbosePut verbosity 3 $ "Assignment: " ++ show a
314 315 316 317
                if refine then do
                    rt <- checkSat $ checkTrapSat net assigned
                    case rt of
                        Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
318
                            verbosePut verbosity 1 "No trap found."
319 320 321
                            return False
                        Just at -> do
                            let trap = trapFromAssignment at
322 323 324
                            verbosePut verbosity 1 "Trap found"
                            verbosePut verbosity 2 $ "Places in trap: " ++
                                                      show trap
325 326
                            verbosePut verbosity 3 $ "Trap assignment: " ++
                                                      show at
327
                            checkSafetyProperty verbosity net refine f
328 329 330 331
                                                (trap:traps)
                else
                    return False

332
checkLivenessProperty :: Int -> PetriNet -> Bool ->
333
        Formula -> [([String],[String])] -> IO Bool
334
checkLivenessProperty verbosity net refine f strans = do
335
        r <- checkSat $ checkTransitionInvariantSat net f strans
Philipp Meyer's avatar
Philipp Meyer committed
336
        case r of
337
            Nothing -> return True
338 339
            Just ax -> do
                let fired = firedTransitionsFromAssignment ax
340 341
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Transitions fired: " ++ show fired
342
                verbosePut verbosity 3 $ "Assignment: " ++ show ax
343 344 345 346
                if refine then do
                    rt <- checkSat $ checkSComponentSat net fired ax
                    case rt of
                        Nothing -> do
347
                            verbosePut verbosity 1 "No S-component found"
348 349 350
                            return False
                        Just as -> do
                            let sOutIn = getSComponentOutIn net ax as
351 352
                            verbosePut verbosity 1 "S-component found"
                            verbosePut verbosity 2 $ "Out/In: " ++ show sOutIn
353 354
                            verbosePut verbosity 3 $ "S-Component assignment: " ++
                                                      show as
355
                            checkLivenessProperty verbosity net refine f
356 357 358
                                                  (sOutIn:strans)
                else
                    return False
359

360
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
361
main = do
362
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
363 364 365 366 367 368 369 370
        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")
371 372
                let verbosity = optVerbosity opts
                    refinement = optRefine opts
373 374
                let parser = case inputFormat opts of
                                 PNET -> PNET.parseContent
Philipp Meyer's avatar
Philipp Meyer committed
375
                                 LOLA -> LOLA.parseContent
376
                                 TPN -> TPN.parseContent
377
                                 MIST -> MIST.parseContent
378 379 380
                let properties = reverse $ optProperties opts
                let transformations = reverse $ optTransformations opts
                rs <- mapM (checkFile parser verbosity refinement properties
381 382
                     transformations (optUseProperties opts) (optOutput opts))
                     files
383 384 385 386 387 388 389 390 391 392 393 394 395
                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
396
        exitWith $ ExitFailure 2
Philipp Meyer's avatar
Philipp Meyer committed
397

398 399 400
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
401
        exitWith $ ExitFailure 3