diff --git a/src/prism-converter/Mdp.hs b/src/prism-converter/Mdp.hs
index b118337bc8fe8e262f80acce8923c17f2505de69..91627285b7588a2edde64129a398f50a48a1491f 100644
--- a/src/prism-converter/Mdp.hs
+++ b/src/prism-converter/Mdp.hs
@@ -1,6 +1,10 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE FlexibleInstances #-}
 
 module Mdp (mdpP, mdpB, valmariMdpB) where
 
@@ -27,23 +31,22 @@ import           StatesFile                     ( Partition(..) )
 ----------------------------------------------------------------------
 
 data Mdp = Mdp
-  { _numStates :: Int
-  , _numChoices :: Int
-  , _transitions :: Vector Transition
+  { mdpNumStates :: Int
+  , mdpNumChoices :: Int
+  , mdpTransitions :: Vector Transition
   }
 
 -- TODO Support optional action label
 data Transition = Transition
-  { _source :: Int
-  , _choice :: Int
-  , _target :: Int
-  , _propability :: Double
-  , _action :: Maybe Text
+  { transitionSource :: Int
+  , transitionChoice :: Int
+  , transitionTarget :: Int
+  , transitionProbability :: Double
+  , transitionAction :: Maybe Text
   }
 
-makeLenses ''Mdp
-
-makeLenses ''Transition
+makeFields ''Mdp
+makeFields ''Transition
 
 ----------------------------------------------------------------------
 -- Parser
@@ -75,9 +78,9 @@ mdpB partition mdp =
   functorB partition <> "\n" <> transitionsB partition (mdp ^. transitions)
 
 functorB :: Maybe Partition -> Build.Builder
-functorB Nothing = "P(DX)\n"
+functorB Nothing = "P(Nx(DX))\n"
 functorB (Just partition) =
-  (Build.decimal (numBlocks partition)) <> " x P(DX)\n"
+  (Build.decimal (numBlocks partition)) <> " x P(Nx(DX))\n"
 
 transitionsB :: Maybe Partition -> Vector Transition -> Build.Builder
 transitionsB partition ts =
@@ -89,19 +92,17 @@ choicesB :: Maybe Partition -> Int -> [Transition] -> Build.Builder
 choicesB partition source ts
   = let choiceMap :: IntMap [Transition] =
           foldl' (\m t -> M.insertWith (++) (t ^. choice) [t] m) M.empty ts
-    in
-      stateB source
-      <> ": "
-      <> partStart partition
-      <> "{"
-      <> fold
-           (intersperse
-             ", "
-             (map (uncurry (transitionB source)) (M.toList choiceMap))
-           )
-      <> "}"
-      <> partEnd partition
-      <> "\n"
+    in  stateB source
+        <> ": "
+        <> partStart partition
+        <> "{"
+        <> fold
+             (intersperse ", "
+                          (map (uncurry transitionB) (M.toList choiceMap))
+             )
+        <> "}"
+        <> partEnd partition
+        <> "\n"
   where
     partStart Nothing = ""
     partStart (Just part) =
@@ -109,15 +110,19 @@ choicesB partition source ts
     partEnd Nothing  = ""
     partEnd (Just _) = ")"
 
-transitionB :: Int -> Int -> [Transition] -> Build.Builder
-transitionB _ _ successors =
-  "{" <> fold (intersperse ", " (map successorB successors)) <> "}"
+transitionB :: Int -> [Transition] -> Build.Builder
+transitionB choice successors =
+  "("
+    <> Build.decimal choice
+    <> ", {"
+    <> fold (intersperse ", " (map successorB successors))
+    <> "})"
   where
     successorB :: Transition -> Build.Builder
     successorB t = stateB (t ^. target) <> ": " <> Build.formatRealFloat
       Build.Fixed
       Nothing
-      (t ^. propability)
+      (t ^. probability)
 
 stateB :: Int -> Build.Builder
 stateB = ("s" <>) . Build.decimal
@@ -141,55 +146,59 @@ stateB = ("s" <>) . Build.decimal
 ----------------------------------------------------------------------
 
 data ValmariMDP = ValmariMDP
-  { _vNumStates :: Int
-  , _vNumActionStates :: Int
-  , _vNumChoices :: Int
-  , _vActions :: Vector (Vector Int) -- From normal states to list of actions
-  , _vProbablilities :: Vector (Vector ValmariTransition)
+  { valmariMDPNumStates :: Int
+  , valmariMDPNumActionStates :: Int
+  , valmariMDPNumChoices :: Int
+  , valmariMDPChoices :: Vector ValmariChoice
+  , valmariMDPProbabilities :: Vector ValmariTransition
   }
 
+data ValmariChoice = ValmariChoice
+  { _valmariChoiceSource :: Int
+  , _valmariChoiceChoice :: Int
+  , _valmariChoiceTarget :: Int
+  }
+
+
 -- From an action state to a normal state
 data ValmariTransition = ValmariTransition
-  { _vProbablility :: Double
-  , _vTarget :: Int
+  { _valmariTransitionSource :: Int
+  , _valmariTransitionProbability :: Double
+  , _valmariTransitionTarget :: Int
   }
 
-makeLenses ''ValmariMDP
-
-makeLenses ''ValmariTransition
+makeFields ''ValmariMDP
+makeFields ''ValmariChoice
+makeFields ''ValmariTransition
 
 type ValmariPartition = [[Int]]
 
 
 convertToValmari :: Maybe Partition -> Mdp -> (ValmariMDP, ValmariPartition)
-convertToValmari maybePart mdp
-  = let
-      nums             = mdp ^. numStates
+convertToValmari maybePart mdp =
+  let nums             = mdp ^. numStates
       (numa, transMap) = mkValmariMap mdp
       numc             = mdp ^. numChoices
-      actions =
-        V.fromList (M.elems transMap & each . each %~ fst & each %~ V.fromList)
-      probsMap = M.fromList
-        (  (transMap ^.. each . each)
-        &  (each . _2 . each)
-        %~ uncurry ValmariTransition
-        )
-      probabilities = V.generate numa $ \a -> V.fromList (probsMap M.! a)
-      part          = maybe [] partToBlocks maybePart
-    in
-      ( ValmariMDP
-        { _vNumStates       = nums
-        , _vNumActionStates = numa
-        , _vNumChoices      = numc
-        , _vActions         = actions
-        , _vProbablilities  = probabilities
+      actions          = V.fromList (concatMap mkChoices (M.toList transMap))
+      probs = V.fromList (concatMap mkTransitions (transMap ^.. each . each))
+      part             = maybe [] partToBlocks maybePart
+  in  ( ValmariMDP
+        { valmariMDPNumStates       = nums
+        , valmariMDPNumActionStates = numa
+        , valmariMDPChoices         = actions
+        , valmariMDPProbabilities   = probs
+        , valmariMDPNumChoices      = numc
         }
       , part
       )
+  where
+    mkChoices (s, cs) = map (mkChoice s) cs
+    mkChoice s (t, c) = ValmariChoice s (fst c) t
+    mkTransitions (s, (_, ts)) = map (uncurry (ValmariTransition s)) ts
 
 -- State -> Choices
--- each choice has many [(Probability, State)]
-type ValmariMap = IntMap [(Int, [(Double, Int)])]
+-- each choice is (choice state, choice number, [(probability, successor)])
+type ValmariMap = IntMap [(Int, (Int, [(Double, Int)]))]
 
 
 -- | Returns the total number of action states and the valmari map
@@ -206,12 +215,12 @@ mkValmariMap mdp = M.mapAccum uniquifyChoices
       m
         &  (at (t ^. source) . non M.empty)
         .  (at (t ^. choice) . non [])
-        %~ ((t ^. propability, t ^. target) :)
+        %~ ((t ^. probability, t ^. target) :)
 
     uniquifyChoices
-      :: Int -> IntMap [(Double, Int)] -> (Int, [(Int, [(Double, Int)])])
+      :: Int -> IntMap [(Double, Int)] -> (Int, [(Int, (Int, [(Double, Int)]))])
     uniquifyChoices current actions =
-      let newActions = zip [current ..] (M.elems actions)
+      let newActions = zip [current ..] (M.toList actions)
       in  (current + length newActions, newActions)
 
 
@@ -237,63 +246,55 @@ valmariMdpB partition mdp =
 
 valmariSizesB :: ValmariMDP -> ValmariPartition -> Build.Builder
 valmariSizesB mdp part =
-  Build.decimal (mdp ^. vNumStates + mdp ^. vNumActionStates)
+  Build.decimal (mdp ^. numStates + mdp ^. numActionStates)
     <> " "
-    <> Build.decimal (mdp ^. vNumChoices)
+    <> Build.decimal (mdp ^. numChoices)
     <> " "
-    <> Build.decimal (length (mdp ^. vActions))
+    <> Build.decimal (length (mdp ^. choices))
     <> " "
-    <> Build.decimal (length (mdp ^. vProbablilities))
+    <> Build.decimal (length (mdp ^. probabilities))
     <> " "
     <> Build.decimal (length part + 1)
 
 
 valmariLTransitions :: ValmariMDP -> Build.Builder
-valmariLTransitions mdp = foldMap (uncurry vChoices)
-                                  (zip [0 ..] (mdp ^.. vActions . each))
+valmariLTransitions mdp = foldMap vChoice (mdp ^.. choices . each)
   where
-    vChoices :: Int -> Vector Int -> Build.Builder
-    vChoices from subs =
-      foldMap (uncurry (vTrans from)) (zip [0 ..] (subs ^.. each))
-
-    vTrans :: Int -> Int -> Int -> Build.Builder
-    vTrans source choice target =
-      vState source
+    vChoice :: ValmariChoice -> Build.Builder
+    vChoice c =
+      vState (c ^. source)
         <> " "
-        <> Build.decimal (choice + 1)
+        <> Build.decimal (c ^. choice + 1)
         <> " "
-        <> vActionState mdp target
+        <> vActionState mdp (c ^. target)
         <> "\n"
 
-
 valmariWTransitions :: ValmariMDP -> Build.Builder
-valmariWTransitions mdp = foldMap
-  (uncurry vProps)
-  (zip [0 ..] (mdp ^.. vProbablilities . each))
-
+valmariWTransitions mdp = foldMap vTrans (mdp ^.. probabilities . each)
   where
-    vProps :: Int -> Vector ValmariTransition -> Build.Builder
-    vProps source trans = trans ^. each . to (vTrans source)
-
-    vTrans :: Int -> ValmariTransition -> Build.Builder
-    vTrans source t =
-      vActionState mdp source
+    vTrans :: ValmariTransition -> Build.Builder
+    vTrans t =
+      vActionState mdp (t ^. source)
         <> " "
-        <> Build.formatRealFloat Build.Fixed Nothing (t ^. vProbablility)
+        <> Build.formatRealFloat Build.Fixed Nothing (t ^. probability)
         <> " "
-        <> vState (t ^. vTarget)
+        <> vState (t ^. target)
         <> "\n"
 
+
 vState :: Int -> Build.Builder
-vState = Build.decimal . (+1)
+vState = Build.decimal . (+ 1)
+
 
 vActionState :: ValmariMDP -> Int -> Build.Builder
-vActionState mdp = Build.decimal . (+ (mdp^.vNumStates)) . (+1)
+vActionState mdp = Build.decimal . (+ (mdp ^. numStates)) . (+ 1)
 
 
 valmariBlocks :: [[Int]] -> Build.Builder
-valmariBlocks part = part & each.each %~ vState
-                          & each %~ intersperse " "
-                          & intersperse [" 0\n"]
-                          & concat
-                          & fold
+valmariBlocks part =
+  part
+    & (each . each %~ vState)
+    & (each %~ intersperse " ")
+    & (each %~ fold)
+    & (each %~ (<> " 0\n"))
+    & fold