diff --git a/src/prism-converter/Main.hs b/src/prism-converter/Main.hs index 8961400d7931ad74094b1d3d6b14f7d95e011524..bc92603a3b90ef095dfd4c438b3a89a71a84e173 100644 --- a/src/prism-converter/Main.hs +++ b/src/prism-converter/Main.hs @@ -37,11 +37,23 @@ instance Show ModelType where show CTMC = "ctmc" show MDP = "mdp" +data OutputFormat = Valmari | Ma + +instance Show OutputFormat where + show Valmari = "valmari" + show Ma = "ma" + +parseOutputFormat :: String -> Either String OutputFormat +parseOutputFormat "valmari" = Right Valmari +parseOutputFormat "ma" = Right Ma +parseOutputFormat other = Left ("Unknown output format '" <> other <> "'") + data Options = Options { optModelType :: ModelType , optInputFile :: Maybe FilePath , optOutputFile :: Maybe FilePath , optStatesFile :: Maybe FilePath + , optOutputFormat :: OutputFormat , optPartitionVariables :: Maybe (Set Text) } @@ -82,6 +94,14 @@ optionsParser = (OptParse.long "states-file" <> OptParse.help ".sta file generated by PRISM with -exportstates." <> OptParse.metavar "FILE")) <*> + (OptParse.option + (OptParse.eitherReader parseOutputFormat) + (OptParse.long "output-format" <> + OptParse.help + "Syntax used for the output file. Can be either 'ma' or 'valmari'" <> + OptParse.metavar "FORMAT" <> + OptParse.value Ma <> + OptParse.showDefault)) <*> optional (OptParse.option (OptParse.eitherReader parseVarIndices) @@ -143,7 +163,18 @@ main = do Right vars -> return (Just (computePartition sf vars)) _ -> return Nothing - case (optModelType opts) of - DTMC -> convert opts (markovChainP DiscreteTime) (markovChainB initPartition) - CTMC -> convert opts (markovChainP ContinuousTime) (markovChainB initPartition) - MDP -> convert opts mdpP (mdpB initPartition) + 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 + (inType, outType) -> + let mcType = + case inType of + DTMC -> DiscreteTime + CTMC -> ContinuousTime + builder = + case outType of + Valmari -> valmariMarkovChainB + Ma -> markovChainB + in convert opts (markovChainP mcType) (builder initPartition) diff --git a/src/prism-converter/MarkovChain.hs b/src/prism-converter/MarkovChain.hs index c41fb7a7a63590b79f7f92c3334b6d4cd693db65..5bb5d8635795c97d485644d5268760fb98ff93e8 100644 --- a/src/prism-converter/MarkovChain.hs +++ b/src/prism-converter/MarkovChain.hs @@ -5,6 +5,7 @@ module MarkovChain ( MarkovType(..) , markovChainP , markovChainB + , valmariMarkovChainB ) where import Data.Semigroup @@ -101,3 +102,58 @@ transitionB partition from successors = "(" <> Build.decimal (stateAssignment part V.! from) <> ", " partEnd Nothing = "" partEnd (Just _) = ")" + +---------------------------------------------------------------------- +-- Builder for Valmari format +-- +-- This format is essentially: +-- +-- MC ::= <sizes> <transitions> <blocks> +-- <sizes> ::= num_states 0 0 num_trans num_blocks +-- <transitions> ::= <transition>* +-- <transition> ::= from weight to +-- <blocks> ::= <block>* +-- <block> ::= state* 0 +-- +-- Where blocks are the blocks of the initial partition. Also, one block is +-- omitted. +---------------------------------------------------------------------- + +valmariMarkovChainB :: Maybe Partition -> MarkovChain -> Build.Builder +valmariMarkovChainB partition mc = + valmariSizesB partition mc <> "\n" <> valmariTransitionsB (transitions mc) <> + valmariBlocksB (numStates mc) partition + +valmariSizesB :: Maybe Partition -> MarkovChain -> Build.Builder +valmariSizesB part mc = + Build.decimal (numStates mc) <> " 0 0 " <> + Build.decimal (length (transitions mc)) <> + " " <> + (Build.decimal partitionSize) + where + partitionSize = + case part of + Nothing -> 1 -- No partition: One block with all states + Just p -> (numBlocks p) + +valmariTransitionsB :: Vector Transition -> Build.Builder +valmariTransitionsB = foldMap (\t -> valmariTransitionB t <> "\n") + +valmariTransitionB :: Transition -> Build.Builder +valmariTransitionB t = + state (from t) <> " " <> Build.formatRealFloat Build.Fixed Nothing (label t) <> + " " <> + state (to t) + where + state = Build.decimal . (+ 1) -- states are numbered from 1 + +valmariBlocksB :: Int -> Maybe Partition -> Build.Builder +valmariBlocksB n Nothing = "" +valmariBlocksB _ (Just p) = + let blockMap :: IntMap [Int] + blockMap = V.ifoldl' (\m s b -> M.insertWith (++) b [s] m) M.empty (stateAssignment p) + in + foldMap (\b -> valmariBlockB b) (tail (M.elems blockMap)) + +valmariBlockB :: [Int] -> Build.Builder +valmariBlockB states = foldMap (\s -> Build.decimal (s+1) <> " ") states <> " 0\n"