Classes
class	spot::postprocessor
	Wrap TGBA/BA/Monitor post-processing algorithms in an easy interface. More...

Functions
twa_graph_ptr	spot::dtba_sat_synthetize (const const_twa_graph_ptr &a, int target_state_number, bool state_based=false)
	Attempt to synthesize an equivalent deterministic TBA with a SAT solver. More...

twa_graph_ptr	spot::dtba_sat_minimize (const const_twa_graph_ptr &a, bool state_based=false, int max_states=-1)
	Attempt to minimize a deterministic TBA with a SAT solver. More...

twa_graph_ptr	spot::dtwa_sat_synthetize (const const_twa_graph_ptr &a, unsigned target_acc_number, const acc_cond::acc_code &target_acc, int target_state_number, bool state_based=false, bool colored=false)
	Attempt to synthesize an equivalent deterministic TωA with a SAT solver. More...

twa_graph_ptr	spot::minimize_monitor (const const_twa_graph_ptr &a)
	Construct a minimal deterministic monitor. More...

twa_graph_ptr	spot::minimize_wdba (const const_twa_graph_ptr &a, const output_aborter *aborter=nullptr)
	Minimize a Büchi automaton in the WDBA class. More...

twa_graph_ptr	spot::minimize_obligation (const const_twa_graph_ptr &aut_f, formula f=nullptr, const_twa_graph_ptr aut_neg_f=nullptr, bool reject_bigger=false, const output_aborter *aborter=nullptr, bool assume_correct=false)
	Minimize an automaton if it represents an obligation property. More...

bool	spot::minimize_obligation_guaranteed_to_work (const const_twa_graph_ptr &aut_f, formula f=nullptr)
	Whether calling minimize_obligation is sure to work. More...

twa_graph_ptr	spot::scc_filter (const const_twa_graph_ptr &aut, bool remove_all_useless=false, scc_info *given_si=nullptr, bool keep_one_color=false)
	Prune unaccepting SCCs and remove superfluous acceptance conditions. More...

twa_graph_ptr	spot::scc_filter_states (const const_twa_graph_ptr &aut, bool remove_all_useless=false, scc_info *given_si=nullptr)
	Prune unaccepting SCCs. More...

twa_graph_ptr	spot::scc_filter_susp (const const_twa_graph_ptr &aut, bool remove_all_useless, bdd suspvars, bdd ignoredvars, bool early_susp, scc_info *given_si=nullptr)
	Prune unaccepting SCCs, superfluous acceptance sets, and suspension variables. More...

twa_graph_ptr	spot::simulation (const const_twa_graph_ptr &automaton, int trans_pruning=-1)
	Attempt to reduce the automaton by direct simulation. More...

twa_graph_ptr	spot::simulation (const const_twa_graph_ptr &automaton, std::vector< bdd > *implications, int trans_pruning=-1)
	Attempt to reduce the automaton by direct simulation. More...

twa_graph_ptr	spot::simulation_sba (const const_twa_graph_ptr &automaton, int trans_pruning=-1)
	Attempt to reduce a state-based acceptance automaton by direct simulation. More...

twa_graph_ptr	spot::cosimulation (const const_twa_graph_ptr &automaton, int trans_pruning=-1)
	Attempt to reduce the automaton by reverse simulation. More...

twa_graph_ptr	spot::cosimulation_sba (const const_twa_graph_ptr &automaton, int trans_pruning=-1)
	Attempt to reduce the automaton by reverse simulation. More...

twa_graph_ptr	spot::iterated_simulations (const const_twa_graph_ptr &automaton, int trans_pruning=-1)
	Iterate simulation() and cosimulation(). More...

twa_graph_ptr	spot::iterated_simulations_sba (const const_twa_graph_ptr &automaton, int trans_pruning=-1)
	Iterate simulation() and cosimulation(). More...

twa_graph_ptr	spot::reduce_direct_sim (const const_twa_graph_ptr &aut)
	Attempt to reduce the automaton by direct simulation. More...

twa_graph_ptr	spot::reduce_direct_sim_sba (const const_twa_graph_ptr &aut)
	Attempt to reduce the automaton by direct simulation. More...

twa_graph_ptr	spot::reduce_direct_cosim (const const_twa_graph_ptr &aut)
	Attempt to reduce the automaton by reverse simulation. More...

