spot Namespace Reference

Classes
class	digraph
	A directed graph. More...
class	named_graph
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 check if the iterator has the good 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
class	kripke_graph
	Kripke Structure. More...
class	ltsmin_model
struct	transition_info
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 menipulated transparently whatever the input format considered. 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 wether the state will be compressed or not. This class aims to simplify this management. More...
struct	inner_callback_parameters
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 >
class	iterable_uf
class	swarmed_bloemen
	This class implements the SCC decomposition algorithm of bloemen as described in PPOPP'16. It uses a shared union-find augmented to manage work stealing between threads. More...
class	iterable_uf_ec
class	swarmed_bloemen_ec
	This class implements the SCC decomposition algorithm of bloemen as described in PPOPP'16. It uses a shared union-find augmented to manage work stealing between threads. More...
class	swarmed_cndfs
class	swarmed_deadlock
	This class aims to explore a model to detect wether it contains a deadlock. This deadlock detection performs a DFS traversal sharing information shared among multiple threads. If Deadlock equals std::true_type performs dealock 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	is_a_mc_algorithm
	This class allows to ensure (at compile time) if a given parameter can be compsidered as a modelchecking algorithm (i.e., usable by instanciate) 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 optimisations (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
class	bitvect
	A bit vector. More...
class	bitvect_array
struct	parse_error
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
class	printable_value
class	printable_id
	The default callback simply writes "%c". More...
class	printable_percent
	Called by default for "%%" and "%\0". More...
class	formater
struct	ptr_hash
	A hash function for pointers. More...
struct	identity_hash
	A hash function that returns identity. More...
struct	pair_hash
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
struct	parsed_aut
	Result of the automaton parser. More...
struct	automaton_parser_options
class	automaton_stream_parser
	Parse a stream of automata. More...
class	ta
	A Testing Automaton. More...
class	ta_succ_iterator
	Iterate over the successors of a state. More...
class	scc_stack_ta
class	ta_explicit
class	state_ta_explicit
class	ta_explicit_succ_iterator
	Successor iterators used by spot::ta_explicit. More...
class	state_ta_product
	A state for spot::ta_product. More...
class	ta_succ_iterator_product
	Iterate over the successors of a product computed on the fly. More...
class	ta_product
	A lazy product between a Testing automaton and a Kripke structure. (States are computed on the fly.) More...
class	ta_succ_iterator_product_by_changeset
class	tgta
	A Transition-based Generalized Testing Automaton (TGTA). More...
class	tgta_explicit
class	tgta_product
	A lazy product. (States are computed on the fly.) More...
class	tgta_succ_iterator_product
	Iterate over the successors of a product computed on the fly. More...
class	ta_check
	Check whether the language of a product (spot::ta_product) between a Kripke structure and a TA is empty. It works also for the product using Generalized TA (GTA and SGTA). More...
class	ta_reachable_iterator
	Iterate over all reachable states of a spot::ta. More...
class	ta_reachable_iterator_depth_first
	An implementation of spot::ta_reachable_iterator that browses states depth first. More...
class	ta_reachable_iterator_breadth_first
	An implementation of spot::ta_reachable_iterator that browses states breadth first. More...
struct	ta_statistics
class	language_containment_checker
	Check containment between LTL formulae. More...
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
class	fnode
	Actual storage for formula nodes. More...
struct	formula_ptr_less_than_bool_first
class	formula
	Main class for temporal logic formula. More...
class	mark_tools
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 formulae. More...
class	random_boolean
	Generate random Boolean formulae. More...
class	random_sere
	Generate random SERE. More...
class	random_psl
	Generate random PSL formulae. More...
class	randltlgenerator
class	tl_simplifier_options
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
class	bdd_dict
	Map BDD variables to formulae. 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
	Set of states deriving from spot::state. More...
class	taa_succ_iterator
class	taa_tgba_labelled
class	taa_tgba_string
class	taa_tgba_formula
class	state
	Abstract class for states. More...
struct	state_ptr_less_than
	Strict Weak Ordering for state*. More...
struct	state_ptr_equal
	An Equivalence Relation for state*. More...
struct	state_ptr_hash
	Hash Function for state*. 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 (shared_ptr<const state*>). More...
struct	state_shared_ptr_equal
	An Equivalence Relation for shared_state (shared_ptr<const state*>). More...
struct	state_shared_ptr_hash
	Hash Function for shared_state (shared_ptr<const 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 spot::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	isomorphism_checker
	Check if two automata are isomorphic. 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
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
	Compute a counter example from a spot::couvreur99_check_status. More...
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
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...
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
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
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	twa_statistics
struct	twa_sub_statistics
class	printable_formula
class	printable_acc_cond
class	printable_scc_info
class	printable_size
class	printable_long_size
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	to_parity_data
struct	to_parity_options
	Options to control various optimizations of to_parity(). More...
class	translator
	Translate an LTL formula into an optimized spot::tgba. 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
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
typedef struct spot::transition_info	transition_info_t
typedef void(*	TransitionCB) (void *ctx, transition_info_t *transition_info, int *dst)
using	spins_interface_ptr = std::shared_ptr< const spins_interface >
typedef int *	cspins_state
	A Spins state is represented as an array of integer Note that this array has two reserved slots (position 0 an 1). More...
typedef std::shared_ptr< spot::kripkecube< spot::cspins_state, spot::cspins_iterator > >	ltsmin_kripkecube_ptr
	shortcut to manipulate the kripke below 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
typedef std::shared_ptr< const parsed_aut >	const_parsed_aut_ptr
typedef std::shared_ptr< ta >	ta_ptr
typedef std::shared_ptr< const ta >	const_ta_ptr
typedef std::shared_ptr< ta_explicit >	ta_explicit_ptr
typedef std::shared_ptr< const ta_explicit >	const_ta_explicit_ptr
typedef std::shared_ptr< ta_product >	ta_product_ptr
typedef std::shared_ptr< const ta_product >	const_ta_product_ptr
typedef std::shared_ptr< tgta >	tgta_ptr
typedef std::shared_ptr< const tgta >	const_tgta_ptr
typedef std::shared_ptr< tgta_explicit >	tgta_explicit_ptr
typedef std::shared_ptr< const tgta_explicit >	const_tgta_explicit_ptr
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
typedef std::unordered_map< formula, formula >	snf_cache
typedef std::shared_ptr< bdd_dict >	bdd_dict_ptr
typedef std::shared_ptr< twa >	twa_ptr
typedef std::shared_ptr< const twa >	const_twa_ptr
typedef std::shared_ptr< const twa_graph >	const_twa_graph_ptr
typedef std::shared_ptr< twa_graph >	twa_graph_ptr
typedef std::shared_ptr< const twa_product >	const_twa_product_ptr
typedef std::shared_ptr< twa_product >	twa_product_ptr
typedef std::shared_ptr< taa_tgba_string >	taa_tgba_string_ptr
typedef std::shared_ptr< const taa_tgba_string >	const_taa_tgba_string_ptr
typedef std::shared_ptr< taa_tgba_formula >	taa_tgba_formula_ptr
typedef std::shared_ptr< const taa_tgba_formula >	const_taa_tgba_formula_ptr
typedef std::shared_ptr< twa_run >	twa_run_ptr
typedef std::shared_ptr< twa_word >	twa_word_ptr
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
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
typedef std::shared_ptr< const aig >	const_aig_ptr
typedef std::vector< struct nca_st_info * >	vect_nca_info
typedef std::shared_ptr< const twa_run >	const_twa_run_ptr
typedef std::shared_ptr< emptiness_check_result >	emptiness_check_result_ptr
typedef std::shared_ptr< emptiness_check >	emptiness_check_ptr
typedef std::shared_ptr< emptiness_check_instantiator >	emptiness_check_instantiator_ptr
typedef std::vector< bool >	region_t
typedef std::vector< unsigned >	strategy_t
typedef std::vector< std::pair< unsigned, unsigned > >	product_states
	Automata constructed by product() contain a property named "product-states" with this type. 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

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 }
enum class	pool_type { Safe , Unsafe }
enum class	parsed_aut_type {   HOA , NeverClaim , LBTT , DRA ,   DSA , PGAME , Unknown }
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 }
	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 }
