Main.hs 899 Bytes
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
12
        r <- checkPropertyConstraintsSat net p
13
14
15
        case r of
            Nothing -> putStrLn "Property satisfied"
            Just m -> putStrLn "Property not satisfied, model:" >> print m
Philipp Meyer's avatar
Philipp Meyer committed
16

17
18
--checkPropertyWithTrapRefinement :: PetriNet -> Property -> IO ()

19
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
20
21
22
main = do
        args <- getArgs
        let file = head args
23
24
25
        putStrLn "Safety and Liveness Analysis of Petri Nets with SMT solvers"
        putStrLn $ "Reading \"" ++ file ++ "\""
        (net,properties) <- parseFile file
26
        putStrLn $ "Analyzing " ++ showName net
27
28
        mapM_ (\p -> do
                  putStrLn $ "Checking " ++ show p
29
                  checkProperty net p
30
              ) properties
Philipp Meyer's avatar
Philipp Meyer committed
31