Implement Builder

copar.cabal

@@ -294,6 +294,7 @@ test-suite prism-converter-tests
                      , microlens-platform ^>= 0.3.11
                      , prism-converter-lib
                      , vector ^>= 0.12.0.2
+                     , text ^>= 1.2.3
   ghc-options:         -Wall
   if !flag(benchmark-generators)
     buildable:       False

src/prism-converter/Tests.hs

@@ -5,6 +5,7 @@ module Main (main) where
 import           Lens.Micro.Platform
 import           Test.Hspec
 import qualified Data.Vector                   as V
+import qualified Data.Text.Lazy.Builder        as Build
 
 import Mdp.Mcrl2
 import Mdp.Types
@@ -12,6 +13,7 @@ import Mdp.Types
 main :: IO ()
 main = hspec $ do
   convertToMcrlSpec
+  mcrl2BSpec
 
 convertToMcrlSpec :: Spec
 convertToMcrlSpec = describe "convertToMcrl" $ do
@@ -32,14 +34,26 @@ convertToMcrlSpec = describe "convertToMcrl" $ do
     res ^? transitions . ix 0 `shouldBe` Just trans
 
   it "generates one out-distribution for two transitions with same label" $ do
-    let mdp = Mdp 2 1 (V.fromList [Transition 0 0 1 0.5 Nothing, Transition 0 0 1 0.5 Nothing])
+    let mdp = Mdp 2 1 (V.fromList [Transition 0 0 0 0.5 Nothing, Transition 0 0 1 0.5 Nothing])
     let res = convertToMcrl mdp
-    let trans = Mcrl2Transition 0 "0" (V.fromList [Mcrl2PropTrans 0.5 1, Mcrl2PropTrans 0.5 1])
+    let trans = Mcrl2Transition 0 "0" (V.fromList [Mcrl2PropTrans 0.5 0, Mcrl2PropTrans 0.5 1])
     res ^? transitions . ix 0 `shouldBe` Just trans
 
   it "generates two two distinct transitions for two transitions with different label" $ do
-    let mdp = Mdp 2 1 (V.fromList [Transition 0 0 1 1.0 Nothing, Transition 0 1 1 1.0 Nothing])
+    let mdp = Mdp 2 2 (V.fromList [Transition 0 0 1 1.0 Nothing, Transition 0 1 1 1.0 Nothing])
     let res = convertToMcrl mdp
     let trans1 = Mcrl2Transition 0 "0" (V.singleton (Mcrl2PropTrans 1.0 1))
     let trans2 = Mcrl2Transition 0 "1" (V.singleton (Mcrl2PropTrans 1.0 1))
     res ^.. transitions . traverse `shouldBe` [trans1, trans2]
+
+mcrl2BSpec :: Spec
+mcrl2BSpec = describe "mcrl2BSpec" $ do
+  it "works for an example" $ do
+    let mdp = Mdp 2 2 (V.fromList [Transition 0 0 1 1.0 Nothing, Transition 0 1 1 1.0 Nothing])
+    let res = "des (0 0.5 1,2,2)\n(0,\"0\",1)\n(0,\"1\",1)\n" -- FIXME Rationals
+    (Build.toLazyText (mcrl2B (convertToMcrl mdp)) ^. strict) `shouldBe` res
+
+  it "works for another example" $ do
+    let mdp = Mdp 2 1 (V.fromList [Transition 0 0 0 0.5 Nothing, Transition 0 0 1 0.5 Nothing])
+    let res = "des (0 0.5 1,1,2)\n(0,\"0\",0 0.5 1)\n"
+    (Build.toLazyText (mcrl2B (convertToMcrl mdp)) ^. strict) `shouldBe` res

src/prism-converter/lib/Mdp.hs

@@ -6,7 +6,7 @@
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE FlexibleInstances #-}
 
