Class List

Here are the classes, structs, unions and interfaces with brief descriptions:

[detail level 123]

Nspot
Cadjlist	A compact adjacency list representation for directed graphs
Csuccessor_iterator	Iterator for traversing successors of a state
Csuccessor_range	Range wrapper for successor iteration
Cdigraph	A directed graph
Cnamed_graph
Cfair_kripke_succ_iterator	Iterator code for a Fair Kripke structure
Cfair_kripke	Interface for a Fair Kripke structure
Ckripkecube	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
Cis_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
Ckripke_succ_iterator	Iterator code for Kripke structure
Ckripke	Interface for a Kripke structure
Ckripke_graph_state	Concrete class for kripke_graph states
Ckripke_graph_succ_iterator
Ckripke_graph	Kripke Structure
Cltsmin_model
Ctransition_info
Cspins_interface	Implementation of the PINS interface. This class is a wrapper that, given a file, will compile it w.r.t the PINS interface. The class can then be manipulated transparently whatever the input format considered
Ccspins_state_equal	This class provides the ability to compare two states
Ccspins_state_hash	This class provides the ability to hash a state
Ccspins_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
Cinner_callback_parameters
Ccspins_iterator	This class provides an iterator over the successors of a state. All successors are computed once when an iterator is recycled or created
Ccspins_iterator_param
Ckripkecube< cspins_state, cspins_iterator >
Citerable_uf
Cuf_element	Represents a Union-Find element
Cuf_element_hasher	The hasher for the previous uf_element.Shortcut to ease shared map manipulation
Cswarmed_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
Citerable_uf_ec
Cuf_element	Represents a Union-Find element
Cuf_element_hasher	The hasher for the previous uf_element.Shortcut to ease shared map manipulation
Cswarmed_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
Cswarmed_cndfs
Cswarmed_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 deadlock algorithm, otherwise perform a simple reachability
Clpar13	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
Cec_stats	This structure contains, for each thread, the collected information during the traversal
Cis_a_mc_algorithm	This class allows to ensure (at compile time) if a given parameter can be considered as a modelchecking algorithm (i.e., usable by instantiate)
Cint_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)
Ckripkecube_to_twa	Convert a (cube) model into a twa. Note that this algorithm cannot be run in parallel but could
Ctodo__element
Cproduct_to_twa	Convert a (cube) product automaton into a twa Note that this algorithm cannot be run in parallel
Cbdd_less_than	Comparison functor for BDDs
Cbdd_less_than_stable	Comparison functor for BDDs
Cbdd_hash	Hash functor for BDDs
Cbitset
Cbitvect	A bit vector
Cbitvect_array
Cparse_error
Cparallel_policy	This class is used to tell parallel algorithms what resources they may use
Cfixed_size_pool	A fixed-size memory pool implementation
Cprintable
Cprintable_value
Cprintable_id	The default callback simply writes "%c"
Cprintable_percent	Called by default for "%%" and "%\0"
Cformater
Cptr_hash	A hash function for pointers
Cidentity_hash	A hash function that returns identity
Cpair_hash
Cfnv	Struct for Fowler-Noll-Vo parameters
Cfnv< T, typename std::enable_if< sizeof(T)==4 >::type >	Fowler-Noll-Vo hash parameters for 32 bits
Cfnv< T, typename std::enable_if< sizeof(T)==8 >::type >	Fowler-Noll-Vo hash parameters for 64 bits
Cchar_ptr_less_than	Strict Weak Ordering for char*
Cminato_isop	Generate an irredundant sum-of-products (ISOP) form of a BDD function
Cmultiple_size_pool	A multiple-size memory pool implementation
Coption_map	Manage a map of options
Cbarand	Compute pseudo-random integer value between 0 and n included, following a binomial distribution with probability p
Csatsolver_command	Interface with a given sat solver
Csatsolver	Interface with a SAT solver
Cstopwatch	A simple stopwatch
Ctime_info	A structure to record elapsed time in clock ticks
Ctimer
Ctimer_map	A map of timer, where each timer has a name
Cprocess_timer	Struct used to start and stop both timer and stopwatch clocks
Ctemporary_file	Temporary file name
Copen_temporary_file	Open temporary file
Ctrival	A class implementing Kleene's three-valued logic
Choa_abort
Cparsed_aut	Result of the automaton parser
Cautomaton_parser_options
Cautomaton_stream_parser	Parse a stream of automata
Crealizability_simplifier_base	Simplify a reactive specification, preserving realizability
Crealizability_simplifier	Simplify a reactive specification, preserving realizability
Clanguage_containment_checker	Check containment between LTL formulae
Cdeclarative_environment	A declarative environment
Cdefault_environment	A laxist environment
Cenvironment	An environment that describes atomic propositions
Cexclusive_ap
Cfnode	Actual storage for formula nodes
Cformula_ptr_less_than_bool_first
Cformula	Main class for temporal logic formula
Cformula_child_iterator	Allow iterating over children
Cltlf_simplifier	Cheap simplification rules for LTLf formulas
Cltlf_one_step_sat_rewrite_with_cache
Cltlf_one_step_unsat_rewrite_with_cache
Cmark_tools
Cparsed_formula	The result of a formula parser
Crandom_formula	Base class for random formula generators
Cop_proba
Crandom_ltl	Generate random LTL formulas
Crandom_boolean	Generate random Boolean formulas
Crandom_sere	Generate random SERE
Crandom_psl	Generate random PSL formulas
Crandltlgenerator
Ctl_simplifier_options
Ctl_simplifier	Rewrite or simplify f in various ways
Cunabbreviator	Clone and rewrite a formula to remove specified operators logical operators
Cacc_cond	An acceptance condition
Cmark_t	An acceptance mark
Cacc_word	A "node" in an acceptance formulas
Cacc_code	An acceptance formula
Crs_pair	Rabin/streett pairs used by is_rabin_like and is_streett_like
Crs_pairs_view
Cbdd_dict	Map BDD variables to formulae
Cbdd_info
Cbdd_dict_preorder
Ctaa_tgba	A self-loop Transition-based Alternating Automaton (TAA) which is seen as a TGBA (abstract class, see below)
Ctransition	Explicit transitions
Cset_state	Set of states deriving from spot::state
Ctaa_succ_iterator
Ctaa_tgba_labelled
Ctaa_tgba_string
Ctaa_tgba_formula
Cstate	Abstract class for states
Cstate_ptr_less_than	Strict Weak Ordering for state*
Cstate_ptr_equal	An Equivalence Relation for state*
Cstate_ptr_hash	Hash Function for state*
Cstate_unicity_table	Render state pointers unique via a hash table
Cstate_shared_ptr_less_than	Strict Weak Ordering for shared_state (shared_ptr<const state*>)
Cstate_shared_ptr_equal	An Equivalence Relation for shared_state (shared_ptr<const state*>)
Cstate_shared_ptr_hash	Hash Function for shared_state (shared_ptr<const state*>)
Ctwa_succ_iterator	Iterate over the successors of a state
Ctwa	A Transition-based ω-Automaton
Cprop_set	A structure for selecting a set of automaton properties to copy
Ctwa_graph_state	Graph-based representation of a TωA
Ctwa_graph_edge_data	Data attached to edges of a twa_graph
Ctwa_graph_succ_iterator	Iterator used by the on-the-fly interface of twa_graph
Ctwa_graph	Graph-based representation of a TωA
Cstate_product	A state for spot::twa_product
Ctwa_product	A lazy product. (States are computed on the fly.)
Ctwa_product_init	A lazy product with different initial states
Caig	A class representing AIG circuits
Coutedge_combiner	Helper class combine outgoing edges in alternating automata
Cuniv_remover_state
Ctwa_univ_remover
Cisomorphism_checker	Check if two automata are isomorphic
Cbackprop_graph
Cbfs_steps	Make a BFS in a spot::tgba to compute a twa_run::steps
Cnca_st_info
Cenumerate_cycles	Enumerate elementary cycles in a SCC
Cstate_info
Cdfs_entry
Cemptiness_check_result	The result of an emptiness check
Cemptiness_check	Common interface to emptiness check algorithms
Cemptiness_check_instantiator	Dynamically create emptiness checks. Given their name and options
Ctwa_run	An accepted run, for a twa
Cstep
Cunsigned_statistics
Cec_statistics	Emptiness-check statistics
Cars_statistics	Accepting Run Search statistics
Cacss_statistics	Accepting Cycle Search Space statistics
Ccouvreur99_check_result	Compute a counter example from a spot::couvreur99_check_status
Ccouvreur99_check	An implementation of the Couvreur99 emptiness-check algorithm
Ccouvreur99_check_shy	A version of spot::couvreur99_check that tries to visit known states first
Csuccessor
Ctodo_item
Cscc_stack
Cconnected_component
Ccouvreur99_check_status	The status of the emptiness-check on success
Choa_alias_formater	Help printing BDDs as text, using aliases
Cmtdfa_stats	Statistics about an mtdfa instance
Cmtdfa	DFA represented using shared multi-terminal BDDs
Cltlf_synthesis_options	Fine-tuning options for LTLf synthesis
Cltlf_translator	"Semi-internal" class used to implement spot::ltlf_to_mtdfa()
Cmtdswa	MTBDD-based representation of a state-based ω-automaton
Csimple_ltl_translator	"Semi-internal" for translating LTL using MTBDDs
Cmtdtwa
Creduce_parity_data	Internal data computed by the reduce_parity function
Cpostprocessor	Wrap TGBA/BA/Monitor post-processing algorithms in an easy interface
Cpower_map
Coutput_aborter	Helper object to specify when an algorithm should abort its construction
Ctwa_reachable_iterator	Iterate over all reachable states of a spot::tgba
Ctwa_reachable_iterator_breadth_first	An implementation of spot::twa_reachable_iterator that browses states breadth first
Ctwa_reachable_iterator_depth_first	Iterate over all states of an automaton using a DFS
Cstack_item
Ctwa_reachable_iterator_depth_first_stack	Iterate over all states of an automaton using a DFS
Cremove_ap
Cscc_info_node	Storage for SCC related information
Cscc_info	Compute an SCC map and gather assorted information
Cscc_and_mark_filter	Create a filter for SCC and marks
Cedge_separator_filter
Citerator
Cedge_separator	Separate edges so that their labels are disjoint
Ctwa_statistics
Ctwa_sub_statistics
Cprintable_formula
Cprintable_acc_cond
Cprintable_scc_info
Cprintable_size
Cprintable_long_size
Cstat_printer	Prints various statistics about a TGBA
Csynthesis_info	Benchmarking data and options for synthesis
Cbench_var
Cmealy_like	A struct that represents different types of mealy like objects
Cgame_relabeling_map
Cto_parity_data
Cto_parity_options	Options to control various optimizations of to_parity()
Ctranslator	Translate an LTL formula into an optimized spot::tgba
Ctwa_word	An infinite word stored as a lasso
Czielonka_tree	Zielonka Tree implementation
Czielonka_node
Cacd	Alternating Cycle Decomposition implementation
Ccubeset
Ccstate	Class for thread-safe states
Ctransition	Class for representing a transition
Ctrans_index	Class for iterators over transitions
Ctwacube	Class for representing a thread-safe twa
Nstd
Chash< spot::bitset< N > >
Chash< spot::formula >
Chash< spot::acc_cond::mark_t >