The name of the initial branch for new projects is now "main" instead of "master". Existing projects remain unchanged. More information: https://doku.lrz.de/display/PUBLIC/GitLab

LOLA.hs 2.38 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 55 56 57 58 59 60 61 62 63 64 65
        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

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 _) =
66
        error "liveness property not supported for lola"
67 68 69

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