Main.hs 15.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 ((<$>))
11
import Control.Arrow (first)
Philipp Meyer's avatar
Philipp Meyer committed
12
import Data.List (partition)
Philipp Meyer's avatar
Philipp Meyer committed
13

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

29 30
data InputFormat = PNET | LOLA | TPN deriving (Show,Read)

31 32
data NetTransformation = TerminationByReachability
                       | ValidateIdentifiers
33

34
data ImplicitProperty = Termination
35
                      | NoDeadlock | NoDeadlockUnlessFinal
Philipp Meyer's avatar
Philipp Meyer committed
36
                      | ProperTermination
37 38 39
                      | Safe | Bounded Integer
                      deriving (Show,Read)

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

startOptions :: Options
startOptions = Options { inputFormat = PNET
52
                       , optVerbosity = 1
53 54
                       , optShowHelp = False
                       , optShowVersion = False
55
                       , optProperties = []
56
                       , optTransformations = []
57
                       , optRefine = True
58
                       , optOutput = Nothing
59 60 61 62
                       }

options :: [ OptDescr (Options -> Either String Options) ]
options =
63 64 65 66 67 68 69 70 71 72 73
        [ 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"
74

75 76 77 78 79 80
        , Option "" ["validate-identifiers"]
        (NoArg (\opt -> Right opt {
            optTransformations = ValidateIdentifiers : optTransformations opt
          }))
        "Make identifiers valid for lola"

81
        , Option "" ["termination-by-reachability"]
82
        (NoArg (\opt -> Right opt {
83
            optTransformations = TerminationByReachability : optTransformations opt
84
          }))
85
        "Prove termination by reducing it to reachability"
86

87
        , Option "" ["terminating"]
88
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
89
                   optProperties = Termination : optProperties opt
90
               }))
91
        "Prove that the net is terminating"
92

Philipp Meyer's avatar
Philipp Meyer committed
93 94 95 96 97 98
        , Option "" ["proper-termination"]
        (NoArg (\opt -> Right opt {
                   optProperties = ProperTermination : optProperties opt
               }))
        "Prove termination in the final marking"

99
        , Option "" ["deadlock-free"]
100
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
101
                   optProperties = NoDeadlock : optProperties opt
102
               }))
103
        "Prove that the net is deadlock-free"
104

105
        , Option "" ["deadlock-free-unless-final"]
Philipp Meyer's avatar
Philipp Meyer committed
106 107 108
        (NoArg (\opt -> Right opt {
                   optProperties = NoDeadlockUnlessFinal : optProperties opt
               }))
109 110
        ("Prove that the net is deadlock-free\n" ++
         "unless it is in the final marking")
Philipp Meyer's avatar
Philipp Meyer committed
111

112 113
        , Option "" ["safe"]
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
114
                   optProperties = Safe : optProperties opt
115 116 117 118 119 120 121 122 123 124 125 126
               }))
        "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"

127 128 129 130
        , Option "n" ["no-refinement"]
        (NoArg (\opt -> Right opt { optRefine = False }))
        "Don't use refinement"

131 132 133 134 135 136 137
        , Option "o" ["output"]
        (ReqArg (\arg opt -> Right opt {
                        optOutput = Just arg
                })
                "FILE")
        "Write net and properties to FILE"

138
        , Option "v" ["verbose"]
139 140 141 142 143 144
        (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)"
145 146 147 148 149 150 151 152 153 154

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

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

155 156 157 158
verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
        when (verbosity >= level) (putStrLn str)

159 160 161 162 163 164 165 166
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

167 168 169
writeFiles :: Int -> String -> PetriNet -> [Property] -> IO ()
writeFiles verbosity basename net props = do
        verbosePut verbosity 1 $ "Writing " ++ showNetName net ++ " to " ++ basename
170
        writeFile basename $ LOLAPrinter.printNet net
171 172 173 174
        mapM_ (\(p,i) -> do
                let file = basename ++ ".task" ++ show i
                verbosePut verbosity 1 $ "Writing " ++ showPropertyName p ++
                                         " to " ++ file
175
                writeFile file $ LOLAPrinter.printProperty p
176
              ) (zip props [(1::Integer)..])
