Commit c51c68df authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Made output much faster by using byte string builders

parent f0373636
...@@ -21,6 +21,8 @@ executable slapnet ...@@ -21,6 +21,8 @@ executable slapnet
main-is: Main.hs main-is: Main.hs
other-modules: other-modules:
-- other-extensions: -- other-extensions:
build-depends: base >=4 && <5, sbv, parsec, containers, transformers build-depends: base >=4 && <5, sbv, parsec, containers, transformers,
bytestring
hs-source-dirs: src hs-source-dirs: src
default-language: Haskell2010 default-language: Haskell2010
ghc-options: -fsimpl-tick-factor=1000
...@@ -10,6 +10,7 @@ import Control.Monad ...@@ -10,6 +10,7 @@ import Control.Monad
import Control.Applicative ((<$>)) import Control.Applicative ((<$>))
import Control.Arrow (first) import Control.Arrow (first)
import Data.List (partition) import Data.List (partition)
import qualified Data.ByteString.Lazy as L
import Parser import Parser
import qualified Parser.PNET as PNET import qualified Parser.PNET as PNET
...@@ -180,16 +181,16 @@ parseArgs = do ...@@ -180,16 +181,16 @@ parseArgs = do
writeFiles :: Int -> String -> PetriNet -> [Property] -> IO () writeFiles :: Int -> String -> PetriNet -> [Property] -> IO ()
writeFiles verbosity basename net props = do writeFiles verbosity basename net props = do
verbosePut verbosity 1 $ "Writing " ++ showNetName net ++ " to " ++ basename verbosePut verbosity 1 $ "Writing " ++ showNetName net ++ " to " ++ basename
writeFile basename $ LOLAPrinter.printNet net L.writeFile basename $ LOLAPrinter.printNet net
mapM_ (\(p,i) -> do mapM_ (\(p,i) -> do
let file = basename ++ ".task" ++ show i let file = basename ++ ".task" ++ show i
verbosePut verbosity 1 $ "Writing " ++ showPropertyName p ++ verbosePut verbosity 1 $ "Writing " ++ showPropertyName p ++
" to " ++ file " to " ++ file
writeFile file $ LOLAPrinter.printProperty p L.writeFile file $ LOLAPrinter.printProperty p
) (zip props [(1::Integer)..]) ) (zip props [(1::Integer)..])
verbosePut verbosity 1 $ "Writing properties to " ++ basename ++ ".sara" verbosePut verbosity 1 $ "Writing properties to " ++ basename ++ ".sara"
writeFile (basename ++ ".sara") $ unlines $ L.writeFile (basename ++ ".sara") $
map (SARAPrinter.printProperty basename net) props SARAPrinter.printProperties basename net props
checkFile :: Parser (PetriNet,[Property]) -> Int -> Bool -> checkFile :: Parser (PetriNet,[Property]) -> Int -> Bool ->
[ImplicitProperty] -> [NetTransformation] -> [ImplicitProperty] -> [NetTransformation] ->
...@@ -206,10 +207,10 @@ checkFile parser verbosity refine implicitProperties transformations ...@@ -206,10 +207,10 @@ checkFile parser verbosity refine implicitProperties transformations
"Places: " ++ show (length $ places net') ++ "; " ++ "Places: " ++ show (length $ places net') ++ "; " ++
"Transitions: " ++ show (length $ transitions net') "Transitions: " ++ show (length $ transitions net')
verbosePut verbosity 3 $ show net' verbosePut verbosity 3 $ show net'
rs <- mapM (checkProperty verbosity net' refine) props'''
case output of case output of
Just outputfile -> writeFiles verbosity outputfile net' props''' Just outputfile -> writeFiles verbosity outputfile net' props'''
Nothing -> return () Nothing -> return ()
rs <- mapM (checkProperty verbosity net' refine) props'''
verbosePut verbosity 0 "" verbosePut verbosity 0 ""
return $ and rs return $ and rs
......
module Printer module Printer
(validateId) (validateId,intercalate)
where where
import Data.Char import Data.Char
import Data.ByteString.Builder
import Data.Monoid
validateId :: String -> String validateId :: String -> String
validateId "" = "_" validateId "" = "_"
validateId (x:xs) = (if isAlpha x then x else '_') : validateId (x:xs) = (if isAlpha x then x else '_') :
map (\c -> if isAlphaNum c then c else '_') xs map (\c -> if isAlphaNum c then c else '_') xs
intercalate :: Builder -> [Builder] -> Builder
intercalate _ [] = mempty
intercalate sep (x:xs) = x <> go xs
where go = foldr (\y -> (<>) (sep <> y)) mempty
{-# LANGUAGE OverloadedStrings #-}
module Printer.LOLA module Printer.LOLA
(printNet,printProperty) (printNet,printProperty)
where where
import Data.List (intercalate) import qualified Data.ByteString.Lazy as L
import Data.ByteString.Builder
import Data.Monoid
import Printer
import PetriNet import PetriNet
import Property import Property
printNet :: PetriNet -> String renderNet :: PetriNet -> Builder
printNet net = renderNet net =
let showWeight (p,x) = p ++ ":" ++ show x let showWeight (p,x) = stringUtf8 p <> ":" <> integerDec x
ps = "PLACE " ++ intercalate "," (places net) ++ ";\n" ps = "PLACE " <> intercalate ","
is = "MARKING " ++ intercalate "," (map stringUtf8 (places net)) <> ";\n"
(map showWeight (initials net)) ++ ";\n" is = "MARKING " <> intercalate ","
(map showWeight (initials net)) <> ";\n"
makeTransition t = makeTransition t =
let (preT,postT) = context net t let (preT,postT) = context net t
preS = "CONSUME " ++ intercalate "," preS = "CONSUME " <> intercalate ","
(map showWeight preT) ++ ";\n" (map showWeight preT) <> ";\n"
postS = "PRODUCE " ++ intercalate "," postS = "PRODUCE " <> intercalate ","
(map showWeight postT) ++ ";\n" (map showWeight postT) <> ";\n"
in "TRANSITION " ++ t ++ "\n" ++ preS ++ postS in "TRANSITION " <> stringUtf8 t <> "\n" <> preS <> postS
ts = map makeTransition (transitions net) ts = map makeTransition (transitions net)
in unlines (ps:is:ts) in intercalate "\n" (ps:is:ts)
printTerm :: Term -> String printNet :: PetriNet -> L.ByteString
printTerm (Var x) = x printNet = toLazyByteString . renderNet
printTerm (Const c) = show c
printTerm (Minus t) = "-" ++ printTerm t renderTerm :: Term -> Builder
printTerm (t :+: u) = "(" ++ printTerm t ++ " + " ++ printTerm u ++ ")" renderTerm (Var x) = stringUtf8 x
printTerm (t :-: u) = "(" ++ printTerm t ++ " - " ++ printTerm u ++ ")" renderTerm (Const c) = integerDec c
printTerm (t :*: u) = printTerm t ++ " * " ++ printTerm u renderTerm (Minus t) = "-" <> renderTerm t
renderTerm (t :+: u) = "(" <> renderTerm t <> " + " <> renderTerm u <> ")"
printOp :: Op -> String renderTerm (t :-: u) = "(" <> renderTerm t <> " - " <> renderTerm u <> ")"
printOp Gt = " > " renderTerm (t :*: u) = renderTerm t <> " * " <> renderTerm u
printOp Ge = " >= "
printOp Eq = " = " renderOp :: Op -> Builder
printOp Ne = " != " renderOp Gt = " > "
printOp Le = " <= " renderOp Ge = " >= "
printOp Lt = " < " renderOp Eq = " = "
renderOp Ne = " != "
printLinIneq :: LinearInequation -> String renderOp Le = " <= "
printLinIneq (LinIneq lhs op rhs) = printTerm lhs ++ printOp op ++ printTerm rhs renderOp Lt = " < "
printFormula :: Formula -> String renderLinIneq :: LinearInequation -> Builder
printFormula FTrue = "TRUE" renderLinIneq (LinIneq lhs op rhs) =
printFormula FFalse = "FALSE" renderTerm lhs <> renderOp op <> renderTerm rhs
printFormula (Atom a) = printLinIneq a
printFormula (Neg p) = "NOT " ++ "(" ++ printFormula p ++ ")" renderFormula :: Formula -> Builder
printFormula (p :&: q) = printFormula p ++ " AND " ++ printFormula q renderFormula FTrue = "TRUE"
printFormula (p :|: q) = "(" ++ printFormula p ++ " OR " ++ printFormula q ++ ")" renderFormula FFalse = "FALSE"
renderFormula (Atom a) = renderLinIneq a
printProperty :: Property -> String renderFormula (Neg p) = "NOT " <> "(" <> renderFormula p <> ")"
printProperty (Property _ Safety f) = "EF (" ++ printFormula f ++ ")\n" renderFormula (p :&: q) = renderFormula p <> " AND " <> renderFormula q
printProperty (Property _ Liveness _) = renderFormula (p :|: q) = "(" <> renderFormula p <> " OR " <> renderFormula q <> ")"
renderProperty :: Property -> Builder
renderProperty (Property _ Safety f) = "EF (" <> renderFormula f <> ")\n"
renderProperty (Property _ Liveness _) =
error "liveness property not supported for lola" error "liveness property not supported for lola"
printProperty :: Property -> L.ByteString
printProperty = toLazyByteString . renderProperty
{-# LANGUAGE OverloadedStrings #-}
module Printer.SARA module Printer.SARA
(printProperty) (printProperties)
where where
import Data.List (intercalate) import qualified Data.ByteString.Lazy as L
import Data.ByteString.Builder
import Data.Monoid
import Printer import Printer
import PetriNet import PetriNet
import Property import Property
printSimpleTerm :: Integer -> Term -> String renderSimpleTerm :: Integer -> Term -> Builder
printSimpleTerm fac (Var x) = if fac == 1 then x else show fac ++ x renderSimpleTerm fac (Var x) = if fac == 1 then stringUtf8 x
printSimpleTerm fac (Const c) = show (fac*c) else integerDec fac <> stringUtf8 x
printSimpleTerm fac (Const c :*: t) = printSimpleTerm (fac*c) t renderSimpleTerm fac (Const c) = integerDec (fac*c)
printSimpleTerm fac (t :*: Const c) = printSimpleTerm (fac*c) t renderSimpleTerm fac (Const c :*: t) = renderSimpleTerm (fac*c) t
printSimpleTerm fac (Minus t) = printSimpleTerm (-fac) t renderSimpleTerm fac (t :*: Const c) = renderSimpleTerm (fac*c) t
printSimpleTerm _ t = error $ "term not supported for sara: " ++ show t renderSimpleTerm fac (Minus t) = renderSimpleTerm (-fac) t
renderSimpleTerm _ t = error $ "term not supported for sara: " <> show t
printTerm :: Term -> String
printTerm (t :+: u) = printTerm t ++ "+" ++ printSimpleTerm 1 u renderTerm :: Term -> Builder
printTerm (t :-: u) = printTerm t ++ "+" ++ printSimpleTerm (-1) u renderTerm (t :+: u) = renderTerm t <> "+" <> renderSimpleTerm 1 u
printTerm t = printSimpleTerm 1 t renderTerm (t :-: u) = renderTerm t <> "+" <> renderSimpleTerm (-1) u
renderTerm t = renderSimpleTerm 1 t
printOp :: Op -> String
printOp Ge = ">" renderOp :: Op -> Builder
printOp Eq = ":" renderOp Ge = ">"
printOp Le = "<" renderOp Eq = ":"
printOp op = error $ "operand not supported for sara: " ++ show op renderOp Le = "<"
renderOp op = error $ "operand not supported for sara: " <> show op
printLinIneq :: LinearInequation -> String
printLinIneq (LinIneq lhs op (Const c)) = printTerm lhs ++ printOp op ++ show c renderLinIneq :: LinearInequation -> Builder
printLinIneq l = error $ "linear inequation not supported for sara: " ++ show l renderLinIneq (LinIneq lhs op (Const c)) =
renderTerm lhs <> renderOp op <> integerDec c
printFormula :: Formula -> String renderLinIneq l = error $ "linear inequation not supported for sara: " <> show l
printFormula (Atom a) = printLinIneq a
printFormula (Neg _) = error "negation not supported for sara" renderFormula :: Formula -> Builder
printFormula (p :&: q) = printFormula p ++ "," ++ printFormula q renderFormula (Atom a) = renderLinIneq a
printFormula f = error $ "formula not supported for sara: " ++ show f renderFormula (Neg _) = error "negation not supported for sara"
renderFormula (p :&: q) = renderFormula p <> "," <> renderFormula q
printProperty :: String -> PetriNet -> Property -> String renderFormula f = error $ "formula not supported for sara: " <> show f
printProperty filename net (Property propname Safety f) =
"PROBLEM " ++ validateId propname ++ ":\n" ++ renderProperty :: String -> PetriNet -> Property -> Builder
"GOAL REACHABILITY;\n" ++ renderProperty filename net (Property propname Safety f) =
"FILE " ++ reverse (takeWhile (/='/') (reverse filename)) ++ "PROBLEM " <> stringUtf8 (validateId propname) <> ":\n" <>
" TYPE LOLA;\n" ++ "GOAL REACHABILITY;\n" <>
"INITIAL " ++ intercalate "," "FILE " <> stringUtf8 (reverse (takeWhile (/='/') (reverse filename)))
(map (\(p,i) -> p ++ ":" ++ show i) (initials net)) ++ ";\n" ++ <> " TYPE LOLA;\n" <>
"FINAL COVER;\n" ++ "INITIAL " <> intercalate ","
"CONSTRAINTS " ++ printFormula f ++ ";" (map (\(p,i) -> stringUtf8 p <> ":" <> integerDec i) (initials net))
printProperty _ _ (Property _ Liveness _) = <> ";\n" <>
"FINAL COVER;\n" <>
"CONSTRAINTS " <> renderFormula f <> ";"
renderProperty _ _ (Property _ Liveness _) =
error "liveness property not supported for sara" error "liveness property not supported for sara"
printProperties :: String -> PetriNet -> [Property] -> L.ByteString
printProperties filename net props =
toLazyByteString $ intercalate "\n" $
map (renderProperty filename net) props
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment