Commit fb53f0c5 authored by Philipp Meyer's avatar Philipp Meyer

Renamed .tasksara files to .sara

parent 8cb27ec5
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"
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