enum	relabeling_style { Abc , Pnn }
enum class	scc_info_options {   NONE = 0 , STOP_ON_ACC = 1 , TRACK_STATES = 2 , TRACK_SUCCS = 4 ,   TRACK_STATES_IF_FIN_USED = 8 , 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 }
	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)
std::ostream &	operator<< (std::ostream &os, const mc_algorithm &ma)
std::ostream &	operator<< (std::ostream &os, const mc_rvalue &mr)
std::ostream &	operator<< (std::ostream &os, const ec_stats &es)
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
int	memusage ()
	Total number of pages in use by the program. More...
const char *	version ()
	Return Spot's version. More...
void	hoayyreset (void *scanner)
int	hoayyopen (const std::string &name, void **scanner)
int	hoayyopen (int fd, void **scanner)
int	hoayystring (const char *data, void **scanner)
void	hoayyclose (void *scanner)
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...
ta_explicit_ptr	make_ta_explicit (const const_twa_ptr &tgba, unsigned n_acc, state_ta_explicit *artificial_initial_state=nullptr)
ta_product_ptr	product (const const_ta_ptr &testing_automaton, const const_kripke_ptr &kripke_structure)
tgta_explicit_ptr	make_tgta_explicit (const const_twa_ptr &tgba, unsigned n_acc, state_ta_explicit *artificial_initial_state=nullptr)
twa_ptr	product (const const_kripke_ptr &left, const const_tgta_ptr &right)
std::ostream &	print_dot (std::ostream &os, const const_ta_ptr &a, const char *opt=nullptr)
ta_explicit_ptr	minimize_ta (const const_ta_ptr &ta_)
	Construct a simplified TA by merging bisimilar states. More...
tgta_explicit_ptr	minimize_tgta (const const_tgta_explicit_ptr &tgta_)
	Construct a simplified TGTA by merging bisimilar states. More...
std::set< const state * >	get_states_set (const const_ta_ptr &t)
	Compute states set for an automaton. More...
ta_statistics	stats_reachable (const const_ta_ptr &t)
	Compute statistics for an automaton. More...
ta_explicit_ptr	tgba_to_ta (const const_twa_ptr &tgba_to_convert, bdd atomic_propositions_set, bool degeneralized=true, bool artificial_initial_state_mode=true, bool single_pass_emptiness_check=false, bool artificial_livelock_state_mode=false, bool no_livelock=false)
	Build a spot::ta_explicit* (TA) from an LTL formula. More...
