Main.hs 18.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
Philipp Meyer's avatar
Philipp Meyer committed
24
import qualified Printer.SPEC as SPECPrinter
25
import Property
26
import Solver
27 28
import Solver.StateEquation
import Solver.TrapConstraints
29 30
import Solver.TransitionInvariant
import Solver.SComponent
31

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

34 35
data NetTransformation = TerminationByReachability
                       | ValidateIdentifiers
36

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

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

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

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

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

86 87 88 89
        , Option "s" ["structure"]
        (NoArg (\opt -> Right opt { optPrintStructure = True }))
        "Print structural information"

90 91 92 93 94 95
        , Option "" ["validate-identifiers"]
        (NoArg (\opt -> Right opt {
            optTransformations = ValidateIdentifiers : optTransformations opt
          }))
        "Make identifiers valid for lola"

96
        , Option "" ["termination-by-reachability"]
97
        (NoArg (\opt -> Right opt {
98
            optTransformations = TerminationByReachability : optTransformations opt
99
          }))
100
        "Prove termination by reducing it to reachability"
101

102
        , Option "" ["terminating"]
103
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
104
                   optProperties = Termination : optProperties opt
105
               }))
106
        "Prove that the net is terminating"
107

Philipp Meyer's avatar
Philipp Meyer committed
108 109 110 111 112 113
        , Option "" ["proper-termination"]
        (NoArg (\opt -> Right opt {
                   optProperties = ProperTermination : optProperties opt
               }))
        "Prove termination in the final marking"

114
        , Option "" ["deadlock-free"]
115
        (NoArg (\opt -> Right opt {
116
                   optProperties = DeadlockFree : optProperties opt
117
               }))
118
        "Prove that the net is deadlock-free"
119

120
        , Option "" ["deadlock-free-unless-final"]
Philipp Meyer's avatar
Philipp Meyer committed
121
        (NoArg (\opt -> Right opt {
122
                   optProperties = DeadlockFreeUnlessFinal : optProperties opt
Philipp Meyer's avatar
Philipp Meyer committed
123
               }))
124 125
        ("Prove that the net is deadlock-free\n" ++
         "unless it is in the final marking")
Philipp Meyer's avatar
Philipp Meyer committed
126

127 128
        , Option "" ["safe"]
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
129
                   optProperties = Safe : optProperties opt
130 131 132 133 134 135 136 137 138 139 140 141
               }))
        "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"

142 143 144 145
        , Option "n" ["no-refinement"]
        (NoArg (\opt -> Right opt { optRefine = False }))
        "Don't use refinement"

146 147 148 149 150 151 152
        , Option "o" ["output"]
        (ReqArg (\arg opt -> Right opt {
                        optOutput = Just arg
                })
                "FILE")
        "Write net and properties to FILE"

153 154 155 156 157 158
        , Option "" ["no-given-properties"]
        (NoArg (\opt -> Right opt {
                   optUseProperties = False
               }))
        "Do not use the properties given in the input file"

159
        , Option "v" ["verbose"]
160 161 162 163 164 165
        (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)"
166 167 168 169 170 171 172 173 174 175

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

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

176 177 178 179
verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
        when (verbosity >= level) (putStrLn str)

180 181 182 183 184 185 186 187
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

188 189 190
writeFiles :: Int -> String -> PetriNet -> [Property] -> IO ()
writeFiles verbosity basename net props = do
        verbosePut verbosity 1 $ "Writing " ++ showNetName net ++ " to " ++ basename
191
        L.writeFile basename $ LOLAPrinter.printNet net
192 193 194 195
        mapM_ (\(p,i) -> do
                let file = basename ++ ".task" ++ show i
                verbosePut verbosity 1 $ "Writing " ++ showPropertyName p ++
                                         " to " ++ file
196
                L.writeFile file $ LOLAPrinter.printProperty p
197
              ) (zip props [(1::Integer)..])
198
        verbosePut verbosity 1 $ "Writing properties to " ++ basename ++ ".sara"
199 200
        L.writeFile (basename ++ ".sara") $
            SARAPrinter.printProperties basename net props
Philipp Meyer's avatar
Philipp Meyer committed
201 202 203 204 205 206
        mapM_ (\(p,i) -> do
                let file = basename ++ ".target" ++ show i
                verbosePut verbosity 1 $ "Writing " ++ showPropertyName p ++
                                         " to " ++ file
                L.writeFile file $ SPECPrinter.printProperty p
              ) (zip props [(1::Integer)..])
207

