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

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

import Parser (parseFile)
6
7
import PetriNet
import Property
8
import Solver
9
10
11
import Solver.StateEquation
import Solver.TransitionInvariant
import Solver.TrapConstraints
12

13
14
-- TODO: check type of property and only do trap refinement for safety
-- properties
Philipp Meyer's avatar
Philipp Meyer committed
15

16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
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
38
        case r of
39
            Nothing -> return True
Philipp Meyer's avatar
Philipp Meyer committed
40
            Just m -> do
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
                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

--checkPropertyWithTrapRefinement :: PetriNet -> Property -> [[String]] -> IO ()
--checkPropertyWithTrapRefinement net p traps = do
--        r <- checkPropertyConstraintsSat net p traps
--        case r of
--            Nothing -> putStrLn "Property is satisfied"
--            Just m -> do
--                putStrLn "Property may not satisfied, model:" >> print m
--                r2 <- checkTrapConstraintsSat net m
--                case r2 of
--                    Nothing -> putStrLn "No trap found"
--                    Just m2 -> do
--                        let trap = map fst $ filter snd m2
--                        putStrLn "Trap found:" >> print trap
--                        checkPropertyWithTrapRefinement net p (trap:traps)
69

70
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
71
72
73
main = do
        args <- getArgs
        let file = head args
74
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
75
76
        putStrLn $ "Reading \"" ++ file ++ "\""
        (net,properties) <- parseFile file
77
        putStrLn $ "Analyzing " ++ showName net
78
        mapM_ (\p -> do
79
80
                  putStrLn $ "\nChecking " ++ show p
                  checkProperty net p
81
              ) properties
Philipp Meyer's avatar
Philipp Meyer committed
82