tgta_explicit_ptr	tgba_to_tgta (const const_twa_ptr &tgba_to_convert, bdd atomic_propositions_set)
	Build a spot::tgta_explicit* (TGTA) from an LTL formula. More...
atomic_prop_set	create_atomic_prop_set (unsigned n)
	construct an atomic_prop_set with n propositions 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...
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 has the recurrence 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 formulae. More...
formula	from_ltlf (formula f, const char *alive="alive")
	Convert an LTLf into an LTL formula. More...
std::vector< formula >	mutate (formula f, unsigned opts=Mut_All, unsigned max_output=-1U, unsigned mutation_count=1, bool sort=true)
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 formulae). 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 formulae). 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	relabel_bse (formula f, relabeling_style style, relabeling_map *m=nullptr)
	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	remove_x (formula f)
	Rewrite a stutter-insensitive formula f without using the X operator. 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...
bdd_dict_ptr	make_bdd_dict ()
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...
formula	bdd_to_formula (bdd f, const bdd_dict_ptr d)
	Convert a BDD into a formula. More...
taa_tgba_string_ptr	make_taa_tgba_string (const bdd_dict_ptr &dict)
taa_tgba_formula_ptr	make_taa_tgba_formula (const bdd_dict_ptr &dict)
void	shared_state_deleter (state *s)
void	prop_copy (const const_twa_ptr &other, prop_set p)
	Copy the properties of another automaton. More...
void	prop_keep (prop_set p)
	Keep only a subset of properties of the current automaton. More...
void	prop_reset ()
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)
	Encode and print an automaton as an AIGER circuit. 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	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	dtwa_complement (const const_twa_graph_ptr &aut)
	Complement a deterministic TωA. 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...
twa_graph_ptr	copy (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...
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	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)
acc_cond::mark_t	is_partially_degeneralizable (const const_twa_graph_ptr &aut, bool allow_inf=true, bool allow_fin=true, std::vector< acc_cond::mark_t > forbid={})
	Is the automaton partially degeneralizable? 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)
twa_graph_ptr	dtba_sat_synthetize (const const_twa_graph_ptr &a, int target_state_number, bool state_based=false)
	Attempt to synthetize 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 synthetize 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...
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)
	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_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_twa_graph_ptr arena, unsigned state)
	Get the winner of a state. More...
const region_t &	get_state_winners (const const_twa_graph_ptr &arena)
	Get the winner of all states. 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...
emptiness_check_ptr	couvreur99 (const const_twa_ptr &a, option_map options=option_map())
	Check whether the language of an automate 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, std::vector< std::pair< std::string, bdd >> aliases)
	Define all aliases used in the HOA format. 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)
unsigned	count_univbranch_edges (const const_twa_graph_ptr &aut)
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 state 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)
	Build a spot::twa_graph_ptr from an LTL or PSL formula. 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)
template<typename Trans >
void	transform_copy (const const_twa_graph_ptr &old, twa_graph_ptr &cpy, Trans trans)
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...
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	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	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)
	Minimize an automaton if it represents an obligation property. More...
bool	minimize_obligation_garanteed_to_work (const const_twa_graph_ptr &aut_f, formula f=nullptr)
	Whether calling minimize_obligation is sure to work. 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)
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 sets 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...
bool	rabin_is_buchi_realizable (const const_twa_graph_ptr &aut)
	Check if aut is Rablin-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)
	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)
scc_info_options	operator& (scc_info_options left, scc_info_options right)
scc_info_options	operator| (scc_info_options left, scc_info_options right)
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 disjoints. 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)
twa_graph_ptr	simulation_sba (const const_twa_graph_ptr &automaton, int trans_pruning=-1)
twa_graph_ptr	split_edges (const const_twa_graph_ptr &aut)
	transform edges into transitions 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 transtitions, even unreachable ones. More...
bool	is_terminal_automaton (const const_twa_graph_ptr &aut, scc_info *sm=nullptr, bool ignore_trivial_scc=false)
	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_strength (const const_twa_graph_ptr &aut, const char *keep)
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)
	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)
	Like split_2step but relying on the named property 'synthesis-outputs'. 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...
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...
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...
	SPOT_DEPRECATED ("use to_parity() instead") twa_graph_ptr iar(const const_twa_graph_ptr &aut
	Turn a Rabin-like or Streett-like automaton into a parity automaton based on the index appearence record (IAR) More...
	SPOT_DEPRECATED ("use to_parity() and spot::acc_cond::is_rabin_like() instead") twa_graph_ptr iar_maybe(const const_twa_graph_ptr &aut
	Turn a Rabin-like or Streett-like automaton into a parity automaton based on the index appearence record (IAR) 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)
zielonka_tree_options	operator& (zielonka_tree_options left, zielonka_tree_options right)
zielonka_tree_options	operator| (zielonka_tree_options left, zielonka_tree_options right)
zielonka_tree_options	operator- (zielonka_tree_options left, zielonka_tree_options right)
twa_graph_ptr	zielonka_tree_transform (const const_twa_graph_ptr &aut)
	Paritize an automaton using Zielonka tree. More...
bool	operator! (acd_options me)
acd_options	operator& (acd_options left, acd_options right)
acd_options	operator| (acd_options left, acd_options right)
acd_options	operator- (acd_options left, acd_options right)
twacube_ptr	make_twacube (const std::vector< std::string > aps)
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 bdd using the map that bind 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 fill the binder, i.e. the mapping between BDD indexes to 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 wether a twacube and a twa are equivalent. More...
bool	is_bare_word (const char *str)
	Whether a word is bare. More...
std::string	quote_unless_bare_word (const std::string &str)
	Double-quote words that are not bare. 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)