208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226
structuralAnalysis :: PetriNet -> IO ()
structuralAnalysis net =  do
        let noGhost t = t `notElem` ghostTransitions net
        let initP  = filter (\x -> (not . any noGhost . pre net) x &&
                             (any noGhost . post net) x) (places net)
        let finalP = filter (\x -> (not . any noGhost . post net) x &&
                             (any noGhost . pre net) x) (places net)
        let isolP  = filter (\x -> (not . any noGhost . post net) x &&
                             (not . any noGhost . pre net) x) (places net)
        let initT  = filter (\t -> noGhost t && null (pre  net t))
                        (transitions net)
        let finalT = filter (\t -> noGhost t && null (post net t))
                        (transitions net)
        putStrLn $ "Initial places     : " ++ show (length initP)
        putStrLn $ "Initial transitions: " ++ show (length initT)
        putStrLn $ "Isolated places    : " ++ show (length isolP)
        putStrLn $ "Final places       : " ++ show (length finalP)
        putStrLn $ "Final transitions  : " ++ show (length finalT)

227
checkFile :: Parser (PetriNet,[Property]) -> Int -> Bool ->
228
            [ImplicitProperty] -> [NetTransformation] ->
229
            Bool -> Maybe String -> Bool -> String -> IO Bool
230
checkFile parser verbosity refine implicitProperties transformations
231
          useProperties output printStruct file = do
232
        verbosePut verbosity 0 $ "Reading \"" ++ file ++ "\""
233
        (net,props) <- parseFile parser file
234 235 236
        let props' = if useProperties then props else []
        let props'' = props' ++ map (makeImplicitProperty net) implicitProperties
        let (net',props''') = foldl transformNet (net,props'') transformations
237 238 239 240
        verbosePut verbosity 1 $ "Analyzing " ++ showNetName net
        verbosePut verbosity 2 $
                "Places: " ++ show (length  $ places net') ++ "; " ++
                "Transitions: " ++ show (length $ transitions net')
241
        when printStruct $ structuralAnalysis net
242
        verbosePut verbosity 3 $ show net'
243
        case output of
244
            Just outputfile -> writeFiles verbosity outputfile net' props'''
245
            Nothing -> return ()
Philipp Meyer's avatar
Philipp Meyer committed
246
        -- TODO: short-circuit?
247
        rs <- mapM (checkProperty verbosity net' refine) props'''
248
        verbosePut verbosity 0 ""
249 250
        return $ and rs

251
placeOp :: Op -> (String, Integer) -> Formula
252
placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w)
253

254 255
transformNet :: (PetriNet, [Property]) -> NetTransformation ->
               (PetriNet, [Property])
256
transformNet (net, props) TerminationByReachability =
257 258 259 260
        let prime = ('\'':)
            ps = ["'sigma", "'m1", "'m2"] ++
                 places net ++ map prime (places net)
            is = [("'m1", 1)] ++
261
                 initials net ++ map (first prime) (initials net)
262 263 264 265 266 267 268 269 270 271
            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'')]
272
            ts = ("'switch", [("'m1",1)], [("'m2",1)]) :
273 274
                 concatMap transformTransition (transitions net)
            gs = ghostTransitions net
275 276
            prop = Property "termination by reachability" Safety $
                    foldl (:&:) (Atom (LinIneq (Var "'sigma") Ge (Const 1)))
277 278
                      (map (\p -> Atom (LinIneq
                                (Var (prime p) :-: Var p) Ge (Const 0)))
279
                        (places net))
280
            -- TODO: map existing liveness properties
281
        in  (makePetriNetWithTrans (name net) ps ts is gs, prop : props)
282
transformNet (net, props) ValidateIdentifiers =
283 284 285 286
        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
287 288
            gs = map validateId $ ghostTransitions net
            net' = makePetriNet (name net) ps ts as is gs
289
            props' = map (rename validateId) props
290
        in  (net', props')
291

292
makeImplicitProperty :: PetriNet -> ImplicitProperty -> Property
293 294 295 296 297
makeImplicitProperty net Termination =
        Property "termination" Liveness $
            foldl (:&:) FTrue
                (map (\t -> Atom (LinIneq (Var t) Eq (Const 0)))
                    (ghostTransitions net))
298
makeImplicitProperty net ProperTermination =
Philipp Meyer's avatar
Philipp Meyer committed
299
        let (finals, nonfinals) = partition (null . lpost net) (places net)
300
        in  Property "proper termination" Safety
Philipp Meyer's avatar
Philipp Meyer committed
301 302
            (foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) finals) :&:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals))
303 304
makeImplicitProperty net DeadlockFree =
        Property "deadlock-free" Safety $
305 306
            foldl (:&:) FTrue
                (map (foldl (:|:) FFalse . map (placeOp Lt) . lpre net)
307
                     (filter (`notElem` ghostTransitions net) (transitions net)))
308 309
makeImplicitProperty net DeadlockFreeUnlessFinal =
        let nodeadlock = makeImplicitProperty net DeadlockFree
310
            (finals, nonfinals) = partition (null . lpost net) (places net)
311
        in  Property "deadlock-free unless final" Safety $
Philipp Meyer's avatar
Philipp Meyer committed
312 313 314
            (foldl (:&:) FTrue  (map (\p -> placeOp Eq (p,0)) finals) :|:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals)) :&:
            pformula nodeadlock
315
makeImplicitProperty net (Bounded k) =
316
        Property (show k ++ "-bounded") Safety $
317
            foldl (:|:) FFalse
