diff --git a/ma.cabal b/ma.cabal index f626c74cee3198796a6f2921cef720f2e669a9e6..28f2f04a005abf7b9d3ef8cb82749b9ef479ddff 100644 --- a/ma.cabal +++ b/ma.cabal @@ -237,3 +237,6 @@ executable prism-converter , prettyprinter , prettyprinter-ansi-terminal , prettyprinter-convert-ansi-wl-pprint + , microlens + , microlens-th + , microlens-platform diff --git a/src/prism-converter/Main.hs b/src/prism-converter/Main.hs index bc92603a3b90ef095dfd4c438b3a89a71a84e173..c6c6e628ca55b00c3a6cc6c7a4cf7874902d4578 100644 --- a/src/prism-converter/Main.hs +++ b/src/prism-converter/Main.hs @@ -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 diff --git a/src/prism-converter/Mdp.hs b/src/prism-converter/Mdp.hs index d30c1c76833ac76e0bcd4a78c7257fd7da83f91a..b118337bc8fe8e262f80acce8923c17f2505de69 100644 --- a/src/prism-converter/Mdp.hs +++ b/src/prism-converter/Mdp.hs @@ -1,48 +1,50 @@ {-# 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