Main.hs 16.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 ((<$>))
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 273
            foldl (:&:) FTrue
                (map (foldl (:|:) FFalse . map (placeOp Lt) . lpre 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 284
            foldl (:|:) FFalse
                (map (\p -> placeOp Gt (p,k)) (places net))
285 286 287
makeImplicitProperty net Safe =
        let bounded = makeImplicitProperty net (Bounded 1)
        in  Property "safe" Safety $ pformula bounded
288

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

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

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

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

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