Paramterize Mdp by weight type (e3e3d22b) · Commits · Software / CoPaR

src/prism-converter/Main.hs

+1 −3

Original line number	Diff line number	Diff line
		@@ -7,12 +7,10 @@ module Main (main) where

		import System.IO
		import System.Exit
		import Data.Semigroup
		import Control.Applicative
		import Data.Maybe (fromMaybe)

		import Data.Set (Set)
		import qualified Data.Set as S
		import Data.Text (Text)
		import qualified Data.Text as T
		import qualified Data.Text.IO as T
		@@ -162,7 +160,7 @@ main = do
		Left err -> do
		hPutStrLn stderr $ "error while parsing --partition-on-variables: " <> T.unpack err
		exitFailure
		Right vars -> return (Just (computePartition sf vars))
		Right vs -> return (Just (computePartition sf vs))
		_ -> return Nothing

		case (optModelType opts, optOutputFormat opts) of

src/prism-converter/lib/Mdp.hs

+17 −17

Original line number	Diff line number	Diff line
		@@ -31,15 +31,15 @@ import qualified Mdp.Mcrl2 as Mcrl2
		-- Parser
		----------------------------------------------------------------------

		mdpP :: Parser Mdp
		mdpP :: Parser (Mdp Double)
		mdpP = Mdp <$> decimalP <> decimalP <> transitionsP

		transitionsP :: Parser (Vector Transition)
		transitionsP :: Parser (Vector (Transition Double))
		transitionsP = do
		numTrans <- decimalP
		V.replicateM numTrans transitionP

		transitionP :: Parser Transition
		transitionP :: Parser (Transition Double)
		transitionP =
		Transition
		<$> decimalP
		@@ -52,7 +52,7 @@ transitionP =
		-- Builder
		----------------------------------------------------------------------

		mdpB :: Maybe Partition -> Mdp -> Build.Builder
		mdpB :: Maybe Partition -> (Mdp Double) -> Build.Builder
		mdpB partition mdp =
		functorB partition <> "\n" <> transitionsB partition (mdp ^. transitions)

		@@ -61,15 +61,15 @@ functorB Nothing = "P(Nx(DX))\n"
		functorB (Just partition) =
		(Build.decimal (numBlocks partition)) <> " x P(Nx(DX))\n"

		transitionsB :: Maybe Partition -> Vector Transition -> Build.Builder
		transitionsB :: Maybe Partition -> Vector (Transition Double) -> Build.Builder
		transitionsB partition ts =
		let stateMap :: IntMap [Transition] =
		let stateMap :: IntMap [(Transition Double)] =
		V.foldl' (\m t -> M.insertWith (++) (t ^. source) [t] m) M.empty ts
		in foldMap (uncurry (choicesB partition)) (M.toList stateMap)

		choicesB :: Maybe Partition -> Int -> [Transition] -> Build.Builder
		choicesB :: Maybe Partition -> Int -> [(Transition Double)] -> Build.Builder
		choicesB partition src ts =
		let choiceMap :: IntMap [Transition] =
		let choiceMap :: IntMap [(Transition Double)] =
		foldl' (\m t -> M.insertWith (++) (t ^. choice) [t] m) M.empty ts
		in stateB src
		<> ": "
		@@ -87,7 +87,7 @@ choicesB partition src ts =
		partEnd Nothing = ""
		partEnd (Just _) = ")"

		transitionB :: Int -> [Transition] -> Build.Builder
		transitionB :: Int -> [(Transition Double)] -> Build.Builder
		transitionB choi successors =
		"("
		<> Build.decimal choi
		@@ -95,7 +95,7 @@ transitionB choi successors =
		<> fold (intersperse ", " (map successorB successors))
		<> "})"
		where
		successorB :: Transition -> Build.Builder
		successorB :: (Transition Double) -> Build.Builder
		successorB t = stateB (t ^. target) <> ": " <> Build.formatRealFloat
		Build.Fixed
		Nothing
		@@ -151,7 +151,7 @@ makeFields ''ValmariTransition
		type ValmariPartition = [[Int]]


		convertToValmari :: Maybe Partition -> Mdp -> (ValmariMDP, ValmariPartition)
		convertToValmari :: Maybe Partition -> (Mdp Double) -> (ValmariMDP, ValmariPartition)
		convertToValmari maybePart mdp =
		let nums = mdp ^. numStates
		(numa, transMap) = mkValmariMap mdp
		@@ -178,7 +178,7 @@ convertToValmari maybePart mdp =
		-- \| Alternative method of modeling the same coalgebra. Here, we don't use
		-- labels but partition the Distribution states on the label that leads to them.
		-- This models the functor P(AxDX) more faithfully.
		convertToValmari2 :: Maybe Partition -> Mdp -> (ValmariMDP, ValmariPartition)
		convertToValmari2 :: Maybe Partition -> (Mdp Double) -> (ValmariMDP, ValmariPartition)
		convertToValmari2 maybePart mdp =
		let
		nums = mdp ^. numStates
		@@ -211,14 +211,14 @@ type ValmariMap = IntMap [(Int, (Int, [(Double, Int)]))]


		-- \| Returns the total number of action states and the valmari map
		mkValmariMap :: Mdp -> (Int, ValmariMap)
		mkValmariMap :: (Mdp Double) -> (Int, ValmariMap)
		mkValmariMap mdp = M.mapAccum uniquifyChoices
		0
		(V.foldl' ins M.empty (mdp ^. transitions))
		where
		ins
		:: IntMap (IntMap [(Double, Int)])
		-> Transition
		-> (Transition Double)
		-> IntMap (IntMap [(Double, Int)])
		ins m t =
		m
		@@ -241,13 +241,13 @@ partToBlocks p =
		in M.elems blockMap


		valmariMdpB :: Maybe Partition -> Mdp -> Build.Builder
		valmariMdpB :: Maybe Partition -> (Mdp Double) -> Build.Builder
		valmariMdpB partition mdp =
		let (vmdp, vpartition) = convertToValmari partition mdp
		in valmariMdpBImpl vmdp vpartition


		valmariMdp2B :: Maybe Partition -> Mdp -> Build.Builder
		valmariMdp2B :: Maybe Partition -> (Mdp Double) -> Build.Builder
		valmariMdp2B partition mdp =
		let (vmdp, vpartition) = convertToValmari2 partition mdp
		in valmariMdpBImpl vmdp vpartition
		@@ -326,5 +326,5 @@ valmariBlocks part =

		-- TODO Support partition

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

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

+4 −4

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

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


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


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


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

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

+4 −6

Original line number	Diff line number	Diff line
		@@ -26,23 +26,21 @@ module Mdp.Types
		) where

		import Data.Vector ( Vector )
		import qualified Data.Vector as V
		import Data.Text ( Text )
		import qualified Data.Text as T
		import Lens.Micro.Platform

		data Mdp = Mdp
		data Mdp p = Mdp
		{ mdpNumStates :: Int
		, mdpNumChoices :: Int
		, mdpTransitions :: Vector Transition
		, mdpTransitions :: Vector (Transition p)
		} deriving (Show)

		-- TODO Support optional action label
		data Transition = Transition
		data Transition p = Transition
		{ transitionSource :: Int
		, transitionChoice :: Int
		, transitionTarget :: Int
		, transitionProbability :: Double
		, transitionProbability :: p
		, transitionAction :: Maybe Text
		} deriving (Show)