mcrl2/lps/state_probability_pair.h

Include file:

#include "mcrl2/lps/state_probability_pair.h"

This file contains a class with a state/probability pair.

A state probability pair consists of a state and a probability. The probability should be larger than 0 and smaller or equal to 1. Jan Friso Groote