stormvogel.examples.knuth_yao_pmc¶

Functions¶

`create_knuth_yao_pmc`()	Build the Knuth--Yao dice as a parametric DTMC.
`create_knuth_yao_pmc_twocoins`()	Build the Knuth--Yao dice as a parametric DTMC.

Module Contents¶

stormvogel.examples.knuth_yao_pmc.create_knuth_yao_pmc()¶

Build the Knuth–Yao dice as a parametric DTMC.

The parameter x is the success probability of the underlying coin. Probabilities are expressed as ordinary sympy expressions, so 1 - x is literally 1 - x — no special constructors needed.

stormvogel.examples.knuth_yao_pmc.create_knuth_yao_pmc_twocoins()¶: Build the Knuth–Yao dice as a parametric DTMC.