Main.hs 2.72 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 -> IO Bool
checkLivenessProperty net f = do
        r <- checkSat $ checkTransitionInvariantSat net f
Philipp Meyer's avatar
Philipp Meyer committed
36
        case r of
37
            Nothing -> return True
38
39
40
41
42
43
44
45
46
47
48
49
50
            Just a -> do
                let fired = firedTransitionsFromAssignment a
                putStrLn $ "Assignment found firing " ++ show fired
                rt <- checkSat $ checkSComponentSat net a
                case rt of
                    Nothing -> do
                        putStrLn "No S-component found"
                        return False
                    Just at -> do
                        --let trap = trapFromAssignment at
                        putStrLn $ "S-component found: " ++ show at
                        -- checkLivenessProperty net f (trap:traps)
                        return False
51
52
53

checkProperty :: PetriNet -> Property -> IO Bool
checkProperty net p = do
54
        putStrLn $ "\nChecking " ++ showPropertyName p
55
56
57
58
59
60
61
        r <- case ptype p of
            Safety -> checkSafetyProperty net (pformula p) []
            Liveness -> checkLivenessProperty net (pformula p)
        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