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

SPEC.hs 1.56 KB
Newer Older
Philipp Meyer's avatar
Philipp Meyer committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47
{-# LANGUAGE OverloadedStrings #-}

module Printer.SPEC
    (printProperty)
where

import qualified Data.ByteString.Lazy as L
import Data.ByteString.Builder
import Data.Monoid

import Property

renderOp :: Op -> Builder
renderOp Ge = ">="
renderOp op = error $ "operand not supported for spec: " <> show op

renderLinIneq :: LinearInequation -> Builder
renderLinIneq (LinIneq (Var x) op (Const c)) =
        stringUtf8 x <> renderOp op <> integerDec c
renderLinIneq l = error $ "linear inequation not supported for spe: " <> show l

renderConjunction :: Formula -> Builder
renderConjunction (Atom a) = renderLinIneq a
renderConjunction (Neg _) = error "negation not supported for spec"
renderConjunction (FTrue :&: p) = renderConjunction p
renderConjunction (p :&: FTrue) = renderConjunction p
renderConjunction (p :&: q) = renderConjunction p <> ", " <> renderConjunction q
renderConjunction f = error $ "formula not supported for spec: " <> show f

renderDisjunction :: Formula -> Builder
renderDisjunction (FFalse :|: p) = renderDisjunction p
renderDisjunction (p :|: FFalse) = renderDisjunction p
renderDisjunction (p :|: q) = renderDisjunction p <> "\n" <> renderDisjunction q
renderDisjunction f = renderConjunction f

renderFormula :: Formula -> Builder
renderFormula = renderDisjunction

renderProperty :: Property -> Builder
renderProperty (Property _ Safety f) = renderFormula f
renderProperty (Property _ Liveness _) =
        error "liveness property not supported for spec"

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