Main.hs 6.62 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
14
import qualified Parser.TPN as TPN
15
16
import PetriNet
import Property
17
import Solver
18
19
import Solver.StateEquation
import Solver.TrapConstraints
20
21
import Solver.TransitionInvariant
import Solver.SComponent
22

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

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

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

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

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

58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
        , 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

79
80
81
checkFile :: Parser (PetriNet,[Property]) -> Bool -> [Property] ->
            String -> IO Bool
checkFile parser verbose addedProperties file = do
82
        putStrLn $ "Reading \"" ++ file ++ "\""
83
        (net,properties) <- parseFile parser file
84
        putStrLn $ "Analyzing " ++ showNetName net
85
        when verbose (do
86
87
88
                putStrLn $ "Places: " ++ show (length  $ places net)
                putStrLn $ "Transitions: " ++ show (length $ transitions net)
            )
89
        rs <- mapM (checkProperty verbose net) (addedProperties ++ properties)
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
        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
105
106
107
108
109
        r <- checkSat $ checkStateEquationSat net f traps
        case r of
            Nothing -> return True
            Just a -> do
                let assigned = markedPlacesFromAssignment net a
110
111
                putStrLn "Assignment found"
                when verbose (putStrLn $ "Places marked: " ++ show assigned)
112
113
114
115
116
117
118
                rt <- checkSat $ checkTrapSat net assigned
                case rt of
                    Nothing -> do
                        putStrLn "No trap found."
                        return False
                    Just at -> do
                        let trap = trapFromAssignment at
119
120
121
                        putStrLn "Trap found"
                        when verbose (putStrLn $ "Places in trap: " ++ show trap)
                        checkSafetyProperty verbose net f (trap:traps)
122

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

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

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