Output true rationals in mcrl2 builder (41bb81a8) · Commits · Software / CoPaR

src/prism-converter/Tests.hs

+2 −2

Original line number	Diff line number	Diff line
		@@ -50,10 +50,10 @@ 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
		let res = "des (0 1/2 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"
		let res = "des (0 1/2 1,1,2)\n(0,\"0\",0 1/2 1)\n"
		(Build.toLazyText (mcrl2B (convertToMcrl mdp)) ^. strict) `shouldBe` res

src/prism-converter/lib/Mdp.hs

+1 −1

Original line number	Diff line number	Diff line
		@@ -326,5 +326,5 @@ valmariBlocks part =

		-- TODO Support partition

		mcrl2B :: Mdp Double -> Build.Builder
		mcrl2B :: Mdp Rational -> Build.Builder
		mcrl2B = Mcrl2.mcrl2B . Mcrl2.convertToMcrl

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

+11 −8

Original line number	Diff line number	Diff line
		@@ -23,6 +23,7 @@ module Mdp.Mcrl2

		import Data.Ord
		import Control.Arrow ((&&&))
		import Data.Ratio

		import Lens.Micro.Platform
		import Data.Vector ( Vector )
		@@ -32,8 +33,6 @@ 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

		@@ -62,7 +61,7 @@ data Mcrl2Transition = Mcrl2Transition
		type Mcrl2Distribution = Vector Mcrl2PropTrans

		data Mcrl2PropTrans = Mcrl2PropTrans
		{ mcrl2PropTransProbability :: Double
		{ mcrl2PropTransProbability :: Rational
		, mcrl2PropTransTarget :: Int
		} deriving (Show, Eq)

		@@ -75,7 +74,7 @@ makeFields ''Mcrl2PropTrans
		-- doesn't correspond to the actual prism model. Maybe we should provide a
		-- uniform initial distribution over all states.

		convertToMcrl :: Mdp Double -> Mcrl2Mdp
		convertToMcrl :: Mdp Rational -> Mcrl2Mdp
		convertToMcrl mdp = Mcrl2Mdp (mdp ^. numStates) (convertTransitionsToMcrl (mdp^.transitions)) initDistri
		where
		initDistri = V.fromList $
		@@ -83,7 +82,7 @@ convertToMcrl mdp = Mcrl2Mdp (mdp ^. numStates) (convertTransitionsToMcrl (mdp^.
		[0 .. mdp ^. numStates - 1]


		convertTransitionsToMcrl :: Vector (Transition Double) -> Vector Mcrl2Transition
		convertTransitionsToMcrl :: Vector (Transition Rational) -> Vector Mcrl2Transition
		convertTransitionsToMcrl trans = mkMcrl2Tans <$> partitionVector (view source &&& view choice) sorted
		where
		sorted = V.create $ do
		@@ -92,12 +91,12 @@ convertTransitionsToMcrl trans = mkMcrl2Tans <$> partitionVector (view source &&
		return v


		mkMcrl2Tans :: Vector (Transition Double) -> Mcrl2Transition
		mkMcrl2Tans :: Vector (Transition Rational) -> Mcrl2Transition
		mkMcrl2Tans distri = Mcrl2Transition (h ^. source) (T.pack $ show $ h ^. choice) (mkPropTrans <$> distri)
		where h = V.head distri


		mkPropTrans :: (Transition Double) -> Mcrl2PropTrans
		mkPropTrans :: (Transition Rational) -> Mcrl2PropTrans
		mkPropTrans t = Mcrl2PropTrans (t ^. probability) (t ^. target)


		@@ -143,7 +142,7 @@ distributionB distri = foldMap (\x -> propTransB x <> " ") (V.init distri)

		propTransB :: Mcrl2PropTrans -> Build.Builder
		propTransB t = Build.decimal (t ^. target) <> " "
		<> Build.formatRealFloat Build.Fixed Nothing (t ^. probability)
		<> ratioB (t ^. probability)


		transitionB :: Mcrl2Transition -> Build.Builder
		@@ -151,3 +150,7 @@ transitionB t = "(" <> Build.decimal (t ^. source) <> ","
		<> "\"" <> Build.fromText (t ^. label)
		<> "\"," <> distributionB (t ^. outDistribution)
		<> ")\n"


		ratioB :: Rational -> Build.Builder
		ratioB r = Build.decimal (numerator r) <> "/" <> Build.decimal (denominator r)