| ►Nspot | |
| ►Cacc_cond | An acceptance condition |
| Cacc_code | An acceptance formula |
| Cacc_word | A "node" in an acceptance formulas |
| Cmark_t | An acceptance mark |
| Crs_pair | Rabin/streett pairs used by is_rabin_like and is_streett_like |
| Cacd | Alternating Cycle Decomposition implementation |
| Cacss_statistics | Accepting Cycle Search Space statistics |
| ►Cadjlist | |
| Csuccessor_iterator | |
| Csuccessor_range | |
| Caig | A class representing AIG circuits |
| Cars_statistics | Accepting Run Search statistics |
| Cautomaton_parser_options | |
| Cautomaton_stream_parser | Parse a stream of automata |
| Cbackprop_graph | |
| Cbarand | Compute pseudo-random integer value between 0 and n included, following a binomial distribution with probability p |
| ►Cbdd_dict | Map BDD variables to formulae |
| Cbdd_info | |
| Cbdd_dict_preorder | |
| Cbdd_hash | Hash functor for BDDs |
| Cbdd_less_than | Comparison functor for BDDs |
| Cbdd_less_than_stable | Comparison functor for BDDs |
| Cbfs_steps | Make a BFS in a spot::tgba to compute a twa_run::steps |
| Cbitset | |
| Cbitvect | A bit vector |
| Cbitvect_array | |
| Cchar_ptr_less_than | Strict Weak Ordering for char* |
| Ccouvreur99_check | An implementation of the Couvreur99 emptiness-check algorithm |
| Ccouvreur99_check_result | Compute a counter example from a spot::couvreur99_check_status |
| ►Ccouvreur99_check_shy | A version of spot::couvreur99_check that tries to visit known states first |
| Csuccessor | |
| Ctodo_item | |
| Ccouvreur99_check_status | The status of the emptiness-check on success |
| ►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 | |
| 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 |
| Ccstate | Class for thread-safe states |
| Ccubeset | |
| Cdeclarative_environment | A declarative environment |
| Cdefault_environment | A laxist environment |
| Cdigraph | A directed graph |
| Cec_statistics | Emptiness-check statistics |
| Cec_stats | This structure contains, for each thread, the collected information during the traversal |
| Cedge_separator | Separate edges so that their labels are disjoint |
| ►Cedge_separator_filter | |
| Citerator | |
| Cemptiness_check | Common interface to emptiness check algorithms |
| Cemptiness_check_instantiator | Dynamically create emptiness checks. Given their name and options |
| Cemptiness_check_result | The result of an emptiness check |
| ►Cenumerate_cycles | Enumerate elementary cycles in a SCC |
| Cdfs_entry | |
| Cstate_info | |
| Cenvironment | An environment that describes atomic propositions |
| Cexclusive_ap | |
| Cfair_kripke | Interface for a Fair Kripke structure |
| Cfair_kripke_succ_iterator | Iterator code for a Fair Kripke structure |
| Cfixed_size_pool | A fixed-size memory pool implementation |
| Cfnode | Actual storage for formula nodes |
| 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 |
| Cformater | |
| ►Cformula | Main class for temporal logic formula |
| Cformula_child_iterator | Allow iterating over children |
| Cformula_ptr_less_than_bool_first | |
| Cgame_relabeling_map | |
| Choa_abort | |
| Choa_alias_formater | Help printing BDDs as text, using aliases |
| Cidentity_hash | A hash function that returns identity |
| Cinner_callback_parameters | |
| 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) |
| 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 |
| 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) |
| Cisomorphism_checker | Check if two automata are isomorphic |
| ►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 |
| ►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 |
| Ckripke | Interface for a Kripke structure |
| Ckripke_graph | Kripke Structure |
| Ckripke_graph_state | Concrete class for kripke_graph states |
| Ckripke_graph_succ_iterator | |
| Ckripke_succ_iterator | Iterator code for 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 |
| Ckripkecube< cspins_state, cspins_iterator > | |
| ►Ckripkecube_to_twa | Convert a (cube) model into a twa. Note that this algorithm cannot be run in parallel but could |
| Ctodo__element | |
| Clanguage_containment_checker | Check containment between LTL formulae |
| 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 |
| Cltlf_simplifier | Cheap simplification rules for LTLf formulas |
| Cltlf_translator | "Semi-internal" class used to implement spot::ltlf_to_mtdfa() |
| Cltsmin_model | |
| Cmark_tools | |
| Cmealy_like | A struct that represents different types of mealy like objects |
| Cminato_isop | Generate an irredundant sum-of-products (ISOP) form of a BDD function |
| Cmtdfa | DFA represented using shared multi-terminal BDDs |
| Cmtdfa_stats | Statistics about an mtdfa instance |
| Cmtdtwa | |
| Cmultiple_size_pool | A multiple-size memory pool implementation |
| Cnamed_graph | |
| Cnca_st_info | |
| Copen_temporary_file | Open temporary file |
| Coption_map | Manage a map of options |
| Coutput_aborter | Helper object to specify when an algorithm should abort its construction |
| Cpair_hash | |
| Cparallel_policy | This class is used to tell parallel algorithms what resources they may use |
| Cparse_error | |
| Cparsed_aut | Result of the automaton parser |
| Cparsed_formula | The result of a formula parser |
| Cpostprocessor | Wrap TGBA/BA/Monitor post-processing algorithms in an easy interface |
| Cpower_map | |
| Cprintable | |
| Cprintable_acc_cond | |
| Cprintable_formula | |
| Cprintable_id | The default callback simply writes "%c" |
| Cprintable_long_size | |
| Cprintable_percent | Called by default for "%%" and "%\0" |
| Cprintable_scc_info | |
| Cprintable_size | |
| Cprintable_value | |
| Cprocess_timer | Struct used to start and stop both timer and stopwatch clocks |
| Cproduct_to_twa | Convert a (cube) product automaton into a twa Note that this algorithm cannot be run in parallel |
| Cptr_hash | A hash function for pointers |
| Crandltlgenerator | |
| Crandom_boolean | Generate random Boolean formulas |
| ►Crandom_formula | Base class for random formula generators |
| Cop_proba | |
| Crandom_ltl | Generate random LTL formulas |
| Crandom_psl | Generate random PSL formulas |
| Crandom_sere | Generate random SERE |
| Crealizability_simplifier | Simplify a reactive specification, preserving realizability |
| Crealizability_simplifier_base | Simplify a reactive specification, preserving realizability |
| Creduce_parity_data | Internal data computed by the reduce_parity function |
| Cremove_ap | |
| Crs_pairs_view | |
| Csatsolver | Interface with a SAT solver |
| Csatsolver_command | Interface with a given sat solver |
| Cscc_and_mark_filter | Create a filter for SCC and marks |
| Cscc_info | Compute an SCC map and gather assorted information |
| Cscc_info_node | Storage for SCC related information |
| ►Cscc_stack | |
| Cconnected_component | |
| ►Cscc_stack_ta | |
| Cconnected_component | |
| Cset_state | Set of states deriving from spot::state |
| 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 |
| Cstat_printer | Prints various statistics about a TGBA |
| Cstate | Abstract class for states |
| Cstate_product | A state for spot::twa_product |
| Cstate_ptr_equal | An Equivalence Relation for state* |
| Cstate_ptr_hash | Hash Function for state* |
| Cstate_ptr_less_than | Strict Weak Ordering for 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*>) |
| Cstate_shared_ptr_less_than | Strict Weak Ordering for shared_state (shared_ptr<const state*>) |
| ►Cstate_ta_explicit | |
| Ctransition | Explicit transitions |
| Cstate_ta_product | A state for spot::ta_product |
| Cstate_unicity_table | Render state pointers unique via a hash table |
| Cstopwatch | A simple stopwatch |
| 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 |
| 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 |
| ►Csynthesis_info | Benchmarking data and options for synthesis |
| Cbench_var | |
| Cta | A Testing Automaton |
| Cta_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) |
| Cta_explicit | |
| Cta_explicit_succ_iterator | Successor iterators used by spot::ta_explicit |
| Cta_product | A lazy product between a Testing automaton and a Kripke structure. (States are computed on the fly.) |
| Cta_reachable_iterator | Iterate over all reachable states of a spot::ta |
| Cta_reachable_iterator_breadth_first | An implementation of spot::ta_reachable_iterator that browses states breadth first |
| Cta_reachable_iterator_depth_first | An implementation of spot::ta_reachable_iterator that browses states depth first |
| Cta_statistics | |
| Cta_succ_iterator | Iterate over the successors of a state |
| Cta_succ_iterator_product | Iterate over the successors of a product computed on the fly |
| Cta_succ_iterator_product_by_changeset | |
| Ctaa_succ_iterator | |
| ►Ctaa_tgba | A self-loop Transition-based Alternating Automaton (TAA) which is seen as a TGBA (abstract class, see below) |
| Ctransition | Explicit transitions |
| Ctaa_tgba_formula | |
| Ctaa_tgba_labelled | |
| Ctaa_tgba_string | |
| Ctemporary_file | Temporary file name |
| Ctgta | A Transition-based Generalized Testing Automaton (TGTA) |
| Ctgta_explicit | |
| Ctgta_product | A lazy product. (States are computed on the fly.) |
| Ctgta_succ_iterator_product | Iterate over the successors of a product computed on the fly |
| Ctime_info | A structure to record elapsed time in clock ticks |
| Ctimer | |
| Ctimer_map | A map of timer, where each timer has a name |
| Ctl_simplifier | Rewrite or simplify f in various ways |
| Ctl_simplifier_options | |
| Cto_parity_data | |
| Cto_parity_options | Options to control various optimizations of to_parity() |
| Ctrans_index | Class for iterators over transitions |
| Ctransition | Class for representing a transition |
| Ctransition_info | |
| Ctranslator | Translate an LTL formula into an optimized spot::tgba |
| Ctrival | A class implementing Kleene's three-valued logic |
| Ctwa | A Transition-based ω-Automaton |
| Ctwa_graph | Graph-based representation of a TωA |
| Ctwa_graph_edge_data | Data attached to edges of a twa_graph |
| Ctwa_graph_state | Graph-based representation of a TωA |
| Ctwa_graph_succ_iterator | Iterator used by the on-the-fly interface of twa_graph |
| Ctwa_product | A lazy product. (States are computed on the fly.) |
| Ctwa_product_init | A lazy product with different initial states |
| 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 |
| ►Ctwa_run | An accepted run, for a twa |
| Cstep | |
| Ctwa_statistics | |
| Ctwa_sub_statistics | |
| Ctwa_succ_iterator | Iterate over the successors of a state |
| Ctwa_word | An infinite word stored as a lasso |
| Ctwacube | Class for representing a thread-safe twa |
| Cunabbreviator | Clone and rewrite a formula to remove specified operators logical operators |
| Cunsigned_statistics | |
| ►Czielonka_tree | Zielonka Tree implementation |
| Czielonka_node | |
