mCRL2
|
Go to the source code of this file.
Namespaces | |
namespace | mcrl2 |
A class that takes a linear process specification and checks all tau-summands of that LPS for confluence. | |
namespace | mcrl2::lts |
The main LTS namespace. | |
namespace | mcrl2::lts::detail |
A base class for the lts_dot labelled transition system. | |
Functions | |
template<class LTS_TYPE > | |
void | mcrl2::lts::detail::probabilistic_bisimulation_reduce_grv (LTS_TYPE &l, utilities::execution_timer &timer) |
Reduce transition system l with respect to probabilistic bisimulation. | |
template<class LTS_TYPE > | |
bool | mcrl2::lts::detail::destructive_probabilistic_bisimulation_compare_grv (LTS_TYPE &l1, LTS_TYPE &l2, utilities::execution_timer &timer) |
Checks whether the two initial states of two plts's are probabilistic bisimilar. | |
template<class LTS_TYPE > | |
bool | mcrl2::lts::detail::probabilistic_bisimulation_compare_grv (const LTS_TYPE &l1, const LTS_TYPE &l2, utilities::execution_timer &timer) |
Checks whether the two initial states of two plts's are probabilistic bisimilar. | |