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

prism-converter: Fix equivalence semantic for MDPs

We previously did not distinguish actions properly by using the
powerset functor for action transitions. By using P(AxX) where A is
the set of possible actions, we correctly distinguish different
action states that behave the same.
parent 4c0692d7
{-# 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
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