Main.hs 14.5 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
import Data.List (partition)
Philipp Meyer's avatar
Philipp Meyer committed
12

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

26 27
data InputFormat = PNET | LOLA | TPN deriving (Show,Read)

28 29
data NetTransformation = TerminationToReachability

30
data ImplicitProperty = Termination
31
                      | NoDeadlock | NoDeadlockUnlessFinal
Philipp Meyer's avatar
Philipp Meyer committed
32
                      | ProperTermination
33 34 35
                      | Safe | Bounded Integer
                      deriving (Show,Read)

36
data Options = Options { inputFormat :: InputFormat
37
                       , optVerbosity :: Int
38 39
                       , optShowHelp :: Bool
                       , optShowVersion :: Bool
40
                       , optProperties :: [ImplicitProperty]
41
                       , optTransformations :: [NetTransformation]
42
                       , optRefine :: Bool
43
                       , optOutput :: Maybe String
44 45 46 47
                       }

startOptions :: Options
startOptions = Options { inputFormat = PNET
48
                       , optVerbosity = 1
49 50
                       , optShowHelp = False
                       , optShowVersion = False
51
                       , optProperties = []
52
                       , optTransformations = []
53
                       , optRefine = True
54
                       , optOutput = Nothing
55 56 57 58
                       }

options :: [ OptDescr (Options -> Either String Options) ]
options =
59 60 61 62 63 64 65 66 67 68 69
        [ 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"
70

71
        , Option "" ["termination-by-reachability"]
72 73 74
        (NoArg (\opt -> Right opt {
            optTransformations = TerminationToReachability : optTransformations opt
          }))
75
        "Prove termination by reducing it to reachability"
76

77
        , Option "" ["terminating"]
78
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
79
                   optProperties = Termination : optProperties opt
80
               }))
81
        "Prove that the net is terminating"
82

Philipp Meyer's avatar
Philipp Meyer committed
83 84 85 86 87 88
        , Option "" ["proper-termination"]
        (NoArg (\opt -> Right opt {
                   optProperties = ProperTermination : optProperties opt
               }))
        "Prove termination in the final marking"

89
        , Option "" ["deadlock-free"]
90
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
91
                   optProperties = NoDeadlock : optProperties opt
92
               }))
93
        "Prove that the net is deadlock-free"
94

95
        , Option "" ["deadlock-free-unless-final"]
Philipp Meyer's avatar
Philipp Meyer committed
96 97 98
        (NoArg (\opt -> Right opt {
                   optProperties = NoDeadlockUnlessFinal : optProperties opt
               }))
99 100
        ("Prove that the net is deadlock-free\n" ++
         "unless it is in the final marking")
Philipp Meyer's avatar
Philipp Meyer committed
101

102 103
        , Option "" ["safe"]
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
104
                   optProperties = Safe : optProperties opt
105 106 107 108 109 110 111 112 113 114 115 116
               }))
        "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"

117 118 119 120
        , Option "n" ["no-refinement"]
        (NoArg (\opt -> Right opt { optRefine = False }))
        "Don't use refinement"

121 122 123 124 125 126 127
        , Option "o" ["output"]
        (ReqArg (\arg opt -> Right opt {
                        optOutput = Just arg
                })
                "FILE")
        "Write net and properties to FILE"

128
        , Option "v" ["verbose"]
129 130 131 132 133 134
        (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)"
135 136 137 138 139 140 141 142 143 144

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

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

145 146 147 148
verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
        when (verbosity >= level) (putStrLn str)

149 150 151 152 153 154 155 156
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

157 158 159 160 161 162 163 164 165 166 167
writeFiles :: Int -> String -> PetriNet -> [Property] -> IO ()
writeFiles verbosity basename net props = do
        verbosePut verbosity 1 $ "Writing " ++ showNetName net ++ " to " ++ basename
        writeFile basename $ printNet net
        mapM_ (\(p,i) -> do
                let file = basename ++ ".task" ++ show i
                verbosePut verbosity 1 $ "Writing " ++ showPropertyName p ++
                                         " to " ++ file
                writeFile file $ printProperty p
              ) (zip props [(1::Integer)..])

