Classes
class	spot::isomorphism_checker
	Check if two automata are isomorphic. More...

class	spot::scc_info_node
	Storage for SCC related information. More...

class	spot::scc_info
	Compute an SCC map and gather assorted information. More...

class	spot::scc_and_mark_filter
	Create a filter for SCC and marks. More...

struct	spot::edge_separator_filter< subsumed >
	A filter for iterating over edge labels compatible with a given BDD condition. More...

class	spot::edge_separator
	separate edges so that their labels are disjoint More...

struct	spot::twa_statistics
	Basic statistics (states and edges counts) for a TωA. More...

struct	spot::twa_sub_statistics
	Extended statistics including transition counts for a TωA. More...

class	spot::printable_formula
	A printable wrapper for a formula, for use in format strings. More...

class	spot::printable_acc_cond
	A printable wrapper for an acceptance condition, for use in format strings. More...

class	spot::printable_scc_info
	A printable wrapper for SCC information of an automaton, for use in format strings. More...

class	spot::printable_size
	A printable wrapper reporting reachable and total state/edge counts. More...

class	spot::printable_long_size
	A printable wrapper reporting reachable and total transition counts as long long. More...

class	spot::stat_printer
	prints various statistics about a TGBA More...

Enumerations
enum	spot::mcs_tie_break { spot::MCS_TIE_ANY = 0 , spot::MCS_TIE_SCC }
	Tie-breaking strategy for maximum cardinality search. More...

enum class	spot::scc_info_options { spot::NONE = 0 , spot::STOP_ON_ACC = 1 , spot::TRACK_STATES = 2 , spot::TRACK_SUCCS = 4 , spot::TRACK_STATES_IF_FIN_USED = 8 , spot::PROCESS_UNREACHABLE_STATES = 16 , spot::ALL = TRACK_STATES \| TRACK_SUCCS }
	Options to alter the behavior of scc_info. More...

Functions
bool	spot::isomorphism_checker::is_isomorphic (const const_twa_graph_ptr aut)
	Check whether an automaton is isomorphic to the one passed to the constructor. More...

static bool	spot::isomorphism_checker::are_isomorphic (const const_twa_graph_ptr ref, const const_twa_graph_ptr aut)
	Check whether two automata are isomorphic. More...

twa_graph_ptr	spot::canonicalize (twa_graph_ptr aut)
	Reorder the states and transitions of aut in a way that will be the same for every isomorphic automata. More...

twa_graph_ptr	spot::restrict_dead_end_edges_here (twa_graph_ptr &aut)
	Restrict labels from "dead-end edges". More...

twa_graph_ptr	spot::dualize (const const_twa_graph_ptr &aut)
	Complement an automaton by dualizing it. More...

twa_graph_ptr	spot::g_f_terminal_inplace (twa_graph_ptr f_terminal, bool state_based=false)
	Given a terminal automaton f_terminal recognizing some formula F(φ), modify it to recognize GF(φ). More...

unsigned	spot::count_nondet_states (const const_twa_graph_ptr &aut)
	Count the number of states with non-deterministic branching in aut. More...

bool	spot::is_universal (const const_twa_graph_ptr &aut)
	Return true iff aut is universal. More...

bool	spot::is_deterministic (const const_twa_graph_ptr &aut)
	Return true iff aut is deterministic. More...

void	spot::highlight_nondet_states (twa_graph_ptr &aut, unsigned color)
	Highlight nondeterministic states. More...

void	spot::highlight_nondet_edges (twa_graph_ptr &aut, unsigned color)
	Highlight nondeterministic edges. More...

void	spot::highlight_semidet_sccs (scc_info &si, unsigned color)
	Highlight the deterministic part of the automaton. More...

bool	spot::is_complete (const const_twa_graph_ptr &aut)
	Return true iff aut is complete. More...

bool	spot::is_semi_deterministic (const const_twa_graph_ptr &aut)
	Return true iff aut is semi-deterministic. More...

std::vector< bool >	spot::semidet_sccs (scc_info &si)
	Whether an SCC is in the deterministic part of an automaton. More...

void	spot::check_determinism (twa_graph_ptr aut)
	Set the deterministic and semi-deterministic properties appropriately. More...

bool	spot::is_unambiguous (const const_twa_graph_ptr &aut)
	Whether the automaton aut is unambiguous. More...

bool	spot::check_unambiguous (const twa_graph_ptr &aut)
	Like is_unambiguous(), but also sets the property in the twa. More...

bool	spot::scc_has_rejecting_cycle (scc_info &map, unsigned scc)
	Whether the SCC number scc in map has a rejecting cycle. More...

bool	spot::is_inherently_weak_scc (scc_info &map, unsigned scc)
	Whether the SCC number scc in map is inherently weak. More...

bool	spot::is_weak_scc (scc_info &map, unsigned scc)
	Whether the SCC number scc in map is weak. More...

bool	spot::is_complete_scc (scc_info &map, unsigned scc)
	Whether the SCC number scc in map is complete. More...