Philipp Meyer's avatar
Philipp Meyer committed
318
                (map (\p -> placeOp Ge (p,k+1))
319 320
                    (filter (`notElem` concatMap (post net) (ghostTransitions net))
                        (places net)))
321 322 323
makeImplicitProperty net Safe =
        let bounded = makeImplicitProperty net (Bounded 1)
        in  Property "safe" Safety $ pformula bounded
324

325 326 327
checkProperty :: Int -> PetriNet -> Bool -> Property -> IO Bool
checkProperty verbosity net refine p = do
        verbosePut verbosity 1 $ "\nChecking " ++ showPropertyName p
328
        verbosePut verbosity 3 $ show p
329
        r <- case ptype p of
330 331 332
            Safety -> checkSafetyProperty verbosity net refine (pformula p) []
            Liveness -> checkLivenessProperty verbosity net refine (pformula p) []
        verbosePut verbosity 0 $ showPropertyName p ++
333
                                    if r then " is satisfied."
334
                                    else " may not be satisfied."
335 336
        return r

337
checkSafetyProperty :: Int -> PetriNet -> Bool ->
338
        Formula -> [[String]] -> IO Bool
339
checkSafetyProperty verbosity net refine f traps = do
340 341 342 343 344
        r <- checkSat $ checkStateEquationSat net f traps
        case r of
            Nothing -> return True
            Just a -> do
                let assigned = markedPlacesFromAssignment net a
345 346
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Places marked: " ++ show assigned
347
                verbosePut verbosity 3 $ "Assignment: " ++ show a
348 349 350 351
                if refine then do
                    rt <- checkSat $ checkTrapSat net assigned
                    case rt of
                        Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
352
                            verbosePut verbosity 1 "No trap found."
353 354 355
                            return False
                        Just at -> do
                            let trap = trapFromAssignment at
356 357 358
                            verbosePut verbosity 1 "Trap found"
                            verbosePut verbosity 2 $ "Places in trap: " ++
                                                      show trap
359 360
                            verbosePut verbosity 3 $ "Trap assignment: " ++
                                                      show at
361
                            checkSafetyProperty verbosity net refine f
362 363 364 365
                                                (trap:traps)
                else
                    return False

366
checkLivenessProperty :: Int -> PetriNet -> Bool ->
367
        Formula -> [([String],[String])] -> IO Bool
368
checkLivenessProperty verbosity net refine f strans = do
369
        r <- checkSat $ checkTransitionInvariantSat net f strans
Philipp Meyer's avatar
Philipp Meyer committed
370
        case r of
371
            Nothing -> return True
372 373
            Just ax -> do
                let fired = firedTransitionsFromAssignment ax
374 375
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Transitions fired: " ++ show fired
376
                verbosePut verbosity 3 $ "Assignment: " ++ show ax
377 378 379 380
                if refine then do
                    rt <- checkSat $ checkSComponentSat net fired ax
                    case rt of
                        Nothing -> do
381
                            verbosePut verbosity 1 "No S-component found"
382 383 384
                            return False
                        Just as -> do
                            let sOutIn = getSComponentOutIn net ax as
385 386
                            verbosePut verbosity 1 "S-component found"
                            verbosePut verbosity 2 $ "Out/In: " ++ show sOutIn
387 388
                            verbosePut verbosity 3 $ "S-Component assignment: " ++
                                                      show as
389
                            checkLivenessProperty verbosity net refine f
390 391 392
                                                  (sOutIn:strans)
                else
                    return False
393

394
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
395
main = do
396
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
397 398 399 400 401 402 403 404
        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")
405 406
                let verbosity = optVerbosity opts
                    refinement = optRefine opts
407 408
                let parser = case inputFormat opts of
                                 PNET -> PNET.parseContent
Philipp Meyer's avatar
Philipp Meyer committed
409
                                 LOLA -> LOLA.parseContent
410
                                 TPN -> TPN.parseContent
411
                                 MIST -> MIST.parseContent
412 413 414
                let properties = reverse $ optProperties opts
                let transformations = reverse $ optTransformations opts
                rs <- mapM (checkFile parser verbosity refinement properties
415 416
                     transformations (optUseProperties opts) (optOutput opts)
                     (optPrintStructure opts)) files
Philipp Meyer's avatar
Philipp Meyer committed
417
                -- TODO: short-circuit with Control.Monad.Loops?
418 419 420 421 422
                if and rs then
                    exitSuccessWith "All properties satisfied."
                else
                    exitFailureWith "Some properties may not be satisfied."

Philipp Meyer's avatar
Philipp Meyer committed
423
-- TODO: Always exit with exit code 0 unless an error occured
424 425 426 427 428 429 430 431
exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
        exitSuccess

exitFailureWith :: String -> IO ()
exitFailureWith msg = do
        putStrLn msg
432
        exitWith $ ExitFailure 2
Philipp Meyer's avatar
Philipp Meyer committed
433

434 435 436
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
437
        exitWith $ ExitFailure 3