-module Mdp (mdpP, mdpB, valmariMdpB, valmariMdp2B) where
+module Mdp (mdpP, mdpB, valmariMdpB, valmariMdp2B, mcrl2B) where
 
 import           Data.List                      ( intersperse )
 import           Data.Foldable
@@ -25,6 +25,7 @@ import           Lens.Micro.Platform
 import           Mdp.Types
 import           Parser
 import           StatesFile                     ( Partition(..) )
+import qualified Mdp.Mcrl2                     as Mcrl2
 
 ----------------------------------------------------------------------
 -- Parser
@@ -319,3 +320,11 @@ valmariBlocks part =
     & (each %~ (<> " 0\n"))
     & fold
 
+----------------------------------------------------------------------
+-- mcrl2
+----------------------------------------------------------------------
+
+-- TODO Support partition
+
+mcrl2B :: Mdp -> Build.Builder
+mcrl2B = Mcrl2.mcrl2B . Mcrl2.convertToMcrl

src/prism-converter/lib/Mdp/Mcrl2.hs

@@ -3,6 +3,7 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE OverloadedStrings #-}
 
 module Mdp.Mcrl2
   ( Mcrl2Mdp(Mcrl2Mdp)
@@ -17,6 +18,7 @@ module Mdp.Mcrl2
   , probability
   , target
   , convertToMcrl
+  , mcrl2B
   ) where
 
 import           Data.Ord
@@ -28,6 +30,10 @@ import qualified Data.Vector                   as V
 import qualified Data.Vector.Algorithms.Intro  as V
 import           Data.Text                      ( Text )
 import qualified Data.Text                     as T
+import qualified Data.Text.Lazy.Builder        as Build
+import qualified Data.Text.Lazy.Builder.Int    as Build
+import qualified Data.Text.Lazy.Builder.RealFloat
+                                               as Build
 
 import           Mdp.Types
 
@@ -101,3 +107,47 @@ partitionVector p = V.unfoldr helper
     helper vec
       | null vec  = Nothing
       | otherwise = Just $ V.span (((p (V.head vec)) ==) . p) vec
+
+----------------------------------------------------------------------
+-- Pretty Printer
+--
+-- The format is something like the following:
+--
+-- des (1 1/4 2 1/4 3 1/4 0,240,240)
+-- (0,"step",5 1/4 6 1/4 7 1/4 4)
+-- (1,"step",9 1/4 10 1/4 11 1/4 8)
+-- (2,"step",13 1/4 14 1/4 15 1/4 12)
+-- (3,"step",17 1/4 18 1/4 19 1/4 16)
+-- (4,"step",21 1/4 22 1/4 23 1/4 20)
+-- (5,"step",1 1/4 2 1/4 3 1/4 0)
+-- ...
+----------------------------------------------------------------------
+
+-- TODO Rationals!!!
+mcrl2B :: Mcrl2Mdp -> Build.Builder
+mcrl2B mdp =
+  "des ("
+    <> distributionB (mdp ^. outDistribution)
+    <> ","
+    <> Build.decimal (mdp ^. transitions . to length)
+    <> ","
+    <> Build.decimal (mdp ^. numStates)
+    <> ")\n"
+    <> foldMap transitionB (mdp^.transitions)
+
+
+distributionB :: Mcrl2Distribution -> Build.Builder
+distributionB distri = foldMap (\x -> propTransB x <> " ") (V.init distri)
+  <> Build.decimal (V.last distri ^. target)
+
+
+propTransB :: Mcrl2PropTrans -> Build.Builder
+propTransB t = Build.decimal (t ^. target) <> " "
+  <> Build.formatRealFloat Build.Fixed Nothing (t ^. probability)
+
+
+transitionB :: Mcrl2Transition -> Build.Builder
+transitionB t = "(" <> Build.decimal (t ^. source) <> ","
+  <> "\"" <> Build.fromText (t ^. label)
+  <> "\"," <> distributionB (t ^. outDistribution)
+  <> ")\n"