bool	spot::is_terminal_scc (scc_info &map, unsigned scc)
	Whether the SCC number scc in map is terminal. More...

std::vector< unsigned >	spot::language_map (const const_twa_graph_ptr &aut)
	Identify states that recognize the same language. More...

void	spot::highlight_languages (twa_graph_ptr &aut)
	Color states that recognize identical language. More...

std::vector< unsigned >	spot::maximum_cardinality_search (const const_twa_graph_ptr &a, mcs_tie_break tie=MCS_TIE_ANY)
	Return an ordering of the vertices computed by a maximum cardinality search. More...

twa_graph_ptr	spot::maximum_cardinality_search_reorder_here (twa_graph_ptr a, mcs_tie_break tie=MCS_TIE_ANY)
	Reorder the states of a according to the order computed by maximum_cardinality_search(). More...

twa_graph_ptr	spot::tgba_powerset (const const_twa_graph_ptr &aut, power_map &pm, bool merge=true, const output_aborter aborter=nullptr, std::vector< unsigned > accepting_sinks=nullptr)
	Build a deterministic automaton, ignoring acceptance conditions. More...

twa_graph_ptr	spot::random_graph (int n, float d, const atomic_prop_set *ap, const bdd_dict_ptr &dict, unsigned n_accs=0, float a=0.1, float t=0.5, bool deterministic=false, bool state_acc=false, bool colored=false)
	Construct a twa randomly. More...

acc_cond::acc_code	spot::random_acceptance (unsigned n_accs)
	Build a random acceptance where each acceptance set is used once. More...

void	spot::randomize (twa_graph_ptr &aut, bool randomize_states=true, bool randomize_edges=true)
	Randomize a TGBA. More...

twa_graph_ptr	spot::split_edges (const const_twa_graph_ptr &aut)
	Transform edges into transitions. More...

twa_graph_ptr	spot::separate_edges (const const_twa_graph_ptr &aut)
	Make edge labels disjoint. More...

twa_statistics	spot::stats_reachable (const const_twa_ptr &g)
	Compute statistics for an automaton. More...

twa_sub_statistics	spot::sub_stats_reachable (const const_twa_ptr &g)
	Compute sub statistics for an automaton. More...

unsigned long long	spot::count_all_transitions (const const_twa_graph_ptr &g)
	Count all transitions, even unreachable ones. More...

bool	spot::is_terminal_automaton (const const_twa_graph_ptr &aut, scc_info *sm=nullptr)
	Check whether an automaton is terminal. More...

bool	spot::is_weak_automaton (const const_twa_graph_ptr &aut, scc_info *sm=nullptr)
	Check whether an automaton is weak. More...

bool	spot::is_very_weak_automaton (const const_twa_graph_ptr &aut, scc_info *sm=nullptr)
	Check whether an automaton is very-weak. More...

bool	spot::is_inherently_weak_automaton (const const_twa_graph_ptr &aut, scc_info *sm=nullptr)
	Check whether an automaton is inherently weak. More...

bool	spot::is_safety_automaton (const const_twa_graph_ptr &aut, scc_info *sm=nullptr)
	Check whether an automaton is a safety automaton. More...

bool	spot::is_liveness_automaton (const const_twa_graph_ptr &aut)
	Whether the automaton represents a liveness property. More...

void	spot::check_strength (const twa_graph_ptr &aut, scc_info *sm=nullptr)
	Check whether an automaton is weak or terminal. More...

twa_graph_ptr	spot::decompose_scc (const const_twa_graph_ptr &aut, const char *keep)
	Extract a sub-automaton of a given strength. More...

twa_graph_ptr	spot::decompose_scc (scc_info &sm, const char *keep)
	Extract a sub-automaton of a given strength. More...

twa_graph_ptr	spot::decompose_scc (scc_info &sm, unsigned scc_num, bool accepting=false)
	Extract a sub-automaton above an SCC. More...

void	spot::strip_acceptance_here (twa_graph_ptr a)
	Remove all acceptance sets from a twa_graph. More...

enum class	spot::edge_filter_choice { keep , ignore , cut }
	An edge_filter may be called on each edge to decide what to do with it. More...

typedef edge_filter_choice(*	spot::edge_filter) (const twa_graph::edge_storage_t &e, unsigned dst, void *filter_data)
	An edge_filter may be called on each edge to decide what to do with it. More...

Detailed Description

Typedef Documentation

◆ edge_filter

typedef edge_filter_choice(* spot::edge_filter) (const twa_graph::edge_storage_t &e, unsigned dst, void *filter_data)

#include <spot/twaalgos/sccinfo.hh>

An edge_filter may be called on each edge to decide what to do with it.

The edge filter is called with an edge and a destination. (In existential automata the destination is already given by the edge, but in alternating automata, one edge may have several destinations, and in this case the filter will be called for each destination.) The filter should return a value from edge_filter_choice.

