Main.hs 812 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
12
checkProperty net p = do
        r <- checkSat 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
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
18
19
20
main = do
        args <- getArgs
        let file = head args
21
22
23
        putStrLn "Safety and Liveness Analysis of Petri Nets with SMT solvers"
        putStrLn $ "Reading \"" ++ file ++ "\""
        (net,properties) <- parseFile file
24
        putStrLn $ "Analyzing " ++ showName net
25
26
        mapM_ (\p -> do
                  putStrLn $ "Checking " ++ show p
27
                  checkProperty net p
28
              ) properties
Philipp Meyer's avatar
Philipp Meyer committed
29