177 178 179
        verbosePut verbosity 1 $ "Writing properties to " ++ basename ++ ".sara"
        writeFile (basename ++ ".sara") $ unlines $
                map (SARAPrinter.printProperty basename net) props
180

181
checkFile :: Parser (PetriNet,[Property]) -> Int -> Bool ->
182 183 184 185
            [ImplicitProperty] -> [NetTransformation] ->
            Maybe String -> String -> IO Bool
checkFile parser verbosity refine implicitProperties transformations
          output file = do
186
        verbosePut verbosity 0 $ "Reading \"" ++ file ++ "\""
187 188 189
        (net,props) <- parseFile parser file
        let props' = props ++ map (makeImplicitProperty net) implicitProperties
        let (net',props'') = foldl transformNet (net,props') transformations
190 191 192 193 194
        verbosePut verbosity 1 $ "Analyzing " ++ showNetName net
        verbosePut verbosity 2 $
                "Places: " ++ show (length  $ places net') ++ "; " ++
                "Transitions: " ++ show (length $ transitions net')
        verbosePut verbosity 3 $ show net'
195
        rs <- mapM (checkProperty verbosity net' refine) props''
196 197 198
        case output of
            Just outputfile -> writeFiles verbosity outputfile net' props''
            Nothing -> return ()
199
        verbosePut verbosity 0 ""
200 201
        return $ and rs

202
placeOp :: Op -> (String, Integer) -> Formula
203
placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w)
204

205 206
transformNet :: (PetriNet, [Property]) -> NetTransformation ->
               (PetriNet, [Property])
207
transformNet (net, props) TerminationByReachability =
208 209 210 211
        let prime = ('\'':)
            ps = ["'sigma", "'m1", "'m2"] ++
                 places net ++ map prime (places net)
            is = [("'m1", 1)] ++
212
                 initials net ++ map (first prime) (initials net)
213 214 215
            ts = ("'switch", [("'m1",1)], [("'m2",1)]) :
                 concatMap (\t ->
                    let (preT, postT) = context net t
216 217 218 219
                        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
220 221 222 223 224
                    in  [(t, pre', post'), (prime t, pre'', post'')]
                 )
                 (transitions net)
            prop = Property "termination by reachability" Safety $
                    foldl (:&:) (Atom (LinIneq (Var "'sigma") Ge (Const 1)))
225 226
                      (map (\p -> Atom (LinIneq
                                (Var (prime p) :-: Var p) Ge (Const 0)))
227
                        (places net))
228
            -- TODO: map existing liveness properties
229
        in  (makePetriNetWithTrans (name net) ps ts is, prop : props)
230
transformNet (net, props) ValidateIdentifiers =
231 232 233 234
        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
235
            net' = makePetriNet (name net) ps ts as is
236
            props' = map (rename validateId) props
237
        in  (net', props')
238

239
makeImplicitProperty :: PetriNet -> ImplicitProperty -> Property
240
makeImplicitProperty _ Termination =
241 242
        Property "termination" Liveness FTrue
makeImplicitProperty net ProperTermination =
Philipp Meyer's avatar
Philipp Meyer committed
243
        let (finals, nonfinals) = partition (null . lpost net) (places net)
244
        in  Property "proper termination" Safety
Philipp Meyer's avatar
Philipp Meyer committed
245 246
            (foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) finals) :&:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals))
247
makeImplicitProperty net NoDeadlock =
248
        Property "no deadlock" Safety $
249 250 251
            foldl (:&:) FTrue
                (map (foldl (:|:) FFalse . map (placeOp Lt) . lpre net)
                     (transitions net))
252 253 254 255
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
256 257 258
            (foldl (:&:) FTrue  (map (\p -> placeOp Eq (p,0)) finals) :|:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals)) :&:
            pformula nodeadlock
259
makeImplicitProperty net (Bounded k) =
260
        Property (show k ++ "-bounded") Safety $
