Include file:
#include "mcrl2/lts/lts_algorithm.h"
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. Jan Friso Groote, Bas Ploeger, Muck van Weerdenburg
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.
The input labelled transition systems are duplicated in memory to carry out the comparison. When space efficiency is a concern, one can consider to use destructive_compare.
Parameters:
Returns: * true if the LTSs are found to be equivalent.
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.
Parameters:
Returns: * true if this LTS is smaller than LTS l according to preorder pre.
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.
Parameters:
Returns: * true if the LTSs are found to be equivalent.
Warning
This function alters the internal data structure of both LTSs for efficiency reasons. After comparison, this LTS is equivalent to the original LTS by equivalence eq, and similarly for the LTS l.
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.
Parameters:
Returns: * true if LTS l1 is smaller than LTS l2 according to preorder pre.
Warning
This function alters the internal data structure of both LTSs for efficiency reasons. After comparison, this LTS is equivalent to the original LTS by equivalence eq, and similarly for the LTS l, where eq is the equivalence induced by the preorder pre (i.e. $eq = pre cap pre^{-1}$).
determinise
(LTS_TYPE &l)¶Determinises this LTS.
is_deterministic
(const LTS_TYPE &l)¶Checks whether this LTS is deterministic.
Returns: * true if this LTS is deterministic;
mcrl2::lts::
merge
(LTS_TYPE &l1, const LTS_TYPE &l2)¶Merge the second lts into the first lts.
Parameters:
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.
Runs in O(num_states * num_transitions) time.
Parameters:
Returns: * true if all states are reachable from the initial state;
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.
Runs in O(num_states * num_transitions) time.
Parameters:
Returns: * true if all states are reachable from the initial state;
reduce
(LTS_TYPE &l, lts_equivalence eq)¶Applies a reduction algorithm to this LTS.
Parameters:
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)¶