Main.hs 7.42 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
                       , optRefine :: Bool
32
33
34
35
36
37
38
                       }

startOptions :: Options
startOptions = Options { inputFormat = PNET
                       , optVerbose = False
                       , optShowHelp = False
                       , optShowVersion = False
39
                       , proveTermination = False
40
                       , optRefine = True
41
42
43
44
                       }

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

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

61
62
63
64
        , Option "n" ["no-refinement"]
        (NoArg (\opt -> Right opt { optRefine = False }))
        "Don't use refinement"

65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
        , 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

86
checkFile :: Parser (PetriNet,[Property]) -> Bool -> Bool -> [Property] ->
87
            String -> IO Bool
88
checkFile parser verbose refine addedProperties file = do
89
        putStrLn $ "Reading \"" ++ file ++ "\""
90
        (net,properties) <- parseFile parser file
91
        putStrLn $ "Analyzing " ++ showNetName net
92
        when verbose (do
93
94
95
                putStrLn $ "Places: " ++ show (length  $ places net)
                putStrLn $ "Transitions: " ++ show (length $ transitions net)
            )
96
97
        rs <- mapM (checkProperty verbose net refine)
                  (addedProperties ++ properties)
98
99
100
        putStrLn ""
        return $ and rs

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

111
112
113
checkSafetyProperty :: Bool -> PetriNet -> Bool ->
        Formula -> [[String]] -> IO Bool
checkSafetyProperty verbose net refine f traps = do
114
115
116
117
118
        r <- checkSat $ checkStateEquationSat net f traps
        case r of
            Nothing -> return True
            Just a -> do
                let assigned = markedPlacesFromAssignment net a
119
120
                putStrLn "Assignment found"
                when verbose (putStrLn $ "Places marked: " ++ show assigned)
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
                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
                            putStrLn "Trap found"
                            when verbose (putStrLn $ "Places in trap: " ++
                                                     show trap)
                            checkSafetyProperty verbose net refine f
                                                (trap:traps)
                else
                    return False

checkLivenessProperty :: Bool -> PetriNet -> Bool ->
        Formula -> [([String],[String])] -> IO Bool
checkLivenessProperty verbose net refine f strans = do
140
        r <- checkSat $ checkTransitionInvariantSat net f strans
Philipp Meyer's avatar
Philipp Meyer committed
141
        case r of
142
            Nothing -> return True
143
144
            Just ax -> do
                let fired = firedTransitionsFromAssignment ax
145
146
                putStrLn "Assignment found"
                when verbose (putStrLn $ "Transitions fired: " ++ show fired)
147
148
149
150
151
152
153
154
155
156
157
158
159
160
                if refine then do
                    rt <- checkSat $ checkSComponentSat net fired ax
                    case rt of
                        Nothing -> do
                            putStrLn "No S-component found"
                            return False
                        Just as -> do
                            let sOutIn = getSComponentOutIn net ax as
                            putStrLn "S-component found"
                            when verbose (putStrLn $ "Out/In: " ++ show sOutIn)
                            checkLivenessProperty verbose net refine f
                                                  (sOutIn:strans)
                else
                    return False
161

162
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
163
main = do
164
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
165
166
167
168
169
170
171
172
173
        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")
174
175
                let parser = case inputFormat opts of
                                 PNET -> PNET.parseContent
Philipp Meyer's avatar
Philipp Meyer committed
176
                                 LOLA -> LOLA.parseContent
177
                                 TPN -> TPN.parseContent
178
179
                let properties = [ Property "termination" Liveness FTrue
                                 | proveTermination opts ]
180
181
                rs <- mapM (checkFile parser (optVerbose opts) (optRefine opts)
                                     properties) files
182
183
184
185
186
187
188
189
190
191
192
193
194
195
                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
196

197
198
199
200
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
        exitWith $ ExitFailure 2