Added problem output for lola and sara

src/Main.hs

@@ -17,6 +17,8 @@ import qualified Parser.LOLA as LOLA
 import qualified Parser.TPN as TPN
 import PetriNet
 import Printer
+import qualified Printer.LOLA as LOLAPrinter
+import qualified Printer.SARA as SARAPrinter
 import Property
 import Solver
 import Solver.StateEquation
@@ -165,13 +167,16 @@ parseArgs = do
 writeFiles :: Int -> String -> PetriNet -> [Property] -> IO ()
 writeFiles verbosity basename net props = do
         verbosePut verbosity 1 $ "Writing " ++ showNetName net ++ " to " ++ basename
-        writeFile basename $ printNet net
+        writeFile basename $ LOLAPrinter.printNet net
         mapM_ (\(p,i) -> do
                 let file = basename ++ ".task" ++ show i
                 verbosePut verbosity 1 $ "Writing " ++ showPropertyName p ++
                                          " to " ++ file
-                writeFile file $ printProperty p
+                writeFile file $ LOLAPrinter.printProperty p
               ) (zip props [(1::Integer)..])
+        verbosePut verbosity 1 $ "Writing properties to " ++ basename ++ ".sara"
+        writeFile (basename ++ ".sara") $ unlines $
+                map (SARAPrinter.printProperty basename net) props
 
 checkFile :: Parser (PetriNet,[Property]) -> Int -> Bool ->
             [ImplicitProperty] -> [NetTransformation] ->
@@ -222,13 +227,12 @@ transformNet (net, props) TerminationByReachability =
             -- TODO: map existing liveness properties
         in  (makePetriNetWithTrans (name net) ps ts is, prop : props)
 transformNet (net, props) ValidateIdentifiers =
-        let validate = map (\c -> if c `elem` ",;:(){}\t \n\r" then '_' else c)
-            ps = map validate $ places net
-            ts = map validate $ transitions net
-            is = map (first validate) $ initials net
-            as = map (\(a,b,x) -> (validate a, validate b, x)) $ arcs net
+        let ps = map validateId $ places net
+            ts = map validateId $ transitions net
+            is = map (first validateId) $ initials net
+            as = map (\(a,b,x) -> (validateId a, validateId b, x)) $ arcs net
             net' = makePetriNet (name net) ps ts as is
-            props' = map (rename validate) props
+            props' = map (rename validateId) props
         in  (net', props')
 
 makeImplicitProperty :: PetriNet -> ImplicitProperty -> Property

src/Printer.hs

+module Printer
+    (validateId)
+where
+
+validateId :: String -> String
+validateId = map (\c -> if c `elem` ",;:(){}\t \n\r" then '_' else c)

src/Printer/LOLA.hs

+module Printer.LOLA
+    (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 for lola"

src/Printer/SARA.hs

+module Printer.SARA
+    (printProperty)
+where
+
+import Data.List (intercalate)
+
+import Printer
+import PetriNet
+import Property
+
+printSimpleTerm :: Integer -> Term -> String
+printSimpleTerm fac (Var x) = if fac == 1 then x else show fac ++ x
+printSimpleTerm fac (Const c) = show (fac*c)
+printSimpleTerm fac (Const c :*: t) = printSimpleTerm (fac*c) t
+printSimpleTerm fac (t :*: Const c) = printSimpleTerm (fac*c) t
+printSimpleTerm fac (Minus t) = printSimpleTerm (-fac) t
+printSimpleTerm _ t = error $ "term not supported for sara: " ++ show t
+
+printTerm :: Term -> String
+printTerm (t :+: u) = printTerm t ++ "+" ++ printSimpleTerm 1 u
+printTerm (t :-: u) = printTerm t ++ "+" ++ printSimpleTerm (-1) u
+printTerm t = printSimpleTerm 1 t
+
+printOp :: Op -> String
+printOp Ge = ">"
+printOp Eq = ":"
+printOp Le = "<"
+printOp op = error $ "operand not supported for sara: " ++ show op
+
+printLinIneq :: LinearInequation -> String
+printLinIneq (LinIneq lhs op (Const c)) = printTerm lhs ++ printOp op ++ show c
+printLinIneq l = error $ "linear inequation not supported for sara: " ++ show l
+
+printFormula :: Formula -> String
+printFormula (Atom a) = printLinIneq a
+printFormula (Neg _) = error "negation not supported for sara"
+printFormula (p :&: q) = printFormula p ++ "," ++ printFormula q
+printFormula f = error $ "formula not supported for sara: " ++ show f
+
+printProperty :: String -> PetriNet -> Property -> String
+printProperty filename net (Property propname Safety f) =
+        "PROBLEM " ++ validateId propname ++ ":\n" ++
+        "GOAL REACHABILITY;\n" ++
+        "FILE " ++ filename ++ " TYPE LOLA;\n" ++
+        "INITIAL " ++ intercalate ","
+            (map (\(p,i) -> p ++ ":" ++ show i) (initials net)) ++ ";\n" ++
+        "FINAL COVER;\n" ++
+        "CONSTRAINTS " ++ printFormula f ++ ";"
+printProperty _ _ (Property _ Liveness _) =
+        error "liveness property not supported for sara"