spot Namespace Reference

Classes
class	adjlist
	A compact adjacency list representation for directed graphs. More...
class	digraph
	A directed graph. More...
class	named_graph
	A graph wrapper associating named states to graph state indices. More...
class	fair_kripke_succ_iterator
	Iterator code for a Fair Kripke structure. More...
class	fair_kripke
	Interface for a Fair Kripke structure. More...
class	kripkecube
	This class is a template representation of a Kripke structure. It is composed of two template parameters: State represents a state of the Kripke structure, SuccIterator is an iterator over the (possible) successors of a state. More...
class	is_a_kripkecube_ptr
	This class allows to ensure (at compile time) if a given parameter is of type kripkecube. It also checks if the iterator has the right interface. More...
class	kripke_succ_iterator
	Iterator code for Kripke structure. More...
class	kripke
	Interface for a Kripke structure. More...
struct	kripke_graph_state
	Concrete class for kripke_graph states. More...
class	kripke_graph_succ_iterator
	Successor iterator for a graph-based Kripke structure state. More...
class	kripke_graph
	Kripke Structure. More...
class	ltsmin_model
	A loaded LTSmin model that can generate Kripke structures on-the-fly. More...
struct	transition_info
	Transition information passed to callbacks during state-space exploration. More...
class	spins_interface
	Implementation of the PINS interface. This class is a wrapper that, given a file, will compile it w.r.t. the PINS interface. The class can then be manipulated transparently, regardless of the input format. More...
struct	cspins_state_equal
	This class provides the ability to compare two states. More...
struct	cspins_state_hash
	This class provides the ability to hash a state. More...
class	cspins_state_manager
	The management of states (i.e. allocation/deallocation) can be painless since every time we have to consider whether the state will be compressed or not. This class aims to simplify this management. More...
struct	inner_callback_parameters
	Parameters passed to callbacks when generating successor states from the shared library produced by LTSmin. More...
class	cspins_iterator
	This class provides an iterator over the successors of a state. All successors are computed once when an iterator is recycled or created. More...
class	kripkecube< cspins_state, cspins_iterator >
	Thread-safe specialization of kripkecube for SpinS states and iterators. More...
class	iterable_uf
	Iterable Union-Find for parallel reachability algorithms. More...
class	swarmed_bloemen
	Bloemen parallel SCC decomposition algorithm for reachability. More...
class	iterable_uf_ec
	Iterable Union-Find for parallel emptiness-check algorithms. More...
class	swarmed_bloemen_ec
	Bloemen parallel SCC decomposition algorithm for emptiness check. More...
class	swarmed_cndfs
	Swarmed variant of the CNDFS parallel emptiness-check algorithm. More...
class	swarmed_deadlock
	This class aims to explore a model to detect whether it contains a deadlock. This deadlock detection performs a DFS traversal sharing information shared among multiple threads. If Deadlock equals std::true_type performs deadlock algorithm, otherwise perform a simple reachability. More...
class	lpar13
	This class implements the sequential emptiness check as presented in "Three SCC-based Emptiness Checks for Generalized Büchi Automata" (Renault et al, LPAR 2013). Among the three emptiness checks that have been proposed, we opted to implement yGabow's one. More...
struct	ec_stats
	This structure contains, for each thread, the collected information during the traversal. More...
class	int_unionfind
	This Union-Find data structure is a particular union-find, dedicated for emptiness checks below, see ec.hh. The key of this union-find is int. Moreover, we suppose that only consecutive int are inserted. This union-find includes most of the classical optimizations (IPC, LR, PC, MS). More...
class	kripkecube_to_twa
	Convert a (cube) model into a twa. Note that this algorithm cannot be run in parallel but could. More...
class	product_to_twa
	Convert a (cube) product automaton into a twa Note that this algorithm cannot be run in parallel. More...
struct	bdd_less_than
	Comparison functor for BDDs. More...
struct	bdd_less_than_stable
	Comparison functor for BDDs. More...
struct	bdd_hash
	Hash functor for BDDs. More...
class	bitset
	A fixed-size bitset backed by N unsigned words. More...
class	bitvect
	A bit vector. More...
class	bitvect_array
	An array of fixed-size bit vectors allocated contiguously. More...
struct	parse_error
	Exception thrown when a parse error is encountered. More...
class	parallel_policy
	This class is used to tell parallel algorithms what resources they may use. More...
class	fixed_size_pool
	A fixed-size memory pool implementation. More...
class	printable
	Abstract base class for objects that can be printed to a stream via a format string. More...
class	printable_value
	A printable wrapper around a value of type T. More...
class	printable_id
	The default callback simply writes "%c". More...
class	printable_percent
	Called by default for "%%" and "%\0". More...
class	formater
	A string formatter that dispatches %-escape sequences to printable objects. More...
struct	ptr_hash
	A hash function for pointers. More...
struct	identity_hash
	A hash function that returns identity. More...
struct	pair_hash
	Hash functor for std::pair combining hashes of both elements. More...
struct	fnv
	Struct for Fowler-Noll-Vo parameters. More...
struct	fnv< T, typename std::enable_if< sizeof(T)==4 >::type >
	Fowler-Noll-Vo hash parameters for 32 bits. More...
struct	fnv< T, typename std::enable_if< sizeof(T)==8 >::type >
	Fowler-Noll-Vo hash parameters for 64 bits. More...
struct	char_ptr_less_than
	Strict Weak Ordering for char*. More...
class	minato_isop
	Generate an irredundant sum-of-products (ISOP) form of a BDD function. More...
class	multiple_size_pool
	A multiple-size memory pool implementation. More...
class	option_map
	Manage a map of options. More...
class	barand
	Compute pseudo-random integer value between 0 and n included, following a binomial distribution with probability p. More...
class	satsolver_command
	Interface with a given sat solver. More...
class	satsolver
	Interface with a SAT solver. More...
struct	stopwatch
	A simple stopwatch. More...
struct	time_info
	A structure to record elapsed time in clock ticks. More...
class	timer
class	timer_map
	A map of timer, where each timer has a name. More...
struct	process_timer
	Struct used to start and stop both timer and stopwatch clocks. More...
class	temporary_file
	Temporary file name. More...
class	open_temporary_file
	Open temporary file. More...
class	trival
	A class implementing Kleene's three-valued logic. More...
struct	hoa_abort
	Exception thrown by the HOA lexer upon reading an "--ABORT--" marker. More...
struct	parsed_aut
	Result of the automaton parser. More...
struct	automaton_parser_options
	Options controlling the behavior of the automaton stream parser. More...
class	automaton_stream_parser
	Parse a stream of automata. More...
class	realizability_simplifier_base
	Simplify a reactive specification, preserving realizability. More...
class	realizability_simplifier
	Simplify a reactive specification, preserving realizability. More...
class	language_containment_checker
class	declarative_environment
	A declarative environment. More...
class	default_environment
	A laxist environment. More...
class	environment
	An environment that describes atomic propositions. More...
class	exclusive_ap
	A set of atomic proposition groups that are mutually exclusive within each group. More...
class	fnode
	Actual storage for formula nodes. More...
struct	formula_ptr_less_than_bool_first
	Comparator for formula pointers that orders Boolean formulas before others. More...
class	formula
	Main class for temporal logic formula. More...
class	ltlf_simplifier
	Cheap simplification rules for LTLf formulas. More...
class	ltlf_one_step_sat_rewrite_with_cache
	Cached version of the one-step satisfiability rewriting for LTLf formulas. More...
class	ltlf_one_step_unsat_rewrite_with_cache
	Cached version of the one-step unsatisfiability rewriting for LTLf formulas. More...
class	mark_tools
	Utilities for marking NegClosure and EConcat operators in temporal formulas. More...
struct	parsed_formula
	The result of a formula parser. More...
class	random_formula
	Base class for random formula generators. More...
class	random_ltl
	Generate random LTL formulas. More...
class	random_boolean
	Generate random Boolean formulas. More...
class	random_sere
	Generate random SERE. More...
class	random_psl
	Generate random PSL formulas. More...
class	randltlgenerator
	Generator of random LTL/PSL/SERE/Boolean formulas with configurable options. More...
class	tl_simplifier_options
	Options controlling which simplification passes the tl_simplifier applies. More...
class	tl_simplifier
	Rewrite or simplify f in various ways. More...
class	unabbreviator
	Clone and rewrite a formula to remove specified operators logical operators. More...
class	acc_cond
	An acceptance condition. More...
struct	rs_pairs_view
	A view over Rabin-Streett pairs restricted to a subset of acceptance marks. More...
class	bdd_dict
	Map BDD variables to formulas. More...
class	bdd_dict_preorder
	A BDD dictionary wrapper that pre-registers atomic propositions before use. More...
class	taa_tgba
	A self-loop Transition-based Alternating Automaton (TAA) which is seen as a TGBA (abstract class, see below). More...
class	set_state
class	taa_succ_iterator
	Successor iterator for alternating automata with tree-and-automata (TAA) transitions. More...
class	taa_tgba_labelled
class	taa_tgba_string
	A TAA-TGBA automaton where states are labelled with strings. More...
class	taa_tgba_formula
	A TAA-TGBA automaton where states are labelled with formulas. More...
class	state
	Abstract class for states. More...
struct	state_ptr_less_than
	Strict Weak Ordering for state pointers. More...
struct	state_ptr_equal
	An Equivalence Relation for state pointers. More...
struct	state_ptr_hash
	Hash Function for state pointers. More...
class	state_unicity_table
	Render state pointers unique via a hash table. More...
struct	state_shared_ptr_less_than
	Strict Weak Ordering for shared_state. More...
struct	state_shared_ptr_equal
	An Equivalence Relation for shared_state. More...
struct	state_shared_ptr_hash
	Hash Function for shared_state. More...
class	twa_succ_iterator
	Iterate over the successors of a state. More...
class	twa
	A Transition-based ω-Automaton. More...
struct	twa_graph_state
	Graph-based representation of a TωA. More...
struct	twa_graph_edge_data
	Data attached to edges of a twa_graph. More...
class	twa_graph_succ_iterator
	Iterator used by the on-the-fly interface of twa_graph. More...
class	twa_graph
	Graph-based representation of a TωA. More...
class	state_product
	A state for twa_product. More...
class	twa_product
	A lazy product. (States are computed on the fly.) More...
class	twa_product_init
	A lazy product with different initial states. More...
class	aig
	A class representing AIG circuits. More...
class	outedge_combiner
	Helper class to combine outgoing edges in alternating automata. More...
class	univ_remover_state
	State used during on-the-fly removal of universal edges from an alternating automaton. More...
class	twa_univ_remover
	On-the-fly TωA that removes universal edges from an alternating automaton. More...
class	isomorphism_checker
	Check if two automata are isomorphic. More...
class	backprop_graph
	Graph used for backward propagation of winning conditions in parity games. More...
class	bfs_steps
	Make a BFS in a spot::tgba to compute a twa_run::steps. More...
struct	nca_st_info
class	enumerate_cycles
	Enumerate elementary cycles in a SCC. More...
class	emptiness_check_result
	The result of an emptiness check. More...
class	emptiness_check
	Common interface to emptiness check algorithms. More...
class	emptiness_check_instantiator
	Dynamically create emptiness checks. Given their name and options. More...
struct	twa_run
	An accepted run, for a twa. More...
struct	unsigned_statistics
	Interface for retrieving unsigned integer statistics from an emptiness check. More...
class	ec_statistics
	Emptiness-check statistics. More...
class	ars_statistics
	Accepting Run Search statistics. More...
class	acss_statistics
	Accepting Cycle Search Space statistics. More...
class	couvreur99_check_result
class	couvreur99_check
	An implementation of the Couvreur99 emptiness-check algorithm. More...
class	couvreur99_check_shy
	A version of spot::couvreur99_check that tries to visit known states first. More...
class	scc_stack
	Stack of strongly connected components for the Tarjan-Couvreur emptiness-check algorithm. More...
class	couvreur99_check_status
	The status of the emptiness-check on success. More...
class	hoa_alias_formater
	Help printing BDDs as text, using aliases. More...
class	lasso_enumerator
	Lazily enumerate lasso-shaped accepted runs/words of bounded size. More...
struct	fm_edge
	A single successor edge from a formula-state. More...
struct	fm_simple_edge
	A simplified successor edge without condition. More...
class	ltl_to_tgba_fm_otf
	On-the-fly LTL→TGBA explorer. More...
struct	mtdfa_stats
	statistics about an mtdfa instance More...
struct	mtdfa
	A DFA represented using shared multi-terminal BDDs. More...
struct	ltlf_synthesis_options
	Fine-tuning options for LTLf synthesis. More...
class	ltlf_translator
	"Semi-internal" class used to implement ltlf_to_mtdfa() More...
struct	mtdswa
	MTBDD-based representation of a state-based ω-automaton. More...
class	simple_ltl_translator
	"Semi-internal" for translating LTL using MTBDDs More...
struct	mtdtwa
	A multi-terminal decision diagram representation of a TωA. More...
struct	reduce_parity_data
	Internal data computed by the reduce_parity function. More...
class	postprocessor
	Wrap TGBA/BA/Monitor post-processing algorithms in an easy interface. More...
struct	power_map
	Maps each powerset-construction state to the set of original states it represents. More...
class	output_aborter
	Helper object to specify when an algorithm should abort its construction. More...
class	twa_reachable_iterator
	Iterate over all reachable states of a spot::tgba. More...
class	twa_reachable_iterator_breadth_first
	An implementation of spot::twa_reachable_iterator that browses states breadth first. More...
class	twa_reachable_iterator_depth_first
	Iterate over all states of an automaton using a DFS. More...
class	twa_reachable_iterator_depth_first_stack
	Iterate over all states of an automaton using a DFS. More...
class	remove_ap
	Helper for stripping or fixing atomic propositions in automata. More...
class	scc_info_node
	Storage for SCC related information. More...
class	scc_info
	Compute an SCC map and gather assorted information. More...
class	scc_and_mark_filter
	Create a filter for SCC and marks. More...
struct	edge_separator_filter
	A filter for iterating over edge labels compatible with a given BDD condition. More...
class	edge_separator
	separate edges so that their labels are disjoint More...
struct	twa_statistics
	Basic statistics (states and edges counts) for a TωA. More...
struct	twa_sub_statistics
	Extended statistics including transition counts for a TωA. More...
class	printable_formula
	A printable wrapper for a formula, for use in format strings. More...
class	printable_acc_cond
	A printable wrapper for an acceptance condition, for use in format strings. More...
class	printable_scc_info
	A printable wrapper for SCC information of an automaton, for use in format strings. More...
class	printable_size
	A printable wrapper reporting reachable and total state/edge counts. More...
class	printable_long_size
	A printable wrapper reporting reachable and total transition counts as long long. More...
class	stat_printer
	prints various statistics about a TGBA More...
struct	synthesis_info
	Benchmarking data and options for synthesis. More...
struct	mealy_like
	A struct that represents different types of mealy like objects. More...
struct	game_relabeling_map
	Pair of relabeling maps for environment and player edges in a synthesis game. More...
struct	to_parity_data
	Structure used by to_parity to store some information about the construction. More...
struct	to_parity_options
	Options to control various optimizations of to_parity(). More...
class	translator
	Translate an LTL formula into an optimized twa_graph. More...
struct	twa_word
	An infinite word stored as a lasso. More...
class	zielonka_tree
	Zielonka Tree implementation. More...
class	acd
	Alternating Cycle Decomposition implementation. More...
class	cubeset
	Manager for allocating and manipulating cubes (bit-encoded partial assignments over APs). More...
class	cstate
	Class for thread-safe states. More...
class	transition
	Class for representing a transition. More...
class	trans_index
	Class for iterators over transitions. More...
class	twacube
	Class for representing a thread-safe twa. More...

Typedefs
typedef std::shared_ptr< fair_kripke >	fair_kripke_ptr
typedef std::shared_ptr< const fair_kripke >	const_fair_kripke_ptr
typedef std::shared_ptr< kripke >	kripke_ptr
typedef std::shared_ptr< const kripke >	const_kripke_ptr
typedef std::shared_ptr< const kripke_explicit >	const_kripke_explicit_ptr
typedef std::shared_ptr< kripke_explicit >	kripke_explicit_ptr
typedef std::shared_ptr< kripke_graph >	kripke_graph_ptr
	Shared pointer to a kripke_graph. More...
typedef std::hash< std::string >	string_hash
	A hash function for strings. More...
typedef std::pair< spot::location, std::string >	parse_aut_error
	A parse diagnostic with its location. More...
typedef std::list< parse_aut_error >	parse_aut_error_list
	A list of parser diagnostics, as filled by parse. More...
typedef std::shared_ptr< parsed_aut >	parsed_aut_ptr
	Shared pointer to parsed_aut. More...
typedef std::shared_ptr< const parsed_aut >	const_parsed_aut_ptr
	Shared pointer to const parsed_aut. More...
typedef std::set< formula >	atomic_prop_set
	Set of atomic propositions. More...
typedef std::pair< location, std::string >	one_parse_error
	A parse diagnostic with its location. More...
typedef std::list< one_parse_error >	parse_error_list
	A list of parser diagnostics, as filled by parse. More...