constexpr bool	operator!= (trival a, trival b)
constexpr trival	operator&& (trival a, trival b)
constexpr trival	operator&& (bool a, trival b)
constexpr trival	operator&& (trival a, bool b)
constexpr trival	operator|| (trival a, trival b)
constexpr trival	operator|| (bool a, trival b)
constexpr trival	operator|| (trival a, bool b)
std::ostream &	operator<< (std::ostream &os, trival v)
std::ostream &	operator<< (std::ostream &os, const acc_cond &acc)
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...
aig_ptr	mealy_machine_to_aig (const const_twa_graph_ptr &m, const char *mode)
	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)
	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)
	Convert a mealy (like) machine into an aig relying on the transformation described by mode. 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)
	Convert a mealy (like) machine 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)
	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)
	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)
	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)
	Convert multiple mealy machines into an aig relying on the transformation described by mode. 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...
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...
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 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...
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...
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)
	Close the automaton by allowing letters to be duplicated. More...
twa_graph_ptr	sl2 (const_twa_graph_ptr aut)
	Close the automaton by allowing letters to be duplicated. More...
twa_graph_ptr	closure_inplace (twa_graph_ptr aut)
	Close the automaton by allowing duplicate letter removal. More...
twa_graph_ptr	closure (const_twa_graph_ptr aut)
	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)
	Determinate the states that are stutter-invariant in pos. More...
std::vector< bool >	stutter_invariant_states (const_twa_graph_ptr pos, formula f_pos)
	Determinate 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)
	Determinate the letters with which each state is stutter-invariant. More...
std::vector< bdd >	stutter_invariant_letters (const_twa_graph_ptr pos, formula f_pos)
	Determinate the letters with which each state is stutter-invariant. More...
twa_graph_ptr	ltl_to_game (const formula &f, const std::vector< std::string > &all_outs, synthesis_info &gi)
	Creates a game from a specification and a set of output propositions. More...
twa_graph_ptr	ltl_to_game (const formula &f, const std::vector< std::string > &all_outs)
	Creates a game from a specification and a set of output propositions. More...
twa_graph_ptr	ltl_to_game (const std::string &f, const std::vector< std::string > &all_outs, synthesis_info &gi)
	Creates a game from a specification and a set of output propositions. More...
twa_graph_ptr	ltl_to_game (const std::string &f, const std::vector< std::string > &all_outs)
	Creates a game from a specification and a set of output propositions. 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_independant_formulas (formula f, const std::vector< std::string > &outs)
	Seeks to decompose a formula into independently synthesizable sub-parts. The conjunction of all sub-parts then satisfies the specification. More...
std::pair< std::vector< formula >, std::vector< std::set< formula > > >	split_independant_formulas (const std::string &f, const std::vector< std::string > &outs)
	Seeks to decompose a formula into independently synthesizable 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^"
bool	pretty_print = false)
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

cspins_state

typedef int* spot::cspins_state

A Spins state is represented as an array of integer Note that this array has two reserved slots (position 0 an 1).

At position 0 we store the hash associated to the state to avoid multiple computations.

At position 1 we store the size of the state: keeping this information allows to compress the state

cube

using spot::cube = typedef unsigned*

A cube is only a set of bits in memory.

This set can be seen as two bitsets

• true_var : a bitset representing variables that are set to true
• false_var : a bitset representing variables that are set to false

In the two vectors a bit set to 1 represent a variable set to true (resp. false) for the true_var (resp. false_var)

Warning : a variable cannot be set in both bitset at the same time (consistency! cannot be true and false)

The cube for (a & !b) will be repensented by :

• true_var = 1 0
• false_var = 0 1

To represent free variables such as in (a & !b) | (a & b) (wich is equivalent to (a) with b free)

• true_var : 1 0
• false_var : 0 0 This exemple shows that the representation of free variables is done by unsetting variable in both vector

To be memory efficient, these two bitsets are contigous in memory i.e. if we want to represent 35 variables, a cube will be represented by 4 unsigned int contiguous in memory. The 35 first bits represent truth values. The 29 bits following are useless. Then, the 35 bits represents false value and the rest is useless.

Note that useless bits are only to perform some action efficiently, i.e. only by ignoring them. The manipulation of cubes must be done using the cubeset class

ltsmin_kripkecube_ptr

typedef std::shared_ptr<spot::kripkecube<spot::cspins_state, spot::cspins_iterator> > spot::ltsmin_kripkecube_ptr

shortcut to manipulate the kripke below

process_timer

typedef struct spot::process_timer spot::process_timer

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

product_states

typedef std::vector<std::pair<unsigned, unsigned> > spot::product_states

Automata constructed by product() contain a property named "product-states" with this type.

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.

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 wether 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

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

A 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 usefull in a multithreaded environnement with multiple fixed_sized_pool allocating the same ressource. In this case it's hard to detect wich pool has allocated some ressource.

Function Documentation

are_equivalent()