twa_graph_ptr	spot::reduce_direct_cosim_sba (const const_twa_graph_ptr &aut)
	Attempt to reduce the automaton by reverse simulation. More...

twa_graph_ptr	spot::reduce_iterated (const const_twa_graph_ptr &aut)
	Iterate reduce_direct_sim() and reduce_direct_cosim(). More...

twa_graph_ptr	spot::reduce_iterated_sba (const const_twa_graph_ptr &aut)
	Iterate reduce_direct_sim() and reduce_direct_cosim(). More...

Detailed Description

Function Documentation

◆ cosimulation()

twa_graph_ptr spot::cosimulation	(	const const_twa_graph_ptr &	automaton,
		int	trans_pruning = `-1`
	)

#include <spot/twaalgos/simulation.hh>

Attempt to reduce the automaton by reverse simulation.

When the prefixes (letter and acceptance conditions) leading to one state are included in the prefixes leading to one, the former state can be merged into the latter. [babiak.13.spin] .

Our reconstruction of the quotient automaton based on this prefix-inclusion relation will also improve codeterminism thanks to a kind of transition pruning.

We recommend to call scc_filter() to first simplify the automaton that should be reduced by cosimulation.

Reducing an automaton by reverse simulation (1) does not change the number of acceptance conditions so the resulting automaton may have superfluous acceptance conditions, and (2) can create SCCs that are terminal and non-accepting. For these reasons, you should call scc_filer() to prune useless SCCs and acceptance conditions afterwards.

If you plan to run both simulation() and cosimulation() on the same automaton, you should start with simulation() so that the codeterminism improvements achieved by cosimulation() does not hinder the determinism improvements attempted by simulation(). (This of course assumes that you prefer determinism over codeterminism.)

Parameters

automaton	the automaton to simulate.
trans_pruning	Transition pruning requires a quadratic number of BDD implication checks between all equivalence classes, so it can be costly on large automata. If trans_pruning is set to a non-negative integer, only (non-deterministic) automata with more states than trans_pruning will be simplified.

Returns: a new automaton which is at worst a copy of the received one

◆ cosimulation_sba()

twa_graph_ptr spot::cosimulation_sba	(	const const_twa_graph_ptr &	automaton,
		int	trans_pruning = `-1`
	)

#include <spot/twaalgos/simulation.hh>

Attempt to reduce the automaton by reverse simulation.

When the prefixes (letter and acceptance conditions) leading to one state are included in the prefixes leading to one, the former state can be merged into the latter. [babiak.13.spin] .

Our reconstruction of the quotient automaton based on this prefix-inclusion relation will also improve codeterminism thanks to a kind of transition pruning.

We recommend to call scc_filter() to first simplify the automaton that should be reduced by cosimulation.

Reducing an automaton by reverse simulation (1) does not change the number of acceptance conditions so the resulting automaton may have superfluous acceptance conditions, and (2) can create SCCs that are terminal and non-accepting. For these reasons, you should call scc_filer() to prune useless SCCs and acceptance conditions afterwards.

If you plan to run both simulation() and cosimulation() on the same automaton, you should start with simulation() so that the codeterminism improvements achieved by cosimulation() does not hinder the determinism improvements attempted by simulation(). (This of course assumes that you prefer determinism over codeterminism.)

Parameters

automaton	the automaton to simulate.
trans_pruning	Transition pruning requires a quadratic number of BDD implication checks between all equivalence classes, so it can be costly on large automata. If trans_pruning is set to a non-negative integer, only (non-deterministic) automata with more states than trans_pruning will be simplified.

Returns: a new automaton which is at worst a copy of the received one

◆ dtba_sat_minimize()

twa_graph_ptr spot::dtba_sat_minimize	(	const const_twa_graph_ptr &	a,
		bool	state_based = `false`,
		int	max_states = `-1`
	)

#include <spot/twaalgos/dtbasat.hh>

Attempt to minimize a deterministic TBA with a SAT solver.

This calls dtba_sat_synthetize() in a loop, with a decreasing number of states, and returns the last successfully built TBA.

If no smaller TBA exist, this returns a null pointer.

◆ dtba_sat_synthetize()

twa_graph_ptr spot::dtba_sat_synthetize	(	const const_twa_graph_ptr &	a,
		int	target_state_number,
		bool	state_based = `false`
	)

#include <spot/twaalgos/dtbasat.hh>

Attempt to synthesize an equivalent deterministic TBA with a SAT solver.

Parameters