keep means to use the edge normally, as if no filter had been given. ignore means to pretend the edge does not exist (if the destination is only reachable through this edge, it will not be visited). cut also ignores the edge, but it remembers to visit the destination state (as if it were an initial state) in case it is not reachable otherwise.

Note that successors between SCCs can only be maintained for edges that are kept. If some edges are ignored or cut, the SCC graph that you can explore with scc_info::initial() and scc_info::succ() will be restricted to the portion reachable with "keep" edges. Additionally, SCCs might be created when edges are cut, but those will not be reachable from scc_info::initial()..

Enumeration Type Documentation

◆ edge_filter_choice

enum spot::edge_filter_choice

strong

#include <spot/twaalgos/sccinfo.hh>

An edge_filter may be called on each edge to decide what to do with it.

The edge filter is called with an edge and a destination. (In existential automata the destination is already given by the edge, but in alternating automata, one edge may have several destinations, and in this case the filter will be called for each destination.) The filter should return a value from edge_filter_choice.

keep means to use the edge normally, as if no filter had been given. ignore means to pretend the edge does not exist (if the destination is only reachable through this edge, it will not be visited). cut also ignores the edge, but it remembers to visit the destination state (as if it were an initial state) in case it is not reachable otherwise.

Note that successors between SCCs can only be maintained for edges that are kept. If some edges are ignored or cut, the SCC graph that you can explore with scc_info::initial() and scc_info::succ() will be restricted to the portion reachable with "keep" edges. Additionally, SCCs might be created when edges are cut, but those will not be reachable from scc_info::initial()..

◆ mcs_tie_break

enum spot::mcs_tie_break

#include <spot/twaalgos/mcs.hh>

Tie-breaking strategy for maximum cardinality search.

Enumerator

MCS_TIE_ANY

Break ties by picking the first possible state.

MCS_TIE_SCC

Break ties by picking states from the "highest" SCCs.

  This is based on the topological ordering of SCCs computed
  by scc_info.  The initial state is always in the highest
  SCC, and the smallest SCC has no exit.

◆ scc_info_options

enum spot::scc_info_options

strong

#include <spot/twaalgos/sccinfo.hh>

Options to alter the behavior of scc_info.

Enumerator
NONE	Explore all SCCs, but do not track the states of each SCC and the successor SCC of each SCC. This is enough to call the scc_of() method.
STOP_ON_ACC	Stop exploring after an accepting SCC has been found. Using this option forbids future uses of is_useful_scc() and is_useful_state(). Using it will also cause the output of succ() to be incomplete.
TRACK_STATES	Keep a vector of all states belonging to each SCC. Using this option is a precondition for using states_of(), edges_of(), inner_edges_of(), states_on_acc_cycle_of(), and determine_unknown_acceptance().
TRACK_SUCCS	Keep a list of successors of each SCCs. Using this option is a precondition for using succ(), is_useful_scc(), and is_useful_state().
TRACK_STATES_IF_FIN_USED	Conditionally track states if the acceptance condition uses Fin. This is sufficient for determine_unknown_acceptance().
PROCESS_UNREACHABLE_STATES	Also compute SCCs for the unreachable states. When this is used, SCCs are first enumerated from state 0, and then from the next unvisited states. In other words the initial state does not play any role. If STOP_ON_ACC is used with PROCESS_UNREACHABLE_STATES, the enumeration will stop as soon as an SCC is found, but that SCC might not be reachable.
ALL	Default behavior: explore everything and track states and succs.

Function Documentation

◆ are_isomorphic()

static bool spot::isomorphism_checker::are_isomorphic	(	const const_twa_graph_ptr	ref,
		const const_twa_graph_ptr	aut
	)

static

#include <spot/twaalgos/are_isomorphic.hh>

Check whether two automata are isomorphic.

◆ canonicalize()

twa_graph_ptr spot::canonicalize ( twa_graph_ptr aut )

#include <spot/twaalgos/canonicalize.hh>

Reorder the states and transitions of aut in a way that will be the same for every isomorphic automata.

◆ check_determinism()

void spot::check_determinism ( twa_graph_ptr aut )

#include <spot/twaalgos/isdet.hh>

Set the deterministic and semi-deterministic properties appropriately.

◆ check_strength()

void spot::check_strength	(	const twa_graph_ptr &	aut,
		scc_info *	sm = `nullptr`
	)

#include <spot/twaalgos/strength.hh>

Check whether an automaton is weak or terminal.

This sets the "inherently weak", "weak", "very-weak" and "terminal" properties as appropriate.

Parameters

aut	the automaton to check
sm	an scc_info object for the automaton if available (it will be built otherwise).

◆ check_unambiguous()

bool spot::check_unambiguous ( const twa_graph_ptr & aut )

#include <spot/twaalgos/isunamb.hh>

Like is_unambiguous(), but also sets the property in the twa.

◆ count_all_transitions()

unsigned long long spot::count_all_transitions ( const const_twa_graph_ptr & g )

#include <spot/twaalgos/stats.hh>

Count all transitions, even unreachable ones.

◆ count_nondet_states()

unsigned spot::count_nondet_states ( const const_twa_graph_ptr & aut )

#include <spot/twaalgos/isdet.hh>

Count the number of states with non-deterministic branching in aut.

The automaton is universal if it has 0 states with non-deterministic branching but it is more efficient to call is_universal() if you do not care about the number of non-deterministic states.

◆ decompose_scc() [1/3]

twa_graph_ptr spot::decompose_scc	(	const const_twa_graph_ptr &	aut,
		const char *	keep
	)

#include <spot/twaalgos/strength.hh>

Extract a sub-automaton of a given strength.

The string keep should be a non-empty combination of the following letters:

'w': keep only inherently weak SCCs (i.e., SCCs in which all transitions belong to the same acceptance sets) that are not terminal.
't': keep terminal SCCs (i.e., inherently weak SCCs that are complete)
's': keep strong SCCs (i.e., SCCs that are not inherently weak). Additionally, the string may contain comma-separated numbers representing SCC number, optionally prefixed by 'a' to denote the Nth accepting SCC.

This algorithm returns a subautomaton that contains all SCCs of the requested strength (or given SCC numbers), plus any upstream SCC (but adjusted not to be accepting). The output may be null if no SCC match a given strength. An exception will be raised if an incorrect SCC number is supplied.

The definition are basically those used in the following paper, except that we extract the "inherently weak" part instead of the weak part because we can now test for inherent weakness efficiently enough (not enumerating all cycles as suggested in the paper). [renault.13.tacas]

Parameters

aut	the automaton to decompose
keep	a string specifying the strengths/SCCs to keep

◆ decompose_scc() [2/3]

twa_graph_ptr spot::decompose_scc	(	scc_info &	sm,
		const char *	keep
	)

#include <spot/twaalgos/strength.hh>

Extract a sub-automaton of a given strength.

This works exactly like decompose_scc(const const_twa_graph_ptr&, const char*) but takes an scc_info as first argument. This avoids wasting time to reconstruct that object if one is already available.

◆ decompose_scc() [3/3]

twa_graph_ptr spot::decompose_scc	(	scc_info &	sm,
		unsigned	scc_num,
		bool	accepting = `false`
	)

#include <spot/twaalgos/strength.hh>

Extract a sub-automaton above an SCC.

This algorithm returns a subautomaton that contains the requested SCC, plus any upstream SCC (but adjusted not to be accepting).

Parameters

sm	the SCC info map of the automaton
scc_num	the index in the map of the SCC to keep
accepting	if true, scc_num is interpreted as the Nth accepting SCC instead of the Nth SCC

◆ dualize()

twa_graph_ptr spot::dualize ( const const_twa_graph_ptr & aut )

#include <spot/twaalgos/dualize.hh>

Complement an automaton by dualizing it.

Given an automaton aut of any type, produces the dual as output. Before dualization, the automaton will be completed if it isn't already, but any sink state in the output might then be removed.

Dualizing the automaton is done by interpreting the outgoing transitions of a state as a Boolean function, and then swapping operators ∧ and ̇∨. This first step does not have to be done on deterministic automata. Additionally, the acceptance condition is dualized by swapping operators ∧ and ̇∨, and swapping Inf and Fin.

For instance, the dual of a generalized Büchi automaton will be a generalized co-Büchi automaton.

If the input acceptance condition accepts every infinite path (such as "t" or "Inf(0)|Fin(0)") and the automaton is not complete, then the input automaton will be assumed to have Büchi acceptance in order to complete it, and the output will then have co-Büchi acceptance.

Due to a defect in the way transition-based alternating automata are represented in Spot and in the HOA format, existential automata with transition-based acceptance will be converted to use state-based acceptance before dualization. See https://github.com/adl/hoaf/issues/68 for more information.

If the input automaton is deterministic, the output will be deterministic. If the input automaton is existential, the output will be universal. If the input automaton is universal, the output will be existential. Finally, if the input automaton is alternating, the result is alternating. More can be found on page 22 (Definition 1.6) of [loding.98.msc] .

Functions like to_generalized_buchi() or remove_fin() are frequently called on existential automata after dualize() to obtain an easier acceptance condition, but maybe at the cost of losing determinism.

Up to version 2.11.6, this function used to call cleanup_acceptance_here() to simplify the acceptance condition after dualization. This caused some surprises, users expected the dual of a Büchi automaton to be a co-Büchi automaton, but cleanup_acceptance_here() sometimes reduced the condition to t when all states where accepting. This function is not called anymore since version 2.12.

◆ g_f_terminal_inplace()

twa_graph_ptr spot::g_f_terminal_inplace	(	twa_graph_ptr	f_terminal,
		bool	state_based = `false`
	)

#include <spot/twaalgos/gfguarantee.hh>

Given a terminal automaton f_terminal recognizing some formula F(φ), modify it to recognize GF(φ).

If state_based is set, the automaton's terminal states are all replaced by a unique accepting state that has the same outgoing transitions as the initial state, and the initial state is actually relocated to that accepting state. The latter point is not necessary, but it favors shorter accepting cycles.

If state_based is not set, all transition going to terminal states are made accepting and redirected to the initial state.

This construction is inspired by a similar construction in the LICS'18 paper by Esparza et al. [esparza.18.lics]

◆ highlight_languages()

void spot::highlight_languages ( twa_graph_ptr & aut )

#include <spot/twaalgos/langmap.hh>

Color states that recognize identical language.

States that recognize a unique language will not be colored.

◆ highlight_nondet_edges()

void spot::highlight_nondet_edges	(	twa_graph_ptr &	aut,
		unsigned	color
	)

#include <spot/twaalgos/isdet.hh>

Highlight nondeterministic edges.

An edge is nondeterministic if there exist another edge leaving the same source state, with a compatible label (i.e., the conjunction of the two labels is not false).

Parameters

aut	the automaton to process
color	the color to give to nondeterministic edges.

◆ highlight_nondet_states()

void spot::highlight_nondet_states	(	twa_graph_ptr &	aut,
		unsigned	color
	)

#include <spot/twaalgos/isdet.hh>

Highlight nondeterministic states.

A state is nondeterministic if it has two outgoing edges whose labels are not incompatible.

Parameters

aut	the automaton to process
color	the color to give to nondeterministic states.

◆ highlight_semidet_sccs()

void spot::highlight_semidet_sccs	(	scc_info &	si,
		unsigned	color
	)

#include <spot/twaalgos/isdet.hh>

Highlight the deterministic part of the automaton.

In the case of a semideterministic automaton, highlights the states reachable from any accepting SCC.

Parameters

si	the SCC information of the automaton to process
color	the color to give to states reachable from accepting SCCs.

◆ is_complete()

bool spot::is_complete ( const const_twa_graph_ptr & aut )

#include <spot/twaalgos/isdet.hh>

Return true iff aut is complete.

An automaton is complete if its translation relation is total, i.e., each state has a successor for any possible configuration.

◆ is_complete_scc()

bool spot::is_complete_scc	(	scc_info &	map,
		unsigned	scc
	)

#include <spot/twaalgos/isweakscc.hh>

Whether the SCC number scc in map is complete.

An SCC is complete iff for all states and all labels there exists a transition that stays into this SCC. For this function, universal transitions are considered in the SCC if all their destinations are into the SCC.

◆ is_deterministic()

bool spot::is_deterministic ( const const_twa_graph_ptr & aut )

#include <spot/twaalgos/isdet.hh>

Return true iff aut is deterministic.

An automaton is called deterministic if it is both universal and existential.

◆ is_inherently_weak_automaton()

bool spot::is_inherently_weak_automaton	(	const const_twa_graph_ptr &	aut,
		scc_info *	sm = `nullptr`
	)

#include <spot/twaalgos/strength.hh>

Check whether an automaton is inherently weak.

An automaton is inherently weak if in any given SCC, there are only accepting cycles, or only rejecting cycles.

Parameters

aut	the automaton to check
sm	an scc_info object for the automaton if available (it will be built otherwise).

In addition to returning the result as a Boolean, this will set the prop_inherently_weak() property of the automaton as a side-effect, so further calls will return in constant-time.

◆ is_inherently_weak_scc()

bool spot::is_inherently_weak_scc	(	scc_info &	map,
		unsigned	scc
	)

#include <spot/twaalgos/isweakscc.hh>

Whether the SCC number scc in map is inherently weak.

An SCC is inherently weak if either its cycles are all accepting, or they are all non-accepting.

Note that terminal SCCs are also inherently weak with that definition.

◆ is_isomorphic()

bool spot::isomorphism_checker::is_isomorphic ( const const_twa_graph_ptr aut )

#include <spot/twaalgos/are_isomorphic.hh>

Check whether an automaton is isomorphic to the one passed to the constructor.

Two automata are considered isomorphic if there exists a bijection f between the states of a1 and the states of a2 such that for any pair of states (s1, s2) of a1, there is a transition from s1 to s2 with condition c and acceptance set A iff there is a transition with condition c and acceptance set A between f(s1) and f(s2) in a2. This can be done simply by checking if canonicalize(aut1) == canonicalize(aut2), but is_isomorphic can do some optimizations in some cases.

◆ is_liveness_automaton()

bool spot::is_liveness_automaton ( const const_twa_graph_ptr & aut )

#include <spot/twaalgos/strength.hh>

Whether the automaton represents a liveness property.

An automaton represents a liveness property if after forcing the acceptance condition to true, the resulting automaton accepts all words. In other words, there is no prefix that cannot be extended into an accepting word.

◆ is_safety_automaton()

bool spot::is_safety_automaton	(	const const_twa_graph_ptr &	aut,
		scc_info *	sm = `nullptr`
	)

#include <spot/twaalgos/strength.hh>

Check whether an automaton is a safety automaton.

An automaton is a safety automaton if its acceptance condition can be changed to "true" without changing its language.

The test performed by this function differs depending on the nature of the input aut.

If aut is an automaton with t acceptance, it is necessarily a safety automaton.

Else we check for the absence of rejecting cycle in the useful part of the automaton. This absence is only a sufficient condition in the non-deterministic case, because a rejecting run might correspond to a word that is accepted by another run.

If the previous test could not conclude, we build the automaton B that is a copy of aut with acceptance set to true, and we check that aut contains all words of B. This last test requires complementing aut.

Parameters

aut	the automaton to check
sm	an scc_info object for the automaton if available (it will be built otherwise).

◆ is_semi_deterministic()

bool spot::is_semi_deterministic ( const const_twa_graph_ptr & aut )

#include <spot/twaalgos/isdet.hh>

Return true iff aut is semi-deterministic.

An automaton is semi-deterministic if the sub-automaton reachable from any accepting SCC is deterministic.

◆ is_terminal_automaton()

bool spot::is_terminal_automaton	(	const const_twa_graph_ptr &	aut,
		scc_info *	sm = `nullptr`
	)

#include <spot/twaalgos/strength.hh>

Check whether an automaton is terminal.

An automaton is terminal if it is weak, all its accepting SCCs are complete, and no accepting SCC may lead to a non-accepting SCC.

This property guarantees that a word is accepted if it has some prefix that reaches an accepting transition.

Parameters

aut	the automaton to check
sm	an scc_info object for the automaton if available (it will be built otherwise).

In addition to returning the result as a Boolean, this will set the prop_terminal() property of the automaton as a side-effect, so further calls will return in constant-time.

◆ is_terminal_scc()

bool spot::is_terminal_scc	(	scc_info &	map,
		unsigned	scc
	)

#include <spot/twaalgos/isweakscc.hh>

Whether the SCC number scc in map is terminal.

An SCC is terminal if it is weak, complete, and accepting.

◆ is_unambiguous()

bool spot::is_unambiguous ( const const_twa_graph_ptr & aut )

#include <spot/twaalgos/isunamb.hh>

Whether the automaton aut is unambiguous.

An automaton is unambiguous if each accepted word is recognized by only one path.

We check unambiguity by synchronizing the automaton with itself, and then making sure that the co-reachable part of the squared automaton has the same size as the co-reachable part of the original automaton.

◆ is_universal()

bool spot::is_universal ( const const_twa_graph_ptr & aut )

#include <spot/twaalgos/isdet.hh>

Return true iff aut is universal.

This function is more efficient than count_nondet_states() when the automaton is nondeterministic, because it can return before the entire automaton has been explored.

In addition to returning the result as a Boolean, this will set the prop_universal() property of the automaton as a side-effect, so further calls will return in constant-time.

◆ is_very_weak_automaton()

bool spot::is_very_weak_automaton	(	const const_twa_graph_ptr &	aut,
		scc_info *	sm = `nullptr`
	)

#include <spot/twaalgos/strength.hh>

Check whether an automaton is very-weak.

An automaton is very-weak if in any given SCC, all transitions belong to the same acceptance sets, and the SCC has only one state.

Parameters

aut	the automaton to check
sm	an scc_info object for the automaton if available (it will be built otherwise).

In addition to returning the result as a Boolean, this will set the prop_very_weak() and prop_weak() properties of the automaton as a side-effect, so further calls will return in constant-time.

◆ is_weak_automaton()

bool spot::is_weak_automaton	(	const const_twa_graph_ptr &	aut,
		scc_info *	sm = `nullptr`
	)

#include <spot/twaalgos/strength.hh>

Check whether an automaton is weak.

An automaton is weak if in any given SCC, all transitions belong to the same acceptance sets.

Parameters

aut	the automaton to check
sm	an scc_info object for the automaton if available (it will be built otherwise).

In addition to returning the result as a Boolean, this will set the prop_weak() property of the automaton as a side-effect, so further calls will return in constant-time.

◆ is_weak_scc()

bool spot::is_weak_scc	(	scc_info &	map,
		unsigned	scc
	)

#include <spot/twaalgos/isweakscc.hh>

Whether the SCC number scc in map is weak.

An SCC is weak if it is non-accepting, or if all its transitions are fully accepting (i.e., they belong to all acceptance sets).

Note that terminal SCCs are also weak with that definition.

◆ language_map()

std::vector<unsigned> spot::language_map ( const const_twa_graph_ptr & aut )

#include <spot/twaalgos/langmap.hh>

Identify states that recognize the same language.

The returned vector is the same size as the automaton's number of states. The number of different values (ignoring occurrences) in the vector is the total number of recognized languages, states recognizing the same language have the same value.

The given automaton must be deterministic.

◆ maximum_cardinality_search()

std::vector<unsigned> spot::maximum_cardinality_search	(	const const_twa_graph_ptr &	a,
		mcs_tie_break	tie = `MCS_TIE_ANY`
	)

#include <spot/twaalgos/mcs.hh>

Return an ordering of the vertices computed by a maximum cardinality search.

Unlike Tarjan's paper [tarjan.84.sicomp] , where states are numbered from N to 1, this numbers the states from 0 to N-1, starting from the initial state. The next number is assigned to a state that maximizes the number of already-numbered neighbors.

This version returns a vector such that RESULTS[I] is the rank of state I in the computed order.

Parameters

a	The automaton to process.
tie	Specify how to break ties.

◆ maximum_cardinality_search_reorder_here()

twa_graph_ptr spot::maximum_cardinality_search_reorder_here	(	twa_graph_ptr	a,
		mcs_tie_break	tie = `MCS_TIE_ANY`
	)

#include <spot/twaalgos/mcs.hh>

Reorder the states of a according to the order computed by maximum_cardinality_search().

This works in place and return the same automaton.

◆ random_acceptance()

acc_cond::acc_code spot::random_acceptance ( unsigned n_accs )

#include <spot/twaalgos/randomgraph.hh>

Build a random acceptance where each acceptance set is used once.

◆ random_graph()

twa_graph_ptr spot::random_graph	(	int	n,
		float	d,
		const atomic_prop_set *	ap,
		const bdd_dict_ptr &	dict,
		unsigned	n_accs = `0`,
		float	a = `0.1`,
		float	t = `0.5`,
		bool	deterministic = `false`,
		bool	state_acc = `false`,
		bool	colored = `false`
	)

#include <spot/twaalgos/randomgraph.hh>

Construct a twa randomly.

Parameters

n	The number of states wanted in the automata (>0). All states will be connected, and there will be no dead state.
d	The density of the automata. This is the probability (between 0.0 and 1.0), to add a transition between two states. All states have at least one outgoing transition, so d is considered only when adding the remaining transition. A density of 1 means all states will be connected to each other.
ap	The list of atomic properties that should label the transitions.
dict	The bdd_dict to used for this automata.
n_accs	The number of acceptance sets to use. If this number is non null, then there is no guarantee that the generated graph contains an accepting cycle (raise the value of a to improve the chances).
a	The probability (between 0.0 and 1.0) that a transition belongs to an acceptance set.
t	The probability (between 0.0 and 1.0) that an atomic proposition is true.
deterministic	build a complete and deterministic automaton
state_acc	build an automaton with state-based acceptance
colored	build an automaton in which each transition (or state) belongs to a single acceptance set.

This algorithm is adapted from the one in Fig 6.2 page 48 of [tauriainen.00.tr] .

Although the intent is similar, there are some differences between the above published algorithm and this implementation. First labels are on transitions, and acceptance conditions are generated too. Second, the number of successors of a node is chosen in $[1,n]$ following a normal distribution with mean $1+(n-1)d$ and variance $(n-1)d(1-d)$ . (This is less accurate, but faster than considering all possible n successors one by one.)

Note that while this constructs an automaton with random acceptance sets, this does not set the acceptance condition.

◆ randomize()

void spot::randomize	(	twa_graph_ptr &	aut,
		bool	randomize_states = `true`,
		bool	randomize_edges = `true`
	)

#include <spot/twaalgos/randomize.hh>

Randomize a TGBA.

Make a random permutation of the states, and of the edges leaving this state.

This function preserves state names, and highlighted states, but it does not preserve highlighted edges.

◆ restrict_dead_end_edges_here()

twa_graph_ptr spot::restrict_dead_end_edges_here ( twa_graph_ptr & aut )

#include <spot/twaalgos/deadends.hh>

Restrict labels from "dead-end edges".

A dead-end edge is an edge between two states S and D such that D has only itself as successor. I.e., once a run goes through this "dead-end" edge, it gets stuck in D.

Let Lab(S,D) denote the disjunction of all labels between S and D. Let UsefulLab(D,D) be the disjunction of labels of any subset of self-loops of D that will intersect all accepting cycles around D.

Now, if the following implications are satisfied

⎧ UsefulLab(D,D) ⇒ Lab(S,D) ⇒ Lab(S,S),
⎨
⎩ Lab(D,D) ⇒ Lab(S,S).

then any edge between S and D, labeled by ℓ⊆Lab(S,D) can be replaced by ℓ∩UsefulLab(D,D).

This algorithm has no effect on deterministic automata (where it is not possible that Lab(S,D) ⇒ Lab(S,S)).

Computing UsefulLab(D,D) is the tricky part, as many subset of selfloops can be considered. For instance, setting UsefulLab(D,D) := Lab(D,D) clearly intersects all accepting cycles, but it is very coarse. Currently the code uses two smaller definitions for UsefulLab(D,D):

the first is like Lab(D,D), but ignoring transitions that will force the acceptance to be unsatisfiable. For instance, if the acceptance condition is Fin(0)&... then any edge colored with ⓪ will not contribute anything to UsefulLab.
the second definition is only used for Fin-less acceptance conditions. In this case, we select one color for each disjunctive branch of the acceptance condition, and collect all labels from edges matching those colors. For instance if the condition is Inf(0)&Inf(1)|Inf(2) any accepting run is forced to visit some edges labeled by ⓪ or ②, so we gather the labels of all edges colored with these two colors.

◆ scc_has_rejecting_cycle()

bool spot::scc_has_rejecting_cycle	(	scc_info &	map,
		unsigned	scc
	)

#include <spot/twaalgos/isweakscc.hh>

Whether the SCC number scc in map has a rejecting cycle.

◆ semidet_sccs()

std::vector<bool> spot::semidet_sccs ( scc_info & si )

#include <spot/twaalgos/isdet.hh>

Whether an SCC is in the deterministic part of an automaton.

◆ separate_edges()

twa_graph_ptr spot::separate_edges ( const const_twa_graph_ptr & aut )

#include <spot/twaalgos/split.hh>

Make edge labels disjoint.

Create a new version of the automaton where all edges are split in such a way that two labels are either equal or disjoint.

For instance if the automaton uses only {a,b,!a&!b&c} as labels, the result should have label among {a&!b,a&b,!a&b,!a&!b&c}.

Using split_edges() also creates an automaton with separated labels, but the separation will be much finer since it will result in a much involves all atomic propositions.

◆ split_edges()

twa_graph_ptr spot::split_edges ( const const_twa_graph_ptr & aut )

#include <spot/twaalgos/split.hh>

Transform edges into transitions.

Create a new version of the automaton where all edges are split so that they are all labeled by a conjunction of all atomic propositions.

So if an edge is labeled by "true", it will be split into $2^{AP}$ distinct edges.

After this we can consider that each edge of the automaton is a transition labeled by one of $2^{AP}$ letters.

See also: separate_edges

◆ stats_reachable()

twa_statistics spot::stats_reachable ( const const_twa_ptr & g )

#include <spot/twaalgos/stats.hh>

Compute statistics for an automaton.

◆ strip_acceptance_here()

void spot::strip_acceptance_here ( twa_graph_ptr a )

#include <spot/twaalgos/stripacc.hh>

Remove all acceptance sets from a twa_graph.

This will also set the acceptance condition to true, and mark the automaton as weak. Doing so obviously makes all recognized infinite runs accepting.

◆ sub_stats_reachable()

twa_sub_statistics spot::sub_stats_reachable ( const const_twa_ptr & g )

#include <spot/twaalgos/stats.hh>

Compute sub statistics for an automaton.

◆ tgba_powerset()

twa_graph_ptr spot::tgba_powerset	(	const const_twa_graph_ptr &	aut,
		power_map &	pm,
		bool	merge = `true`,
		const output_aborter *	aborter = `nullptr`,
		std::vector< unsigned > *	accepting_sinks = `nullptr`
	)

#include <spot/twaalgos/powerset.hh>

Build a deterministic automaton, ignoring acceptance conditions.

This create a deterministic automaton that recognizes the same language as aut would if its acceptance conditions were ignored. This is the classical powerset algorithm.

If pm is supplied it will be filled with the set of original states associated to each state of the deterministic automaton. The merge argument can be set to false to prevent merging of transitions.

If an aborter is given, abort the construction whenever it would build an automaton that is too large, and return nullptr.

If a vector of accepting sinks is given, all power-state that contains any accepting sink will be merged into a single state with number 0.

Classes

Enumerations

Functions

Detailed Description

Typedef Documentation

◆ edge_filter

Enumeration Type Documentation

◆ edge_filter_choice

◆ mcs_tie_break

◆ scc_info_options

Function Documentation

◆ are_isomorphic()

◆ canonicalize()

◆ check_determinism()

◆ check_strength()

◆ check_unambiguous()

◆ count_all_transitions()

◆ count_nondet_states()

◆ decompose_scc() [1/3]

◆ decompose_scc() [2/3]

◆ decompose_scc() [3/3]

◆ dualize()

◆ g_f_terminal_inplace()

◆ highlight_languages()

◆ highlight_nondet_edges()

◆ highlight_nondet_states()

◆ highlight_semidet_sccs()

◆ is_complete()

◆ is_complete_scc()

◆ is_deterministic()

◆ is_inherently_weak_automaton()

◆ is_inherently_weak_scc()

◆ is_isomorphic()

◆ is_liveness_automaton()

◆ is_safety_automaton()

◆ is_semi_deterministic()

◆ is_terminal_automaton()

◆ is_terminal_scc()

◆ is_unambiguous()

◆ is_universal()

◆ is_very_weak_automaton()

◆ is_weak_automaton()

◆ is_weak_scc()

◆ language_map()

◆ maximum_cardinality_search()

◆ maximum_cardinality_search_reorder_here()

◆ random_acceptance()

◆ random_graph()

◆ randomize()

◆ restrict_dead_end_edges_here()

◆ scc_has_rejecting_cycle()

◆ semidet_sccs()

◆ separate_edges()

◆ split_edges()

◆ stats_reachable()

◆ strip_acceptance_here()

◆ sub_stats_reachable()

◆ tgba_powerset()