typedef std::map< formula, formula >	relabeling_map
	Map associating new (key) formula names to old (value) ones. More...
typedef std::unordered_map< formula, formula >	snf_cache
	Cache mapping formulas to their star normal form. More...
typedef std::shared_ptr< bdd_dict >	bdd_dict_ptr
	Shared pointer to a bdd_dict. More...
typedef std::shared_ptr< twa >	twa_ptr
	Shared pointer to a mutable twa. More...
typedef std::shared_ptr< const twa >	const_twa_ptr
	Shared pointer to a const twa. More...
typedef std::shared_ptr< const twa_graph >	const_twa_graph_ptr
	Shared pointer to a const twa_graph. More...
typedef std::shared_ptr< twa_graph >	twa_graph_ptr
	Shared pointer to a mutable twa_graph. More...
typedef std::shared_ptr< const twa_product >	const_twa_product_ptr
	Shared pointer to a const twa_product. More...
typedef std::shared_ptr< twa_product >	twa_product_ptr
	Shared pointer to a mutable twa_product. More...
typedef std::shared_ptr< const twa_word >	const_twa_word_ptr
	Shared pointer to a const twa_word. More...
typedef std::shared_ptr< twa_word >	twa_word_ptr
	Shared pointer to a mutable twa_word. More...
typedef std::shared_ptr< taa_tgba_string >	taa_tgba_string_ptr
	Shared pointer to a taa_tgba_string automaton. More...
typedef std::shared_ptr< const taa_tgba_string >	const_taa_tgba_string_ptr
	Shared pointer to a const taa_tgba_string automaton. More...
typedef std::shared_ptr< taa_tgba_formula >	taa_tgba_formula_ptr
	Shared pointer to a taa_tgba_formula automaton. More...
typedef std::shared_ptr< const taa_tgba_formula >	const_taa_tgba_formula_ptr
	Shared pointer to a const taa_tgba_formula automaton. More...
typedef std::shared_ptr< twa_run >	twa_run_ptr
	Shared pointer to a twa_run. More...
typedef std::unordered_set< const state *, state_ptr_hash, state_ptr_equal >	state_set
	Unordered set of abstract states. More...
template<class val >
using	state_map = std::unordered_map< const state *, val, state_ptr_hash, state_ptr_equal >
	Unordered map of abstract states. More...
typedef std::shared_ptr< const state >	shared_state
	Shared pointer to a const state. More...
typedef std::unordered_set< shared_state, state_shared_ptr_hash, state_shared_ptr_equal >	shared_state_set
	Unordered set of shared states. More...
typedef std::shared_ptr< aig >	aig_ptr
	Shared pointer to an aig. More...
typedef std::shared_ptr< const aig >	const_aig_ptr
	Shared pointer to a const aig. More...
typedef std::shared_ptr< twa_univ_remover >	twa_univ_remover_ptr
	Shared pointer to a twa_univ_remover. More...
typedef std::vector< struct nca_st_info * >	vect_nca_info
	Vector of nca_st_info pointers used by the co-Büchi construction. More...
typedef std::shared_ptr< const twa_run >	const_twa_run_ptr
	Shared pointer to const twa_run. More...
typedef std::shared_ptr< emptiness_check_result >	emptiness_check_result_ptr
	Shared pointer to emptiness_check_result. More...
typedef std::shared_ptr< emptiness_check >	emptiness_check_ptr
	Shared pointer to emptiness_check. More...
typedef std::shared_ptr< emptiness_check_instantiator >	emptiness_check_instantiator_ptr
	Shared pointer to emptiness_check_instantiator. More...
typedef std::vector< bool >	region_t
	Winning region: false = player 0 (env), true = player 1. More...
typedef std::vector< unsigned >	strategy_t
	Strategy: maps each state index to the chosen global edge number. More...
typedef std::shared_ptr< mtdfa >	mtdfa_ptr
	Shared pointer to a mtdfa. More...
typedef std::shared_ptr< const mtdfa >	const_mtdfa_ptr
	Shared pointer to a const mtdfa. More...
typedef std::shared_ptr< mtdswa >	mtdswa_ptr
	Shared pointer to an mtdswa. More...
typedef std::shared_ptr< const mtdswa >	const_mtdswa_ptr
	Shared pointer to a const mtdswa. More...
typedef std::pair< acc_cond::mark_t, unsigned >	terminal_data_t
	Data associated with a terminal BDD node. More...
typedef std::vector< terminal_data_t >	terminal_data_map_t
	Map from terminal BDD values to terminal data. More...
typedef std::shared_ptr< mtdtwa >	mtdtwa_ptr
	Shared pointer to an mtdtwa. More...
typedef std::shared_ptr< const mtdtwa >	const_mtdtwa_ptr
	Shared pointer to a const mtdtwa. More...
typedef std::vector< std::pair< unsigned, unsigned > >	product_states
	Automata constructed by product() contain a property named "product-states" with this type. More...
typedef std::vector< std::pair< bool, bdd > >	quantifier_list
	List of quantifiers: each pair holds a Boolean (true = universal, false = existential) and a BDD over the quantified propositions. More...
using	cube = unsigned *
	A cube is only a set of bits in memory. More...
typedef std::shared_ptr< twacube >	twacube_ptr
typedef std::shared_ptr< const twacube >	const_twacube_ptr
typedef struct spot::transition_info	transition_info_t
	Transition information passed to callbacks during state-space exploration. More...
typedef void(*	TransitionCB) (void *ctx, transition_info_t *transition_info, int *dst)
	Callback used by the PINS interface. More...
typedef std::shared_ptr< const spins_interface >	spins_interface_ptr
	Shared pointer to a Spins interface. More...
typedef int *	cspins_state
	A Spins state is represented as an array of integer Note that this array has two reserved slots (position 0 and 1). More...
typedef std::shared_ptr< spot::kripkecube< spot::cspins_state, spot::cspins_iterator > >	ltsmin_kripkecube_ptr
	shortcut to manipulate the kripke below More...

Enumerations
enum class	mc_algorithm {   BLOEMEN_EC , BLOEMEN_SCC , CNDFS , DEADLOCK ,   REACHABILITY , SWARMING }
	The list of parallel model-checking algorithms available. More...
enum class	mc_rvalue {   DEADLOCK , EMPTY , FAILURE , NO_DEADLOCK ,   NOT_EMPTY , SUCCESS }
	Return value of a parallel model-checking algorithm. More...
enum class	pool_type { Safe , Unsafe }
enum class	parsed_aut_type {   HOA , NeverClaim , LBTT , DRA ,   DSA , PGAME , Unknown }
	Format type of a parsed automaton. More...
enum class	op : uint8_t {   ff , tt , eword , ap ,   Not , X , F , G ,   Closure , NegClosure , NegClosureMarked , Xor ,   Implies , Equiv , U , R ,   W , M , EConcat , EConcatMarked ,   UConcat , Or , OrRat , And ,   AndRat , AndNLM , Concat , Fusion ,   Star , FStar , first_match , strong_X ,   exists , forall }
	Operator types. More...
enum class	prcheck { Auto , via_CoBuchi , via_Rabin , via_Parity }
	Enum used to change the behavior of is_persistence() or is_recurrence(). More...
enum class	ocheck { Auto , via_CoBuchi , via_Rabin , via_WDBA }
	Enum used to change the behavior of is_obligation(). More...
enum	mut_opts {   Mut_Ap2Const = 1U << 0 , Mut_Simplify_Bounds = 1U << 1 , Mut_Remove_Multop_Operands = 1U << 2 , Mut_Remove_Ops = 1U << 3 ,   Mut_Split_Ops = 1U << 4 , Mut_Rewrite_Ops = 1U << 5 , Mut_Remove_One_Ap = 1U << 6 , Mut_All = -1U }
	Types of mutations supported by mutate(). More...
enum	relabeling_style { Abc , Pnn }
	Style for relabeling atomic propositions. More...
enum	ltlf_synthesis_backprop { state_refine , bfs_node_backprop , dfs_node_backprop }
	Backpropagation mode for LTLf synthesis. More...
enum	mcs_tie_break { MCS_TIE_ANY = 0 , MCS_TIE_SCC }
	Tie-breaking strategy for maximum cardinality search. More...
enum class	scc_info_options {   NONE = 0 , STOP_ON_ACC = 1 , TRACK_STATES = 2 , TRACK_SUCCS = 4 ,   TRACK_STATES_IF_FIN_USED = 8 , PROCESS_UNREACHABLE_STATES = 16 , ALL = TRACK_STATES | TRACK_SUCCS }
	Options to alter the behavior of scc_info. More...
enum class	zielonka_tree_options {   NONE = 0 , CHECK_RABIN = 1 , CHECK_STREETT = 2 , CHECK_PARITY = CHECK_RABIN | CHECK_STREETT ,   ABORT_WRONG_SHAPE = 4 , MERGE_SUBTREES = 8 , NO_EMPTY_LAYER = 16 }
	Options to alter the behavior of acd. More...
enum class	acd_options {   NONE = 0 , CHECK_RABIN = 1 , CHECK_STREETT = 2 , CHECK_PARITY = CHECK_RABIN | CHECK_STREETT ,   ABORT_WRONG_SHAPE = 4 , ORDER_HEURISTIC = 8 }
	Options to alter the behavior of acd. More...

Functions
kripke_graph_ptr	make_kripke_graph (const bdd_dict_ptr &d)
	Create a new kripke_graph. More...
std::ostream &	operator<< (std::ostream &os, const mc_algorithm &ma)
	Print an mc_algorithm value to a stream. More...
std::ostream &	operator<< (std::ostream &os, const mc_rvalue &mr)
	Print an mc_rvalue value to a stream. More...
std::ostream &	operator<< (std::ostream &os, const ec_stats &es)
	Print ec_stats to a stream. More...
const mc_rvalue	operator| (const mc_rvalue &lhs, const mc_rvalue &rhs)
	This function helps to find the output value from a set of threads that may have different values. More...
template<typename T , typename U >
T	down_cast (U *u) noexcept
template<typename T , typename U >
T	down_cast (const std::shared_ptr< U > &u) noexcept
template<typename T , typename U >
T	down_cast (U u)
template<typename Type , typename = std::enable_if_t<std::is_unsigned<Type>::value>>
constexpr unsigned	clz (Type n) noexcept
	Count leading zeros of an unsigned integer. More...
int	memusage ()
	Total number of pages in use by the program. More...
template<typename values >
void	permute_vector (std::vector< values > &data, const std::vector< unsigned > &indices)
	Reorder data in place according to the permutation indices. More...
const char *	version ()
	Return Spot's version. More...
parsed_aut_ptr	parse_aut (const std::string &filename, const bdd_dict_ptr &dict, environment &env=default_environment::instance(), automaton_parser_options opts={})
	Read the first spot::twa_graph from a file. More...
atomic_prop_set	create_atomic_prop_set (unsigned n, const char *prefix="p")
	construct an atomic_prop_set with n propositions starting with prefix More...
atomic_prop_set *	atomic_prop_collect (formula f, atomic_prop_set *s=nullptr)
	Return the set of atomic propositions occurring in a formula. More...
bdd	atomic_prop_collect_as_bdd (formula f, const twa_ptr &a)
	Return the set of atomic propositions occurring in a formula, as a BDD. More...
atomic_prop_set	collect_literals (formula f)
	Collect the literals occurring in f. More...
std::vector< std::vector< spot::formula > >	collect_equivalent_literals (formula f)
	Collect equivalent APs. More...
formula	to_delta2 (formula f, tl_simplifier *tls=nullptr)
	Convert an LTL formula to Δ₂ More...
formula	distribute_next (formula f)
	Distribute X at the top-level of a formula. More...
std::ostream &	print_dot_psl (std::ostream &os, formula f)
	Write a formula tree using dot's syntax. More...
int	atomic_prop_cmp (const fnode *f, const fnode *g)
	Order two atomic propositions. More...
std::ostream &	print_formula_props (std::ostream &out, const formula &f, bool abbreviated=false)
	Print the properties of formula f on stream out. More...
std::list< std::string >	list_formula_props (const formula &f)
	List the properties of formula f. More...
std::ostream &	operator<< (std::ostream &os, const formula &f)
	Print a formula. More...
bool	is_persistence (formula f, twa_graph_ptr aut=nullptr, prcheck algo=prcheck::Auto)
	Return true if f represents a persistence property. More...
bool	is_recurrence (formula f, twa_graph_ptr aut=nullptr, prcheck algo=prcheck::Auto)
	Return true if f represents a recurrence property. More...
bool	is_obligation (formula f, twa_graph_ptr aut=nullptr, ocheck algo=ocheck::Auto)
	Return true if f represents an obligation property. More...
