mCRL2
Loading...
Searching...
No Matches
lts_algorithm.h File Reference

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.
 

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)
 

Detailed Description

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.

Author
Jan Friso Groote, Bas Ploeger, Muck van Weerdenburg

Definition in file lts_algorithm.h.