From 1363ee6d8273b7a1b5227f0fb6020122b1a219df Mon Sep 17 00:00:00 2001 From: Philipp Meyer Date: Tue, 15 Jul 2014 14:55:10 +0200 Subject: [PATCH] Added output of petri net and formula in lola format --- src/Main.hs | 32 ++++++++++++++++++++++++++--- src/Printer.hs | 55 ++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 84 insertions(+), 3 deletions(-) create mode 100644 src/Printer.hs diff --git a/src/Main.hs b/src/Main.hs index 49437149..b95d60a1 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -15,6 +15,7 @@ import qualified Parser.PNET as PNET import qualified Parser.LOLA as LOLA import qualified Parser.TPN as TPN import PetriNet +import Printer import Property import Solver import Solver.StateEquation @@ -39,6 +40,7 @@ data Options = Options { inputFormat :: InputFormat , optProperties :: [ImplicitProperty] , optTransformations :: [NetTransformation] , optRefine :: Bool + , optOutput :: Maybe String } startOptions :: Options @@ -49,6 +51,7 @@ startOptions = Options { inputFormat = PNET , optProperties = [] , optTransformations = [] , optRefine = True + , optOutput = Nothing } options :: [ OptDescr (Options -> Either String Options) ] @@ -115,6 +118,13 @@ options = (NoArg (\opt -> Right opt { optRefine = False })) "Don't use refinement" + , Option "o" ["output"] + (ReqArg (\arg opt -> Right opt { + optOutput = Just arg + }) + "FILE") + "Write net and properties to FILE" + , Option "v" ["verbose"] (NoArg (\opt -> Right opt { optVerbosity = optVerbosity opt + 1 })) "Increase verbosity (may be specified more than once)" @@ -144,9 +154,22 @@ parseArgs = do return $ (,files) <$> foldl (>>=) (return startOptions) actions (_, _, errs) -> return $ Left $ concat errs +writeFiles :: Int -> String -> PetriNet -> [Property] -> IO () +writeFiles verbosity basename net props = do + verbosePut verbosity 1 $ "Writing " ++ showNetName net ++ " to " ++ basename + writeFile basename $ printNet net + mapM_ (\(p,i) -> do + let file = basename ++ ".task" ++ show i + verbosePut verbosity 1 $ "Writing " ++ showPropertyName p ++ + " to " ++ file + writeFile file $ printProperty p + ) (zip props [(1::Integer)..]) + checkFile :: Parser (PetriNet,[Property]) -> Int -> Bool -> - [ImplicitProperty] -> [NetTransformation] -> String -> IO Bool -checkFile parser verbosity refine implicitProperties transformations file = do + [ImplicitProperty] -> [NetTransformation] -> + Maybe String -> String -> IO Bool +checkFile parser verbosity refine implicitProperties transformations + output file = do verbosePut verbosity 0 $ "Reading \"" ++ file ++ "\"" (net,props) <- parseFile parser file let props' = props ++ map (makeImplicitProperty net) implicitProperties @@ -157,6 +180,9 @@ checkFile parser verbosity refine implicitProperties transformations file = do "Transitions: " ++ show (length $ transitions net') verbosePut verbosity 3 $ show net' rs <- mapM (checkProperty verbosity net' refine) props'' + case output of + Just outputfile -> writeFiles verbosity outputfile net' props'' + Nothing -> return () verbosePut verbosity 0 "" return $ and rs @@ -305,7 +331,7 @@ main = do let properties = reverse $ optProperties opts let transformations = reverse $ optTransformations opts rs <- mapM (checkFile parser verbosity refinement properties - transformations) files + transformations (optOutput opts)) files if and rs then exitSuccessWith "All properties satisfied." else diff --git a/src/Printer.hs b/src/Printer.hs new file mode 100644 index 00000000..11c78e20 --- /dev/null +++ b/src/Printer.hs @@ -0,0 +1,55 @@ +module Printer + (printNet,printProperty) +where + +import Data.List (intercalate) + +import PetriNet +import Property + +printNet :: PetriNet -> String +printNet net = + let showWeight (p,x) = p ++ ":" ++ show x + ps = "PLACE " ++ intercalate "," (places net) ++ ";\n" + is = "MARKING " ++ intercalate "," + (map showWeight (initials net)) ++ ";\n" + makeTransition t = + let (preT,postT) = context net t + preS = "CONSUME " ++ intercalate "," + (map showWeight preT) ++ ";\n" + postS = "PRODUCE " ++ intercalate "," + (map showWeight postT) ++ ";\n" + in "TRANSITION " ++ t ++ "\n" ++ preS ++ postS + ts = map makeTransition (transitions net) + in unlines (ps:is:ts) + +printTerm :: Term -> String +printTerm (Var x) = x +printTerm (Const c) = show c +printTerm (Minus t) = "-" ++ printTerm t +printTerm (t :+: u) = "(" ++ printTerm t ++ " + " ++ printTerm u ++ ")" +printTerm (t :-: u) = "(" ++ printTerm t ++ " - " ++ printTerm u ++ ")" +printTerm (t :*: u) = printTerm t ++ " * " ++ printTerm u + +printOp :: Op -> String +printOp Gt = " > " +printOp Ge = " >= " +printOp Eq = " = " +printOp Ne = " != " +printOp Le = " <= " +printOp Lt = " < " + +printLinIneq :: LinearInequation -> String +printLinIneq (LinIneq lhs op rhs) = printTerm lhs ++ printOp op ++ printTerm rhs + +printFormula :: Formula -> String +printFormula FTrue = "TRUE" +printFormula FFalse = "FALSE" +printFormula (Atom a) = printLinIneq a +printFormula (Neg p) = "NOT " ++ "(" ++ printFormula p ++ ")" +printFormula (p :&: q) = "(" ++ printFormula p ++ " AND " ++ printFormula q ++ ")" +printFormula (p :|: q) = "(" ++ printFormula p ++ " OR " ++ printFormula q ++ ")" + +printProperty :: Property -> String +printProperty (Property _ Safety f) = "EF (" ++ printFormula f ++ ")\n" +printProperty (Property _ Liveness _) = error "Liveness property not supported" -- GitLab