char	mp_class (formula f)
	Return the class of f in the temporal hierarchy of Manna and Pnueli (PODC'90). More...
std::string	mp_class (formula f, const char *opt)
	Return the class of f in the temporal hierarchy of Manna and Pnueli (PODC'90). More...
std::string	mp_class (char mpc, const char *opt)
	Expand a class in the temporal hierarchy of Manna and Pnueli (PODC'90). More...
unsigned	nesting_depth (formula f, op oper)
	Compute the nesting depth of an operator. More...
unsigned	nesting_depth (formula f, const op *begin, const op *end)
	Compute the nesting depth of a set of operators. More...
unsigned	nesting_depth (formula f, const char *opers)
	Compute the nesting depth of a set of operators. More...
bool	is_liveness (formula f)
	Check whether a formula represents a liveness property. More...
int	length (formula f)
	Compute the length of a formula. More...
int	length_boolone (formula f)
	Compute the length of a formula, squashing Boolean formulas. More...
formula	from_ltlf (formula f, const char *alive, int algo)
	Convert an LTLf into an LTL formula. More...
formula	from_ltlf (formula f, const char *alive="alive")
	Convert an LTLf into an LTL formula. More...
formula	ltlf_one_step_sat_rewrite (formula f)
	One-step satisfiability rewriting for LTLf formulas. More...
formula	ltlf_one_step_unsat_rewrite (formula f, bool negate=false)
	One-step unsatisfiability rewriting for LTLf formulas. More...
std::vector< formula >	mutate (formula f, unsigned opts=Mut_All, unsigned max_output=-1U, unsigned mutation_count=1, bool sort=true)
	Generate mutations of a formula. More...
formula	negative_normal_form (formula f, bool negated=false)
	Build the negative normal form of f. More...
parsed_formula	parse_infix_psl (const std::string &ltl_string, environment &env=default_environment::instance(), bool debug=false, bool lenient=false)
	Build a formula from an LTL string. More...
parsed_formula	parse_infix_boolean (const std::string &ltl_string, environment &env=default_environment::instance(), bool debug=false, bool lenient=false)
	Build a Boolean formula from a string. More...
parsed_formula	parse_prefix_ltl (const std::string &ltl_string, environment &env=default_environment::instance(), bool debug=false)
	Build a formula from an LTL string in LBT's format. More...
formula	parse_formula (const std::string &ltl_string, environment &env=default_environment::instance())
	A simple wrapper to parse_infix_psl() and parse_prefix_ltl(). More...
parsed_formula	parse_infix_sere (const std::string &sere_string, environment &env=default_environment::instance(), bool debug=false, bool lenient=false)
	Build a formula from a string representing a SERE. More...
void	fix_utf8_locations (const std::string &input_string, parse_error_list &error_list)
	Fix location of diagnostics assuming the input is utf8. More...
std::ostream &	print_psl (std::ostream &os, formula f, bool full_parent=false)
	Output a PSL formula as a string which is parsable. More...
std::string	str_psl (formula f, bool full_parent=false)
	Convert a PSL formula into a string which is parsable. More...
std::ostream &	print_utf8_psl (std::ostream &os, formula f, bool full_parent=false)
	Output a PSL formula as an utf-8 string which is parsable. More...
std::string	str_utf8_psl (formula f, bool full_parent=false)
	Convert a PSL formula into a utf-8 string which is parsable. More...
std::ostream &	print_sere (std::ostream &os, formula f, bool full_parent=false)
	Output a SERE formula as a string which is parsable. More...
std::string	str_sere (formula f, bool full_parent=false)
	Convert a SERE formula into a string which is parsable. More...
std::ostream &	print_utf8_sere (std::ostream &os, formula f, bool full_parent=false)
	Output a SERE formula as a utf-8 string which is parsable. More...
std::string	str_utf8_sere (formula f, bool full_parent=false)
	Convert a SERE formula into a string which is parsable. More...
std::ostream &	print_spin_ltl (std::ostream &os, formula f, bool full_parent=false)
	Output an LTL formula as a string parsable by Spin. More...
std::string	str_spin_ltl (formula f, bool full_parent=false)
	Convert an LTL formula into a string parsable by Spin. More...
std::ostream &	print_wring_ltl (std::ostream &os, formula f)
	Output an LTL formula as a string parsable by Wring. More...
std::string	str_wring_ltl (formula f)
	Convert a formula into a string parsable by Wring. More...
std::ostream &	print_latex_psl (std::ostream &os, formula f, bool full_parent=false)
	Output a PSL formula as a LaTeX string. More...
std::string	str_latex_psl (formula f, bool full_parent=false)
	Output a formula as a LaTeX string which is parsable. unless the formula contains automaton operators (used in ELTL formulas). More...
std::ostream &	print_latex_sere (std::ostream &os, formula f, bool full_parent=false)
	Output a SERE formula as a LaTeX string. More...
std::string	str_latex_sere (formula f, bool full_parent=false)
	Output a SERE formula as a LaTeX string which is parsable. unless the formula contains automaton operators (used in ELTL formulas). More...
std::ostream &	print_sclatex_psl (std::ostream &os, formula f, bool full_parent=false)
	Output a PSL formula as a self-contained LaTeX string. More...
std::string	str_sclatex_psl (formula f, bool full_parent=false)
	Output a PSL formula as a self-contained LaTeX string. More...
std::ostream &	print_sclatex_sere (std::ostream &os, formula f, bool full_parent=false)
	Output a SERE formula as a self-contained LaTeX string. More...
std::string	str_sclatex_sere (formula f, bool full_parent=false)
	Output a SERE formula as a self-contained LaTeX string. More...
std::ostream &	print_lbt_ltl (std::ostream &os, formula f)
	Output an LTL formula as a string in LBT's format. More...
std::string	str_lbt_ltl (formula f)
	Output an LTL formula as a string in LBT's format. More...
formula	relabel (formula f, relabeling_style style, relabeling_map *m=nullptr)
	Relabel the atomic propositions in a formula. More...
formula	remove_x (formula f)
	Rewrite a stutter-insensitive formula f without using the X operator. More...
bool	ltl_satisfiable (formula f)
	Decide if an LTL formula is satisfiable. More...
formula	normalize_quantifiers (formula)
	Remove unnecessary quantified variables. More...
formula	star_normal_form (formula sere, snf_cache *cache=nullptr)
	Helper to rewrite a sere in Star Normal Form. More...
formula	star_normal_form_bounded (formula sere, snf_cache *cache=nullptr)
	A variant of star_normal_form() for r[*0..j] where j < ω. More...
std::pair< formula, std::vector< std::string > >	suffix_operator_normal_form (formula f, const std::string prefix)
	Helper to rewrite a PSL formula in Suffix Operator Normal Form. More...
formula	unabbreviate (formula in, const char *opt=default_unabbrev_string)
	Clone and rewrite a formula to remove specified operators logical operators. More...
formula	unit_propagate (formula f)
	Simplify a formula via one-pass unit propagation. More...
bdd_dict_ptr	make_bdd_dict ()
	Create a new, empty bdd_dict wrapped in a shared pointer. More...
std::ostream &	bdd_print_sat (std::ostream &os, const bdd_dict_ptr &dict, bdd b)
	Print a BDD as a list of literals. More...
std::string	bdd_format_sat (const bdd_dict_ptr &dict, bdd b)
	Format a BDD as a list of literals. More...
std::ostream &	bdd_print_accset (std::ostream &os, const bdd_dict_ptr &dict, bdd b)
	Print a BDD as a set of acceptance conditions. More...
std::string	bdd_format_accset (const bdd_dict_ptr &dict, bdd b)
	Format a BDD as a set of acceptance conditions. More...
std::ostream &	bdd_print_set (std::ostream &os, const bdd_dict_ptr &dict, bdd b)
	Print a BDD as a set. More...
std::string	bdd_format_set (const bdd_dict_ptr &dict, bdd b)
	Format a BDD as a set. More...
std::ostream &	bdd_print_formula (std::ostream &os, const bdd_dict_ptr &dict, bdd b)
	Print a BDD as a formula. More...
std::string	bdd_format_formula (const bdd_dict_ptr &dict, bdd b)
	Format a BDD as a formula. More...
void	enable_utf8 ()
	Enable UTF-8 output for bdd printers. More...
std::string	bdd_format_isop (const bdd_dict_ptr &dict, bdd b)
	Format a BDD as an irredundant sum of product. More...
std::ostream &	bdd_print_isop (std::ostream &os, const bdd_dict_ptr &dict, bdd b)
	Print a BDD as an irredundant sum of product. More...
taa_tgba_string_ptr	make_taa_tgba_string (const bdd_dict_ptr &dict)
	Construct a taa_tgba_string automaton. More...
taa_tgba_formula_ptr	make_taa_tgba_formula (const bdd_dict_ptr &dict)
	Construct a taa_tgba_formula automaton. More...
void	shared_state_deleter (state *s)
	Deleter for shared_state: calls state::destroy(). More...
twa_graph_ptr	make_twa_graph (const bdd_dict_ptr &dict)
	Build an explicit automaton from all states of aut,. More...
twa_graph_ptr	make_twa_graph (const twa_graph_ptr &aut, twa::prop_set p)
	Build an explicit automaton from all states of aut,. More...
twa_graph_ptr	make_twa_graph (const const_twa_graph_ptr &aut, twa::prop_set p, bool preserve_name_properties=false)
	Clone a twa_graph. More...
twa_graph_ptr	make_twa_graph (const const_twa_ptr &aut, twa::prop_set p, bool preserve_names=false, unsigned max_states=-(1U))
	Build an explicit automaton from all states of aut,. More...
twa_product_ptr	otf_product (const const_twa_ptr &left, const const_twa_ptr &right)
	on-the-fly TGBA product More...
twa_product_ptr	otf_product_at (const const_twa_ptr &left, const const_twa_ptr &right, const state *left_init, const state *right_init)
	on-the-fly TGBA product with forced initial states More...
std::ostream &	print_aiger (std::ostream &os, const_aig_ptr circuit)
	Print the aig to stream in AIGER format. More...
std::ostream &	print_aiger (std::ostream &os, const const_twa_graph_ptr &aut, const char *mode, const std::string *terminating_signal=nullptr)
	Encode and print an automaton as an AIGER circuit. More...
twa_graph_ptr	remove_alternation (const const_twa_graph_ptr &aut, bool named_states=false, const output_aborter *aborter=nullptr, bool raise_if_too_many_sets=true)
	Remove universal edges from a weak alternating automaton. More...
twa_univ_remover_ptr	remove_univ_otf (const const_twa_graph_ptr &aut)
	Remove universal edges on the fly from an alternating Büchi automaton. More...
twa_graph_ptr	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	reduce_buchi_acceptance_set_here (twa_graph_ptr &aut, bool preserve_sbacc=false)
	Reduce the acceptance set of a Büchi automaton. More...
twa_graph_ptr	enlarge_buchi_acceptance_set_here (twa_graph_ptr &aut, bool preserve_sbacc=false)
	Enlarge the acceptance set of a Büchi automaton. More...
twa_graph_ptr	nsa_to_nca (const_twa_graph_ptr aut, bool named_states=false, vect_nca_info *nca_info=nullptr)
	Converts a nondet Streett-like aut. to a nondet. co-Büchi aut. More...
twa_graph_ptr	dnf_to_nca (const_twa_graph_ptr aut, bool named_states=false, vect_nca_info *nca_info=nullptr)
	Converts an aut. with acceptance in DNF to a nondet. co-Büchi aut. More...
twa_graph_ptr	to_nca (const_twa_graph_ptr aut, bool named_states=false)
	Converts any ω-automata to non-deterministic co-buchi. More...
twa_graph_ptr	nsa_to_dca (const_twa_graph_ptr aut, bool named_states=false)
	Converts a nondet Streett-like aut. to a det. co-Büchi aut. More...
twa_graph_ptr	dnf_to_dca (const_twa_graph_ptr aut, bool named_states=false)
	Converts an aut. with acceptance in DNF to a det. co-Büchi aut. More...
twa_graph_ptr	to_dca (const_twa_graph_ptr aut, bool named_states=false)
	Converts any ω-automata to deterministic co-buchi. More...
twa_graph_ptr	complement_semidet (const const_twa_graph_ptr &aut, bool show_names=false)
	Complement a semideterministic TωA. More...
twa_graph_ptr	complement (const const_twa_graph_ptr &aut, const output_aborter *aborter=nullptr)
	Complement a TωA. More...
void	complete_here (twa_graph_ptr aut)
	Complete a twa_graph in place. More...
twa_graph_ptr	complete (const const_twa_ptr &aut)
	Clone a twa and complete it. More...
twa_graph_ptr	compsusp (formula f, const bdd_dict_ptr &dict, bool no_wdba=false, bool no_simulation=false, bool early_susp=false, bool no_susp_product=false, bool wdba_smaller=false, bool oblig=false)
	Compositional translation algorithm with resetable suspension. More...
int	containment_select_version (const char *version=nullptr)
emptiness_check_ptr	get_couvreur99_new (const const_twa_ptr &a, option_map o)
	A rewritten version of the Couvreur emptiness check. More...
emptiness_check_ptr	get_couvreur99_new_abstract (const const_twa_ptr &a, option_map o)
	Same as above, but always uses the abstract interface. More...
emptiness_check_result_ptr	couvreur99_new_check (const const_twa_ptr &a)
	A shortcut to run the optimized emptiness check directly. More...
bool	delay_branching_here (const twa_graph_ptr &aut)
	Merge states to delay. More...
twa_graph_ptr	restrict_dead_end_edges_here (twa_graph_ptr &aut)
	Restrict labels from "dead-end edges". More...
twa_graph_ptr	degeneralize (const const_twa_graph_ptr &a, bool use_z_lvl=true, bool use_cust_acc_orders=false, int use_lvl_cache=1, bool skip_levels=true, bool ignaccsl=false, bool remove_extra_scc=true)
	Degeneralize a generalized (co)Büchi automaton into an equivalent (co)Büchi automaton. More...
twa_graph_ptr	degeneralize_tba (const const_twa_graph_ptr &a, bool use_z_lvl=true, bool use_cust_acc_orders=false, int use_lvl_cache=1, bool skip_levels=true, bool ignaccsl=false, bool remove_extra_scc=true)
	Transition-based variant of degeneralize(). More...
acc_cond::mark_t	is_partially_degeneralizable (const const_twa_graph_ptr &aut, bool allow_inf=true, bool allow_fin=true, const std::vector< acc_cond::mark_t > &forbid={})
	Is the automaton partially degeneralizable? More...
std::vector< int >	analyze_dependent_output (const const_twa_graph_ptr &aut, const std::vector< int > &outputs)
	Analyze dependent outputs in an NBA represented as a graph. More...
twa_graph_ptr	tgba_determinize (const const_twa_graph_ptr &aut, bool pretty_print=false, bool use_scc=true, bool use_simulation=true, bool use_stutter=true, const output_aborter *aborter=nullptr, int trans_pruning=-1, bool want_classes=false)
	Determinize a TGBA. More...
std::ostream &	print_dot (std::ostream &os, const const_twa_ptr &g, const char *options=nullptr)
	Print reachable states in dot format. More...
std::ostream &	print_dot (std::ostream &os, aig_ptr circuit, const char *=nullptr)
	Print an AIG circuit in dot format. More...
twa_graph_ptr	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	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	dtba_sat_minimize_dichotomy (const const_twa_graph_ptr &a, bool state_based=false, bool langmap=false, int max_states=-1)
	Attempt to minimize a deterministic TBA with a SAT solver. More...
twa_graph_ptr	dtba_sat_minimize_incr (const const_twa_graph_ptr &a, bool state_based=false, int max_states=-1, int param=2)
	Attempt to minimize a det. TBA with a SAT solver. More...
twa_graph_ptr	dtba_sat_minimize_assume (const const_twa_graph_ptr &a, bool state_based=false, int max_states=-1, int param=6)
	Attempt to minimize a deterministic TBA incrementally with a SAT solver. More...
twa_graph_ptr	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	dtwa_sat_minimize (const const_twa_graph_ptr &a, unsigned target_acc_number, const acc_cond::acc_code &target_acc, bool state_based=false, int max_states=-1, bool colored=false)
	Attempt to minimize a deterministic TωA with a SAT solver. More...
twa_graph_ptr	dtwa_sat_minimize_dichotomy (const const_twa_graph_ptr &a, unsigned target_acc_number, const acc_cond::acc_code &target_acc, bool state_based=false, bool langmap=false, int max_states=-1, bool colored=false)
	Attempt to minimize a deterministic TωA with a SAT solver. More...
twa_graph_ptr	dtwa_sat_minimize_incr (const const_twa_graph_ptr &a, unsigned target_acc_number, const acc_cond::acc_code &target_acc, bool state_based=false, int max_states=-1, bool colored=false, int param=2)
	Attempt to minimize a deterministic TωA with a SAT solver. More...
twa_graph_ptr	dtwa_sat_minimize_assume (const const_twa_graph_ptr &a, unsigned target_acc_number, const acc_cond::acc_code &target_acc, bool state_based=false, int max_states=-1, bool colored=false, int param=6)
	Attempt to minimize a deterministic TωA with a SAT solver. More...
twa_graph_ptr	sat_minimize (twa_graph_ptr aut, const char *opt, bool state_based=false)
	High-level interface to SAT-based minimization. More...
twa_graph_ptr	dualize (const const_twa_graph_ptr &aut)
	Complement an automaton by dualizing it. More...
emptiness_check_instantiator_ptr	make_emptiness_check_instantiator (const char *name, const char **err)
	Create an emptiness-check instantiator, given the name of an emptiness check. More...
twa_word_ptr	difference_word_forq (const_twa_graph_ptr left, const_twa_graph_ptr right)
	Returns a word accepted by left that is rejected by right, or nullptr. More...
bool	contains_forq (const_twa_graph_ptr left, const_twa_graph_ptr right)
	Returns a boolean value indicating whether the language of left includes the language of right. More...
void	alternate_players (spot::twa_graph_ptr &arena, bool first_player=false, bool complete0=true)
	Transform an automaton into a parity game by propagating players. More...
bool	solve_parity_game (const twa_graph_ptr &arena, bool solve_globally=false)
	Solve a parity game. More...
bool	solve_safety_game (const twa_graph_ptr &game)
	Solve a safety game. More...
bool	solve_game (const twa_graph_ptr &arena)
	Generic interface for game solving. More...
twa_graph_ptr	highlight_strategy (twa_graph_ptr &arena, int player0_color=5, int player1_color=4)
	Highlight the edges of a strategy on an automaton. More...
void	set_state_player (twa_graph_ptr &arena, unsigned state, bool owner)
	Set the owner of a state. More...
bool	get_state_player (const const_twa_graph_ptr &arena, unsigned state)
	Get the owner of a state. More...
void	set_synthesis_outputs (const twa_graph_ptr &arena, const bdd &outs)
	Set all synthesis outputs as a conjunction. More...
bdd	get_synthesis_outputs (const const_twa_graph_ptr &arena)
	Get all synthesis outputs as a conjunction. More...
std::vector< std::string >	get_synthesis_output_aps (const const_twa_graph_ptr &arena)
	Get the vector with the names of the output propositions. More...
void	set_state_winner (twa_graph_ptr &arena, unsigned state, bool winner)
	Set the winner of a state. More...
bool	get_state_winner (const const_twa_graph_ptr &arena, unsigned state)
	Get the winner of a state. More...
bool	generic_emptiness_check (const const_twa_graph_ptr &aut)
	Emptiness check of an automaton, for any acceptance condition. More...
twa_run_ptr	generic_accepting_run (const const_twa_graph_ptr &aut)
	Accepting run search in an automaton, for any acceptance condition. More...
bool	generic_emptiness_check_for_scc (const scc_info &si, unsigned scc)
	Emptiness check of one SCC, for any acceptance condition. More...
bool	generic_emptiness_check_for_scc (const scc_info &si, unsigned scc, const acc_cond &forced_acc)
	Emptiness check of one SCC, for any acceptance condition. More...
bool	maximal_accepting_loops_for_scc (const scc_info &si, unsigned scc, const acc_cond &forced_acc, const bitvect &keep, std::function< void(const scc_info &, unsigned)> callback)
	Compute set of maximal accepting loops in one SCC, for any acceptance condition. More...
void	generic_emptiness_check_select_version (const char *emversion=nullptr)
bool	accepting_transitions_scc (const scc_info &si, unsigned scc, const acc_cond aut_acc, acc_cond::mark_t removed_colors, std::vector< bool > &accepting_transitions, const bitvect &kept)
std::vector< bool >	accepting_transitions (const const_twa_graph_ptr aut, acc_cond cond)
twa_graph_ptr	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...
twa_graph_ptr	gf_guarantee_to_ba_maybe (formula gf, const bdd_dict_ptr &dict, bool deterministic=true, bool state_based=false)
	Convert GF(φ) into a (D)BA if φ is a guarantee property. More...
twa_graph_ptr	gf_guarantee_to_ba (formula gf, const bdd_dict_ptr &dict, bool deterministic=true, bool state_based=false)
	Convert GF(φ) into a (D)BA if φ is a guarantee property. More...
twa_graph_ptr	fg_safety_to_dca_maybe (formula fg, const bdd_dict_ptr &dict, bool state_based)
	Convert FG(φ) into a DCA if φ is a safety property. More...
twa_graph_ptr	fg_safety_to_dca (formula fg, const bdd_dict_ptr &dict, bool state_based=false)
	Convert FG(φ) into a DCA if φ is a safety property. More...
twa_graph_ptr	stutterize_given (twa_graph_ptr &aut, std::vector< const_twa_graph_ptr > &facts, bool relax=true)
	Attempt to make an automaton stutter-invariant given some knowledge. More...
emptiness_check_ptr	couvreur99 (const const_twa_ptr &a, option_map options=option_map())
	Check whether the language of an automaton is empty. More...
emptiness_check_ptr	explicit_gv04_check (const const_twa_ptr &a, option_map o=option_map())
	Emptiness check based on Geldenhuys and Valmari's TACAS'04 paper. More...
std::ostream &	print_hoa (std::ostream &os, const const_twa_ptr &g, const char *opt=nullptr)
	Print reachable states in Hanoi Omega Automata format. More...
std::vector< std::pair< std::string, bdd > > *	get_aliases (const const_twa_ptr &g)
	Obtain aliases used in the HOA format. More...
void	set_aliases (twa_ptr g, const std::vector< std::pair< std::string, bdd >> &aliases)
	Define all aliases used in the HOA format. More...
void	create_alias_basis (const twa_graph_ptr &aut)
	Create an alias basis. More...
bool	is_colored (const const_twa_graph_ptr &aut)
	Return true iff aut is colored. More...
unsigned	count_nondet_states (const const_twa_graph_ptr &aut)
	Count the number of states with non-deterministic branching in aut. More...
bool	is_universal (const const_twa_graph_ptr &aut)
	Return true iff aut is universal. More...
bool	is_deterministic (const const_twa_graph_ptr &aut)
	Return true iff aut is deterministic. More...
void	highlight_nondet_states (twa_graph_ptr &aut, unsigned color)
	Highlight nondeterministic states. More...
void	highlight_nondet_edges (twa_graph_ptr &aut, unsigned color)
	Highlight nondeterministic edges. More...
void	highlight_semidet_sccs (scc_info &si, unsigned color)
	Highlight the deterministic part of the automaton. More...
bool	is_complete (const const_twa_graph_ptr &aut)
	Return true iff aut is complete. More...
bool	is_semi_deterministic (const const_twa_graph_ptr &aut)
	Return true iff aut is semi-deterministic. More...
std::vector< bool >	semidet_sccs (scc_info &si)
	Whether an SCC is in the deterministic part of an automaton. More...
void	check_determinism (twa_graph_ptr aut)
	Set the deterministic and semi-deterministic properties appropriately. More...
unsigned	count_univbranch_states (const const_twa_graph_ptr &aut)
	Count states with some universal branching. More...
unsigned	count_univbranch_edges (const const_twa_graph_ptr &aut)
	Count edges with universal branching. More...
bool	is_unambiguous (const const_twa_graph_ptr &aut)
	Whether the automaton aut is unambiguous. More...
bool	check_unambiguous (const twa_graph_ptr &aut)
	Like is_unambiguous(), but also sets the property in the twa. More...
bool	scc_has_rejecting_cycle (scc_info &map, unsigned scc)
	Whether the SCC number scc in map has a rejecting cycle. More...
bool	is_inherently_weak_scc (scc_info &map, unsigned scc)
	Whether the SCC number scc in map is inherently weak. More...
bool	is_weak_scc (scc_info &map, unsigned scc)
	Whether the SCC number scc in map is weak. More...
bool	is_complete_scc (scc_info &map, unsigned scc)
	Whether the SCC number scc in map is complete. More...
bool	is_terminal_scc (scc_info &map, unsigned scc)
	Whether the SCC number scc in map is terminal. More...
std::vector< unsigned >	language_map (const const_twa_graph_ptr &aut)
	Identify states that recognize the same language. More...
void	highlight_languages (twa_graph_ptr &aut)
	Color states that recognize identical language. More...
std::ostream &	print_lbtt (std::ostream &os, const const_twa_ptr &g, const char *opt=nullptr)
	Print reachable states in LBTT's format. More...
taa_tgba_formula_ptr	ltl_to_taa (formula f, const bdd_dict_ptr &dict, bool refined_rules=false)
	Build a spot::taa* from an LTL formula. More...
twa_graph_ptr	ltl_to_tgba_fm (formula f, const bdd_dict_ptr &dict, bool exprop=false, bool symb_merge=true, bool branching_postponement=false, bool fair_loop_approx=false, const atomic_prop_set *unobs=nullptr, tl_simplifier *simplifier=nullptr, bool unambiguous=false, const output_aborter *aborter=nullptr, bool label_with_ltl=false, bool force_obligation=false)
	Build a spot::twa_graph_ptr from an LTL or PSL formula. More...
mtdfa_ptr	ltlf_to_mtdfa (formula f, const bdd_dict_ptr &dict, bool fuse_same_bdds=true, bool simplify_terms=true, bool detect_empty_univ=true, bool preserve_quantifiers_in_names=false)
	Convert an LTLf formula into an MTDFA. More...
mtdfa_ptr	ltlf_to_mtdfa_for_synthesis (formula f, const bdd_dict_ptr &dict, const std::vector< std::string > &outvars, ltlf_synthesis_backprop backprop=dfs_node_backprop, bool realizability=false, ltlf_synthesis_options options={})
	Solve (or start solving) LTLf synthesis. More...
mtdfa_ptr	ltlf_to_mtdfa_compose (formula f, const bdd_dict_ptr &dict, bool minimize=true, bool order_for_aps=true, bool want_names=true, bool fuse_same_bdds=true, bool simplify_terms=true)
	Convert an LTLf formula into a MTDFA, with a compositional approach. More...
mtdfa_ptr	minimize_mtdfa (const mtdfa_ptr &dfa)
	Minimize a MTDFA. More...
mtdfa_ptr	product (const mtdfa_ptr &dfa1, const mtdfa_ptr &dfa2)
	Combine two MTDFAs to intersect their languages. More...
mtdfa_ptr	product_or (const mtdfa_ptr &dfa1, const mtdfa_ptr &dfa2)
	Combine two MTDFAs to sum their languages. More...
mtdfa_ptr	product_xor (const mtdfa_ptr &dfa1, const mtdfa_ptr &dfa2)
	Combine two MTDFAs to build the exclusive sum of their languages. More...
mtdfa_ptr	product_xnor (const mtdfa_ptr &dfa1, const mtdfa_ptr &dfa2)
	Combine two MTDFAs to keep words that are handled similarly in both operands. More...
mtdfa_ptr	product_implies (const mtdfa_ptr &dfa1, const mtdfa_ptr &dfa2)
	Combine two MTDFAs to build an implication. More...
mtdfa_ptr	complement (const mtdfa_ptr &dfa)
	Complement an MTDFA. More...
mtdfa_ptr	trim (const mtdfa_ptr &dfa)
	Trim an MTDFA. More...
mtdfa_ptr	twadfa_to_mtdfa (const twa_graph_ptr &twa)
	Convert a TWA (representing a DFA) into an MTDFA. More...
std::vector< bool >	mtdfa_winning_region (mtdfa_ptr dfa)
	Compute the winning region of the MTDFA interpreted as a game. More...
backprop_graph	mtdfa_to_backprop (mtdfa_ptr dfa, bool early_stop=true, bool preserve_names=false)
	Build a backprop_graph from dfa. More...
mtdfa_ptr	mtdfa_winning_strategy (mtdfa_ptr dfa, bool backprop_nodes)
	Compute a strategy for an MTDFA interpreted as a game. More...
twa_graph_ptr	mtdfa_strategy_to_mealy (mtdfa_ptr strategy, bool labels=true, bool loop=false)
	Convert an MTDFA representing a strategy to a TwA with the "synthesis-output" property. More...
emptiness_check_ptr	explicit_magic_search (const const_twa_ptr &a, option_map o=option_map())
	Returns an emptiness checker on the spot::tgba automaton a. More...
emptiness_check_ptr	bit_state_hashing_magic_search (const const_twa_ptr &a, size_t size, option_map o=option_map())
	Returns an emptiness checker on the spot::tgba automaton a. More...
emptiness_check_ptr	magic_search (const const_twa_ptr &a, option_map o=option_map())
	Wrapper for the two magic_search implementations. More...
template<typename Trans >
void	transform_accessible (const const_twa_graph_ptr &old, twa_graph_ptr &cpy, Trans trans, unsigned int init, bool drop_univ_branches=false)
	Clone and mask an automaton. More...
template<typename Trans >
void	transform_copy (const const_twa_graph_ptr &old, twa_graph_ptr &cpy, Trans trans, unsigned int init)
	Copy an automaton and update each edge. More...
template<typename Trans >
void	transform_accessible (const const_twa_graph_ptr &old, twa_graph_ptr &cpy, Trans trans)
	Clone and mask an automaton starting from its initial state. More...
template<typename Trans >
void	transform_copy (const const_twa_graph_ptr &old, twa_graph_ptr &cpy, Trans trans)
	Copy an automaton and update each edge, from its initial state. More...
twa_graph_ptr	mask_acc_sets (const const_twa_graph_ptr &in, acc_cond::mark_t to_remove)
	Remove all edges that belong to some given acceptance sets. More...
twa_graph_ptr	mask_keep_states (const const_twa_graph_ptr &in, std::vector< bool > &to_keep, unsigned int init)
	Keep only the states as specified by to_keep. More...
twa_graph_ptr	mask_keep_accessible_states (const const_twa_graph_ptr &in, std::vector< bool > &to_keep, unsigned int init, bool drop_univ_branches=false)
	Keep only the states specified by to_keep that are accessible. More...
std::vector< std::vector< unsigned > >	match_states (const const_twa_graph_ptr &aut1, const const_twa_graph_ptr &aut2)
	Match the states of aut1 with the states of aut2. More...
std::vector< formula >	match_states (const const_twa_graph_ptr &aut, formula f)
	Match the states of aut with formulas "reachable" from f. More...
void	match_states_decorate (twa_graph_ptr &aut, formula f)
	Label the states of aut with the result of match_states(aut,f). More...
std::vector< unsigned >	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	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...
bool	is_mealy (const const_twa_graph_ptr &m)
	Checks whether the automaton is a mealy machine. More...
bool	is_separated_mealy (const const_twa_graph_ptr &m)
	Checks whether the automaton is a separated mealy machine. More...
bool	is_split_mealy (const const_twa_graph_ptr &m)
	Checks whether or not the automaton is a split mealy machine. More...
bool	is_input_deterministic_mealy (const const_twa_graph_ptr &m)
	Checks whether a mealy machine is input deterministic. More...
twa_graph_ptr	unsplit_mealy (const const_twa_graph_ptr &m)
	The inverse of split_separated_mealy. More...
twa_graph_ptr	reduce_mealy (const const_twa_graph_ptr &mm, bool output_assignment=true)
	Reduce an (in)completely specified mealy machine. More...
void	reduce_mealy_here (twa_graph_ptr &mm, bool output_assignment=true)
	Reduce an (in)completely specified mealy machine in place. More...
twa_graph_ptr	minimize_mealy (const const_twa_graph_ptr &mm, int premin=-1)
	Minimizes an (in)completely specified mealy machine. More...
twa_graph_ptr	minimize_mealy (const const_twa_graph_ptr &mm, synthesis_info &si)
	Minimizes an (in)completely specified mealy machine. More...
bool	is_split_mealy_specialization (const_twa_graph_ptr left, const_twa_graph_ptr right, bool verbose=false)
	Test if the split mealy machine right is a specialization of the split mealy machine left. More...
twa_graph_ptr	mealy_product (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right)
	Product between two mealy machines left and right. More...
twa_graph_ptr	terminating_mealy_to_buchi (const const_twa_graph_ptr &mealy, const std::string &signal_name)
	Convert a terminating Mealy machine to a Büchi automaton. More...
twa_graph_ptr	minimize_monitor (const const_twa_graph_ptr &a)
	Construct a minimal deterministic monitor. More...
twa_graph_ptr	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	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	minimize_obligation_guaranteed_to_work (const const_twa_graph_ptr &aut_f, formula f=nullptr)
	Whether calling minimize_obligation is sure to work. More...
mtdswa_ptr	dtwa_to_mtdswa (const twa_graph_ptr &aut)
	Convert deterministic TwA to MTDSwA. More...
std::vector< int >	scc_vector (const mtdswa_ptr &aut, std::vector< bool > *transient=nullptr, std::vector< std::vector< int >> *succs=nullptr)
	Find the SCC of each state. More...
std::vector< unsigned >	loding_weak_ranking (const mtdswa_ptr &aut, bool fix=false)
	Preprocess a weak MTDSwA before minimization. More...
mtdswa_ptr	product (const mtdswa_ptr &swa1, const mtdswa_ptr &swa2)
	Combine two MTDSwAs to intersect their languages. More...
mtdswa_ptr	product_or (const mtdswa_ptr &swa1, const mtdswa_ptr &swa2)
	Combine two MTDSwAs to sum their languages. More...
mtdswa_ptr	product_xor (const mtdswa_ptr &swa1, const mtdswa_ptr &swa2)
	Combine two MTDSwAs to build the exclusive sum of their languages. More...
mtdswa_ptr	product_xnor (const mtdswa_ptr &swa1, const mtdswa_ptr &swa2)
	Combine two MTDSwAs to keep words that are handled similarly in both operands. More...
mtdswa_ptr	product_implies (const mtdswa_ptr &swa1, const mtdswa_ptr &swa2)
	Combine two MTDSwAs to build an implication. More...
mtdswa_ptr	complement (const mtdswa_ptr &swa)
	Complement an MTDSwA. More...
mtdswa_ptr	obligation_to_mtdswa (formula f, const bdd_dict_ptr &dict, bool fuse_same_bdds=true, bool simplify_terms=true)
	Convert a syntactic-obligation to an MTDSwA. More...
mtdswa_ptr	obligation_synthesis (formula f, const bdd_dict_ptr &dict, const std::vector< std::string > &outvars, bool realizability=false, bool simplify_terms=true, int debug=-1)
	Reactive synthesis of syntactic-obligations. More...
twa_graph_ptr	mtdswa_strategy_to_mealy (mtdswa_ptr strategy, bool labels=true, bool loop=false)
	Convert a strategy represented as MTDSwA into a Mealy machine. More...
void	trim (mtdswa_ptr swa, bool trim_useless_sccs_too=false)
	Remove unnecessary states from an MTDSwA. More...
mtdtwa_ptr	dtwa_to_mtdtwa (const twa_graph_ptr &aut)
	Convert a deterministic TωA to an MTDTwA. More...
std::ostream &	print_never_claim (std::ostream &os, const const_twa_ptr &g, const char *opt=nullptr)
	Print reachable states in Spin never claim format. More...
twa_graph_ptr	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	tgba_powerset (const const_twa_graph_ptr &aut, const output_aborter *aborter=nullptr, std::vector< unsigned > *accepting_sinks=nullptr)
	Compute the powerset construction of a TGBA. More...
twa_graph_ptr	tba_determinize (const const_twa_graph_ptr &aut, unsigned threshold_states=0, unsigned threshold_cycles=0)
	Determinize a TBA using the powerset construction. More...
twa_graph_ptr	tba_determinize_check (const twa_graph_ptr &aut, unsigned threshold_states=0, unsigned threshold_cycles=0, formula f=nullptr, const_twa_graph_ptr neg_aut=nullptr)
	Determinize a TBA and make sure it is correct. More...
twa_graph_ptr	product (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right, const output_aborter *aborter=nullptr)
	Intersect two automata using a synchronous product. More...
twa_graph_ptr	product (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right, unsigned left_state, unsigned right_state, const output_aborter *aborter=nullptr)
	Intersect two automata using a synchronous product. More...
twa_graph_ptr	product_or (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right)
	Sum two automata using a synchronous product. More...
twa_graph_ptr	product_or (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right, unsigned left_state, unsigned right_state)
	Sum two automata using a synchronous product. More...
twa_graph_ptr	product_xor (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right)
	XOR two deterministic automata using a synchronous product. More...
twa_graph_ptr	product_xnor (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right)
	XNOR two automata using a synchronous product. More...
twa_graph_ptr	product_susp (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right_susp)
	Build the product of an automaton with a suspendable automaton. More...
twa_graph_ptr	product_or_susp (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right_susp)
	Build the "or" product of an automaton with a suspendable automaton. More...
twa_graph_ptr	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	random_acceptance (unsigned n_accs)
	Build a random acceptance where each acceptance set is used once. More...
void	randomize (twa_graph_ptr &aut, bool randomize_states=true, bool randomize_edges=true)
	Randomize a TGBA. More...
void	relabel_here (twa_graph_ptr &aut, relabeling_map *relmap)
	replace atomic propositions in an automaton More...
relabeling_map	partitioned_relabel_here (twa_graph_ptr &aut, bool split=false, unsigned max_letter=-1u, unsigned max_letter_mult=-1u, const bdd &concerned_ap=bddtrue, std::string var_prefix="__nv")
	Replace conditions in aut with non-overlapping conditions over fresh variables. More...
bool	rabin_is_buchi_realizable (const const_twa_graph_ptr &aut)
	Check if aut is Rabin-like and Büchi-realizable. More...
twa_graph_ptr	rabin_to_buchi_if_realizable (const const_twa_graph_ptr &aut)
	Convert a Rabin-like automaton into a Büchi automaton only when it can be done without changing the automaton structure. More...
twa_graph_ptr	rabin_to_buchi_maybe (const const_twa_graph_ptr &aut)
	Convert a Rabin-like automaton into a Büchi automaton, preserving determinism when possible. More...
twa_graph_ptr	remove_fin (const const_twa_graph_ptr &aut)
	Rewrite an automaton without Fin or f acceptance. More...
twa_graph_ptr	to_finite (const_twa_graph_ptr aut, const char *alive="alive")
	Interpret the "live" part of an automaton as finite automaton. More...
twa_graph_ptr	sbacc (twa_graph_ptr aut)
	Transform an automaton to use state-based acceptance. More...
twa_graph_ptr	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	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	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...
bool	operator! (scc_info_options me)
	Test if an scc_info_options value equals NONE. More...
scc_info_options	operator& (scc_info_options left, scc_info_options right)
	Bitwise AND of two scc_info_options values. More...
scc_info_options	operator| (scc_info_options left, scc_info_options right)
	Bitwise OR of two scc_info_options values. More...
std::ostream &	dump_scc_info_dot (std::ostream &out, const_twa_graph_ptr aut, scc_info *sccinfo=nullptr)
	Dump the SCC graph of aut on out. More...
emptiness_check_ptr	explicit_se05_search (const const_twa_ptr &a, option_map o=option_map())
	Returns an emptiness check on the spot::tgba automaton a. More...
emptiness_check_ptr	bit_state_hashing_se05_search (const const_twa_ptr &a, size_t size, option_map o=option_map())
	Returns an emptiness checker on the spot::tgba automaton a. More...
emptiness_check_ptr	se05 (const const_twa_ptr &a, option_map o)
	Wrapper for the two se05 implementations. More...
bool	has_separate_sets (const const_twa_graph_ptr &aut)
	Whether the Inf and Fin numbers are disjoint. More...
twa_graph_ptr	separate_sets_here (const twa_graph_ptr &aut)
	Separate the Fin and Inf sets used by an automaton. More...
twa_graph_ptr	simulation (const const_twa_graph_ptr &automaton, int trans_pruning=-1)
	Attempt to reduce the automaton by direct simulation. More...
twa_graph_ptr	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	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	split_edges (const const_twa_graph_ptr &aut)
	Transform edges into transitions. More...
twa_graph_ptr	separate_edges (const const_twa_graph_ptr &aut)
	Make edge labels disjoint. More...
twa_statistics	stats_reachable (const const_twa_ptr &g)
	Compute statistics for an automaton. More...
twa_sub_statistics	sub_stats_reachable (const const_twa_ptr &g)
	Compute sub statistics for an automaton. More...
unsigned long long	count_all_transitions (const const_twa_graph_ptr &g)
	Count all transitions, even unreachable ones. More...
bool	is_terminal_automaton (const const_twa_graph_ptr &aut, scc_info *sm=nullptr)
	Check whether an automaton is terminal. More...
bool	is_weak_automaton (const const_twa_graph_ptr &aut, scc_info *sm=nullptr)
	Check whether an automaton is weak. More...
bool	is_very_weak_automaton (const const_twa_graph_ptr &aut, scc_info *sm=nullptr)
	Check whether an automaton is very-weak. More...
bool	is_inherently_weak_automaton (const const_twa_graph_ptr &aut, scc_info *sm=nullptr)
	Check whether an automaton is inherently weak. More...
bool	is_safety_automaton (const const_twa_graph_ptr &aut, scc_info *sm=nullptr)
	Check whether an automaton is a safety automaton. More...
bool	is_liveness_automaton (const const_twa_graph_ptr &aut)
	Whether the automaton represents a liveness property. More...
void	check_strength (const twa_graph_ptr &aut, scc_info *sm=nullptr)
	Check whether an automaton is weak or terminal. More...
twa_graph_ptr	decompose_scc (const const_twa_graph_ptr &aut, const char *keep)
	Extract a sub-automaton of a given strength. More...
twa_graph_ptr	decompose_scc (scc_info &sm, const char *keep)
	Extract a sub-automaton of a given strength. More...
twa_graph_ptr	decompose_scc (scc_info &sm, unsigned scc_num, bool accepting=false)
	Extract a sub-automaton above an SCC. More...
void	strip_acceptance_here (twa_graph_ptr a)
	Remove all acceptance sets from a twa_graph. More...
twa_graph_ptr	sl (const_twa_graph_ptr aut)
	Close the automaton by allowing letters to be duplicated. More...
bool	is_stutter_invariant (formula f, twa_graph_ptr aut_f=nullptr)
	Check if a formula is stutter invariant. More...
bool	is_stutter_invariant (twa_graph_ptr aut_f, const_twa_graph_ptr aut_nf=nullptr, int algo=0)
	Check if an automaton has the stutter invariance property. More...
trival	check_stutter_invariance (twa_graph_ptr aut_f, formula f=nullptr, bool do_not_determinize=false, bool find_counterexamples=false)
	Check whether aut is stutter-invariant. More...
int	is_stutter_invariant_forward_closed (twa_graph_ptr aut, const std::vector< bool > &sistates)
	Test if the set of stutter-invariant states is forward-closed. More...
std::vector< bool >	make_stutter_invariant_forward_closed_inplace (twa_graph_ptr aut, const std::vector< bool > &sistates)
	Change the automaton so its set of stutter-invariant state is forward-closed. More...
twa_graph_ptr	sum (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right)
	Sum two twa into a new twa, performing the union of the two input automata. More...
twa_graph_ptr	sum (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right, unsigned left_state, unsigned right_state)
	Sum two twa into a new twa, performing the union of the two input automata. More...
twa_graph_ptr	sum_and (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right)
	Sum two twa into a new twa, using a universal initial transition, performing the intersection of the two languages of the input automata. More...
twa_graph_ptr	sum_and (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right, unsigned left_state, unsigned right_state)
	Sum two twa into a new twa, using a universal initial transition, performing the intersection of the two languages of the input automata. More...
twa_graph_ptr	split_2step (const const_twa_graph_ptr &aut, const bdd &output_bdd, bool complete_env=true, synthesis_info::splittype sp=synthesis_info::splittype::AUTO, bool moore=false)
	make each transition a 2-step transition, transforming the graph into an alternating arena More...
twa_graph_ptr	split_2step (const const_twa_graph_ptr &aut, bool complete_env=true, synthesis_info::splittype sp=synthesis_info::splittype::AUTO, bool moore=false)
	Like split_2step but relying on the named property 'synthesis-outputs'. More...
twa_graph_ptr	split_2step (const const_twa_graph_ptr &aut, synthesis_info &gi)
	Like split_2step but allows to fine-tune the splitting via the options set in gi, always completes the environment states and relies on the named property to extract the output proposition. More...
twa_graph_ptr	unsplit_2step (const const_twa_graph_ptr &aut)
	the inverse of split_2step More...
std::ostream &	operator<< (std::ostream &os, synthesis_info::algo s)
	Stream algo. More...
std::ostream &	operator<< (std::ostream &os, const synthesis_info &gi)
	Stream benchmarks and options. More...
twa_graph_ptr	ltl_to_game (formula f, const std::vector< std::string > &all_outs, synthesis_info &gi, const std::vector< std::string > *unobs=nullptr)
	Creates a game from a specification and a set of output propositions. More...
twa_graph_ptr	ltl_to_game (formula f, const std::vector< std::string > &all_outs, const std::vector< std::string > *unobs=nullptr)
	Creates a game from a specification and a set of output propositions. More...
mealy_like	try_create_direct_strategy (formula f, const std::vector< std::string > &output_aps, synthesis_info &gi, bool want_strategy=false)
	Creates a strategy for the formula given by calling all intermediate steps. More...
bool	solve_game (twa_graph_ptr arena, synthesis_info &gi)
	Solve a game, and update synthesis_info. More...
game_relabeling_map	partitioned_game_relabel_here (twa_graph_ptr &arena, bool relabel_env, bool relabel_play, bool split_env=false, bool split_play=false, unsigned max_letter=-1u, unsigned max_letter_mult=-1u)
	Tries to relabel a SPLIT game arena using fresh propositions. Can be applied to env or player depending on relabel_env and relabel_play. The arguments split_env and split_play determine whether or not env and player edges are to be split into several transitions labelled by letters not conditions. More...
void	relabel_game_here (twa_graph_ptr &arena, game_relabeling_map &rel_maps)
	Undoes a relabeling done by partitioned_game_relabel_here. A dedicated function is necessary in order to remove the variables tagging env and player conditions. More...
emptiness_check_ptr	explicit_tau03_search (const const_twa_ptr &a, option_map o=option_map())
	Returns an emptiness checker on the spot::tgba automaton a. More...
emptiness_check_ptr	explicit_tau03_opt_search (const const_twa_ptr &a, option_map o=option_map())
	Returns an emptiness checker on the spot::tgba automaton a. More...
twa_graph_ptr	to_parity (const const_twa_graph_ptr &aut, const to_parity_options options=to_parity_options())
	Take an automaton with any acceptance condition and return an equivalent parity automaton. More...
twa_graph_ptr	to_parity_old (const const_twa_graph_ptr &aut, bool pretty_print=false)
	Take an automaton with any acceptance condition and return an equivalent parity automaton. More...
twa_graph_ptr	parity_type_to_parity (const twa_graph_ptr &aut)
	Convert an automaton into a parity max automaton preserving structure when possible. More...
twa_graph_ptr	buchi_type_to_buchi (const twa_graph_ptr &aut)
	Convert an automaton into a Büchi automaton preserving structure when possible. More...
twa_graph_ptr	co_buchi_type_to_co_buchi (const twa_graph_ptr &aut)
	Convert an automaton into a co-Büchi automaton preserving structure when possible. More...
twa_graph_ptr	to_generalized_buchi (const const_twa_graph_ptr &aut)
	Take an automaton with any acceptance condition and return an equivalent Generalized Büchi automaton. More...
twa_graph_ptr	streett_to_generalized_buchi (const const_twa_graph_ptr &in)
	Convert Streett acceptance into generalized Büchi acceptance. More...
twa_graph_ptr	streett_to_generalized_buchi_maybe (const const_twa_graph_ptr &in)
	Convert Streett acceptance into generalized Büchi. More...
twa_graph_ptr	to_generalized_rabin (const const_twa_graph_ptr &aut, bool share_inf=false)
	Take an automaton with any acceptance condition and return an equivalent Generalized Rabin automaton. More...
twa_graph_ptr	to_generalized_streett (const const_twa_graph_ptr &aut, bool share_fin=false)
	Take an automaton with any acceptance condition and return an equivalent Generalized Streett automaton. More...
twa_graph_ptr	dnf_to_streett (const const_twa_graph_ptr &aut, bool original_states=false)
	Converts any DNF acceptance condition into Streett-like. More...
twa_graph_ptr	to_weak_alternating (const_twa_graph_ptr &aut, bool less=false)
	Convert an alternating automaton to a weak alternating automaton. More...
twa_word_ptr	make_twa_word (const bdd_dict_ptr &dict)
	Create an empty twa_word. More...
twa_word_ptr	make_twa_word (const twa_run_ptr &run)
	Create a twa_word from a twa_run. More...
twa_word_ptr	parse_word (const std::string &word, const bdd_dict_ptr &dict)
	Parse a twa_word. More...
bool	operator! (zielonka_tree_options me)
	Test whether no options are set. More...
zielonka_tree_options	operator& (zielonka_tree_options left, zielonka_tree_options right)
	Bitwise AND of two zielonka_tree_options sets. More...
zielonka_tree_options	operator| (zielonka_tree_options left, zielonka_tree_options right)
	Bitwise OR of two zielonka_tree_options sets. More...
zielonka_tree_options	operator- (zielonka_tree_options left, zielonka_tree_options right)
	Remove options from a zielonka_tree_options set (bitwise AND NOT). More...
twa_graph_ptr	zielonka_tree_transform (const const_twa_graph_ptr &aut)
	Paritize an automaton using Zielonka tree. More...
bool	operator! (acd_options me)
	Test whether no options are set. More...
acd_options	operator& (acd_options left, acd_options right)
	Bitwise AND of two acd_options sets. More...
acd_options	operator| (acd_options left, acd_options right)
	Bitwise OR of two acd_options sets. More...
acd_options	operator- (acd_options left, acd_options right)
	Remove options from an acd_options set (bitwise AND NOT). More...
twacube_ptr	make_twacube (const std::vector< std::string > aps)
	Build a shared twacube automaton. More...
spot::cube	satone_to_cube (bdd one, cubeset &cubeset, std::unordered_map< int, int > &binder)
	Transform one truth assignment represented as a BDD into a cube cube passed in parameter. The parameter binder map bdd indexes to cube indexes. More...
bdd	cube_to_bdd (spot::cube cube, const cubeset &cubeset, std::unordered_map< int, int > &reverse_binder)
	Transform a cube cube into a BDD using the map that binds cube indexes to BDD indexes. More...
std::vector< std::string > *	extract_aps (spot::const_twa_graph_ptr aut, std::unordered_map< int, int > &ap_binder)
	Extract the atomic propositions from the automaton. This method also fills the binder, i.e., the mapping between BDD indexes and cube indexes. More...
twacube_ptr	twa_to_twacube (spot::const_twa_graph_ptr aut)
	Convert a twa into a twacube. More...
spot::twa_graph_ptr	twacube_to_twa (spot::twacube_ptr twacube, spot::bdd_dict_ptr d=nullptr)
	Convert a twacube into a twa. When d is specified, the BDD_dict in parameter is used rather than creating a new one. More...
bool	are_equivalent (const spot::twacube_ptr twacube, const spot::const_twa_graph_ptr twa)
	Check whether a twacube and a twa are equivalent. More...
bool	is_spin_ap (const char *str)
	Whether a word can be used as an atomic proposition for Spin 5. More...
bitvect *	make_bitvect (size_t bitcount)
	Allocate a bit-vector of bitcount bits. More...
bitvect_array *	make_bitvect_array (size_t bitcount, size_t vectcount)
	Allocate vectcount bit-vectors of bitcount bits. More...
std::ostream &	escape_rfc4180 (std::ostream &os, const std::string &str)
	Double characters " in strings. More...
std::ostream &	escape_latex (std::ostream &os, const std::string &str)
	Escape special LaTeX characters. More...
std::ostream &	escape_html (std::ostream &os, const std::string &str)
	Escape special HTML characters. More...
std::ostream &	escape_str (std::ostream &os, const std::string &str)
	Escape characters ", \, and \n in str. More...
std::string	escape_str (const std::string &str)
	Escape characters ", \, and \n in str. More...
std::ostream &	quote_shell_string (std::ostream &os, const char *str)
	Output str between simple quote or double quotes. More...
size_t	wang32_hash (size_t key)
	Thomas Wang's 32 bit hash function. More...
size_t	knuth32_hash (size_t key)
	Knuth's Multiplicative hash function. More...
template<class It >
size_t	fnv_hash (It begin, It end)
	Fowler-Noll-Vo hash function. More...
void	int_array_array_compress2 (const int *array, size_t n, int *dest, size_t &dest_size)
	Compress an int array of size n into a int array. More...
void	int_array_array_decompress2 (const int *array, size_t array_size, int *res, size_t size)
	Uncompress an int array of size array_size into a int array of size size. More...
void	int_vector_vector_compress (const std::vector< int > &input, std::vector< unsigned int > &output)
	Compress an int vector into a vector of unsigned int. More...
void	int_vector_vector_decompress (const std::vector< unsigned int > &array, std::vector< int > &output, size_t size)
	Uncompress a vector of unsigned int into a vector of size size. More...
const std::vector< unsigned int > *	int_array_vector_compress (const int *array, size_t n)
	Compress an int array if size n into a vector of unsigned int. More...
void	int_vector_array_decompress (const std::vector< unsigned int > *array, int *res, size_t size)
	Uncompress a vector of unsigned int into an int array of size size. More...
void	int_array_array_compress (const int *array, size_t n, int *dest, size_t &dest_size)
	Compress an int array of size n into a int array. More...
void	int_array_array_decompress (const int *array, size_t array_size, int *res, size_t size)
	Uncompress an int array of size array_size into a int array of size size. More...
void	srand (unsigned int seed)
	Reset the seed of the pseudo-random number generator. More...
int	rrand (int min, int max)
	Compute a pseudo-random integer value between min and max included. More...
int	mrand (int max)
	Compute a pseudo-random integer value between 0 and max-1 included. More...
double	drand ()
	Compute a pseudo-random double value between 0.0 and 1.0 (1.0 excluded). More...
double	nrand ()
	Compute a pseudo-random double value following a standard normal distribution. (Odeh & Evans) More...
template<class iterator_type >
void	mrandom_shuffle (iterator_type &&first, iterator_type &&last)
	Shuffle the container using mrand function above. This allows to get rid off shuffle or random_shuffle that use uniform_distribution and RandomIterator that are not portables. More...
temporary_file *	create_tmpfile (const char *prefix, const char *suffix=nullptr)
	Create a temporary file. More...
open_temporary_file *	create_open_tmpfile (const char *prefix, const char *suffix=nullptr)
	Create a temporary file and leave it open for writing. More...
void	cleanup_tmpfiles ()
	Delete all temporary files. More...
constexpr bool	operator== (trival a, trival b)
	Equality comparison of two trival values. More...
constexpr bool	operator!= (trival a, trival b)
	Inequality comparison of two trival values. More...
constexpr trival	operator&& (trival a, trival b)
	Three-valued Kleene logical AND. More...
constexpr trival	operator&& (bool a, trival b)
	Three-valued AND with bool left operand. More...
constexpr trival	operator&& (trival a, bool b)
	Three-valued AND with bool right operand. More...
constexpr trival	operator|| (trival a, trival b)
	Three-valued Kleene logical OR. More...
constexpr trival	operator|| (bool a, trival b)
	Three-valued OR with bool left operand. More...
constexpr trival	operator|| (trival a, bool b)
	Three-valued OR with bool right operand. More...
std::ostream &	operator<< (std::ostream &os, trival v)
	Print a trival value to os. More...
void	hoayyreset (void *scanner)
	Reset the HOA lexer state. More...
int	hoayyopen (const std::string &name, void **scanner)
	Open an HOA file from a path. More...
int	hoayyopen (int fd, void **scanner)
	Open an HOA file from a descriptor. More...
int	hoayystring (const char *data, void **scanner)
	Scan HOA data from a string. More...
void	hoayyclose (void *scanner)
	Close the HOA lexer. More...
std::vector< unsigned char >	collect_apids_with_polarities (formula f)
	Collect the APs occurring in f, along with their polarities. More...
void	collect_apids_with_polarities (formula f, std::vector< unsigned char > &v)
	Collect the APs occurring in f, along with their polarities. More...
std::vector< unsigned char >	collect_quantified_apids (formula f)
	Collect quantified APs occurring in f. More...
void	collect_quantified_apids (formula f, std::vector< unsigned char > &v)
	Collect quantified APs occurring in f. More...
formula	relabel_bse (formula f, relabeling_style style, relabeling_map *m=nullptr)
	Relabel Boolean subexpressions in a formula using atomic propositions. More...
formula	relabel_overlapping_bse (formula f, relabeling_style style, relabeling_map *m)
	Relabel Boolean subexpressions in a formula using atomic propositions. More...
formula	relabel_apply (formula f, relabeling_map *m)
	Replace atomic propositions of f by subformulas specified in m. More...
formula	relabel_apply (formula f, const std::vector< formula > &m)
	Relabel Boolean subexpressions in a formula using atomic propositions. More...
std::ostream &	operator<< (std::ostream &os, const acc_cond &acc)
	prints the acceptance formula as text More...
std::ostream &	operator<< (std::ostream &os, acc_cond::mark_t m)
	prints the acceptance formula as text More...
std::ostream &	operator<< (std::ostream &os, const acc_cond::acc_code &code)
	prints the acceptance formula as text More...
bdd	formula_to_bdd (formula f, const bdd_dict_ptr &d, void *for_me)
	Convert a Boolean formula into a BDD. More...
template<typename T >
bdd	formula_to_bdd (formula f, const bdd_dict_ptr &d, const std::shared_ptr< T > &for_me)
	Convert a Boolean formula into a BDD. More...
formula	bdd_to_formula (bdd f, const bdd_dict_ptr d)
	Convert a BDD into a formula. More...
formula	bdd_to_cnf_formula (bdd f, const bdd_dict_ptr d)
	Convert a BDD into a formula. More...
aig_ptr	mealy_machine_to_aig (const const_twa_graph_ptr &m, const char *mode, const std::string *terminating_signal=nullptr)
	Convert a mealy (like) machine into an aig relying on the transformation described by mode. More...
aig_ptr	mealy_machine_to_aig (const mealy_like &m, const char *mode, const std::string *terminating_signal=nullptr)
	Convert a mealy (like) machine into an aig relying on the transformation described by mode. More...
aig_ptr	mealy_machine_to_aig (const twa_graph_ptr &m, const char *mode, const std::vector< std::string > &ins, const std::vector< std::string > &outs, const realizability_simplifier *rs=nullptr, const std::string *terminating_signal=nullptr)
	Convert a mealy (like) machine into an aig relying on the transformation described by mode, with explicit AP lists. More...
aig_ptr	mealy_machine_to_aig (mealy_like &m, const char *mode, const std::vector< std::string > &ins, const std::vector< std::string > &outs, const realizability_simplifier *rs=nullptr, const std::string *terminating_signal=nullptr)
	Convert a mealy (like) machine into an aig relying on the transformation described by mode, with explicit AP lists. More...
aig_ptr	mealy_machines_to_aig (const std::vector< const_twa_graph_ptr > &m_vec, const char *mode, const std::string *terminating_signal=nullptr)
	Convert multiple mealy machines into an aig relying on the transformation described by mode. More...
aig_ptr	mealy_machines_to_aig (const std::vector< mealy_like > &m_vec, const char *mode, const std::string *terminating_signal=nullptr)
	Convert multiple mealy machines into an aig relying on the transformation described by mode. More...
aig_ptr	mealy_machines_to_aig (const std::vector< const_twa_graph_ptr > &m_vec, const char *mode, const std::vector< std::string > &ins, const std::vector< std::vector< std::string >> &outs, const realizability_simplifier *rs=nullptr, const std::string *terminating_signal=nullptr)
	Convert multiple mealy machines into an aig relying on the transformation described by mode. More...
aig_ptr	mealy_machines_to_aig (const std::vector< twa_graph_ptr > &m_vec, const char *mode, const std::vector< std::string > &ins, const std::vector< std::vector< std::string >> &outs, const realizability_simplifier *rs=nullptr, const std::string *terminating_signal=nullptr)
	Convert multiple mealy machines into an aig relying on the transformation described by mode. More...
aig_ptr	mealy_machines_to_aig (const std::vector< mealy_like > &m_vec, const char *mode, const std::vector< std::string > &ins, const std::vector< std::vector< std::string >> &outs, const realizability_simplifier *rs=nullptr, const std::string *terminating_signal=nullptr)
	Convert multiple mealy machines into an aig relying on the transformation described by mode. More...
template<class I >
unsigned	states_and (const twa_graph_ptr &aut, I begin, I end)
	Combine two states in a conjunction. More...
template<class T >
unsigned	states_and (const twa_graph_ptr &aut, const std::initializer_list< T > &il)
	Combine two states in a conjunction. More...
twa_graph_ptr	cleanup_acceptance_here (twa_graph_ptr aut, bool strip=true)
	Remove useless acceptance sets. More...
twa_graph_ptr	cleanup_acceptance (const_twa_graph_ptr aut, bool strip=true)
	Remove useless acceptance sets. More...
twa_graph_ptr	simplify_acceptance_here (twa_graph_ptr aut)
	Simplify an acceptance condition. More...
twa_graph_ptr	simplify_acceptance (const_twa_graph_ptr aut)
	Simplify an acceptance condition. More...
bool	contains (const_twa_graph_ptr left, const_twa_ptr right)
	Test if the language of right is included in that of left. More...
bool	contains (const_twa_graph_ptr left, formula right)
	Test if the language of right is included in that of left. More...
bool	contains (formula left, const_twa_ptr right)
	Test if the language of right is included in that of left. More...
bool	contains (formula left, formula right)
	Test if the language of right is included in that of left. More...
bool	are_equivalent (const_twa_graph_ptr left, const_twa_graph_ptr right)
	Test if the language of left is equivalent to that of right. More...
bool	are_equivalent (const_twa_graph_ptr left, formula right)
	Test if the language of left is equivalent to that of right. More...
bool	are_equivalent (formula left, const_twa_graph_ptr right)
	Test if the language of left is equivalent to that of right. More...
bool	are_equivalent (formula left, formula right)
	Test if the language of left is equivalent to that of right. More...
twa_graph_ptr	partial_degeneralize (const const_twa_graph_ptr &a, acc_cond::mark_t todegen)
	@} More...
twa_graph_ptr	partial_degeneralize (twa_graph_ptr a)
	@} More...
std::vector< acc_cond::mark_t >	propagate_marks_vector (const const_twa_graph_ptr &aut, const scc_info *si=nullptr)
	Propagate marks around the automaton. More...
void	propagate_marks_here (twa_graph_ptr &aut, const scc_info *si=nullptr)
	Propagate marks around the automaton. More...
std::ostream &	print_pg (std::ostream &os, const const_twa_graph_ptr &arena)
	Print a parity game using PG-solver syntax. More...
void	pg_print (std::ostream &os, const const_twa_graph_ptr &arena)
	Print a parity game using PG-solver syntax. More...
void	set_state_players (twa_graph_ptr &arena, const region_t &owners)
	Set the owner for all the states. More...
void	set_state_players (twa_graph_ptr &arena, region_t &&owners)
	Set the owner for all the states. More...
const region_t &	get_state_players (const const_twa_graph_ptr &arena)
	Get the owner of all states. More...
const region_t &	get_state_players (twa_graph_ptr &arena)
	Get the owner of all states. More...
const strategy_t &	get_strategy (const const_twa_graph_ptr &arena)
	Get or set the strategy. More...
void	set_strategy (twa_graph_ptr &arena, const strategy_t &strat)
	Get or set the strategy. More...
void	set_strategy (twa_graph_ptr &arena, strategy_t &&strat)
	Get or set the strategy. More...
void	set_state_winners (twa_graph_ptr &arena, const region_t &winners)
	Set the winner for all the states. More...
void	set_state_winners (twa_graph_ptr &arena, region_t &&winners)
	Set the winner for all the states. More...
const region_t &	get_state_winners (const const_twa_graph_ptr &arena)
	Get the winner of all states. More...
const region_t &	get_state_winners (twa_graph_ptr &arena)
	Get the winner of all states. More...
twa_graph_ptr	update_bounds_given_here (twa_graph_ptr &aut, const_twa_graph_ptr &fact, bool *changed=nullptr)
	Build "bounded automata" from knowledge. More...
twa_graph_ptr	update_bounds_given (const_twa_graph_ptr &aut, const_twa_graph_ptr &fact)
	Build "bounded automata" from knowledge. More...
twa_graph_ptr	update_bounds_given_here (twa_graph_ptr &aut, formula fact, bool *changed=nullptr)
	Build "bounded automata" from knowledge. More...
twa_graph_ptr	update_bounds_given (const_twa_graph_ptr &aut, formula fact)
	Build "bounded automata" from knowledge. More...
twa_graph_ptr	bounds_simplify_here (twa_graph_ptr &aut, bool *changedptr=nullptr)
	Choose labels in a bounded automaton. More...
twa_graph_ptr	bounds_simplify (const_twa_graph_ptr &aut, bool *changedptr=nullptr)
	Choose labels in a bounded automaton. More...
mtdfa_ptr	quantify_exists (const mtdfa_ptr &dfa, bdd vars, bool trim=true)
	Existentially quantify variables in an MTDFA. More...
mtdfa_ptr	quantify_exists (const mtdfa_ptr &dfa, const formula &ap, bool trim=true)
	Existentially quantify variables in an MTDFA. More...
mtdfa_ptr	quantify_exists (const mtdfa_ptr &dfa, const std::vector< formula > &aps, bool trim=true)
	Existentially quantify variables in an MTDFA. More...
mtdfa_ptr	quantify_forall (const mtdfa_ptr &dfa, bdd vars, bool trim=true)
	Universally quantify variables in an MTDFA. More...
mtdfa_ptr	quantify_forall (const mtdfa_ptr &dfa, const formula &ap, bool trim=true)
	Universally quantify variables in an MTDFA. More...
mtdfa_ptr	quantify_forall (const mtdfa_ptr &dfa, const std::vector< formula > &aps, bool trim=true)
	Universally quantify variables in an MTDFA. More...
std::vector< bool >	mtdfa_winning_region_lazy (mtdfa_ptr dfa)
	Compute the winning region of the MTDFA interpreted as a game. Lazy version. More...
std::vector< trival >	mtdfa_winning_region_lazy3 (mtdfa_ptr dfa)
	Compute the winning region of the MTDFA interpreted as a game. Lazy version. More...
mtdfa_ptr	mtdfa_restrict_as_game (mtdfa_ptr dfa)
	Build a generalized strategy from a set of winning states. More...
mtdfa_ptr	mtdfa_restrict_as_game (mtdfa_ptr dfa, const std::vector< bool > &winning_states)
	Build a generalized strategy from a set of winning states. More...
mtdfa_ptr	mtdfa_restrict_as_game (mtdfa_ptr dfa, const std::vector< trival > &winning_states)
	Build a generalized strategy from a set of winning states. More...
twa_graph_ptr	split_separated_mealy (const const_twa_graph_ptr &m)
	Split a separated mealy machine. More...
void	split_separated_mealy_here (const twa_graph_ptr &m)
	Split a separated mealy machine. More...
void	simplify_mealy_here (twa_graph_ptr &m, int minimize_lvl, bool split_out)
	Convenience function to call minimize_mealy or reduce_mealy. Uses the same convention as ltlsynt for minimize_lvl (or the field minimize_lvl of si): More...
void	simplify_mealy_here (twa_graph_ptr &m, synthesis_info &si, bool split_out)
	Convenience function to call minimize_mealy or reduce_mealy. Uses the same convention as ltlsynt for minimize_lvl (or the field minimize_lvl of si): More...
mtdswa_ptr	minimize_mtdswa (const mtdswa_ptr &dfa)
	Minimization of MTDSwA. More...
mtdswa_ptr	minimize_mtdswa (const mtdswa_ptr &dfa, const std::vector< unsigned > &initial_partition)
	Minimization of MTDSwA. More...
mtdswa_ptr	quantify_exists (const mtdswa_ptr &swa, bdd vars, bool trim=true)
	Existentially quantify variables in a weak MTDSwA. More...
mtdswa_ptr	quantify_exists (const mtdswa_ptr &swa, const formula &ap, bool trim=true)
	Existentially quantify variables in a weak MTDSwA. More...
mtdswa_ptr	quantify_exists (const mtdswa_ptr &swa, const std::vector< formula > &aps, bool trim=true)
	Existentially quantify variables in a weak MTDSwA. More...
mtdswa_ptr	quantify_forall (const mtdswa_ptr &swa, bdd vars, bool trim=true)
	Universally quantify variables in a weak MTDSwA. More...
mtdswa_ptr	quantify_forall (const mtdswa_ptr &swa, const formula &ap, bool trim=true)
	Universally quantify variables in a weak MTDSwA. More...
mtdswa_ptr	quantify_forall (const mtdswa_ptr &swa, const std::vector< formula > &aps, bool trim=true)
	Universally quantify variables in a weak MTDSwA. More...
twa_graph_ptr	cleanup_parity (const const_twa_graph_ptr &aut, bool keep_style=false)
	Remove useless acceptance sets of an automaton with parity acceptance. More...
twa_graph_ptr	cleanup_parity_here (twa_graph_ptr aut, bool keep_style=false)
	Remove useless acceptance sets of an automaton with parity acceptance. More...
twa_graph_ptr	colorize_parity (const const_twa_graph_ptr &aut, bool keep_style=false)
	Colorize an automaton with parity acceptance. More...
twa_graph_ptr	colorize_parity_here (twa_graph_ptr aut, bool keep_style=false)
	Colorize an automaton with parity acceptance. More...
twa_graph_ptr	reduce_parity (const const_twa_graph_ptr &aut, bool colored=false, bool layered=false)
	Reduce the parity acceptance condition to use a minimal number of colors. More...
twa_graph_ptr	reduce_parity_here (twa_graph_ptr aut, bool colored=false, bool layered=false)
	Reduce the parity acceptance condition to use a minimal number of colors. More...
std::pair< quantifier_list, formula >	extract_quantifier_list (formula f, bdd_dict_ptr dict, void *for_me)
	Convert quantified LTL to unquantified LTL + quantifier_list. More...
template<typename T >
std::pair< quantifier_list, formula >	extract_quantifier_list (formula f, bdd_dict_ptr dict, std::shared_ptr< T > for_me)
	Convert quantified LTL to unquantified LTL + quantifier_list. More...
twa_graph_ptr	cosimulation (const const_twa_graph_ptr &automaton, int trans_pruning=-1)
	Attempt to reduce the automaton by reverse simulation. More...
twa_graph_ptr	cosimulation_sba (const const_twa_graph_ptr &automaton, int trans_pruning=-1)
	Attempt to reduce the automaton by reverse simulation. More...
twa_graph_ptr	iterated_simulations (const const_twa_graph_ptr &automaton, int trans_pruning=-1)
	Iterate simulation() and cosimulation(). More...
twa_graph_ptr	iterated_simulations_sba (const const_twa_graph_ptr &automaton, int trans_pruning=-1)
	Iterate simulation() and cosimulation(). More...
twa_graph_ptr	reduce_direct_sim (const const_twa_graph_ptr &aut)
	Attempt to reduce the automaton by direct simulation. More...
twa_graph_ptr	reduce_direct_sim_sba (const const_twa_graph_ptr &aut)
	Attempt to reduce the automaton by direct simulation. More...
twa_graph_ptr	reduce_direct_cosim (const const_twa_graph_ptr &aut)
	Attempt to reduce the automaton by reverse simulation. More...
twa_graph_ptr	reduce_direct_cosim_sba (const const_twa_graph_ptr &aut)
	Attempt to reduce the automaton by reverse simulation. More...
twa_graph_ptr	reduce_iterated (const const_twa_graph_ptr &aut)
	Iterate reduce_direct_sim() and reduce_direct_cosim(). More...
twa_graph_ptr	reduce_iterated_sba (const const_twa_graph_ptr &aut)
	Iterate reduce_direct_sim() and reduce_direct_cosim(). More...
twa_graph_ptr	sl2_inplace (twa_graph_ptr aut, bool *changedptr=nullptr)
	Close the automaton by allowing letters to be duplicated. More...
twa_graph_ptr	sl2 (const_twa_graph_ptr aut, bool *changedptr=nullptr)
	Close the automaton by allowing letters to be duplicated. More...
twa_graph_ptr	closure_inplace (twa_graph_ptr aut, bool *changedptr=nullptr)
	Close the automaton by allowing duplicate letter removal. More...
twa_graph_ptr	closure (const_twa_graph_ptr aut, bool *changedptr=nullptr)
	Close the automaton by allowing duplicate letter removal. More...
std::vector< bool >	stutter_invariant_states (const_twa_graph_ptr pos, const_twa_graph_ptr neg=nullptr)
	Determine the states that are stutter-invariant in pos. More...
std::vector< bool >	stutter_invariant_states (const_twa_graph_ptr pos, formula f_pos)
	Determine the states that are stutter-invariant in pos. More...
void	highlight_stutter_invariant_states (twa_graph_ptr pos, formula f_pos, unsigned color=0)
	Highlight the states of pos that are stutter-invariant. More...
void	highlight_stutter_invariant_states (twa_graph_ptr pos, const_twa_graph_ptr neg=nullptr, unsigned color=0)
	Highlight the states of pos that are stutter-invariant. More...
std::vector< bdd >	stutter_invariant_letters (const_twa_graph_ptr pos, const_twa_graph_ptr neg=nullptr)
	Determine the letters with which each state is stutter-invariant. More...
std::vector< bdd >	stutter_invariant_letters (const_twa_graph_ptr pos, formula f_pos)
	Determine the letters with which each state is stutter-invariant. More...
twa_graph_ptr	solved_game_to_mealy (twa_graph_ptr arena, synthesis_info &gi)
	creates a mealy machine from a solved game arena taking into account the options given in gi. This concerns in particular whether or not the machine is to be reduced and how. solved_game_to_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations More...
twa_graph_ptr	solved_game_to_mealy (twa_graph_ptr arena)
	creates a mealy machine from a solved game arena taking into account the options given in gi. This concerns in particular whether or not the machine is to be reduced and how. solved_game_to_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations More...
twa_graph_ptr	solved_game_to_separated_mealy (twa_graph_ptr arena, synthesis_info &gi)
	creates a mealy machine from a solved game arena taking into account the options given in gi. This concerns in particular whether or not the machine is to be reduced and how. solved_game_to_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations More...
twa_graph_ptr	solved_game_to_separated_mealy (twa_graph_ptr arena)
	creates a mealy machine from a solved game arena taking into account the options given in gi. This concerns in particular whether or not the machine is to be reduced and how. solved_game_to_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations More...
twa_graph_ptr	solved_game_to_split_mealy (twa_graph_ptr arena, synthesis_info &gi)
	creates a mealy machine from a solved game arena taking into account the options given in gi. This concerns in particular whether or not the machine is to be reduced and how. solved_game_to_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations More...
twa_graph_ptr	solved_game_to_split_mealy (twa_graph_ptr arena)
	creates a mealy machine from a solved game arena taking into account the options given in gi. This concerns in particular whether or not the machine is to be reduced and how. solved_game_to_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations More...
std::pair< std::vector< formula >, std::vector< std::set< formula > > >	split_independent_formulas (formula f, const std::vector< std::string > &outs)
	Seeks to decompose a formula into independently synthetizable sub-parts. The conjunction of all sub-parts then satisfies the specification. More...
std::pair< std::vector< formula >, std::vector< std::set< formula > > >	split_independent_formulas (const std::string &f, const std::vector< std::string > &outs)
	Seeks to decompose a formula into independently synthetizable sub-parts. The conjunction of all sub-parts then satisfies the specification. More...
twa_graph_ptr	acd_transform (const const_twa_graph_ptr &aut, bool colored=false)
	Paritize an automaton using ACD. More...
twa_graph_ptr	acd_transform_sbacc (const const_twa_graph_ptr &aut, bool colored=false, bool order_heuristic=true)
	Paritize an automaton using ACD. More...

Variables
constexpr const char *	default_unabbrev_string = "eFGiMW^"
	Default string of operators to unabbreviate. More...
enum	parity_kind { parity_kind_max , parity_kind_min , parity_kind_same , parity_kind_any }
	Parity kind type. More...
enum	parity_style { parity_style_odd , parity_style_even , parity_style_same , parity_style_any }
	Parity style type. More...
twa_graph_ptr	change_parity (const const_twa_graph_ptr &aut, parity_kind kind, parity_style style)
	Change the parity acceptance of an automaton. More...
twa_graph_ptr	change_parity_here (twa_graph_ptr aut, parity_kind kind, parity_style style)
	Parity kind type. More...
enum class	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(*	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...
typedef struct spot::process_timer	process_timer
	Struct used to start and stop both timer and stopwatch clocks. More...
std::ostream &	operator<< (std::ostream &os, const timer &dt)
	Struct used to start and stop both timer and stopwatch clocks. More...

Detailed Description

This file aggregates all classes and typedefs necessary to build a kripke that is thread safe.

Typedef Documentation

const_twa_run_ptr

typedef std::shared_ptr<const twa_run> spot::const_twa_run_ptr

Shared pointer to const twa_run.

kripke_graph_ptr

typedef std::shared_ptr<kripke_graph> spot::kripke_graph_ptr

Shared pointer to a kripke_graph.

process_timer

typedef struct spot::process_timer spot::process_timer

Struct used to start and stop both timer and stopwatch clocks.

relabeling_map

typedef std::map<formula, formula> spot::relabeling_map

Map associating new (key) formula names to old (value) ones.

shared_state_set

typedef std::unordered_set<shared_state, state_shared_ptr_hash, state_shared_ptr_equal> spot::shared_state_set

Unordered set of shared states.

snf_cache

typedef std::unordered_map<formula, formula> spot::snf_cache

Cache mapping formulas to their star normal form.

state_map

template<class val >

using spot::state_map = typedef std::unordered_map<const state*, val, state_ptr_hash, state_ptr_equal>

Unordered map of abstract states.

Destroying each state if needed is the user's responsibility.

state_set

typedef std::unordered_set<const state*, state_ptr_hash, state_ptr_equal> spot::state_set

Unordered set of abstract states.

Destroying each state if needed is the user's responsibility.

See also

state_unicity_table

Enumeration Type Documentation

mc_algorithm

enum spot::mc_algorithm

strong

The list of parallel model-checking algorithms available.

Enumerator
BLOEMEN_EC	Bloemen.16.hvc emptiness check.
BLOEMEN_SCC	Bloemen.16.ppopp SCC computation.
CNDFS	Evangelista.12.atva emptiness check.
DEADLOCK	Check whether there is a deadlock.
REACHABILITY	Only perform a reachability algorithm.
SWARMING	Holzmann.11.ieee applied to renault.13.lpar.

mc_rvalue

enum spot::mc_rvalue

strong

Return value of a parallel model-checking algorithm.

Enumerator
DEADLOCK	A deadlock has been found.
EMPTY	The product is empty.
FAILURE	The algorithm finished abnormally.
NO_DEADLOCK	No deadlock has been found.
NOT_EMPTY	The product is not empty.
SUCCESS	The algorithm finished normally.

ocheck

enum spot::ocheck

strong

Enum used to change the behavior of is_obligation().

pool_type

enum spot::pool_type

strong

An enum class to define the policy of the fixed_sized_pool. We propose 2 policies for the pool:

• Safe: ensure (when used with memcheck) that each allocation is deallocated one at a time
• Unsafe: rely on the fact that deallocating the pool also release all elements it contains. This case is useful in a multithreaded environment with multiple fixed_sized_pool allocating the same resource. In this case it's hard to detect which pool has allocated some resource.

relabeling_style

enum spot::relabeling_style

Style for relabeling atomic propositions.

Function Documentation

atomic_prop_cmp()

int spot::atomic_prop_cmp	(	const fnode *	f,
		const fnode *	g
	)

Order two atomic propositions.

Referenced by spot::formula_ptr_less_than_bool_first::operator()().

cleanup_parity()

twa_graph_ptr spot::cleanup_parity	(	const const_twa_graph_ptr &	aut,
		bool	keep_style = false
	)

Remove useless acceptance sets of an automaton with parity acceptance.

If two sets with the same parity are separated by unused sets, then these two sets are merged. The input must be an automaton with a parity acceptance, otherwise an invalid_argument exception is thrown.

Parameters

aut	the input automaton
keep_style	whether the style of the parity acc is kept.

Returns

the automaton without useless acceptance sets.

cleanup_parity_here()

twa_graph_ptr spot::cleanup_parity_here	(	twa_graph_ptr	aut,
		bool	keep_style = false
	)

Remove useless acceptance sets of an automaton with parity acceptance.

If two sets with the same parity are separated by unused sets, then these two sets are merged. The input must be an automaton with a parity acceptance, otherwise an invalid_argument exception is thrown.

Parameters

aut	the input automaton
keep_style	whether the style of the parity acc is kept.

Returns

the automaton without useless acceptance sets.

cleanup_tmpfiles()

void spot::cleanup_tmpfiles

(

)

Delete all temporary files.

Delete all temporary files that have been created but haven't been deleted so far. The verb "delete" should be understood as both the C++ delete operator (all temporary_file and open_temporary_file instance are destroyed) and as the file system operation (the actual files are removed).

Even in programs where temporary_file instance are consciously destroyed when they are not needed, cleanup_tmpfiles() could still be useful in signal handlers, for instance to clean all temporary files upon SIGINT.

colorize_parity()

twa_graph_ptr spot::colorize_parity	(	const const_twa_graph_ptr &	aut,
		bool	keep_style = false
	)

Colorize an automaton with parity acceptance.

An automaton is said colored iff all the transitions belong to exactly one acceptance set. The algorithm achieves that by removing superfluous acceptance marks. It may introduce a new set to mark the transitions with no acceptance sets and a second set may be introduced to keep the style. The input must be an automaton with a parity acceptance, otherwise an invalid_argument exception is thrown.

Parameters

aut	the input automaton
keep_style	whether the style of the parity acc is kept.

Returns

the colorized automaton

colorize_parity_here()

twa_graph_ptr spot::colorize_parity_here	(	twa_graph_ptr	aut,
		bool	keep_style = false
	)

Colorize an automaton with parity acceptance.

An automaton is said colored iff all the transitions belong to exactly one acceptance set. The algorithm achieves that by removing superfluous acceptance marks. It may introduce a new set to mark the transitions with no acceptance sets and a second set may be introduced to keep the style. The input must be an automaton with a parity acceptance, otherwise an invalid_argument exception is thrown.

Parameters

aut	the input automaton
keep_style	whether the style of the parity acc is kept.

Returns

the colorized automaton

count_univbranch_edges()

unsigned spot::count_univbranch_edges

(

const const_twa_graph_ptr &

aut

)

Count edges with universal branching.

This counts the number of edges going to several destination at once (as reported by aut->is_univ_dest(...)).

If the automaton starts in multiple initial states at once, this is considered as a universal "initial edge", and adds one to the total count.

Nondeterministic automata (which include deterministic automata) have 0 edges with universal branching.

See also

count_univbranch_states()

count_univbranch_states()

unsigned spot::count_univbranch_states

(

const const_twa_graph_ptr &

aut

)

Count states with some universal branching.

This counts the number of states that have edges going to several destinations at once (as reported by aut->is_univ_dest(...)).

Note that nondeterministic automata (which include deterministic automata) have 0 such state, but additionally they also have "singleton" initial state (which this function does not check).

See also

count_univbranch_edges()

create_open_tmpfile()

open_temporary_file* spot::create_open_tmpfile	(	const char *	prefix,
		const char *	suffix = nullptr
	)

Create a temporary file and leave it open for writing.

Same as create_tmpfile, be leave the file open for writing. The open_temporary_file::fd() method returns the file descriptor.

create_tmpfile()

temporary_file* spot::create_tmpfile	(	const char *	prefix,
		const char *	suffix = nullptr
	)

Create a temporary file.

The file name will start with prefix, be followed by 6 randomish characters and will end in suffix. Usually suffix is used to set an extension (you should include the dot).

The temporary file is created and left empty. If you need to fill it, consider using create_open_tmpfile() instead.

degeneralize_tba()

twa_graph_ptr spot::degeneralize_tba	(	const const_twa_graph_ptr &	a,
		bool	use_z_lvl = true,
		bool	use_cust_acc_orders = false,
		int	use_lvl_cache = 1,
		bool	skip_levels = true,
		bool	ignaccsl = false,
		bool	remove_extra_scc = true
	)

Transition-based variant of degeneralize().

dtba_sat_minimize_assume()

twa_graph_ptr spot::dtba_sat_minimize_assume	(	const const_twa_graph_ptr &	a,
		bool	state_based = false,
		int	max_states = -1,
		int	param = 6
	)

Attempt to minimize a deterministic TBA incrementally with a SAT solver.

This acts like dtba_sat_synthetize() and obtains a first minimized automaton. Then, it adds param assumptions, such that each assumption removes a new state and implies the previous assumptions. A first resolution is attempted assuming the last assumption (thus involving all the previous ones). If the problem is SAT several stages have just been won and all this process is restarted. Otherwise, we know that the minimal automaton can be obtained with fewer assumption. This automaton is found dichotomously.

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

dtba_sat_minimize_dichotomy()

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

Attempt to minimize a deterministic TBA with a SAT solver.

This calls dtba_sat_synthetize() in a loop, but attempting to find the minimum number of states using a binary search. If no smaller TBA exist, this returns a null pointer.

dtba_sat_minimize_incr()

twa_graph_ptr spot::dtba_sat_minimize_incr	(	const const_twa_graph_ptr &	a,
		bool	state_based = false,
		int	max_states = -1,
		int	param = 2
	)

Attempt to minimize a det. TBA with a SAT solver.

This acts like dtba_sat_synthetize() and obtains a first minimized automaton. Then, incrementally, it encodes the deletion of one state and solves it as many times as param value. If param >= 0, this process is fully repeated until the minimal automaton is found. Otherwise, it continues to delete states one by one incrementally until the minimal automaton is found.

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

dtwa_sat_minimize()

twa_graph_ptr spot::dtwa_sat_minimize	(	const const_twa_graph_ptr &	a,
		unsigned	target_acc_number,
		const acc_cond::acc_code &	target_acc,
		bool	state_based = false,
		int	max_states = -1,
		bool	colored = false
	)

Attempt to minimize a deterministic TωA with a SAT solver.

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

If no smaller TGBA exists, this returns a null pointer.

dtwa_sat_minimize_assume()

twa_graph_ptr spot::dtwa_sat_minimize_assume	(	const const_twa_graph_ptr &	a,
		unsigned	target_acc_number,
		const acc_cond::acc_code &	target_acc,
		bool	state_based = false,
		int	max_states = -1,
		bool	colored = false,
		int	param = 6
	)

Attempt to minimize a deterministic TωA with a SAT solver.

This acts like dtba_sat_synthetize() and obtains a first minimized automaton. Then, it adds param assumptions, such that each assumption removes a new state and implies the previous assumptions. A first resolution is attempted assuming the last assumption (thus involving all the previous ones). If the problem is SAT several stages have just been won and all this process is restarted. Otherwise, it is known that the minimal automaton can be obtained with fewer assumption. This automaton is found dichotomously.

If no smaller TGBA exists, this returns a null pointer.

dtwa_sat_minimize_dichotomy()

twa_graph_ptr spot::dtwa_sat_minimize_dichotomy	(	const const_twa_graph_ptr &	a,
		unsigned	target_acc_number,
		const acc_cond::acc_code &	target_acc,
		bool	state_based = false,
		bool	langmap = false,
		int	max_states = -1,
		bool	colored = false
	)

Attempt to minimize a deterministic TωA with a SAT solver.

This calls dtwa_sat_synthetize() in a loop, but attempting to find the minimum number of states using a binary search. If no smaller TBA exist, this returns a null pointer.

dtwa_sat_minimize_incr()

twa_graph_ptr spot::dtwa_sat_minimize_incr	(	const const_twa_graph_ptr &	a,
		unsigned	target_acc_number,
		const acc_cond::acc_code &	target_acc,
		bool	state_based = false,
		int	max_states = -1,
		bool	colored = false,
		int	param = 2
	)

Attempt to minimize a deterministic TωA with a SAT solver.

It acts like dtwa_sat_synthetize() and obtains a first minimized automaton. Then, incrementally, it encodes and solves the deletion of one state as many times as param value. If param >= 0, this process is fully repeated until the minimal automaton is found. Otherwise, it continues to delete states one by one incrementally until the minimal automaton is found.

If no smaller TGBA exists, this returns a null pointer.

dump_scc_info_dot()

std::ostream& spot::dump_scc_info_dot	(	std::ostream &	out,
		const_twa_graph_ptr	aut,
		scc_info *	sccinfo = nullptr
	)

Dump the SCC graph of aut on out.

If sccinfo is not given, it will be computed.

get_synthesis_output_aps()

std::vector<std::string> spot::get_synthesis_output_aps

(

const const_twa_graph_ptr &

arena

)

Get the vector with the names of the output propositions.

is_input_deterministic_mealy()

bool spot::is_input_deterministic_mealy

(

const const_twa_graph_ptr &

m

)

Checks whether a mealy machine is input deterministic.

A machine is input deterministic if none of the states has two outgoing transitions that can agree on a common assignment of the input propositions. In case the mealy machine is split, the previous condition is tested only on states owned by player 0 (the environment).

Parameters

m	The automaton to be verified

See also

is_mealy

is_liveness()

bool spot::is_liveness

(

formula

f

)

Check whether a formula represents a liveness property.

A formula represents a liveness property if any finite prefix can be extended into a word accepted by the formula.

The test is done by conversion to automaton. If you already have an automaton, use spot::is_liveness_automaton() instead.

is_partially_degeneralizable()

acc_cond::mark_t spot::is_partially_degeneralizable	(	const const_twa_graph_ptr &	aut,
		bool	allow_inf = true,
		bool	allow_fin = true,
		const std::vector< acc_cond::mark_t > &	forbid = {}
	)

Is the automaton partially degeneralizable?

Return a mark M={m₁, m₂, ..., mₙ} such that either Inf(m₁)&Inf(m₂)&...&Inf(mₙ) or Fin(m₁)|Fin(m₂)|...|Fin(mₙ) appears in the acceptance condition of aut.

If multiple such marks exist the smallest such mark is returned. (This is important in case of overlapping options. E.g., in the formula Inf(0)&Inf(1)&Inf(3) | (Inf(0)&Inf(1))&Fin(2) we have two possible degeneralizations options {0,1,3}, and {0,1}. Degeneralizing for {0,1,3} and then {0,1} could enlarge the automaton by a factor 6, while degeneralizing by {0,1} and then some {x,y} may enlarge the automaton only by a factor 4.)

Return an empty mark otherwise if the automaton is not partially degeneralizable.

The optional arguments allow_inf and allow_fin, can be set to false to disallow one type of match.

If you need to disallow certain marks from being returned, pass them in the forbid vector.

list_formula_props()

std::list<std::string> spot::list_formula_props

(

const formula &

f

)

List the properties of formula f.

make_bitvect()

bitvect* spot::make_bitvect

(

size_t

bitcount

)

Allocate a bit-vector of bitcount bits.

The resulting object should be released with delete.

make_bitvect_array()

bitvect_array* spot::make_bitvect_array	(	size_t	bitcount,
		size_t	vectcount
	)

Allocate vectcount bit-vectors of bitcount bits.

The resulting bitvect_array should be released with delete.

make_kripke_graph()

kripke_graph_ptr spot::make_kripke_graph ( const bdd_dict_ptr &  d )

inline

Create a new kripke_graph.

mtdfa_winning_region_lazy()

std::vector<bool> spot::mtdfa_winning_region_lazy

(

mtdfa_ptr

dfa

)

Compute the winning region of the MTDFA interpreted as a game. Lazy version.

This is similar to mtdfa_winning_region, but it will only compute the winning status of states that are reachable from the initial state without crossing any accepting terminal.

In the trivial version, the returned vector indicates whether the environment can force the game to reach false (false), the controller can force the game to reach an accepting state (true), or no player can force the game to reach its target (maybe).

mtdfa_winning_region_lazy3()

std::vector<trival> spot::mtdfa_winning_region_lazy3

(

mtdfa_ptr

dfa

)

Compute the winning region of the MTDFA interpreted as a game. Lazy version.

This is similar to mtdfa_winning_region, but it will only compute the winning status of states that are reachable from the initial state without crossing any accepting terminal.

In the trivial version, the returned vector indicates whether the environment can force the game to reach false (false), the controller can force the game to reach an accepting state (true), or no player can force the game to reach its target (maybe).

nesting_depth() [1/3]

unsigned spot::nesting_depth	(	formula	f,
		const char *	opers
	)

Compute the nesting depth of a set of operators.

Return the maximum number of occurrence of any operator listed opers, among all branches of the AST of f.

Operators to count should be supplied in opers as a string of letters among 'X', 'F', 'G', 'U', 'R', 'M', 'W', '&', '|', '!', 'i' (implication), 'e' (equivalence).

Add letter '~' to force into negative normal form before processing it.

The string should be terminated by '\0' or ']'.

nesting_depth() [2/3]

unsigned spot::nesting_depth	(	formula	f,
		const op *	begin,
		const op *	end
	)

Compute the nesting depth of a set of operators.

Return the maximum number of occurrence of any operator between begin and end among all branches of the AST of f.

nesting_depth() [3/3]

unsigned spot::nesting_depth	(	formula	f,
		op	oper
	)

Compute the nesting depth of an operator.

Return the maximum number of occurrence of oper among all branches of the AST of f.

normalize_quantifiers()

formula spot::normalize_quantifiers

(

formula

)

Remove unnecessary quantified variables.

If a quantified variable does not appear in the body of the formula, simply remove it from the list of quantified variables. If a quantified variable always has the same polarity in the formula, it can be replaced by the appropriate constant.

operator!() [1/2]

bool spot::operator! ( acd_options  me )

inline

Test whether no options are set.

References NONE.

operator!() [2/2]

bool spot::operator! ( zielonka_tree_options  me )

inline

Test whether no options are set.

References NONE.

operator!=()

constexpr bool spot::operator!= ( trival  a, trival  b  )

constexpr

Inequality comparison of two trival values.

operator&() [1/2]

acd_options spot::operator& ( acd_options  left, acd_options  right  )

inline

Bitwise AND of two acd_options sets.

operator&() [2/2]

zielonka_tree_options spot::operator& ( zielonka_tree_options  left, zielonka_tree_options  right  )

inline

Bitwise AND of two zielonka_tree_options sets.

operator&&() [1/3]

constexpr trival spot::operator&& ( bool  a, trival  b  )

constexpr

Three-valued AND with bool left operand.

operator&&() [2/3]

constexpr trival spot::operator&& ( trival  a, bool  b  )

constexpr

Three-valued AND with bool right operand.

operator&&() [3/3]

constexpr trival spot::operator&& ( trival  a, trival  b  )

constexpr

Three-valued Kleene logical AND.

References spot::trival::maybe(), and spot::trival::val().

operator-() [1/2]

acd_options spot::operator- ( acd_options  left, acd_options  right  )

inline

Remove options from an acd_options set (bitwise AND NOT).

operator-() [2/2]

zielonka_tree_options spot::operator- ( zielonka_tree_options  left, zielonka_tree_options  right  )

inline

Remove options from a zielonka_tree_options set (bitwise AND NOT).

operator<<() [1/9]

std::ostream& spot::operator<<	(	std::ostream &	os,
		acc_cond::mark_t	m
	)

prints the acceptance formula as text

operator<<() [2/9]

std::ostream& spot::operator<<	(	std::ostream &	os,
		const acc_cond &	acc
	)

prints the acceptance formula as text

operator<<() [3/9]

std::ostream& spot::operator<<	(	std::ostream &	os,
		const acc_cond::acc_code &	code
	)

prints the acceptance formula as text

operator<<() [4/9]

std::ostream& spot::operator<<	(	std::ostream &	os,
		const ec_stats &	es
	)

Print ec_stats to a stream.

References spot::ec_stats::finisher, spot::ec_stats::name, spot::ec_stats::sccs, spot::ec_stats::states, spot::ec_stats::transitions, spot::ec_stats::value, and spot::ec_stats::walltime.

operator<<() [5/9]

std::ostream& spot::operator<<	(	std::ostream &	os,
		const formula &	f
	)

Print a formula.

operator<<() [6/9]

std::ostream& spot::operator<<	(	std::ostream &	os,
		const mc_algorithm &	ma
	)

Print an mc_algorithm value to a stream.

References BLOEMEN_EC, BLOEMEN_SCC, CNDFS, DEADLOCK, REACHABILITY, and SWARMING.

operator<<() [7/9]

std::ostream& spot::operator<<	(	std::ostream &	os,
		const mc_rvalue &	mr
	)

Print an mc_rvalue value to a stream.

References DEADLOCK, EMPTY, FAILURE, NO_DEADLOCK, NOT_EMPTY, and SUCCESS.

operator<<() [8/9]

std::ostream& spot::operator<< ( std::ostream &  os, const timer &  dt  )

inline

Struct used to start and stop both timer and stopwatch clocks.

operator<<() [9/9]

std::ostream& spot::operator<< ( std::ostream &  os, trival  v  )

inline

Print a trival value to os.

References spot::trival::val().

operator==()

constexpr bool spot::operator== ( trival  a, trival  b  )

constexpr

Equality comparison of two trival values.

References spot::trival::val().

Referenced by spot::bitset< N >::operator!=().

operator|() [1/3]

acd_options spot::operator| ( acd_options  left, acd_options  right  )

inline

Bitwise OR of two acd_options sets.

operator|() [2/3]

const mc_rvalue spot::operator|	(	const mc_rvalue &	lhs,
		const mc_rvalue &	rhs
	)

This function helps to find the output value from a set of threads that may have different values.

References DEADLOCK, EMPTY, FAILURE, NO_DEADLOCK, NOT_EMPTY, and SUCCESS.

operator|() [3/3]

zielonka_tree_options spot::operator| ( zielonka_tree_options  left, zielonka_tree_options  right  )

inline

Bitwise OR of two zielonka_tree_options sets.

operator||() [1/3]

constexpr trival spot::operator|| ( bool  a, trival  b  )

constexpr

Three-valued OR with bool left operand.

operator||() [2/3]

constexpr trival spot::operator|| ( trival  a, bool  b  )

constexpr

Three-valued OR with bool right operand.

operator||() [3/3]

constexpr trival spot::operator|| ( trival  a, trival  b  )

constexpr

Three-valued Kleene logical OR.

References spot::trival::maybe(), and spot::trival::val().

otf_product()

twa_product_ptr spot::otf_product ( const const_twa_ptr &  left, const const_twa_ptr &  right  )

inline

on-the-fly TGBA product

otf_product_at()

twa_product_ptr spot::otf_product_at ( const const_twa_ptr &  left, const const_twa_ptr &  right, const state *  left_init, const state *  right_init  )

inline

on-the-fly TGBA product with forced initial states

print_formula_props()

std::ostream& spot::print_formula_props	(	std::ostream &	out,
		const formula &	f,
		bool	abbreviated = false
	)

Print the properties of formula f on stream out.

reduce_parity()

twa_graph_ptr spot::reduce_parity	(	const const_twa_graph_ptr &	aut,
		bool	colored = false,
		bool	layered = false
	)

Reduce the parity acceptance condition to use a minimal number of colors.

This implements an algorithm derived from the following article, but generalized to all types of parity acceptance. [carton.99.ita]

The kind of parity (min/max) is preserved, but the style (odd/even) may be altered to reduce the number of colors used.

If colored is true, colored automata are output (this is what the above paper assumes). Otherwise, the smallest or highest colors (depending on the parity kind) is removed to simplify the acceptance condition.

If the input uses state-based acceptance, the output will use state-based acceptance as well.

A parity automaton, sometimes called a chain automaton, can be seen as a stack of layers that are alternatively rejecting and accepting. For instance imagine a parity max automaton that is strongly connected. Removing the transitions with the maximal color might leave a few transitions that were not labeled by this maximal color, but that are part of any cycle anymore: those transitions could have been colored with the maximal color, since any cycle going through them would have seen the maximal color. (Once you remove this maximal layer, you can define the next layer similarly.)

When layered is true, all transitions that belong to the same layer receive the same color. When layer is false, only the transitions that were used initially to define the layers (i.e, the transition with the maximal color in the previous example), get their color adjusted. The others will receive either no color (if colored is false), or a useless color (if colored is true). Here "useless color" means the smallest color for parity max, and the largest color for parity min.

When layered is true, the output of this function is comparable to what acd_transform() would produce. The difference is that this function preserves the kind (min/max) of parity input, while acd_transform() always outputs a parity min automaton. Additionally, this function needs fewer resources than acd_transform() because it is already known that the input is a parity automaton. In some (historically inaccurate) way, reduce_parity() can be seen as a specialized version of acd_transform().

The reason layered is false by default, is that not introducing colors in place where there were none occasionally help with simulation-based reductions.

reduce_parity_here()

twa_graph_ptr spot::reduce_parity_here	(	twa_graph_ptr	aut,
		bool	colored = false,
		bool	layered = false
	)

Reduce the parity acceptance condition to use a minimal number of colors.

This implements an algorithm derived from the following article, but generalized to all types of parity acceptance. [carton.99.ita]

The kind of parity (min/max) is preserved, but the style (odd/even) may be altered to reduce the number of colors used.

If colored is true, colored automata are output (this is what the above paper assumes). Otherwise, the smallest or highest colors (depending on the parity kind) is removed to simplify the acceptance condition.

If the input uses state-based acceptance, the output will use state-based acceptance as well.

A parity automaton, sometimes called a chain automaton, can be seen as a stack of layers that are alternatively rejecting and accepting. For instance imagine a parity max automaton that is strongly connected. Removing the transitions with the maximal color might leave a few transitions that were not labeled by this maximal color, but that are part of any cycle anymore: those transitions could have been colored with the maximal color, since any cycle going through them would have seen the maximal color. (Once you remove this maximal layer, you can define the next layer similarly.)

When layered is true, all transitions that belong to the same layer receive the same color. When layer is false, only the transitions that were used initially to define the layers (i.e, the transition with the maximal color in the previous example), get their color adjusted. The others will receive either no color (if colored is false), or a useless color (if colored is true). Here "useless color" means the smallest color for parity max, and the largest color for parity min.

When layered is true, the output of this function is comparable to what acd_transform() would produce. The difference is that this function preserves the kind (min/max) of parity input, while acd_transform() always outputs a parity min automaton. Additionally, this function needs fewer resources than acd_transform() because it is already known that the input is a parity automaton. In some (historically inaccurate) way, reduce_parity() can be seen as a specialized version of acd_transform().

The reason layered is false by default, is that not introducing colors in place where there were none occasionally help with simulation-based reductions.

sat_minimize()

twa_graph_ptr spot::sat_minimize	(	twa_graph_ptr	aut,
		const char *	opt,
		bool	state_based = false
	)

High-level interface to SAT-based minimization.

Minimize the automaton aut, using options opt. These options are given as a comma-separated list of assignments of the form:

states = 10 // synthesize automaton with fixed number of states max-states = 20 // minimize starting from this upper bound acc = "generalized-Buchi 2" acc = "Rabin 3" acc = "same" /* default *‍/ dichotomy = 1 // use dichotomy incr = 1 // use satsolver incrementally to attempt to delete a fixed number of states before starting from scratch incr < 0 // use satsolver incrementally, never restart colored = 1 // build a colored TωA log = "filename"

tba_determinize()

twa_graph_ptr spot::tba_determinize	(	const const_twa_graph_ptr &	aut,
		unsigned	threshold_states = 0,
		unsigned	threshold_cycles = 0
	)

Determinize a TBA using the powerset construction.

The input automaton should have at most one acceptance condition. Beware that not all Büchi automata can be determinized, and this procedure does not ensure that the produced automaton is equivalent to aut.

The construction is adapted from Section 3.2 of [dax.07.atva] only adapted to work on TBA rather than BA.

If threshold_states is non null, abort the construction whenever it would build an automaton that is more than threshold_states time bigger (in term of states) than the original automaton.

If threshold_cycles is non null, abort the construction whenever an SCC of the constructed automaton has more than threshold_cycles cycles.

tba_determinize_check()

twa_graph_ptr spot::tba_determinize_check	(	const twa_graph_ptr &	aut,
		unsigned	threshold_states = 0,
		unsigned	threshold_cycles = 0,
		formula	f = nullptr,
		const_twa_graph_ptr	neg_aut = nullptr
	)

Determinize a TBA and make sure it is correct.

Apply tba_determinize(), then check that the result is equivalent. If it isn't, return the original automaton.

Only one of f or neg_aut needs to be supplied. If neg_aut is not given, it will be built from f.

Parameters

aut	the automaton to minimize
threshold_states	if non null, abort the construction whenever it would build an automaton that is more than threshold time bigger (in term of states) than the original automaton.
threshold_cycles	can be used to abort the construction if the number of cycles in a SCC of the constructed automaton is bigger than the supplied value.
f	the formula represented by the original automaton
neg_aut	an automaton representing the negation of aut

Returns

a new tgba if the automaton could be determinized, aut if the automaton cannot be determinized, 0 if we do not know if the determinization is correct because neither f nor neg_aut were supplied.

Variable Documentation

default_unabbrev_string

constexpr const char* spot::default_unabbrev_string = "eFGiMW^"

constexpr

Default string of operators to unabbreviate.