Main.hs 2.23 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
12
import Solver.StateEquation
import Solver.TransitionInvariant
import Solver.TrapConstraints
13

14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
checkSafetyProperty :: PetriNet -> Formula -> [[String]] -> IO Bool
checkSafetyProperty net f traps = do
    r <- checkSat $ checkStateEquationSat net f traps
    case r of
        Nothing -> return True
        Just a -> do
            --print a
            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)

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
Philipp Meyer's avatar
Philipp Meyer committed
38
            Just m -> do
39
40
41
42
43
44
45
46
47
48
49
50
51
52
                putStrLn "Assignment found:"
                print m
                return False


checkProperty :: PetriNet -> Property -> IO Bool
checkProperty net p = do
        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

53
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
54
55
56
main = do
        args <- getArgs
        let file = head args
57
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
58
59
        putStrLn $ "Reading \"" ++ file ++ "\""
        (net,properties) <- parseFile file
60
61
62
63
64
65
66
67
68
        putStrLn $ "Analyzing " ++ showNetName net
        rs <- mapM (\p -> do
                      putStrLn $ "\nChecking " ++ showPropertyName p
                      checkProperty net p
                  ) properties
        if and rs then
            exitSuccess
        else
            exitWith $ ExitFailure 2
Philipp Meyer's avatar
Philipp Meyer committed
69