bool spot::are_equivalent	(	const spot::twacube_ptr	twacube,
		const spot::const_twa_graph_ptr	twa
	)

Check wether a twacube and a twa are equivalent.

atomic_prop_cmp()

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

Order two atomic propositions.

bdd_format_accset()

std::string spot::bdd_format_accset	(	const bdd_dict_ptr &	dict,
		bdd	b
	)

Format a BDD as a set of acceptance conditions.

This is used when saving a TGBA.

Parameters

dict	The dictionary to use, to lookup variables.
b	The BDD to print.

Returns

The BDD formated as a string.

bdd_format_formula()

std::string spot::bdd_format_formula	(	const bdd_dict_ptr &	dict,
		bdd	b
	)

Format a BDD as a formula.

Parameters

dict	The dictionary to use, to lookup variables.
b	The BDD to print.

Returns

The BDD formated as a string.

bdd_format_isop()

std::string spot::bdd_format_isop	(	const bdd_dict_ptr &	dict,
		bdd	b
	)

Format a BDD as an irredundant sum of product.

Parameters

dict	The dictionary to use, to lookup variables.
b	The BDD to print.

Returns

The BDD formated as a string.

bdd_format_sat()

std::string spot::bdd_format_sat	(	const bdd_dict_ptr &	dict,
		bdd	b
	)

Format a BDD as a list of literals.

This assumes that b is a conjunction of literals.

Parameters

dict	The dictionary to use, to lookup variables.
b	The BDD to print.

Returns

The BDD formated as a string.

bdd_format_set()

std::string spot::bdd_format_set	(	const bdd_dict_ptr &	dict,
		bdd	b
	)

Format a BDD as a set.

Parameters

dict	The dictionary to use, to lookup variables.
b	The BDD to print.

Returns

The BDD formated as a string.

bdd_print_accset()

std::ostream& spot::bdd_print_accset	(	std::ostream &	os,
		const bdd_dict_ptr &	dict,
		bdd	b
	)

Print a BDD as a set of acceptance conditions.

This is used when saving a TGBA.

Parameters

os	The output stream.
dict	The dictionary to use, to lookup variables.
b	The BDD to print.

Returns

The BDD formated as a string.

bdd_print_formula()

std::ostream& spot::bdd_print_formula	(	std::ostream &	os,
		const bdd_dict_ptr &	dict,
		bdd	b
	)

Print a BDD as a formula.

Parameters

os	The output stream.
dict	The dictionary to use, to lookup variables.
b	The BDD to print.

bdd_print_isop()

std::ostream& spot::bdd_print_isop	(	std::ostream &	os,
		const bdd_dict_ptr &	dict,
		bdd	b
	)

Print a BDD as an irredundant sum of product.

Parameters

os	The output stream.
dict	The dictionary to use, to lookup variables.
b	The BDD to print.

bdd_print_sat()

std::ostream& spot::bdd_print_sat	(	std::ostream &	os,
		const bdd_dict_ptr &	dict,
		bdd	b
	)

Print a BDD as a list of literals.

This assumes that b is a conjunction of literals.

Parameters

os	The output stream.
dict	The dictionary to use, to lookup variables.
b	The BDD to print.

bdd_print_set()

std::ostream& spot::bdd_print_set	(	std::ostream &	os,
		const bdd_dict_ptr &	dict,
		bdd	b
	)

Print a BDD as a set.

Parameters

os	The output stream.
dict	The dictionary to use, to lookup variables.
b	The BDD to print.

bdd_to_formula()

formula spot::bdd_to_formula	(	bdd	f,
		const bdd_dict_ptr	d
	)

Convert a BDD into a formula.

Format the BDD as an irredundant sum of product (see the minato_isop class for details) and map the BDD variables back into their atomic propositions. This works only for Boolean formulas, and all the BDD variables used in f should have been registered in d. Although the result has type formula, it obviously does not use any temporal operator.

check_determinism()

void spot::check_determinism

(

twa_graph_ptr

aut

)

Set the deterministic and semi-deterministic properties appropriately.

check_strength()

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

Check whether an automaton is weak or terminal.

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

Parameters

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

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

complement()

twa_graph_ptr spot::complement	(	const const_twa_graph_ptr &	aut,
		const output_aborter *	aborter = nullptr
	)

Complement a TωA.

This employs different complementation strategies depending on the type of the automaton.

If the input is alternating, the output may be alternating and is simply the result of calling dualize().

If the input is not alternating, the output will not be alternating, but could have any acceptance condition.

• deterministic inputs are passed to dualize()
• very weak automata are also dualized, and then passed to remove_alternation() to obtain a TGBA
• any other type of input is determized before complementation.

If an output_aborter is supplied, it is used to abort the construction of larger automata.

complement_semidet() is not yet used.

complement_semidet()

twa_graph_ptr spot::complement_semidet	(	const const_twa_graph_ptr &	aut,
		bool	show_names = false
	)

Complement a semideterministic TωA.

The automaton aut should be semideterministic.

Uses the NCSB algorithm described by F. Blahoudek, et al. [4]

complete()

twa_graph_ptr spot::complete

(

const const_twa_ptr &

aut

)

Clone a twa and complete it.

If the TωA is incomplete and has an acceptance condition that is a tautology, it will be changed into a Büchi automaton.

complete_here()

void spot::complete_here

(

twa_graph_ptr

aut

)

Complete a twa_graph in place.

