Commit 4c0692d7 authored by Hans-Peter Deifel's avatar Hans-Peter Deifel
Browse files

prism-converter: Implement valmari format for MDPs

parent 1c2c76d1
......@@ -237,3 +237,6 @@ executable prism-converter
, prettyprinter
, prettyprinter-ansi-terminal
, prettyprinter-convert-ansi-wl-pprint
, microlens
, microlens-th
, microlens-platform
......@@ -164,10 +164,11 @@ main = do
_ -> return Nothing
case (optModelType opts, optOutputFormat opts) of
(MDP, Ma) -> convert opts mdpP (mdpB initPartition)
(MDP, Valmari) -> do
hPutStrLn stderr "error: Output format 'valmari' not implemented for MDPs"
exitFailure
(MDP, outType) ->
let builder = case outType of
Valmari -> valmariMdpB
Ma -> mdpB
in convert opts mdpP (builder initPartition)
(inType, outType) ->
let mcType =
case inType of
......
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell #-}
module Mdp
( mdpP
, mdpB
) where
module Mdp (mdpP, mdpB, valmariMdpB) where
import Data.Semigroup
import Data.List (intersperse)
import Data.List ( intersperse )
import Data.Foldable
import Control.Applicative
import Data.IntMap (IntMap)
import qualified Data.IntMap as M
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 Data.Vector (Vector)
import qualified Data.Vector as V
import Data.Text (Text)
import qualified Data.Text as T
import Data.IntMap ( IntMap )
import qualified Data.IntMap as M
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 Data.Vector ( Vector )
import qualified Data.Vector as V
import Data.Text ( Text )
import Lens.Micro.Platform
import Parser
import StatesFile (Partition(..))
import StatesFile ( Partition(..) )
----------------------------------------------------------------------
-- Types
----------------------------------------------------------------------
data Mdp = Mdp
{ numStates :: Int
, numChoices :: Int
, transitions :: Vector Transition
{ _numStates :: Int
, _numChoices :: Int
, _transitions :: Vector Transition
}
-- TODO Support optional action label
data Transition = Transition
{ from :: Int
, choice :: Int
, to :: Int
, propability :: Double
, action :: Maybe Text
{ _source :: Int
, _choice :: Int
, _target :: Int
, _propability :: Double
, _action :: Maybe Text
}
makeLenses ''Mdp
makeLenses ''Transition
----------------------------------------------------------------------
-- Parser
----------------------------------------------------------------------
......@@ -56,12 +58,13 @@ transitionsP = do
V.replicateM numTrans transitionP
transitionP :: Parser Transition
transitionP = Transition
<$> decimalP
<*> decimalP
<*> decimalP
<*> doubleP
<*> optional nameP
transitionP =
Transition
<$> decimalP
<*> decimalP
<*> decimalP
<*> doubleP
<*> optional nameP
----------------------------------------------------------------------
-- Builder
......@@ -69,36 +72,41 @@ transitionP = Transition
mdpB :: Maybe Partition -> Mdp -> Build.Builder
mdpB partition mdp =
functorB partition <> "\n" <> transitionsB partition (transitions mdp)
functorB partition <> "\n" <> transitionsB partition (mdp ^. transitions)
functorB :: Maybe Partition -> Build.Builder
functorB Nothing = "P(DX)\n"
functorB Nothing = "P(DX)\n"
functorB (Just partition) =
(Build.decimal (numBlocks partition)) <> " x P(DX)\n"
transitionsB :: Maybe Partition -> Vector Transition -> Build.Builder
transitionsB partition ts =
let stateMap :: IntMap [Transition] =
V.foldl' (\m t -> M.insertWith (++) (from t) [t] m) M.empty ts
in foldMap (uncurry (choicesB partition)) (M.toList stateMap)
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 partition from ts =
let choiceMap :: IntMap [Transition] =
foldl' (\m t -> M.insertWith (++) (choice t) [t] m) M.empty ts
in stateB from <> ": " <> partStart partition <> "{" <>
fold
(intersperse
", "
(map (uncurry (transitionB from)) (M.toList choiceMap))) <>
"}" <>
partEnd partition <>
"\n"
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"
where
partStart Nothing = ""
partStart (Just part) =
"(" <> Build.decimal (stateAssignment part V.! from) <> ", "
partEnd Nothing = ""
"(" <> Build.decimal (stateAssignment part V.! source) <> ", "
partEnd Nothing = ""
partEnd (Just _) = ")"
transitionB :: Int -> Int -> [Transition] -> Build.Builder
......@@ -106,9 +114,186 @@ transitionB _ _ successors =
"{" <> fold (intersperse ", " (map successorB successors)) <> "}"
where
successorB :: Transition -> Build.Builder
successorB t =
stateB (to t) <> ": " <>
Build.formatRealFloat Build.Fixed Nothing (propability t)
successorB t = stateB (t ^. target) <> ": " <> Build.formatRealFloat
Build.Fixed
Nothing
(t ^. propability)
stateB :: Int -> Build.Builder
stateB = ("s"<>) . Build.decimal
stateB = ("s" <>) . Build.decimal
----------------------------------------------------------------------
-- Builder for Valmari format
--
-- This format is essentially:
--
-- MC ::= <sizes> <l_transitions> <w_transitions> <blocks>
-- <sizes> ::= num_states num_choices num_l_trans num_w_trans num_blocks
-- <l_transitions> ::= <l_transition>*
-- <l_transition> ::= source choice target
-- <w_transitions> ::= <w_transition>*
-- <w_transition> ::= source weight target
-- <blocks> ::= <block>*
-- <block> ::= state* 0
--
-- Where blocks are the blocks of the initial partition. Also, one block is
-- omitted.
----------------------------------------------------------------------
data ValmariMDP = ValmariMDP
{ _vNumStates :: Int
, _vNumActionStates :: Int
, _vNumChoices :: Int
, _vActions :: Vector (Vector Int) -- From normal states to list of actions
, _vProbablilities :: Vector (Vector ValmariTransition)
}
-- From an action state to a normal state
data ValmariTransition = ValmariTransition
{ _vProbablility :: Double
, _vTarget :: Int
}
makeLenses ''ValmariMDP
makeLenses ''ValmariTransition
type ValmariPartition = [[Int]]
convertToValmari :: Maybe Partition -> Mdp -> (ValmariMDP, ValmariPartition)
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
}
, part
)
-- State -> Choices
-- each choice has many [(Probability, State)]
type ValmariMap = IntMap [(Int, [(Double, Int)])]
-- | Returns the total number of action states and the valmari map
mkValmariMap :: Mdp -> (Int, ValmariMap)
mkValmariMap mdp = M.mapAccum uniquifyChoices
0
(V.foldl' ins M.empty (mdp ^. transitions))
where
ins
:: IntMap (IntMap [(Double, Int)])
-> Transition
-> IntMap (IntMap [(Double, Int)])
ins m t =
m
& (at (t ^. source) . non M.empty)
. (at (t ^. choice) . non [])
%~ ((t ^. propability, t ^. target) :)
uniquifyChoices
:: Int -> IntMap [(Double, Int)] -> (Int, [(Int, [(Double, Int)])])
uniquifyChoices current actions =
let newActions = zip [current ..] (M.elems actions)
in (current + length newActions, newActions)
partToBlocks :: Partition -> [[Int]]
partToBlocks p =
let blockMap = V.ifoldl' (\m s b -> m & at b . non [] %~ (s :))
M.empty
(stateAssignment p)
in M.elems blockMap
valmariMdpB :: Maybe Partition -> Mdp -> Build.Builder
valmariMdpB partition mdp =
let (vmdp, vpartition) = convertToValmari partition mdp
in valmariSizesB vmdp vpartition
<> "\n"
<> valmariLTransitions vmdp
<> "\n"
<> valmariWTransitions vmdp
<> "\n"
<> valmariBlocks vpartition
valmariSizesB :: ValmariMDP -> ValmariPartition -> Build.Builder
valmariSizesB mdp part =
Build.decimal (mdp ^. vNumStates + mdp ^. vNumActionStates)
<> " "
<> Build.decimal (mdp ^. vNumChoices)
<> " "
<> Build.decimal (length (mdp ^. vActions))
<> " "
<> Build.decimal (length (mdp ^. vProbablilities))
<> " "
<> Build.decimal (length part + 1)
valmariLTransitions :: ValmariMDP -> Build.Builder
valmariLTransitions mdp = foldMap (uncurry vChoices)
(zip [0 ..] (mdp ^.. vActions . 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
<> " "
<> Build.decimal (choice + 1)
<> " "
<> vActionState mdp target
<> "\n"
valmariWTransitions :: ValmariMDP -> Build.Builder
valmariWTransitions mdp = foldMap
(uncurry vProps)
(zip [0 ..] (mdp ^.. vProbablilities . 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
<> " "
<> Build.formatRealFloat Build.Fixed Nothing (t ^. vProbablility)
<> " "
<> vState (t ^. vTarget)
<> "\n"
vState :: Int -> Build.Builder
vState = Build.decimal . (+1)
vActionState :: ValmariMDP -> Int -> Build.Builder
vActionState mdp = Build.decimal . (+ (mdp^.vNumStates)) . (+1)
valmariBlocks :: [[Int]] -> Build.Builder
valmariBlocks part = part & each.each %~ vState
& each %~ intersperse " "
& intersperse [" 0\n"]
& concat
& fold
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment