prism: Add output for mcrl2 format

src/prism-converter/Mdp.hs

@@ -11,6 +11,7 @@ module Mdp (mdpP, mdpB, valmariMdpB, valmariMdp2B) where
 import           Data.List                      ( intersperse )
 import           Data.Foldable
 import           Control.Applicative
+import           Data.Ord
 
 import           Data.IntMap                    ( IntMap )
 import qualified Data.IntMap                   as M
@@ -20,7 +21,9 @@ import qualified Data.Text.Lazy.Builder.RealFloat
                                                as Build
 import           Data.Vector                    ( Vector )
 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           Lens.Micro.Platform
 
 import           Parser
@@ -341,3 +344,74 @@ valmariBlocks part =
     & (each %~ fold)
     & (each %~ (<> " 0\n"))
     & fold
+
+----------------------------------------------------------------------
+-- Builder for .aut-Format used in mcrl2
+--
+-- This format is informally:
+--
+-- des (initial distribution, nr transitions, nr states)
+-- (state, "label", out distribution)
+-- ...
+----------------------------------------------------------------------
+
+data Mcrl2Mdp = Mcrl2Mdp
+  { mcrl2MdpNumStates :: Int
+  , mcrl2MdpTransitions :: Vector Mcrl2Transition
+  , mcrl2MdpOutDistribution :: Mcrl2Distribution
+  } deriving (Show)
+
+data Mcrl2Transition = Mcrl2Transition
+  { mcrl2TransitionSource :: Int
+  , mcrl2TransitionLabel :: Text
+  , mcrl2TransitionOutDistribution :: Mcrl2Distribution
+  } deriving (Show)
+
+type Mcrl2Distribution = Vector Mcrl2PropTrans
+
+data Mcrl2PropTrans = Mcrl2PropTrans
+  { mcrl2PropTransProbability :: Double
+  , mcrl2PropTransTarget :: Int
+  } deriving (Show)
+
+makeFields ''Mcrl2Mdp
+makeFields ''Mcrl2Transition
+makeFields ''Mcrl2PropTrans
+
+
+-- TODO Fix initial state: For now the initial state is always 0, but that
+-- doesn't correspond to the actual prism model. Maybe we should provide a
+-- uniform initial distribution over all states.
+
+convertToMcrl :: Mdp -> Mcrl2Mdp
+convertToMcrl mdp = Mcrl2Mdp (mdp ^. numStates) (convertTransitionsToMcrl (mdp^.transitions)) (pure initEdge)
+  where
+    initEdge = Mcrl2PropTrans 1.0 0
+
+
+convertTransitionsToMcrl :: Vector Transition -> Vector Mcrl2Transition
+convertTransitionsToMcrl trans = mkMcrl2Tans <$> partitionVector (view source) sorted
+  where
+    sorted = V.create $ do
+      v <- V.thaw trans -- TODO Maybe use unsafe thaw
+      V.sortBy (comparing $ view source) v
+      return v
+
+    shouldGroup t = (t^.source, t^.choice)
+
+
+mkMcrl2Tans :: Vector Transition -> Mcrl2Transition
+mkMcrl2Tans distri = Mcrl2Transition (h ^. source) (T.pack $ show $ h ^. choice) (mkPropTrans <$> distri)
+  where h = V.head distri
+
+
+mkPropTrans :: Transition -> Mcrl2PropTrans
+mkPropTrans t = Mcrl2PropTrans (t ^. probability) (t ^. target)
+
+
+partitionVector :: Eq b => (a -> b) -> Vector a -> Vector (Vector a)
+partitionVector pred = V.unfoldr helper
+  where
+    helper vec
+      | null vec  = Nothing
+      | otherwise = Just $ V.span (((pred (V.head vec)) ==) . pred) vec