261 262
            foldl (:|:) FFalse
                (map (\p -> placeOp Gt (p,k)) (places net))
263 264 265
makeImplicitProperty net Safe =
        let bounded = makeImplicitProperty net (Bounded 1)
        in  Property "safe" Safety $ pformula bounded
266

267 268 269
checkProperty :: Int -> PetriNet -> Bool -> Property -> IO Bool
checkProperty verbosity net refine p = do
        verbosePut verbosity 1 $ "\nChecking " ++ showPropertyName p
270
        verbosePut verbosity 3 $ show p
271
        r <- case ptype p of
272 273 274
            Safety -> checkSafetyProperty verbosity net refine (pformula p) []
            Liveness -> checkLivenessProperty verbosity net refine (pformula p) []
        verbosePut verbosity 0 $ showPropertyName p ++
275
                                    if r then " is satisfied."
276
                                    else " may not be satisfied."
277 278
        return r

279
checkSafetyProperty :: Int -> PetriNet -> Bool ->
280
        Formula -> [[String]] -> IO Bool
281
checkSafetyProperty verbosity net refine f traps = do
282 283 284 285 286
        r <- checkSat $ checkStateEquationSat net f traps
        case r of
            Nothing -> return True
            Just a -> do
                let assigned = markedPlacesFromAssignment net a
287 288
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Places marked: " ++ show assigned
289
                verbosePut verbosity 3 $ "Assignment: " ++ show a
290 291 292 293 294 295 296 297
                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
298 299 300
                            verbosePut verbosity 1 "Trap found"
                            verbosePut verbosity 2 $ "Places in trap: " ++
                                                      show trap
301 302
                            verbosePut verbosity 3 $ "Trap assignment: " ++
                                                      show at
303
                            checkSafetyProperty verbosity net refine f
304 305 306 307
                                                (trap:traps)
                else
                    return False

308
checkLivenessProperty :: Int -> PetriNet -> Bool ->
309
        Formula -> [([String],[String])] -> IO Bool
310
checkLivenessProperty verbosity net refine f strans = do
311
        r <- checkSat $ checkTransitionInvariantSat net f strans
Philipp Meyer's avatar
Philipp Meyer committed
312
        case r of
313
            Nothing -> return True
314 315
            Just ax -> do
                let fired = firedTransitionsFromAssignment ax
316 317
                verbosePut verbosity 1 "Assignment found"
                verbosePut verbosity 2 $ "Transitions fired: " ++ show fired
318
                verbosePut verbosity 3 $ "Assignment: " ++ show ax
319 320 321 322
                if refine then do
                    rt <- checkSat $ checkSComponentSat net fired ax
                    case rt of
                        Nothing -> do
323
                            verbosePut verbosity 1 "No S-component found"
324 325 326
                            return False
                        Just as -> do
                            let sOutIn = getSComponentOutIn net ax as
327 328
                            verbosePut verbosity 1 "S-component found"
                            verbosePut verbosity 2 $ "Out/In: " ++ show sOutIn
329 330
                            verbosePut verbosity 3 $ "S-Component assignment: " ++
                                                      show as
331
                            checkLivenessProperty verbosity net refine f
332 333 334
                                                  (sOutIn:strans)
                else
                    return False
335

336
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
337
main = do
338
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
339 340 341 342 343 344 345 346
        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")
347 348
                let verbosity = optVerbosity opts
                    refinement = optRefine opts
349 350
                let parser = case inputFormat opts of
                                 PNET -> PNET.parseContent
Philipp Meyer's avatar
Philipp Meyer committed
351
                                 LOLA -> LOLA.parseContent
352
                                 TPN -> TPN.parseContent
353 354 355
                let properties = reverse $ optProperties opts
                let transformations = reverse $ optTransformations opts
                rs <- mapM (checkFile parser verbosity refinement properties
356
                                transformations (optOutput opts)) files
357 358 359 360 361 362 363 364 365 366 367 368 369
                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
370
        exitWith $ ExitFailure 2
Philipp Meyer's avatar
Philipp Meyer committed
371

372 373 374
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
375
        exitWith $ ExitFailure 3