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