mCRL2
|
Algorithms for LTS, such as equivalence reductions, determinisation, etc. More...
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. | |
Macros | |
#define | BRANCH_BIS_EXPERIMENT_JFG |
#define | MCRL2_LTS_LTS_ALGORITHM_H |
Functions | |
template<class LTS_TYPE > | |
void | mcrl2::lts::reduce (LTS_TYPE &l, lts_equivalence eq) |
Applies a reduction algorithm to this LTS. | |
template<class LTS_TYPE > | |
bool | mcrl2::lts::destructive_compare (LTS_TYPE &l1, LTS_TYPE &l2, const lts_equivalence eq, const bool generate_counter_examples=false, const std::string &counter_example_file=std::string(), const bool structured_output=false) |
Checks whether this LTS is equivalent to another LTS. | |
template<class LTS_TYPE > | |
bool | mcrl2::lts::compare (const LTS_TYPE &l1, const LTS_TYPE &l2, const lts_equivalence eq, const bool generate_counter_examples=false, const std::string &counter_example_file="", const bool structured_output=false) |
Checks whether this LTS is equivalent to another LTS. | |
template<class LTS_TYPE > | |
bool | mcrl2::lts::destructive_compare (LTS_TYPE &l1, LTS_TYPE &l2, const lts_preorder pre, const bool generate_counter_example, const std::string &counter_example_file="", const bool structured_output=false, const lps::exploration_strategy strategy=lps::es_breadth, const bool preprocess=true) |
Checks whether this LTS is smaller than another LTS according to a preorder. | |
template<class LTS_TYPE > | |
bool | mcrl2::lts::compare (const LTS_TYPE &l1, const LTS_TYPE &l2, const lts_preorder pre, const bool generate_counter_example, const std::string &counter_example_file="", const bool structured_output=false, const lps::exploration_strategy strategy=lps::es_breadth, const bool preprocess=true) |
Checks whether this LTS is smaller than another LTS according to a preorder. | |
template<class LTS_TYPE > | |
void | mcrl2::lts::determinise (LTS_TYPE &l) |
Determinises this LTS. | |
template<class SL , class AL , class BASE > | |
bool | mcrl2::lts::reachability_check (lts< SL, AL, BASE > &l, bool remove_unreachable=false) |
Checks whether all states in this LTS are reachable from the initial state and remove unreachable states if required. | |
template<class SL , class AL , class PROBABILISTIC_STATE , class BASE > | |
bool | mcrl2::lts::reachability_check (probabilistic_lts< SL, AL, PROBABILISTIC_STATE, BASE > &l, bool remove_unreachable=false) |
Checks whether all states in a probabilistic LTS are reachable from the initial state and remove unreachable states if required. | |
template<class LTS_TYPE > | |
bool | mcrl2::lts::is_deterministic (const LTS_TYPE &l) |
Checks whether this LTS is deterministic. | |
template<class LTS_TYPE > | |
void | mcrl2::lts::merge (LTS_TYPE &l1, const LTS_TYPE &l2) |
Merge the second lts into the first lts. | |
template<class LTS_TYPE > | |
void | mcrl2::lts::detail::get_trans (const outgoing_transitions_per_state_t &begin, tree_set_store &tss, std::size_t d, std::vector< transition > &d_trans, LTS_TYPE &aut) |
Algorithms for LTS, such as equivalence reductions, determinisation, etc.
This contains the main algorithms useful to manipulate with labelled transition systems. Typically, it contains algorithms for bisimulation reduction, removal of tau loops, making an lts deterministic etc.
Definition in file lts_algorithm.h.
#define BRANCH_BIS_EXPERIMENT_JFG |
Definition at line 19 of file lts_algorithm.h.
#define MCRL2_LTS_LTS_ALGORITHM_H |
Definition at line 22 of file lts_algorithm.h.