MC Analyzer - a tool to calculate edge-reward expects, variances and covariances in discrete time markov chains
See theoretical considerations, the basis for this implementation as well as some additional stuff here (in German language).
You may use this documentation to get a quick overview how to use this solution. You may use the compiled code as a standalone command line tool or the code as header-only library to build up your own application on top. To use the C++ class and function definitions directly when writing your own code on top of it, see the Doxymentation of the code generated by Doxygen.
To build the command line tool (executable) you may have a look at how it is built on Travis CI. The configuration for Travis can be found in .travis.yml. There you can see what packages are needed to build on Linux. You may also use the following explanation to get started.
Download (compile and install where necessary) the following tools:
Clone this repository and make sure you pulled submodules, e.g. type:
git clone 'https://github.com/Necktschnagge/markov_chain_analyzer' './markov_chain_analyzer'
cd './markov_chain_analyzer'
git submodule init
git submodule update
Move into the directory where the CMakeLists.txt
is located (cd './markov_chain_analyzer'
). Run cmake .
to setup a platform-dependent project.
Run cmake --build .
to build the command line tool or open the created project with your custom tool of choice.
To use single classes and functions in your custom tool build upon MC_Analyzer, see the Doxymentation of the code. For using the command line tool MC_Analyzer read the following lines.
MC_Analyzer CLI stores markov chains as well as target sets associated to some integer id. For state enumeration integers 0,1, ... n-1
are used. MC_Analyzer CLI offers you various commands in order to obtain expects, variances and covariances and to create or destroy a markov chain. You may find the single instructions and their detailed descriptions here. We provide some example workflow here:
On construction of a markov chain object a number of state decorations (i.e. number of double
values that can be assigned to each state later) and a number of edge decorations (respectively) is assigned to the markov chain. You will need edge decorations in order to store edge-based rewards and state decorations in order to store e.g. expects and variances. These numbers are fixed during the lifetime of a markov chain object. In order to do so, start your executable like:
>mc_analyzer.exe
Then MC_Analyzer CLI will wait for input. So type an instruction like:
reset_mc>0>2>2
A markov chain is created and associated to id 0
. It provides two cells for double
values per edge and node.
MC_Analyzer CLI supports reading from a file format introduced with this tool, called General Markov Chain Format (gmc) as well as reading from PRISM's explicit model files. In this guide we use the former option. So suppose you have an input file markov_chain.gmc
with the following content
$from, $to, $prob,$1
1,2,0.5,4
1,3,0.5,5
2,0,1,2
3,2,0.25,5
3,4,0.5,2
3,5,0.25,3
4,4,0.8,2
4,5,0.2,3
5,0,1,3
0,5,1,7
You may also find this file here.
The first line defines the semantics of the following content, saying the first value of the line is the state where the edge represented by the line is coming from, the second where it is going to. The third states the probability assigned to the edge. The third defines some edge-wise reward that will be assigned to the edge decoration at index 1. ! Note: Indexes of edge as well as state decorations start at zero and end with n-1 where n is the number given on construction. So here the reward function will be placed into the last cells of the edge decoration arrays. ! Note: Probabilities are stored separately. There is no need to provid a cell edge decoration to store probabilities. There is also no option to convert edge decorations into probabilities. ! Note: You need to use numbers 0, 1, ... ,n-1
as state ids. Otherwise behavior will be undefined.
In order to read the file just type read_gmc>0>./markov_chain.gmc
. This way the file is loaded to the markov chain with id 0
.
Again, see instructions and their detailed descriptions here for more information, including e.g. how to read from PRSIM's file formats.
_You may also see the next instructions here_
Type read_target>0>./target_set.intset
to read a set of integers representing the goal states from file, where ./target_set.intset
(see also here) just contains state ids separated by spaces:
5 0
Like markov chains, target sets are stored by id, independently from markov chain ids. After running the instruction above the set {0, 5}
is stored at id 0
.
To do so, simply type calc_variance>0>1>0>1>0>0
. Here, as arguments you have to pass the id of the markov chain (0), the index of the reward for which you want to calculate variance (1), the id of the target set (0), the index of state decorations where the resulting variances should be stored (1), the index of state decorations where the expect values should be stored (0), an index of edge decorations that can be used for intrim results (0). ! Note: Expect values have to be calculated before calculating variances. This command already does this job. But you need to provide some free state decoration index for this. ! Note: You also need an index of edge decorations to store interim results.
write_state_decorations>0>./output.decos
. This will write all state decoration arrays to file. See this example output The data are displayed in the form {state-id}: {state-deco @ index 0} {state-deco @ index 1} ...