168
checkFile :: Parser (PetriNet,[Property]) -> Int -> Bool ->
169 170 171 172
            [ImplicitProperty] -> [NetTransformation] ->
            Maybe String -> String -> IO Bool
checkFile parser verbosity refine implicitProperties transformations
          output file = do
173
        verbosePut verbosity 0 $ "Reading \"" ++ file ++ "\""
174 175 176
        (net,props) <- parseFile parser file
        let props' = props ++ map (makeImplicitProperty net) implicitProperties
        let (net',props'') = foldl transformNet (net,props') transformations
177 178 179 180 181
        verbosePut verbosity 1 $ "Analyzing " ++ showNetName net
        verbosePut verbosity 2 $
                "Places: " ++ show (length  $ places net') ++ "; " ++
                "Transitions: " ++ show (length $ transitions net')
        verbosePut verbosity 3 $ show net'
182
        rs <- mapM (checkProperty verbosity net' refine) props''
183 184 185
        case output of
            Just outputfile -> writeFiles verbosity outputfile net' props''
            Nothing -> return ()
186
        verbosePut verbosity 0 ""
187 188
        return $ and rs

189
placeOp :: Op -> (String, Integer) -> Formula
190
placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w)
191

192 193
transformNet :: (PetriNet, [Property]) -> NetTransformation ->
               (PetriNet, [Property])
194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215
transformNet (net, props) TerminationToReachability =
        let prime = ('\'':)
            primeFst (p,x) = (prime p, x)
            ps = ["'sigma", "'m1", "'m2"] ++
                 places net ++ map prime (places net)
            is = [("'m1", 1)] ++
                 initials net ++ map primeFst (initials net)
            ts = ("'switch", [("'m1",1)], [("'m2",1)]) :
                 concatMap (\t ->
                    let (preT, postT) = context net t
                        pre'  = [("'m1",1)] ++ preT  ++ map primeFst preT
                        post' = [("'m1",1)] ++ postT ++ map primeFst postT
                        pre''  = ("'m2",1) : map primeFst preT
                        post'' = [("'m2",1), ("'sigma",1)] ++ map primeFst postT
                    in  [(t, pre', post'), (prime t, pre'', post'')]
                 )
                 (transitions net)
            prop = Property "termination by reachability" Safety $
                    foldl (:&:) (Atom (LinIneq (Var "'sigma") Ge (Const 1)))
                      (map (\p -> Atom (LinIneq (Var (prime p)) Ge (Var p)))
                        (places net))
        in  (makePetriNetWithTrans (name net) ps ts is, prop : props)
216

217
makeImplicitProperty :: PetriNet -> ImplicitProperty -> Property
218
makeImplicitProperty _ Termination =
219 220
        Property "termination" Liveness FTrue
makeImplicitProperty net ProperTermination =
Philipp Meyer's avatar
Philipp Meyer committed
221
        let (finals, nonfinals) = partition (null . lpost net) (places net)
222
        in  Property "proper termination" Safety
Philipp Meyer's avatar
Philipp Meyer committed
223 224
            (foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) finals) :&:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals))
225
makeImplicitProperty net NoDeadlock =
226
        Property "no deadlock" Safety $
227 228 229
            foldl (:&:) FTrue
                (map (foldl (:|:) FFalse . map (placeOp Lt) . lpre net)
                     (transitions net))
230 231 232 233
makeImplicitProperty net NoDeadlockUnlessFinal =
        let nodeadlock = makeImplicitProperty net NoDeadlock
            (finals, nonfinals) = partition (null . lpost net) (places net)
        in  Property "no deadlock unless final" Safety $
Philipp Meyer's avatar
Philipp Meyer committed
234 235 236
            (foldl (:&:) FTrue  (map (\p -> placeOp Eq (p,0)) finals) :|:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals)) :&:
            pformula nodeadlock
237
makeImplicitProperty net (Bounded k) =
238
        Property (show k ++ "-bounded") Safety $
