liblts_failures_refinement.h File Reference

Go to the source code of this file.

Classes
class	mcrl2::lts::detail::state_states_counter_example_index_triple< COUNTER_EXAMPLE_CONSTRUCTOR >
class	mcrl2::lts::detail::lts_cache< LTS_TYPE >
struct	mcrl2::lts::refinement_statistics< T >

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.

Typedefs
typedef std::set< state_type >	mcrl2::lts::detail::set_of_states
typedef std::multimap< detail::state_type, detail::set_of_states >	mcrl2::lts::detail::anti_chain_type
typedef std::set< label_type >	mcrl2::lts::detail::action_label_set

Enumerations
enum class	mcrl2::lts::refinement_type { mcrl2::lts::trace , mcrl2::lts::failures , mcrl2::lts::failures_divergence }

Functions
template<class COUNTER_EXAMPLE_CONSTRUCTOR >
bool	mcrl2::lts::detail::antichain_insert (anti_chain_type &anti_chain, const state_states_counter_example_index_triple< COUNTER_EXAMPLE_CONSTRUCTOR > &impl_spec)
template<class LTS_TYPE >
set_of_states	mcrl2::lts::detail::collect_reachable_states_via_taus (const state_type s, const lts_cache< LTS_TYPE > &weak_property_cache, const bool weak_reduction)
template<class LTS_TYPE >
set_of_states	mcrl2::lts::detail::collect_reachable_states_via_an_action (const state_type s, const label_type e, const lts_cache< LTS_TYPE > &weak_property_cache, const bool weak_reduction, const LTS_TYPE &l)
template<class LTS_TYPE >
bool	mcrl2::lts::detail::refusals_contained_in (const state_type impl, const set_of_states &spec, const lts_cache< LTS_TYPE > &weak_property_cache, label_type &culprit, const LTS_TYPE &l, const bool provide_a_counter_example, const bool structured_output)
	This function checks that the refusals(impl) are contained in the refusals of spec, where the refusals of spec are defined by { r | exists s in spec. r in refusals(s) and stable(r) }.
template<typename T >
void	mcrl2::lts::report_statistics (refinement_statistics< T > &stats)
	Print a message to debugging containing information about the given statistics.
template<typename LTS_TYPE >
std::pair< std::size_t, bool >	mcrl2::lts::reduce (LTS_TYPE &lts, const bool weak_reduction, const bool preserve_divergence, std::size_t l2_init)
	Preprocess the LTS for destructive refinement checking.
template<class LTS_TYPE , class COUNTER_EXAMPLE_CONSTRUCTOR = detail::dummy_counter_example_constructor>
bool	mcrl2::lts::destructive_refinement_checker (LTS_TYPE &l1, LTS_TYPE &l2, const refinement_type refinement, const bool weak_reduction, const lps::exploration_strategy strategy, const bool preprocess=true, COUNTER_EXAMPLE_CONSTRUCTOR generate_counter_example=detail::dummy_counter_example_constructor())
	This function checks using algorithms in the paper mentioned above whether transition system l1 is included in transition system l2, in the sense of trace inclusions, failures inclusion and divergence failures inclusion.
template<class LTS_TYPE >
set_of_states	mcrl2::lts::detail::collect_reachable_states_via_taus (const set_of_states &s, const lts_cache< LTS_TYPE > &weak_property_cache, const bool weak_reduction)
template<class LTS_TYPE >
const set_of_states &	mcrl2::lts::detail::calculate_tau_reachable_states (const set_of_states &states, const lts_cache< LTS_TYPE > &weak_property_cache)