a	the input TGA. It should have only one acceptance set and be deterministic. I.e., it should be a deterministic TBA.
target_state_number	the desired number of states wanted in the resulting automaton. The result may have less than target_state_number reachable states.
state_based	set to true to force all outgoing transitions of a state to share the same acceptance condition, effectively turning the TBA into a BA.

If no equivalent deterministic TBA with target_state_number states is found, this returns a null pointer.

◆ dtwa_sat_synthetize()

twa_graph_ptr spot::dtwa_sat_synthetize	(	const const_twa_graph_ptr &	a,
		unsigned	target_acc_number,
		const acc_cond::acc_code &	target_acc,
		int	target_state_number,
		bool	state_based = `false`,
		bool	colored = `false`
	)

#include <spot/twaalgos/dtwasat.hh>

Attempt to synthesize an equivalent deterministic TωA with a SAT solver.

Parameters

a	the input TωA. It should be a deterministic TωA.
target_acc_number	is the number of acceptance sets wanted in the result.
target_acc	the target acceptance condition
target_state_number	is the desired number of states in the result. The output may have less than target_state_number reachable states.
state_based	set to true to force all outgoing transitions of a state to share the same acceptance conditions.
colored	if true, force all transitions to belong to exactly one acceptance set.

This function attempts to find a TωA with target_acc_number acceptance sets and target_state_number states that is equivalent to a. If no such TωA is found, a null pointer is returned.

◆ iterated_simulations()

twa_graph_ptr spot::iterated_simulations	(	const const_twa_graph_ptr &	automaton,
		int	trans_pruning = `-1`
	)

#include <spot/twaalgos/simulation.hh>

Iterate simulation() and cosimulation().

Runs simulation(), cosimulation(), and scc_filter() in a loop, until the automaton does not change size (states and transitions).

We recommend to call scc_filter() to first simplify the automaton that should be reduced by iterated simulations, since this algorithm will only call scc_filter() at the end of the loop.

Parameters

automaton	the automaton to simulate.
trans_pruning	Transition pruning requires a quadratic number of BDD implication checks between all equivalence classes, so it can be costly on large automata. If trans_pruning is set to a non-negative integer, only (non-deterministic) automata with more states than trans_pruning will be simplified.

Returns: a new automaton which is at worst a copy of the received one

◆ iterated_simulations_sba()

twa_graph_ptr spot::iterated_simulations_sba	(	const const_twa_graph_ptr &	automaton,
		int	trans_pruning = `-1`
	)

#include <spot/twaalgos/simulation.hh>

Iterate simulation() and cosimulation().

Runs simulation(), cosimulation(), and scc_filter() in a loop, until the automaton does not change size (states and transitions).

We recommend to call scc_filter() to first simplify the automaton that should be reduced by iterated simulations, since this algorithm will only call scc_filter() at the end of the loop.

Parameters

automaton	the automaton to simulate.
trans_pruning	Transition pruning requires a quadratic number of BDD implication checks between all equivalence classes, so it can be costly on large automata. If trans_pruning is set to a non-negative integer, only (non-deterministic) automata with more states than trans_pruning will be simplified.

Returns: a new automaton which is at worst a copy of the received one

◆ minimize_monitor()

twa_graph_ptr spot::minimize_monitor ( const const_twa_graph_ptr & a )

#include <spot/twaalgos/minimize.hh>

Construct a minimal deterministic monitor.

The automaton will be converted into minimal deterministic monitor. All useless SCCs should have been previously removed (using scc_filter() for instance). Then the automaton will be determinized and minimized using the standard DFA construction as if all states were accepting states.

For more detail about monitors, see [tabakov.10.rv] . (Note: although the above paper uses Spot, this function did not exist in Spot at that time.)

Parameters

a	the automaton to convert into a minimal deterministic monitor

Precondition: Dead SCCs should have been removed from a before calling this function.

◆ minimize_obligation()

twa_graph_ptr spot::minimize_obligation	(	const const_twa_graph_ptr &	aut_f,
		formula	f = `nullptr`,
		const_twa_graph_ptr	aut_neg_f = `nullptr`,
		bool	reject_bigger = `false`,
		const output_aborter *	aborter = `nullptr`,
		bool	assume_correct = `false`
	)

#include <spot/twaalgos/minimize.hh>

Minimize an automaton if it represents an obligation property.

This function attempts to minimize the automaton aut_f using the algorithm implemented in the minimize_wdba() function, and presented by [dax.07.atva] .

