Main.hs 6.66 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
10
import System.IO
import System.Console.GetOpt
import Control.Monad
import Control.Applicative
Philipp Meyer's avatar
Philipp Meyer committed
11

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

24
25
26
27
28
29
data InputFormat = PNET | LOLA | TPN deriving (Show,Read)

data Options = Options { inputFormat :: InputFormat
                       , optVerbose :: Bool
                       , optShowHelp :: Bool
                       , optShowVersion :: Bool
30
                       , proveTermination :: Bool
31
32
33
34
35
36
37
                       }

startOptions :: Options
startOptions = Options { inputFormat = PNET
                       , optVerbose = False
                       , optShowHelp = False
                       , optShowVersion = False
38
                       , proveTermination = False
39
40
41
42
                       }

options :: [ OptDescr (Options -> Either String Options) ]
options =
43
44
45
46
47
48
49
50
51
52
53
        [ 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"
54

55
56
57
58
        , Option "" ["termination"]
        (NoArg (\opt -> Right opt { proveTermination = True }))
        "Prove termination"

59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
        , Option "v" ["verbose"]
        (NoArg (\opt -> Right opt { optVerbose = True }))
        "Enable verbose messages"

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

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

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

80
81
82
checkFile :: Parser (PetriNet,[Property]) -> Bool -> [Property] ->
            String -> IO Bool
checkFile parser verbose addedProperties file = do
83
        putStrLn $ "Reading \"" ++ file ++ "\""
84
        (net,properties) <- parseFile parser file
85
        putStrLn $ "Analyzing " ++ showNetName net
86
        when verbose (do
Philipp Meyer's avatar
Philipp Meyer committed
87
                print net
88
89
90
                putStrLn $ "Places: " ++ show (length  $ places net)
                putStrLn $ "Transitions: " ++ show (length $ transitions net)
            )
91
        rs <- mapM (checkProperty verbose net) (addedProperties ++ properties)
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
        putStrLn ""
        return $ and rs

checkProperty :: Bool -> PetriNet -> Property -> IO Bool
checkProperty verbose net p = do
        putStrLn $ "\nChecking " ++ showPropertyName p
        r <- case ptype p of
            Safety -> checkSafetyProperty verbose net (pformula p) []
            Liveness -> checkLivenessProperty verbose net (pformula p) []
        putStrLn $ if r then "Property is satisfied."
                        else "Property may not be satisfied."
        return r

checkSafetyProperty :: Bool -> PetriNet -> Formula -> [[String]] -> IO Bool
checkSafetyProperty verbose net f traps = do
107
108
109
110
111
        r <- checkSat $ checkStateEquationSat net f traps
        case r of
            Nothing -> return True
            Just a -> do
                let assigned = markedPlacesFromAssignment net a
112
113
                putStrLn "Assignment found"
                when verbose (putStrLn $ "Places marked: " ++ show assigned)
114
115
116
117
118
119
120
                rt <- checkSat $ checkTrapSat net assigned
                case rt of
                    Nothing -> do
                        putStrLn "No trap found."
                        return False
                    Just at -> do
                        let trap = trapFromAssignment at
121
122
123
                        putStrLn "Trap found"
                        when verbose (putStrLn $ "Places in trap: " ++ show trap)
                        checkSafetyProperty verbose net f (trap:traps)
124

125
126
checkLivenessProperty :: Bool -> PetriNet -> Formula -> [([String],[String])] -> IO Bool
checkLivenessProperty verbose net f strans = do
127
        r <- checkSat $ checkTransitionInvariantSat net f strans
Philipp Meyer's avatar
Philipp Meyer committed
128
        case r of
129
            Nothing -> return True
130
131
            Just ax -> do
                let fired = firedTransitionsFromAssignment ax
132
133
                putStrLn "Assignment found"
                when verbose (putStrLn $ "Transitions fired: " ++ show fired)
134
                rt <- checkSat $ checkSComponentSat net fired ax
135
136
137
138
                case rt of
                    Nothing -> do
                        putStrLn "No S-component found"
                        return False
139
                    Just as -> do
140
                        let sOutIn = getSComponentOutIn net ax as
141
142
143
                        putStrLn "S-component found"
                        when verbose (putStrLn $ "Out/In: " ++ show sOutIn)
                        checkLivenessProperty verbose net f (sOutIn:strans)
144

145
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
146
main = do
147
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
148
149
150
151
152
153
154
155
156
        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")
157
158
                let parser = case inputFormat opts of
                                 PNET -> PNET.parseContent
Philipp Meyer's avatar
Philipp Meyer committed
159
                                 LOLA -> LOLA.parseContent
160
                                 TPN -> TPN.parseContent
161
162
163
                let properties = [ Property "termination" Liveness FTrue
                                 | proveTermination opts ]
                rs <- mapM (checkFile parser (optVerbose opts) properties) files
164
165
166
167
168
169
170
171
172
173
174
175
176
177
                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
        exitWith $ ExitFailure 1
Philipp Meyer's avatar
Philipp Meyer committed
178

179
180
181
182
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
        exitWith $ ExitFailure 2