Main.hs 2.84 KB
Newer Older
1
2
module Main where

Philipp Meyer's avatar
Philipp Meyer committed
3
import System.Environment (getArgs)
4
import System.Exit
Philipp Meyer's avatar
Philipp Meyer committed
5

6
import qualified Data.Map as M
Philipp Meyer's avatar
Philipp Meyer committed
7
import Parser (parseFile)
8
9
import PetriNet
import Property
10
import Solver
11
12
import Solver.StateEquation
import Solver.TrapConstraints
13
14
import Solver.TransitionInvariant
import Solver.SComponent
15

16
17
checkSafetyProperty :: PetriNet -> Formula -> [[String]] -> IO Bool
checkSafetyProperty net f traps = do
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
        r <- checkSat $ checkStateEquationSat net f traps
        case r of
            Nothing -> return True
            Just a -> do
                let assigned = markedPlacesFromAssignment net a
                putStrLn $ "Assignment found marking " ++ show assigned
                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 with places " ++ show trap
                        checkSafetyProperty net f (trap:traps)
33

34
35
36
checkLivenessProperty :: PetriNet -> Formula -> [([String],[String])] -> IO Bool
checkLivenessProperty net f strans = do
        r <- checkSat $ checkTransitionInvariantSat net f strans
Philipp Meyer's avatar
Philipp Meyer committed
37
        case r of
38
            Nothing -> return True
39
40
            Just ax -> do
                let fired = firedTransitionsFromAssignment ax
41
                putStrLn $ "Assignment found firing " ++ show fired
42
                rt <- checkSat $ checkSComponentSat net ax
43
44
45
46
                case rt of
                    Nothing -> do
                        putStrLn "No S-component found"
                        return False
47
48
49
50
51
                    Just as -> do
                        let sOutIn = getSComponentInOut net ax as
                        putStrLn $ "S-component found: " ++ show (M.filter (> 0) as)
                        putStrLn $ "Out/In: " ++ show sOutIn
                        checkLivenessProperty net f (sOutIn:strans)
52
53
54

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

63
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
64
65
66
main = do
        args <- getArgs
        let file = head args
67
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
68
69
        putStrLn $ "Reading \"" ++ file ++ "\""
        (net,properties) <- parseFile file
70
        putStrLn $ "Analyzing " ++ showNetName net
71
        rs <- mapM (checkProperty net) properties
72
73
74
75
        if and rs then
            exitSuccess
        else
            exitWith $ ExitFailure 2
Philipp Meyer's avatar
Philipp Meyer committed
76