11.3.2021, 9:00 - 11:00: Due to updates GitLab may be unavailable for some minutes between 09:00 and 11:00.

LOLA.hs 2.42 KB
Newer Older
1 2
{-# LANGUAGE OverloadedStrings #-}

3 4 5 6
module Printer.LOLA
    (printNet,printProperty)
where

7 8 9
import qualified Data.ByteString.Lazy as L
import Data.ByteString.Builder
import Data.Monoid
10

11
import Printer
12 13 14
import PetriNet
import Property

15 16 17 18 19 20 21
renderNet :: PetriNet -> Builder
renderNet net =
        let showWeight (p,x) = stringUtf8 p <> ":" <> integerDec x
            ps = "PLACE " <> intercalate ","
                    (map stringUtf8 (places net)) <> ";\n"
            is = "MARKING " <> intercalate ","
                    (map showWeight (initials net)) <> ";\n"
22 23
            makeTransition t =
                let (preT,postT) = context net t
24 25 26 27 28
                    preS = "CONSUME " <> intercalate ","
                                (map showWeight preT) <> ";\n"
                    postS = "PRODUCE " <> intercalate ","
                                (map showWeight postT) <> ";\n"
                in  "TRANSITION " <> stringUtf8 t <> "\n" <> preS <> postS
29
            ts = map makeTransition (transitions net)
30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54
        in  intercalate "\n" (ps:is:ts)

printNet :: PetriNet -> L.ByteString
printNet = toLazyByteString . renderNet

renderTerm :: Term -> Builder
renderTerm (Var x) = stringUtf8 x
renderTerm (Const c) = integerDec c
renderTerm (Minus t) = "-" <> renderTerm t
renderTerm (t :+: u) = "(" <> renderTerm t <> " + " <> renderTerm u <> ")"
renderTerm (t :-: u) = "(" <> renderTerm t <> " - " <> renderTerm u <> ")"
renderTerm (t :*: u) = renderTerm t <> " * " <> renderTerm u

renderOp :: Op -> Builder
renderOp Gt = " > "
renderOp Ge = " >= "
renderOp Eq = " = "
renderOp Ne = " != "
renderOp Le = " <= "
renderOp Lt = " < "

renderLinIneq :: LinearInequation -> Builder
renderLinIneq (LinIneq lhs op rhs) =
        renderTerm lhs <> renderOp op <> renderTerm rhs

Philipp Meyer's avatar
Philipp Meyer committed
55
-- TODO: reduce parantheses in built formula
56 57 58 59 60 61 62 63 64 65 66
renderFormula :: Formula -> Builder
renderFormula FTrue = "TRUE"
renderFormula FFalse = "FALSE"
renderFormula (Atom a) = renderLinIneq a
renderFormula (Neg p) = "NOT " <> "(" <> renderFormula p <> ")"
renderFormula (p :&: q) = renderFormula p <> " AND " <> renderFormula q
renderFormula (p :|: q) = "(" <> renderFormula p <> " OR " <> renderFormula q <> ")"

renderProperty :: Property -> Builder
renderProperty (Property _ Safety f) = "EF (" <> renderFormula f <> ")\n"
renderProperty (Property _ Liveness _) =
67
        error "liveness property not supported for lola"
68 69 70

printProperty :: Property -> L.ByteString
printProperty = toLazyByteString . renderProperty