prism: Add tests for mcrl2 conversion

copar.cabal

@@ -280,6 +280,21 @@ executable prism-converter
                      , prettyprinter-ansi-terminal ^>= 1.1
                      , prettyprinter-convert-ansi-wl-pprint ^>= 1.1
                      , text ^>= 1.2.3
+  ghc-options:         -Wall
+  if !flag(benchmark-generators)
+    buildable:       False
+
+test-suite prism-converter-tests
+  type:                exitcode-stdio-1.0
+  hs-source-dirs:      src/prism-converter
+  main-is:             Tests.hs
+  default-language:    Haskell2010
+  build-depends:       base >= 4.11
+                     , hspec >= 2.6 && <2.8
+                     , microlens-platform ^>= 0.3.11
+                     , prism-converter-lib
+                     , vector ^>= 0.12.0.2
+  ghc-options:         -Wall
   if !flag(benchmark-generators)
     buildable:       False
 

src/prism-converter/Tests.hs

+{-# LANGUAGE OverloadedStrings #-}
+
+module Main (main) where
+
+import           Lens.Micro.Platform
+import           Test.Hspec
+import qualified Data.Vector                   as V
+
+import Mdp.Mcrl2
+import Mdp.Types
+
+main :: IO ()
+main = hspec $ do
+  convertToMcrlSpec
+
+convertToMcrlSpec :: Spec
+convertToMcrlSpec = describe "convertToMcrl" $ do
+  it "generates the correct number of states" $ do
+    let mdp = Mdp 4 1 mempty
+    let res = convertToMcrl mdp
+    res ^. numStates `shouldBe` mdp ^. numStates
+
+  it "generates a uniform initial distribution" $ do
+    let mdp = Mdp 4 1 mempty
+    let res = convertToMcrl mdp
+    res ^.. outDistribution . each . probability `shouldBe` (replicate 4 0.25)
+
+  it "generates the correct transition if there's only one" $ do
+    let mdp = Mdp 2 1 (V.singleton (Transition 0 0 1 1.0 Nothing))
+    let res = convertToMcrl mdp
+    let trans = Mcrl2Transition 0 "0" (V.singleton (Mcrl2PropTrans 1.0 1))
+    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 res = convertToMcrl mdp
+    let trans = Mcrl2Transition 0 "0" (V.fromList [Mcrl2PropTrans 0.5 1, 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 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]