spot::scc_and_mark_filter Class Reference

Create a filter for SCC and marks. More...

#include <spot/twaalgos/sccinfo.hh>

Collaboration diagram for spot::scc_and_mark_filter:

Public Member Functions
	scc_and_mark_filter (const scc_info &lower_si, unsigned lower_scc, acc_cond::mark_t cut_sets)
	Specify how to restrict scc_info to some SCC and acceptance sets.
	scc_and_mark_filter (const scc_info &lower_si, unsigned lower_scc, acc_cond::mark_t cut_sets, const bitvect &keep)
	Construct with an additional bitvect of edges to keep.
	scc_and_mark_filter (const const_twa_graph_ptr &aut, acc_cond::mark_t cut_sets)
	Specify how to restrict scc_info to some acceptance sets.
void	override_acceptance (const acc_cond &new_acc)
	Temporarily override the automaton's acceptance condition.
void	restore_acceptance ()
	Restore the original acceptance condition.
const_twa_graph_ptr	get_aut () const
	Return the filtered automaton.
unsigned	start_state () const
	Return the starting state for scc_info exploration.
scc_info::edge_filter	get_filter () const
	Return the appropriate edge filter function.

Static Protected Member Functions
static scc_info::edge_filter_choice	filter_scc_and_mark_ (const twa_graph::edge_storage_t &e, unsigned dst, void *data)
	Filter by SCC membership and cut sets.
static scc_info::edge_filter_choice	filter_mark_ (const twa_graph::edge_storage_t &e, unsigned, void *data)
	Filter by acceptance marks only.
static scc_info::edge_filter_choice	filter_scc_and_mark_and_edges_ (const twa_graph::edge_storage_t &e, unsigned dst, void *data)
	Filter by SCC, marks, and edge set.

Protected Attributes
const scc_info *	lower_si_
	The original scc_info used to filter.
unsigned	lower_scc_
	SCC number in lower_si_ to restrict to.
acc_cond::mark_t	cut_sets_
	Acceptance sets treated as cut edges.
const_twa_graph_ptr	aut_
	The automaton being filtered.
acc_cond	old_acc_
	Saved acceptance for restoration.
bool	restore_old_acc_ = false
	Whether to restore old_acc_.
const bitvect *	keep_ = nullptr
	Optional set of edges to keep.

Detailed Description

Create a filter for SCC and marks.

An scc_and_mark_filter can be passed to scc_info to explore only a specific SCC of the original automaton, and to prevent some acceptance sets from being considered as part of SCCs.

Constructor & Destructor Documentation

scc_and_mark_filter() [1/3]

spot::scc_and_mark_filter::scc_and_mark_filter ( const scc_info &  lower_si, unsigned  lower_scc, acc_cond::mark_t  cut_sets  )

inline

Specify how to restrict scc_info to some SCC and acceptance sets.

Parameters

lower_si	the original scc_info that specifies the SCC
lower_scc	the SCC number in lower_si
cut_sets	the acceptance sets that should not be part of SCCs.

References spot::scc_info::get_filter(), and spot::scc_info::get_filter_data().

scc_and_mark_filter() [2/3]

spot::scc_and_mark_filter::scc_and_mark_filter ( const scc_info &  lower_si, unsigned  lower_scc, acc_cond::mark_t  cut_sets, const bitvect &  keep  )

inline

Construct with an additional bitvect of edges to keep.

scc_and_mark_filter() [3/3]

spot::scc_and_mark_filter::scc_and_mark_filter ( const const_twa_graph_ptr &  aut, acc_cond::mark_t  cut_sets  )

inline

Specify how to restrict scc_info to some acceptance sets.

Parameters

aut	the automaton to filter
cut_sets	the acceptance sets that should not be part of SCCs.

Member Function Documentation

filter_mark_()

static scc_info::edge_filter_choice spot::scc_and_mark_filter::filter_mark_ ( const twa_graph::edge_storage_t &  e, unsigned  , void *  data  )

staticprotected

Filter by acceptance marks only.

filter_scc_and_mark_()

static scc_info::edge_filter_choice spot::scc_and_mark_filter::filter_scc_and_mark_ ( const twa_graph::edge_storage_t &  e, unsigned  dst, void *  data  )

staticprotected

Filter by SCC membership and cut sets.

filter_scc_and_mark_and_edges_()

static scc_info::edge_filter_choice spot::scc_and_mark_filter::filter_scc_and_mark_and_edges_ ( const twa_graph::edge_storage_t &  e, unsigned  dst, void *  data  )

staticprotected

Filter by SCC, marks, and edge set.

get_aut()

const_twa_graph_ptr spot::scc_and_mark_filter::get_aut ( ) const

inline

Return the filtered automaton.

get_filter()

scc_info::edge_filter spot::scc_and_mark_filter::get_filter ( ) const

inline

Return the appropriate edge filter function.

override_acceptance()

void spot::scc_and_mark_filter::override_acceptance ( const acc_cond &  new_acc )

inline

Temporarily override the automaton's acceptance condition.

restore_acceptance()

void spot::scc_and_mark_filter::restore_acceptance ( )

inline

Restore the original acceptance condition.

start_state()

unsigned spot::scc_and_mark_filter::start_state ( ) const

inline

Return the starting state for scc_info exploration.

References spot::scc_info::one_state_of().

Member Data Documentation

aut_

const_twa_graph_ptr spot::scc_and_mark_filter::aut_

protected

The automaton being filtered.

cut_sets_

acc_cond::mark_t spot::scc_and_mark_filter::cut_sets_

protected

Acceptance sets treated as cut edges.

keep_

const bitvect* spot::scc_and_mark_filter::keep_ = nullptr

protected

Optional set of edges to keep.

lower_scc_

unsigned spot::scc_and_mark_filter::lower_scc_

protected

SCC number in lower_si_ to restrict to.

lower_si_

const scc_info* spot::scc_and_mark_filter::lower_si_

protected

The original scc_info used to filter.

old_acc_

acc_cond spot::scc_and_mark_filter::old_acc_

protected

Saved acceptance for restoration.

restore_old_acc_

bool spot::scc_and_mark_filter::restore_old_acc_ = false

protected

Whether to restore old_acc_.

---

The documentation for this class was generated from the following file:

• spot/twaalgos/sccinfo.hh