If the TωA is incomplete and has an acceptance condition that is a tautology, it will be changed into a Büchi automaton.

compsusp()

twa_graph_ptr spot::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.

Described in "Compositional Approach to Suspension and Other Improvements to LTL Translation", Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír Křetínský, Jan Strejček (SPIN'13).

If no_wdba or no_simulation is true, the corresponding operation is not performed on the skeleton automaton. If early_susp is true, then composition starts on the transition that enters the accepting SCC, not just in the SCC itself. If no_susp_product is true, then the composition is not performed and the skeleton automaton is returned for debugging. If wdba_smaller is true, then the WDBA-minimization of the skeleton is used only if it produces a smaller automaton.

Finally the oblig flag is a work in progress and should not be set to true.

This interface is subject to change, and clients aiming for long-term stability should better use the services of the spot::translator class instead.

couvreur99_new_check()

emptiness_check_result_ptr spot::couvreur99_new_check

(

const const_twa_ptr &

a

)

A shortcut to run the optimized emptiness check directly.

This is the same as get_couvreur99_new(a, {})->check().

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.

cube_to_bdd()

bdd spot::cube_to_bdd	(	spot::cube	cube,
		const cubeset &	cubeset,
		std::unordered_map< int, int > &	reverse_binder
	)

Transform a cube cube into bdd using the map that bind cube indexes to bdd indexes.

decompose_scc() [1/3]

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

Extract a sub-automaton of a given strength.

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

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

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

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

Parameters

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

decompose_scc() [2/3]

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

Extract a sub-automaton of a given strength.

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

decompose_scc() [3/3]

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

Extract a sub-automaton above an SCC.

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

Parameters

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

dnf_to_dca()

twa_graph_ptr spot::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.

This function calls first nra_to_nca() in order to retrieve som information and then runs a breakpoint construction. The algorithm is described in section 4 of [5] .

aut The automaton to convert. named_states name each state for easier debugging.

dnf_to_nca()

twa_graph_ptr spot::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.

This function converts the Rabin-like automaton into a Strett-like automaton and then calls nsa_to_nca() on it. It is described in section 3.2 of [5] .

aut The automaton to convert. named_states name each state for easier debugging. nca_info retrieve information about state visited infinitely often.

dtba_sat_minimize()

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

Attempt to minimize a deterministic TBA with a SAT solver.

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

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

dtba_sat_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 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 time 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.

dtba_sat_synthetize()

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

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

Parameters

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

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

dtwa_complement()

twa_graph_ptr spot::dtwa_complement

(

const const_twa_graph_ptr &

aut

)

Complement a deterministic TωA.

The automaton aut should be deterministic. It will be completed if it isn't already. In these conditions, complementing the automaton can be done by just complementing the acceptance condition.

In particular, this implies that an input that use generalized Büchi will be output as generalized co-Büchi.

Functions like to_generalized_buchi() or remove_fin() are frequently called after dtwa_complement() to obtain an easier acceptance condition (maybe at the cost of losing determinism.)

This function was deprecated in spot 2.4. Call the function spot::dualize() instead, that is able to complement any input automaton, not only deterministic ones.

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 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_synthetisze() and obtains a first minimized automaton. Then, incrementally, it encodes and solves the deletion of one state as many time 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.

dtwa_sat_synthetize()

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

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

Parameters

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

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

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.

enable_utf8()

void spot::enable_utf8

(

)

Enable UTF-8 output for bdd printers.

extract_aps()

std::vector<std::string>* spot::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 fill the binder, i.e. the mapping between BDD indexes to cube indexes.

formula_to_bdd() [1/2]

template<typename T >

bdd spot::formula_to_bdd	(	formula	f,
		const bdd_dict_ptr &	d,
		const std::shared_ptr< T > &	for_me
	)

Convert a Boolean formula into a BDD.

Convert the Boolean formula f into a BDD, using existing variables from d, and registering new ones as necessary. for_me, the address of the user of these BDD variables will be passed to d when registering the variables.

If you only use the BDD representation temporarily, for instance passing it right away to bdd_to_formula(), you should not forget to unregister the variables that have been registered for for_me. See bdd_dict::unregister_all_my_variables().

References formula_to_bdd().

formula_to_bdd() [2/2]

bdd spot::formula_to_bdd	(	formula	f,
		const bdd_dict_ptr &	d,
		void *	for_me
	)

Convert a Boolean formula into a BDD.

Convert the Boolean formula f into a BDD, using existing variables from d, and registering new ones as necessary. for_me, the address of the user of these BDD variables will be passed to d when registering the variables.

If you only use the BDD representation temporarily, for instance passing it right away to bdd_to_formula(), you should not forget to unregister the variables that have been registered for for_me. See bdd_dict::unregister_all_my_variables().

Referenced by formula_to_bdd().

get_couvreur99_new()

emptiness_check_ptr spot::get_couvreur99_new	(	const const_twa_ptr &	a,
		option_map	o
	)

A rewritten version of the Couvreur emptiness check.

It is optimized to run on explicit automata (avoiding the memory allocations of the virtual, abstract interface. It also has specializations for weak and terminal automata.

get_couvreur99_new_abstract()

emptiness_check_ptr spot::get_couvreur99_new_abstract	(	const const_twa_ptr &	a,
		option_map	o
	)

Same as above, but always uses the abstract interface.

This function is provided to test the efficiency of specializing our algorithms for explicit automata. It uses the same optimizations for weak and terminal automata as the one above.

get_states_set()

std::set<const state*> spot::get_states_set

(

const const_ta_ptr &

t

)

Compute states set for an automaton.

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.

highlight_languages()

void spot::highlight_languages

(

twa_graph_ptr &

aut

)

Color state that recognize identical language.

State that recognize a unique language will not be colored.

highlight_semidet_sccs()

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

Highlight the deterministic part of the automaton.

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

Parameters

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

is_complete()

bool spot::is_complete

(

const const_twa_graph_ptr &

aut

)

Return true iff aut is complete.

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

is_inherently_weak_automaton()

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

Check whether an automaton is inherently weak.

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

Parameters

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

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

is_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_liveness_automaton()

bool spot::is_liveness_automaton

(

const const_twa_graph_ptr &

aut

)

Whether the automaton represents a liveness property.

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

is_partially_degeneralizable()

acc_cond::mark_t spot::is_partially_degeneralizable	(	const const_twa_graph_ptr &	aut,
		bool	allow_inf = true,
		bool	allow_fin = true,
		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.

is_safety_automaton()

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

Check whether an automaton is a safety automaton.

A safety automaton has only accepting SCCs (or trivial SCCs).

A minimized WDBA (as returned by a successful run of minimize_obligation()) represents safety property if it is a safety automaton.

Parameters

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

is_semi_deterministic()

bool spot::is_semi_deterministic

(

const const_twa_graph_ptr &

aut

)

Return true iff aut is semi-deterministic.

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

is_terminal_automaton()

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

Check whether an automaton is terminal.

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

If ignore_trivial_scc is set, accepting transitions from trivial SCCs are ignored.

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

Parameters

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

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

is_very_weak_automaton()

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

Check whether an automaton is very-weak.

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

Parameters

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

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

is_weak_automaton()

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

Check whether an automaton is weak.

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

Parameters

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

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

language_map()

std::vector<unsigned> spot::language_map

(

const const_twa_graph_ptr &

aut

)

Identify states that recognize the same language.

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

The given automaton must be deterministic.

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_twa_word() [1/2]

twa_word_ptr spot::make_twa_word ( const bdd_dict_ptr &  dict )

inline

Create an empty twa_word.

Note that empty twa_word are invalid and cannot be printed. After creating an empty twa_word, you should at least populate the cycle.

make_twa_word() [2/2]

twa_word_ptr spot::make_twa_word ( const twa_run_ptr &  run )

inline

Create a twa_word from a twa_run.

mask_acc_sets()

twa_graph_ptr spot::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.

mask_keep_accessible_states()

twa_graph_ptr spot::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.

Each index in the vector to_keep specifies wether or not to keep the transition that exit this state. The initial state will be set to init. Only states that are accessible from init via states in to_keep will be preserved.

If drop_univ_branches branch is set, universal branching is replaced by existential branching during the copy.

See also

mask_keep_states

mask_keep_states()

twa_graph_ptr spot::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.

Each index in the vector to_keep specifies wether or not to keep the transition that exit this state. The initial state will be set to init.

Note that the number of states in the result automaton is the same as in the input: only transitions have been removed.

See also

mask_keep_accessible_states

memusage()

int spot::memusage

(

)

Total number of pages in use by the program.

Returns

The total number of pages in use by the program if known. -1 otherwise.

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.

nsa_to_dca()

twa_graph_ptr spot::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.

This function calls first nsa_to_nca() in order to retrieve som information and then runs a breakpoint construction. The algorithm is described in section 4 of [5] .

aut The automaton to convert. named_states name each state for easier debugging.

nsa_to_nca()

twa_graph_ptr spot::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.

This function works in top of the augmented subset construction algorithm and is described in section 3.1 of [5] .

This implementation is quite different from the described algorithm. It is made to work with automaton with Street-like acceptance (including Büchi).

aut The automaton to convert. named_states name each state for easier debugging. nca_info retrieve information about state visited infinitely often.

operator<<() [1/2]

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

Print a formula.

operator<<() [2/2]

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

inline

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

operator|()

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.

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

parse_word()

twa_word_ptr spot::parse_word	(	const std::string &	word,
		const bdd_dict_ptr &	dict
	)

Parse a twa_word.

The input should have the form

BF;BF;...;BF;cycle{BF;BF;...;BF}

where BF can be any Boolean formula, and the prefix sequence (before cycle{...}) may be empty.

Parameters

word	the string to parse
dict	the bdd_dict where atomic propositions should be registered

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.

prop_copy()

void spot::prop_copy	(	const const_twa_ptr &	other,
		prop_set	p
	)

Copy the properties of another automaton.

Copy the property specified with p from other to the current automaton.

There is no default value for p on purpose. This way any time we add a new property we have to update every call to prop_copy().

See also

prop_set

prop_keep()

void spot::prop_keep

(

prop_set

p

)

Keep only a subset of properties of the current automaton.

All properties part of a group set to false in p are reset to their default value of trival::maybe().

random_acceptance()

acc_cond::acc_code spot::random_acceptance

(

unsigned

n_accs

)

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

randomize()

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

Randomize a TGBA.

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

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

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. [7]

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 transition could have been colored with the maximal color, since any cycle going through them would have seen the maximal color. (Once your remove this maximal layer, your can define the next layer similarly.)

When layered is true all transition that belong to the same layer receive the same color. When layer is false, only the transition that where used initially to define the layers (i.e, the transition with the maximal color in the previous exemple), get their color adjusted. The other 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 preserve the kind (min/max) of parity input, while acd_transform() always output 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 where 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. [7]

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 transition could have been colored with the maximal color, since any cycle going through them would have seen the maximal color. (Once your remove this maximal layer, your can define the next layer similarly.)

When layered is true all transition that belong to the same layer receive the same color. When layer is false, only the transition that where used initially to define the layers (i.e, the transition with the maximal color in the previous exemple), get their color adjusted. The other 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 preserve the kind (min/max) of parity input, while acd_transform() always output 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 where none occasionally help with simulation-based reductions.

relabel_here()

void spot::relabel_here	(	twa_graph_ptr &	aut,
		relabeling_map *	relmap
	)

replace atomic propositions in an automaton

The relabeling map relmap should have keys that are atomic propositions, and values that are Boolean formulas.

This function is typically used with maps produced by relabel() or relabel_bse().

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 // synthetize 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"

satone_to_cube()

spot::cube spot::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.

scc_filter()

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

Prune unaccepting SCCs and remove superfluous acceptance conditions.

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

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

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

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

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

Warning

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

scc_filter_states()

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

Prune unaccepting SCCs.

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

scc_filter_susp()

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

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

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

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

semidet_sccs()

std::vector<bool> spot::semidet_sccs

(

scc_info &

si

)

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

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 [15] 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.

to_dca()

twa_graph_ptr spot::to_dca	(	const_twa_graph_ptr	aut,
		bool	named_states = false
	)

Converts any ω-automata to deterministic co-buchi.

The language of the resulting automaton always include the original language, and is a superset iff the original language can not be expressed using a co-Büchi acceptance condition.

The implementation dispatches between dnf_to_dca, nsa_to_dca, degeneralize(), and a trivial implementation for deterministic weak automata.

to_finite()

twa_graph_ptr spot::to_finite	(	const_twa_graph_ptr	aut,
		const char *	alive = "alive"
	)

Interpret the "live" part of an automaton as finite automaton.

This functions assumes that there is a property "alive" is that either true or false on all transitions, and that can only switch from true to false.

Because Spot does not support finite automata, this creates a state-based Büchi automaton where any states with a !alive outgoing transition in the original automaton is accepting, and all alive/!alive occurrences are removed.

to_nca()

twa_graph_ptr spot::to_nca	(	const_twa_graph_ptr	aut,
		bool	named_states = false
	)

Converts any ω-automata to non-deterministic co-buchi.

The language of the resulting automaton always include the original language, and is a superset iff the original language can not be expressed using a co-Büchi acceptance condition.

The implementation dispatches between dnf_to_nca(), nsa_to_nca(), degeneralize_tba(), and a trivial implementation for weak automata.

to_weak_alternating()

twa_graph_ptr spot::to_weak_alternating	(	const_twa_graph_ptr &	aut,
		bool	less = false
	)

Convert an alternating automaton to a weak alternating automaton.

 

The input automaton must have a generalized co-Büchi or Büchi acceptance condition. The automaton will be converted into a weak Büchi automaton. If the input automaton is already weak, it will simply be copied.

For details about the algorithm used, see the following papers: [33] , [35] .

Although at the end of the above paper there is a hint at an optimization that greatly reduces the number of transition in the resulting automaton, but in return makes the run of remove_alternation algorithm way slower. Hence, the optimization is disabled by default.

Parameters

aut	the automaton to convert to weak
less	whether to activate the optimization on the number of transitions or not, disabled by default

transform_accessible()

template<typename Trans >

void spot::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.

Copy the edges of automaton old into the empty automaton cpy, creating new states as needed. The argument trans should behave as a function with the following prototype: void (*trans) (unsigned src, bdd& cond, acc_cond::mark_t& acc, unsigned dst)

The trans function may modify either the condition or the acceptance sets of the edges. Set the condition to bddfalse to remove the edge (this will also remove the destination state and its descendants if they are not reachable by another edge).

The mapping between each state of the resulting automaton and the original state of the input automaton is stored in the "original-states" named property of the produced automaton. Call aut->get_named_prop<std::vector<unsigned>>("original-states") to retrieve it.

If drop_univ_branches branch is set, universal branching is replaced by existential branching during the copy.

Parameters

init	The optional new initial state.

transform_copy()

template<typename Trans >

void spot::transform_copy	(	const const_twa_graph_ptr &	old,
		twa_graph_ptr &	cpy,
		Trans	trans,
		unsigned int	init
	)

Copy an automaton and update each edge.

Copy the states of automaton old, into automaton cpy. Each state in cpy will have the same id as the ones in old. The argument trans should behave as a function with the following prototype: void (*trans) (unsigned srcbdd& cond, acc_cond::mark_t& acc, unsigned dst) It can modify either the condition or the acceptance sets of the edges. Set the condition to bddfalse to remove it. Note that all transtions will be processed.

Parameters

init	The optional new initial state.

twa_to_twacube()

twacube_ptr spot::twa_to_twacube

(

spot::const_twa_graph_ptr

aut

)

Convert a twa into a twacube.

twacube_to_twa()

spot::twa_graph_ptr spot::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.