Because it is hard to determine if an automaton corresponds to an obligation property, you should supply either the formula f expressed by the automaton aut_f, or aut_neg_f the negation of the automaton aut_neg_f.

Parameters

aut_f	the automaton to minimize
f	the LTL formula represented by the automaton aut_f
aut_neg_f	an automaton representing the negation of aut_f
reject_bigger	Whether the minimal WDBA should be discarded if it has more states than the input.
aborter	When given, aborts the determinization whenever the automaton would become larger than specified; in that case, aut_f is returned unchanged.
assume_correct	When set, the resulting WDBA is not checked for correctness, which can be used if the input is known to be an obligation property.

Returns: a new tgba if the automaton could be minimized, aut_f if the automaton cannot be minimized, 0 if we do not know if the minimization is correct because neither f nor aut_neg_f were supplied.

The function proceeds as follows. If the formula f or the automaton aut can easily be proved to represent an obligation formula, then the result of minimize(aut) is returned. Otherwise, if aut_neg_f was not supplied but f was, aut_neg_f is built from the negation of f. Then we check that product(aut,!minimize(aut_f)) and product(aut_neg_f,minimize(aut)) are both empty. If they are, the minimization was sound. (See the paper for full details.)

If reject_bigger is set, this function will return the input automaton aut_f when the minimized WDBA has more states than the input automaton. (More states are possible because of determinization step during minimize_wdba().) Note that checking the size of the minimized WDBA occurs before ensuring that the minimized WDBA is correct.

If an output_aborter is given, the determinization is aborted whenever it would produce an automaton that is too large. In this case, aut_f is returned unchanged.

If assume_correct is set, the resulting WDBA is not checked for correctness. Note that the correctness check is already skipped in all cases captured by minimize_obligation_guaranteed_to_work(). Setting this allows to skip the correctness checks in more cases, if you know that the input is an obligation property.

◆ minimize_obligation_guaranteed_to_work()

bool spot::minimize_obligation_guaranteed_to_work	(	const const_twa_graph_ptr &	aut_f,
		formula	f = `nullptr`
	)

#include <spot/twaalgos/minimize.hh>

Whether calling minimize_obligation is sure to work.

This checks whether f is a syntactic obligation, or if aut_f obviously corresponds to an obligation (for instance if this is a terminal automaton, or if it is both weak and deterministic). In this case, calling minimize_obligation() should not be a waste of time, as it will return a new automaton.

If this function returns false, the input property might still be a pathological obligation. The only way to know is to call minimize_obligation(), but as it is less likely, you might decide to save time.

◆ minimize_wdba()

twa_graph_ptr spot::minimize_wdba	(	const const_twa_graph_ptr &	a,
		const output_aborter *	aborter = `nullptr`
	)

#include <spot/twaalgos/minimize.hh>

Minimize a Büchi automaton in the WDBA class.

