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