liblts_impossible_futures.h File Reference

Go to the source code of this file.

Namespaces
namespace	mcrl2
namespace	mcrl2::lts
	The main LTS namespace.
namespace	mcrl2::lts::detail
	A base class for the lts_dot labelled transition system.

Typedefs
using	mcrl2::lts::state_type_if = detail::state_states_counter_example_index_triple< detail::counter_example_constructor >

Functions
std::ostream &	mcrl2::lts::operator<< (std::ostream &out, const detail::anti_chain_type &a)
template<typename LTS_TYPE >
std::pair< bool, trace >	mcrl2::lts::check_trace_inclusion (LTS_TYPE &l1, const detail::lts_cache< LTS_TYPE > &weak_property_cache, std::deque< state_type_if > &working, refinement_statistics< state_type_if > &stats, detail::anti_chain_type &anti_chain, detail::anti_chain_type &anti_chain_positive, detail::anti_chain_type &anti_chain_negative, detail::state_type init_l1, detail::state_type init_l2, bool weak_reduction, const lps::exploration_strategy strategy, bool enable_counter_example=false)
template<typename LTS >
void	mcrl2::lts::write_counter_example (const LTS &lts, std::ostream &stream, const trace &initial_trace, const std::vector< trace > &inner_traces)
template<typename LTS >
bool	mcrl2::lts::detail::destructive_impossible_futures (LTS &l1, LTS &l2, const lps::exploration_strategy strategy, std::string counter_example_file, bool generate_counter_example, bool structured_output)
	Checks impossible futures refinement for the given LTSs.