Main.hs 2.82 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 Parser (parseFile)
7
8
import PetriNet
import Property
9
import Solver
10
11
import Solver.StateEquation
import Solver.TrapConstraints
12
13
import Solver.TransitionInvariant
import Solver.SComponent
14

15
16
checkSafetyProperty :: PetriNet -> Formula -> [[String]] -> IO Bool
checkSafetyProperty net f traps = do
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
        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)
32

33
34
35
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
36
        case r of
37
            Nothing -> return True
38
39
            Just ax -> do
                let fired = firedTransitionsFromAssignment ax
40
                putStrLn $ "Assignment found firing " ++ show fired
41
                rt <- checkSat $ checkSComponentSat net fired ax
42
43
44
45
                case rt of
                    Nothing -> do
                        putStrLn "No S-component found"
                        return False
46
47
                    Just as -> do
                        let sOutIn = getSComponentInOut net ax as
48
                        putStrLn $ "S-component found: " ++ show (mElemsWith (> 0) as)
49
50
                        putStrLn $ "Out/In: " ++ show sOutIn
                        checkLivenessProperty net f (sOutIn:strans)
51
52
53

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

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