Building DTMCs

A Discrete Time Markov Chain is a transition system that has * states (includig an initial state) * probabilistic transitions. * labels

Below is an example of how to construct the same simple model of a 6-sided die using 4 different APIs. We would recommend at least looking at the code for the first example, using the pgcAPI in detail, as we will mainly use this in other chapters. For more information on how to use the PRISM and stormpy APIs, we refer to their respective documentations.

Note: unfortunately, the position of the network is not always correct when it is rendered out of view. To re-center, you can simply double click inside the window.

from stormvogel import pgc
from stormvogel.model import EmptyAction, ModelType
from stormvogel.show import show
from stormvogel.layout import Layout

# Create an initial state.
# In the model API, any state that you create takes a number of keyword arguments.
# These keyword arguments store some information about the state and can be of any type.
# In this case, we have a single piece of information called 'x', and for the initial state, we give it "".
init = pgc.State(x="")

# This delta function takes as an argument a single state, and returns a
# list of 2-tuples where the first argument is a probability and the second elment is a state.
# Our pgc API uses this function to know where to go from a state.
def delta(s: pgc.State):
    if s == init: # If we are in the initial state, roll the die, we could also test this with s.x == "".
        return [(1 / 6, pgc.State(x=[f"rolled{i}"])) for i in range(1, 7)]
    else: # If we are *not* in the initial state, do a self-loop with probability 1.
        return [(1, s)]

# Labels is a function that tells the pgc API to use x as the label.
# It is written as a lambda here, but it means exactly the same as
# def labels(s):
#    return s.x
labels = lambda s: s.x

pgc_die = pgc.build_pgc(
    delta=delta,
    initial_state_pgc=init,
    labels=labels,
    modeltype=ModelType.DTMC
)

vis2 = show(pgc_die, layout=Layout("layouts/die.json"))

Test request failed. See 'Communication server remark' in docs. Disable warning by use_server=False.

# If we use the model API, we need to create all states and transitions explicitly.
from stormvogel.show import show
from stormvogel.layout import Layout
import stormvogel.model

# Create a new model with the name "Die"
die_dtmc = stormvogel.model.new_dtmc("Die", create_initial_state=True)
# By default, a new model starts with an initial state, use get_initial_state to retrieve it.
init = die_dtmc.get_initial_state()
# From the initial state, add the transition to 6 new states with probability 1/6th.
# The set_transitions function takes a list of 2-tuples where the first argument is a probability and the second elment is a state.
init.set_transitions(
    [(1 / 6, die_dtmc.new_state(f"rolled{i}")) for i in range(1, 7)]
)
# Add self loops to make the model *absorbing* (i.e. there are no states where you get stuck because there are no more transitions available).
die_dtmc.add_self_loops()
vis = show(die_dtmc, layout=Layout("layouts/die.json"))

We could also use the pgc API to create the exact same model. This API uses higher order functions, which means that you use functions in parameters for other functions. This might be difficult to understand if you are not from a computing science background, but we will try to explain.

For this simple model, it might not be immediately obvious why we would want such an API, but hopefully that will become clear in later examples.

We can also construct our die model in PRISM. The concepts here are similar to the pgc API. This requires stormpy.

%%prism die_prism_code
dtmc

module die
    // The integers 0..7 represent our states, and 0 is the initial state.
    s : [0..7] init 0;
    // From s=0, we can go to 1,2,3,4,5,6 with 1/6th probability.
    // The + sign can be interpreted as an 'or'
    // Note that this is similar to our delta function.
    [] s=0 -> 1/6 : (s'=1) +
                1/6: (s'=2) +
                1/6: (s'=3) +
                1/6: (s'=4) +
                1/6: (s'=5) +
                1/6: (s'=6);
    // Self loops
    [] s>0 -> (s'=s);
endmodule

// Add the desired labels
label "rolled1" = s=1;
label "rolled2" = s=2;
label "rolled3" = s=3;
label "rolled4" = s=4;
label "rolled5" = s=5;
label "rolled6" = s=6;

<stormpy.storage.storage.PrismProgram at 0x7f7d58914530>

Under the hood, stormpy parses the prism model which is then converted to a stormpy model and a stormvogel model.

import stormvogel.stormpy_utils.mapping as mapping
prism_die = mapping.from_prism(die_prism_code)
vis3 = show(prism_die, layout=Layout("layouts/die.json"))

Finally, we could also use the stormpy’s SparseMatrix API directly. Obviously, also requires stormpy

import stormpy
import stormvogel.stormpy_utils.mapping as mapping
builder = stormpy.SparseMatrixBuilder(rows=0, columns=0, entries=0, force_dimensions=False, has_custom_row_grouping=False)
for s in range(1,7):
    builder.add_next_value(0, s, 1/6)
for s in range(1,7):
    builder.add_next_value(s, s, 1)
transition_matrix = builder.build()
state_labeling = stormpy.storage.StateLabeling(7)

labels = {"init"}.union({f"rolled{s}" for s in range(1,7)})
for label in labels:
    state_labeling.add_label(label)
state_labeling.add_label_to_state("init", 0)
for s in range(1,7):
    state_labeling.add_label_to_state(f"rolled{s}", s)
components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling)
stormpy_dtmc = mapping.stormpy_to_stormvogel(stormpy.storage.SparseDtmc(components))
vis4 = show(stormpy_dtmc, layout=Layout("layouts/die.json"))