Parametric models

Instead of setting numeric values as transition probabilities, we may also use parameters, polynomials or even rational functions in multiple variables.

from stormvogel import parametric

Polynomials are represented as dictionaries where the keys are the exponents and the values are coefficients. In addition, we must also supply a list of variable names. Rational functions are then represented as a pair of two polynomials (numerator and denominator).

polynomial1 = parametric.Polynomial(["x","y"])
polynomial1.add_term((2,0),1)
polynomial1.add_term((0,2),1)

print(polynomial1)

polynomial2 = parametric.Polynomial(["z"])
polynomial2.add_term((0,),2)
polynomial2.add_term((1,),1)
polynomial2.add_term((3,),6)

print(polynomial2)

rational_function = parametric.RationalFunction(polynomial1, polynomial2)

print(rational_function)

x^2 + y^2
2.0*1 + z + 6.0*z^3
(x^2 + y^2)/(2.0*1 + z + 6.0*z^3)

To create a parametric model (e.g. pmc or pmdp) we simply have to set such a value as a transition probability. As an example, we provide the knuth yao dice, but with parameters instead of concrete probabilities.

from stormvogel import model, pgc
from stormvogel.show import show

#we first make polynomials 'x' and '1-x'
x = parametric.Polynomial(["x"])
x.add_term((1,),1)

invx = parametric.Polynomial(["x"])
invx.add_term((1,),-1)
invx.add_term((0,),1)

#we build the knuth yao dice using the pgc model builder
def delta(s: pgc.State):
    match s.s:
        case 0:
            return [(x, pgc.State(s=1)), (invx, pgc.State(s=2))]
        case 1:
            return [(x, pgc.State(s=3)), (invx, pgc.State(s=4))]
        case 2:
            return [(x, pgc.State(s=5)), (invx, pgc.State(s=6))]
        case 3:
            return [(x, pgc.State(s=1)), (invx, pgc.State(s=7, d=1))]
        case 4:
            return [
                (x, pgc.State(s=7, d=2)),
                (invx, pgc.State(s=7, d=3)),
            ]
        case 5:
            return [
                (x, pgc.State(s=7, d=4)),
                (invx, pgc.State(s=7, d=5)),
            ]
        case 6:
            return [(x, pgc.State(s=2)), (invx, pgc.State(s=7, d=6))]
        case 7:
            return [(1, s)]

def labels(s: pgc.State):
    if s.s == 7:
        return f"rolled{str(s.d)}"

knuth_yao = pgc.build_pgc(
    delta=delta,
    initial_state_pgc=pgc.State(s=0),
    labels=labels,
    modeltype=model.ModelType.DTMC,
)

vis = show(knuth_yao)

We can now evaluate the model by assigning the variable x to any concrete value. This induces a regular dtmc with fixed probabilities.

p = 1/2

eval_knuth_yao = knuth_yao.parameter_valuation({"x":p})
vis = show(eval_knuth_yao)