No Matches
liblts_failures_refinement.h File Reference

Go to the source code of this file.


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 >


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.


typedef std::set< state_typemcrl2::lts::detail::set_of_states
typedef std::multimap< detail::state_type, detail::set_of_statesmcrl2::lts::detail::anti_chain_type
typedef std::set< label_typemcrl2::lts::detail::action_label_set


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


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_statesmcrl2::lts::detail::calculate_tau_reachable_states (const set_of_states &states, const lts_cache< LTS_TYPE > &weak_property_cache)