This takes a TGBA whose language is representable by a Weak Deterministic Büchi Automaton, and construct a minimal WDBA for this language. This essentially chains three algorithms: determinization, acceptance adjustment (Löding's coloring algorithm), and minimization (using a Moore-like approach).

If the input automaton does not represent a WDBA language, the resulting automaton is still a WDBA, but it will accept a superset of the original language. Use the minimize_obligation() function if you are not sure whether it is safe to call this function.

The construction is inspired by the following paper, however we guarantee that the output language is a subset of the original language while they don't. [dax.07.atva]

If an output_aborter is given, the determinization is aborted whenever it would produce an automaton that is too large. In that case, a nullptr is returned.

◆ reduce_direct_cosim()

twa_graph_ptr spot::reduce_direct_cosim ( const const_twa_graph_ptr & aut )

#include <spot/twaalgos/simulation.hh>

Attempt to reduce the automaton by reverse simulation.

Reverse the automaton, compute the simulation and reduce it in the same way as reduce_direct_sim().

There is no need to call scc_filter() before as it is always applied to remove dead and unreachable states.

Parameters

aut	the automaton to simulate.

Returns: a new automaton which is at worst a copy of the received one

◆ reduce_direct_cosim_sba()

twa_graph_ptr spot::reduce_direct_cosim_sba ( const const_twa_graph_ptr & aut )

#include <spot/twaalgos/simulation.hh>

Attempt to reduce the automaton by reverse simulation.

Reverse the automaton, compute the simulation and reduce it in the same way as reduce_direct_sim().

There is no need to call scc_filter() before as it is always applied to remove dead and unreachable states.

Parameters

aut	the automaton to simulate.

Returns: a new automaton which is at worst a copy of the received one

◆ reduce_direct_sim()

twa_graph_ptr spot::reduce_direct_sim ( const const_twa_graph_ptr & aut )

#include <spot/twaalgos/simulation.hh>

Attempt to reduce the automaton by direct simulation.

Compute direct simulation for all states using [clemente.2.17.corr], then reduce the automaton.

There is no need to call scc_filter() before as it is always applied to remove dead and unreachable states.

Parameters

aut	the automaton to simulate.

Returns: a new automaton which is at worst a copy of the received one

◆ reduce_direct_sim_sba()

twa_graph_ptr spot::reduce_direct_sim_sba ( const const_twa_graph_ptr & aut )

#include <spot/twaalgos/simulation.hh>

Attempt to reduce the automaton by direct simulation.

Compute direct simulation for all states using [clemente.2.17.corr], then reduce the automaton.

There is no need to call scc_filter() before as it is always applied to remove dead and unreachable states.

Parameters

aut	the automaton to simulate.

Returns: a new automaton which is at worst a copy of the received one

◆ reduce_iterated()

twa_graph_ptr spot::reduce_iterated ( const const_twa_graph_ptr & aut )

#include <spot/twaalgos/simulation.hh>

Iterate reduce_direct_sim() and reduce_direct_cosim().

Runs reduce_direct_sim() and reduce_direct_cosim() in a loop, until the automaton does not change size (states and transitions).

There is no need to call scc_filter() before as it is always applied to remove dead and unreachable states.

Parameters

aut	the automaton to simulate.

Returns: a new automaton which is at worst a copy of the received one

◆ reduce_iterated_sba()

twa_graph_ptr spot::reduce_iterated_sba ( const const_twa_graph_ptr & aut )

#include <spot/twaalgos/simulation.hh>

Iterate reduce_direct_sim() and reduce_direct_cosim().

Runs reduce_direct_sim() and reduce_direct_cosim() in a loop, until the automaton does not change size (states and transitions).

There is no need to call scc_filter() before as it is always applied to remove dead and unreachable states.

Parameters

aut	the automaton to simulate.

Returns: a new automaton which is at worst a copy of the received one

◆ scc_filter()

twa_graph_ptr spot::scc_filter	(	const const_twa_graph_ptr &	aut,
		bool	remove_all_useless = `false`,
		scc_info *	given_si = `nullptr`,
		bool	keep_one_color = `false`
	)

#include <spot/twaalgos/sccfilter.hh>

Prune unaccepting SCCs and remove superfluous acceptance conditions.

This function will explore the SCCs of the automaton and remove dead SCCs (i.e. SCC that are not accepting, and those with no exit path leading to an accepting SCC).

Additionally, for Generalized Büchi acceptance, this will try to remove useless acceptance conditions. This operation may diminish the number of acceptance condition of the automaton (for instance when two acceptance conditions are always used together we only keep one) but it will never remove all acceptance conditions, even if it would be OK to have zero.

Acceptance conditions on transitions going to rejecting SCCs are all removed. Acceptance conditions going to an accepting SCC and coming from another SCC are only removed if remove_all_useless is set. The default value of remove_all_useless is false because some algorithms (like the degeneralization) will work better if transitions going to an accepting SCC are accepting.

If the input is inherently weak, the output will be a weak automaton with state-based acceptance. If the automaton had no rejecting SCC, the acceptance condition is set to "t". Otherwise, the acceptance condition is set to Büchi unless the input was co-Büchi (in which case we keep this acceptance).

If given_si is supplied, the function will use its result without computing a map of its own.

If keep_one_color is set, the output will keep at least color if the input had colors. Normally scc_filter removes as many colors as possible.

Warning: Calling scc_filter on a TωA that is not inherently weak and has the SBA property (i.e., transitions leaving accepting states are all marked as accepting) may destroy this property. Use scc_filter_states() instead.

If the properties "state-names", "highlight-states", "original-states", or "degen-levels" are present in the input automaton, they will be preserved (and adjusted) in the output automaton.

◆ scc_filter_states()

twa_graph_ptr spot::scc_filter_states	(	const const_twa_graph_ptr &	aut,
		bool	remove_all_useless = `false`,
		scc_info *	given_si = `nullptr`
	)

#include <spot/twaalgos/sccfilter.hh>

Prune unaccepting SCCs.

This is an abridged version of scc_filter(), that preserves state-based acceptance. I.e., if the input TωA has the SBA property, (i.e., transitions leaving accepting states are all marked as accepting), then the output TωA will also have that property.

◆ scc_filter_susp()

twa_graph_ptr spot::scc_filter_susp	(	const const_twa_graph_ptr &	aut,
		bool	remove_all_useless,
		bdd	suspvars,
		bdd	ignoredvars,
		bool	early_susp,
		scc_info *	given_si = `nullptr`
	)

#include <spot/twaalgos/sccfilter.hh>

Prune unaccepting SCCs, superfluous acceptance sets, and suspension variables.

In addition to removing useless states, and acceptance sets, this remove all ignoredvars occurring in conditions, and all suspvars in conditions leadings to non-accepting SCC (as well as the conditions between two SCCs if early_susp is false).

This is used by compsusp(), and is probably useless for any other use.

◆ simulation() [1/2]

twa_graph_ptr spot::simulation	(	const const_twa_graph_ptr &	automaton,
		int	trans_pruning = `-1`
	)

#include <spot/twaalgos/simulation.hh>

Attempt to reduce the automaton by direct simulation.

When the suffixes (letter and acceptance conditions) reachable from one state are included in the suffixes seen by another one, the former state can be merged into the latter. The algorithm is described in [babiak.13.spin] .

Our reconstruction of the quotient automaton based on this suffix-inclusion relation will also improve determinism thanks to a kind of transition-pruning.

We recommend to call scc_filter() to first simplify the automaton that should be reduced by simulation.

Reducing an automaton by simulation does not change the number of acceptance conditions. In some rare cases (1 out of more than 500 in our benchmark), the reduced automaton will use more acceptance conditions than necessary, and running scc_filter() again afterwards will remove these superfluous conditions.

The resulting automaton has a named property "simulated-states", that is a vector mapping each state of the input to a state of the output. Note that some input states may be mapped to -1, as a by-product of transition pruning.

Parameters

automaton	the automaton to simulate.
trans_pruning	Transition pruning requires a quadratic number of BDD implication checks between all equivalence classes, so it can be costly on large automata. If trans_pruning is set to a non-negative integer, only (non-deterministic) automata with more states than trans_pruning will be simplified.

Returns: a new automaton which is at worst a copy of the received one

◆ simulation() [2/2]

twa_graph_ptr spot::simulation	(	const const_twa_graph_ptr &	automaton,
		std::vector< bdd > *	implications,
		int	trans_pruning = `-1`
	)

#include <spot/twaalgos/simulation.hh>

Attempt to reduce the automaton by direct simulation.

Like simulation(), but also returns the computed implications vector.

Parameters

automaton	the automaton to simulate.
implications	output parameter for simulation implications.
trans_pruning	threshold for transition pruning (see simulation()).

Returns: a new automaton which is at worst a copy of the received one.

◆ simulation_sba()

twa_graph_ptr spot::simulation_sba	(	const const_twa_graph_ptr &	automaton,
		int	trans_pruning = `-1`
	)

#include <spot/twaalgos/simulation.hh>

Attempt to reduce a state-based acceptance automaton by direct simulation.

Like simulation(), but preserves state-based acceptance.

Parameters

automaton	the automaton to simulate.
trans_pruning	threshold for transition pruning (see simulation()).

Returns: a new automaton which is at worst a copy of the received one.

Classes

Functions

Detailed Description

Function Documentation

◆ cosimulation()

◆ cosimulation_sba()

◆ dtba_sat_minimize()

◆ dtba_sat_synthetize()

◆ dtwa_sat_synthetize()

◆ iterated_simulations()

◆ iterated_simulations_sba()

◆ minimize_monitor()

◆ minimize_obligation()

◆ minimize_obligation_guaranteed_to_work()

◆ minimize_wdba()

◆ reduce_direct_cosim()

◆ reduce_direct_cosim_sba()

◆ reduce_direct_sim()

◆ reduce_direct_sim_sba()

◆ reduce_iterated()

◆ reduce_iterated_sba()

◆ scc_filter()

◆ scc_filter_states()

◆ scc_filter_susp()

◆ simulation() [1/2]

◆ simulation() [2/2]

◆ simulation_sba()