Main.hs 1.53 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
checkProperty :: PetriNet -> Property -> IO ()
11
checkProperty net p = do
Philipp Meyer's avatar
Philipp Meyer committed
12
        r <- checkPropertyConstraintsSat net p []
13
14
        case r of
            Nothing -> putStrLn "Property satisfied"
Philipp Meyer's avatar
Philipp Meyer committed
15
            Just m -> putStrLn "Property may not satisfied, model:" >> print m
Philipp Meyer's avatar
Philipp Meyer committed
16

Philipp Meyer's avatar
Philipp Meyer committed
17
18
19
20
21
22
23
24
25
26
27
28
29
30
checkPropertyWithTrapRefinement :: PetriNet -> Property -> [[String]] -> IO ()
checkPropertyWithTrapRefinement net p traps = do
        r <- checkPropertyConstraintsSat net p traps
        case r of
            Nothing -> putStrLn "Property satisfied"
            Just m -> do
                putStrLn "Property 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)
31

32
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
33
34
35
main = do
        args <- getArgs
        let file = head args
36
37
38
        putStrLn "Safety and Liveness Analysis of Petri Nets with SMT solvers"
        putStrLn $ "Reading \"" ++ file ++ "\""
        (net,properties) <- parseFile file
39
        putStrLn $ "Analyzing " ++ showName net
40
41
        mapM_ (\p -> do
                  putStrLn $ "Checking " ++ show p
Philipp Meyer's avatar
Philipp Meyer committed
42
                  checkPropertyWithTrapRefinement net p []
43
              ) properties
Philipp Meyer's avatar
Philipp Meyer committed
44