Commit 9a88e665 authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Added structural output of number of places and transitions

parent abecc460
...@@ -187,6 +187,7 @@ parseArgs = do ...@@ -187,6 +187,7 @@ 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
-- TODO: add options for different outputs
verbosePut verbosity 1 $ "Writing " ++ showNetName net ++ " to " ++ basename verbosePut verbosity 1 $ "Writing " ++ showNetName net ++ " to " ++ basename
L.writeFile basename $ LOLAPrinter.printNet net L.writeFile basename $ LOLAPrinter.printNet net
mapM_ (\(p,i) -> do mapM_ (\(p,i) -> do
...@@ -198,12 +199,12 @@ writeFiles verbosity basename net props = do ...@@ -198,12 +199,12 @@ writeFiles verbosity basename net props = do
verbosePut verbosity 1 $ "Writing properties to " ++ basename ++ ".sara" verbosePut verbosity 1 $ "Writing properties to " ++ basename ++ ".sara"
L.writeFile (basename ++ ".sara") $ L.writeFile (basename ++ ".sara") $
SARAPrinter.printProperties basename net props SARAPrinter.printProperties basename net props
mapM_ (\(p,i) -> do --mapM_ (\(p,i) -> do
let file = basename ++ ".target" ++ show i -- let file = basename ++ ".target" ++ show i
verbosePut verbosity 1 $ "Writing " ++ showPropertyName p ++ -- verbosePut verbosity 1 $ "Writing " ++ showPropertyName p ++
" to " ++ file -- " to " ++ file
L.writeFile file $ SPECPrinter.printProperty p -- L.writeFile file $ SPECPrinter.printProperty p
) (zip props [(1::Integer)..]) -- ) (zip props [(1::Integer)..])
structuralAnalysis :: PetriNet -> IO () structuralAnalysis :: PetriNet -> IO ()
structuralAnalysis net = do structuralAnalysis net = do
...@@ -218,6 +219,8 @@ structuralAnalysis net = do ...@@ -218,6 +219,8 @@ structuralAnalysis net = do
(transitions net) (transitions net)
let finalT = filter (\t -> noGhost t && null (post net t)) let finalT = filter (\t -> noGhost t && null (post net t))
(transitions net) (transitions net)
putStrLn $ "Places : " ++ show (length (places net))
putStrLn $ "Transitions : " ++ show (length (transitions net))
putStrLn $ "Initial places : " ++ show (length initP) putStrLn $ "Initial places : " ++ show (length initP)
putStrLn $ "Initial transitions: " ++ show (length initT) putStrLn $ "Initial transitions: " ++ show (length initT)
putStrLn $ "Isolated places : " ++ show (length isolP) putStrLn $ "Isolated places : " ++ show (length isolP)
......
...@@ -37,14 +37,23 @@ renderLinIneq (LinIneq lhs op (Const c)) = ...@@ -37,14 +37,23 @@ renderLinIneq (LinIneq lhs op (Const c)) =
renderTerm lhs <> renderOp op <> integerDec c renderTerm lhs <> renderOp op <> integerDec c
renderLinIneq l = error $ "linear inequation not supported for sara: " <> show l renderLinIneq l = error $ "linear inequation not supported for sara: " <> show l
renderFormula :: Formula -> Builder renderConjunction :: Formula -> Builder
renderFormula (Atom a) = renderLinIneq a renderConjunction (Atom a) = renderLinIneq a
renderFormula (Neg _) = error "negation not supported for sara" renderConjunction (Neg _) = error "negation not supported for sara"
renderFormula (p :&: q) = renderFormula p <> "," <> renderFormula q renderConjunction (FTrue :&: p) = renderConjunction p
renderFormula f = error $ "formula not supported for sara: " <> show f renderConjunction (p :&: FTrue) = renderConjunction p
renderConjunction (p :&: q) = renderConjunction p <> ", " <> renderConjunction q
renderConjunction f = error $ "formula not supported for sara: " <> show f
renderProperty :: String -> PetriNet -> Property -> Builder renderDisjunction :: String -> String -> PetriNet -> Formula -> Builder
renderProperty filename net (Property propname Safety f) = renderDisjunction propname filename net (FFalse :|: p) =
renderDisjunction propname filename net p
renderDisjunction propname filename net (p :|: FFalse) =
renderDisjunction propname filename net p
renderDisjunction propname filename net (p :|: q) =
renderDisjunction propname filename net p <> "\n\n" <>
renderDisjunction propname filename net q
renderDisjunction propname filename net f =
"PROBLEM " <> stringUtf8 (validateId propname) <> ":\n" <> "PROBLEM " <> stringUtf8 (validateId propname) <> ":\n" <>
"GOAL REACHABILITY;\n" <> "GOAL REACHABILITY;\n" <>
"FILE " <> stringUtf8 (reverse (takeWhile (/='/') (reverse filename))) "FILE " <> stringUtf8 (reverse (takeWhile (/='/') (reverse filename)))
...@@ -53,7 +62,14 @@ renderProperty filename net (Property propname Safety f) = ...@@ -53,7 +62,14 @@ renderProperty filename net (Property propname Safety f) =
(map (\(p,i) -> stringUtf8 p <> ":" <> integerDec i) (initials net)) (map (\(p,i) -> stringUtf8 p <> ":" <> integerDec i) (initials net))
<> ";\n" <> <> ";\n" <>
"FINAL COVER;\n" <> "FINAL COVER;\n" <>
"CONSTRAINTS " <> renderFormula f <> ";" "CONSTRAINTS " <> renderConjunction f <> ";"
renderFormula :: String -> String -> PetriNet -> Formula -> Builder
renderFormula = renderDisjunction
renderProperty :: String -> PetriNet -> Property -> Builder
renderProperty filename net (Property propname Safety f) =
renderFormula propname filename net f
renderProperty _ _ (Property _ Liveness _) = renderProperty _ _ (Property _ Liveness _) =
error "liveness property not supported for sara" error "liveness property not supported for sara"
......
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