239 240
            foldl (:|:) FFalse
                (map (\p -> placeOp Gt (p,k)) (places net))
241 242 243
makeImplicitProperty net Safe =
        let bounded = makeImplicitProperty net (Bounded 1)
        in  Property "safe" Safety $ pformula bounded
244

245 246 247
checkProperty :: Int -> PetriNet -> Bool -> Property -> IO Bool
checkProperty verbosity net refine p = do
        verbosePut verbosity 1 $ "\nChecking " ++ showPropertyName p
248
        verbosePut verbosity 3 $ show p
249
        r <- case ptype p of
250 251 252
            Safety -> checkSafetyProperty verbosity net refine (pformula p) []
            Liveness -> checkLivenessProperty verbosity net refine (pformula p) []
        verbosePut verbosity 0 $ showPropertyName p ++
253
                                    if r then " is satisfied."
254
                                    else " may not be satisfied."
255 256
        return r

257
checkSafetyProperty :: Int -> PetriNet -> Bool ->
258
        Formula -> [[String]] -> IO Bool
259
checkSafetyProperty verbosity net refine f traps = do
260 261 262 263 264
        r <- checkSat $ checkStateEquationSat net f traps
        case r of
            Nothing -> return True
            Just a -> do
                let assigned = markedPlacesFromAssignment net a
265 266
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Places marked: " ++ show assigned
267
                verbosePut verbosity 3 $ "Assignment: " ++ show a
268 269 270 271 272 273 274 275
                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
276 277 278
                            verbosePut verbosity 1 "Trap found"
                            verbosePut verbosity 2 $ "Places in trap: " ++
                                                      show trap
279 280
                            verbosePut verbosity 3 $ "Trap assignment: " ++
                                                      show at
281
                            checkSafetyProperty verbosity net refine f
282 283 284 285
                                                (trap:traps)
                else
                    return False

286
checkLivenessProperty :: Int -> PetriNet -> Bool ->
287
        Formula -> [([String],[String])] -> IO Bool
288
checkLivenessProperty verbosity net refine f strans = do
289
        r <- checkSat $ checkTransitionInvariantSat net f strans
Philipp Meyer's avatar
Philipp Meyer committed
290
        case r of
291
            Nothing -> return True
292 293
            Just ax -> do
                let fired = firedTransitionsFromAssignment ax
294 295
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Transitions fired: " ++ show fired
296
                verbosePut verbosity 3 $ "Assignment: " ++ show ax
297 298 299 300
                if refine then do
                    rt <- checkSat $ checkSComponentSat net fired ax
                    case rt of
                        Nothing -> do
301
                            verbosePut verbosity 1 "No S-component found"
302 303 304
                            return False
                        Just as -> do
                            let sOutIn = getSComponentOutIn net ax as
305 306
                            verbosePut verbosity 1 "S-component found"
                            verbosePut verbosity 2 $ "Out/In: " ++ show sOutIn
307 308
                            verbosePut verbosity 3 $ "S-Component assignment: " ++
                                                      show as
309
                            checkLivenessProperty verbosity net refine f
310 311 312
                                                  (sOutIn:strans)
                else
                    return False
313

314
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
315
main = do
316
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
317 318 319 320 321 322 323 324
        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")
325 326
                let verbosity = optVerbosity opts
                    refinement = optRefine opts
327 328
                let parser = case inputFormat opts of
                                 PNET -> PNET.parseContent
Philipp Meyer's avatar
Philipp Meyer committed
329
                                 LOLA -> LOLA.parseContent
330
                                 TPN -> TPN.parseContent
331 332 333
                let properties = reverse $ optProperties opts
                let transformations = reverse $ optTransformations opts
                rs <- mapM (checkFile parser verbosity refinement properties
334
                                transformations (optOutput opts)) files
335 336 337 338 339 340 341 342 343 344 345 346 347
                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
348
        exitWith $ ExitFailure 2
Philipp Meyer's avatar
Philipp Meyer committed
349

350 351 352
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
353
        exitWith $ ExitFailure 3