Added printer for spec target

src/Main.hs

@@ -21,6 +21,7 @@ import PetriNet
 import Printer
 import qualified Printer.LOLA as LOLAPrinter
 import qualified Printer.SARA as SARAPrinter
+import qualified Printer.SPEC as SPECPrinter
 import Property
 import Solver
 import Solver.StateEquation
@@ -197,6 +198,12 @@ writeFiles verbosity basename net props = do
         verbosePut verbosity 1 $ "Writing properties to " ++ basename ++ ".sara"
         L.writeFile (basename ++ ".sara") $
             SARAPrinter.printProperties basename net props
+        mapM_ (\(p,i) -> do
+                let file = basename ++ ".target" ++ show i
+                verbosePut verbosity 1 $ "Writing " ++ showPropertyName p ++
+                                         " to " ++ file
+                L.writeFile file $ SPECPrinter.printProperty p
+              ) (zip props [(1::Integer)..])
 
 structuralAnalysis :: PetriNet -> IO ()
 structuralAnalysis net =  do
@@ -236,6 +243,7 @@ checkFile parser verbosity refine implicitProperties transformations
         case output of
             Just outputfile -> writeFiles verbosity outputfile net' props'''
             Nothing -> return ()
+        -- TODO: short-circuit?
         rs <- mapM (checkProperty verbosity net' refine) props'''
         verbosePut verbosity 0 ""
         return $ and rs
@@ -307,7 +315,7 @@ makeImplicitProperty net DeadlockFreeUnlessFinal =
 makeImplicitProperty net (Bounded k) =
         Property (show k ++ "-bounded") Safety $
             foldl (:|:) FFalse
-                (map (\p -> placeOp Gt (p,k))
+                (map (\p -> placeOp Ge (p,k+1))
                     (filter (`notElem` concatMap (post net) (ghostTransitions net))
                         (places net)))
 makeImplicitProperty net Safe =
@@ -406,11 +414,13 @@ main = do
                 rs <- mapM (checkFile parser verbosity refinement properties
                      transformations (optUseProperties opts) (optOutput opts)
                      (optPrintStructure opts)) files
+                -- TODO: short-circuit with Control.Monad.Loops?
                 if and rs then
                     exitSuccessWith "All properties satisfied."
                 else
                     exitFailureWith "Some properties may not be satisfied."
 
+-- TODO: Always exit with exit code 0 unless an error occured
 exitSuccessWith :: String -> IO ()
 exitSuccessWith msg = do
         putStrLn msg

src/Printer/LOLA.hs

@@ -52,6 +52,7 @@ renderLinIneq :: LinearInequation -> Builder
 renderLinIneq (LinIneq lhs op rhs) =
         renderTerm lhs <> renderOp op <> renderTerm rhs
 
+-- TODO: reduce parantheses in built formula
 renderFormula :: Formula -> Builder
 renderFormula FTrue = "TRUE"
 renderFormula FFalse = "FALSE"

src/Printer/SPEC.hs

+{-# 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
+