Commit 7071e249 authored by Hans-Peter Deifel's avatar Hans-Peter Deifel 🐢
Browse files

prism: Split up Mdp to allow for easier testing

parent 437ce601

copar.cabal

+3 −0
Original line number Diff line number Diff line
@@ -250,7 +250,9 @@ library prism-converter-lib 
  exposed-modules:     Parser

                     , MarkovChain

                     , Mdp

                     , Mdp.Types

                     , StatesFile

                     , Mdp.Mcrl2

  default-language:    Haskell2010

  build-depends:       base >= 4.11

                     , containers ^>= 0.6
@@ -261,6 +263,7 @@ library prism-converter-lib 
                     , text ^>= 1.2.3

                     , vector ^>= 0.12

                     , vector-algorithms ^>= 0.8.0.1

  ghc-options:         -Wall

  if !flag(benchmark-generators)

    buildable:       False

src/prism-converter/lib/Mdp.hs

+1 −93
Original line number Diff line number Diff line
@@ -11,7 +11,6 @@ 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
@@ -26,31 +25,10 @@ import Data.Text ( Text ) 
import qualified Data.Text                     as T

import           Lens.Micro.Platform



import           Mdp.Types

import           Parser

import           StatesFile                     ( Partition(..) )



----------------------------------------------------------------------

-- Types

----------------------------------------------------------------------



data Mdp = Mdp

  { mdpNumStates :: Int

  , mdpNumChoices :: Int

  , mdpTransitions :: Vector Transition

  } deriving (Show)



-- TODO Support optional action label

data Transition = Transition

  { transitionSource :: Int

  , transitionChoice :: Int

  , transitionTarget :: Int

  , transitionProbability :: Double

  , transitionAction :: Maybe Text

  } deriving (Show)



makeFields ''Mdp

makeFields ''Transition



----------------------------------------------------------------------

-- Parser

----------------------------------------------------------------------
@@ -345,73 +323,3 @@ valmariBlocks part = 
    & (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

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

0 → 100644
+102 −0
Original line number Diff line number Diff line 
{-# LANGUAGE TemplateHaskell #-}

{-# LANGUAGE FlexibleContexts #-}

{-# LANGUAGE MultiParamTypeClasses #-}

{-# LANGUAGE FunctionalDependencies #-}

{-# LANGUAGE FlexibleInstances #-}



module Mdp.Mcrl2

  ( Mcrl2Mdp(Mcrl2Mdp)

  , Mcrl2Transition(Mcrl2Transition)

  , Mcrl2Distribution

  , Mcrl2PropTrans(Mcrl2PropTrans)

  , numStates

  , transitions

  , outDistribution

  , source

  , label

  , probability

  , target

  , convertToMcrl

  ) where



import           Data.Ord



import           Lens.Micro.Platform

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           Mdp.Types



----------------------------------------------------------------------

-- 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, Eq)



type Mcrl2Distribution = Vector Mcrl2PropTrans



data Mcrl2PropTrans = Mcrl2PropTrans

  { mcrl2PropTransProbability :: Double

  , mcrl2PropTransTarget :: Int

  } deriving (Show, Eq)



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)) initDistri

  where

    initDistri = V.fromList $

      map (Mcrl2PropTrans (1.0/(fromIntegral $ mdp ^. numStates)))

          [0 .. mdp ^. numStates - 1]





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





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 p = V.unfoldr helper

  where

    helper vec

      | null vec  = Nothing

      | otherwise = Just $ V.span (((p (V.head vec)) ==) . p) vec

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

0 → 100644
+50 −0
Original line number Diff line number Diff line 
{-# LANGUAGE TemplateHaskell #-}

{-# LANGUAGE FlexibleContexts #-}

{-# LANGUAGE MultiParamTypeClasses #-}

{-# LANGUAGE FunctionalDependencies #-}

{-# LANGUAGE FlexibleInstances #-}



module Mdp.Types

  ( Mdp(Mdp)

  , Transition(Transition)

  , numStates

  , numChoices

  , transitions

  , source

  , choice

  , target

  , probability

  , action

  , HasNumStates

  , HasNumChoices

  , HasTransitions

  , HasSource

  , HasChoice

  , HasTarget

  , HasProbability

  , HasAction

  ) 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

  { mdpNumStates :: Int

  , mdpNumChoices :: Int

  , mdpTransitions :: Vector Transition

  } deriving (Show)



-- TODO Support optional action label

data Transition = Transition

  { transitionSource :: Int

  , transitionChoice :: Int

  , transitionTarget :: Int

  , transitionProbability :: Double

  , transitionAction :: Maybe Text

  } deriving (Show)



makeFields ''Mdp

makeFields ''Transition