Cspot::internal::_32acc< bool > | |
►Cspot::internal::_32acc< SPOT_MAX_ACCSETS==8 *sizeof(unsigned)> | |
Cspot::acc_cond::mark_t | An acceptance mark |
Cspot::internal::_32acc< true > | |
Cspot::acc_cond | An acceptance condition |
Cspot::acc_cond::acc_word | A "node" in an acceptance formulas |
Cspot::acd | Alternating Cycle Decomposition implementation |
Cspot::aig | A class representing AIG circuits |
Cspot::internal::all_edge_iterator< Graph > | |
Cspot::internal::all_trans< Graph > | |
Cspot::automaton_parser_options | |
Cspot::automaton_stream_parser | Parse a stream of automata |
Cspot::barand< gen > | Compute pseudo-random integer value between 0 and n included, following a binomial distribution with probability p |
►CBase | |
Choayy::parser::basic_symbol< Base > | |
►Ctlyy::parser::basic_symbol< Base > | |
Ctlyy::parser::symbol_type | "External" symbols: returned by the scanner |
Choayy::parser::basic_symbol< by_state > | |
Cspot::bdd_dict | Map BDD variables to formulae |
Cspot::bdd_hash | Hash functor for BDDs |
Cspot::bdd_dict::bdd_info | |
Cspot::bdd_less_than | Comparison functor for BDDs |
Cspot::bdd_less_than_stable | Comparison functor for BDDs |
Cspot::synthesis_info::bench_var | |
Cspot::bfs_steps | Make a BFS in a spot::tgba to compute a twa_run::steps |
Cspot::bitset< N > | |
Cspot::bitset< SPOT_MAX_ACCSETS/(8 *sizeof(unsigned))> | |
Cspot::bitvect | A bit vector |
Cspot::bitvect_array | |
Cspot::internal::boxed_label< Data, boxed > | |
►Choayy::parser::by_kind | Type access provider for token (enum) based symbols |
►Choayy::parser::basic_symbol< by_kind > | |
Choayy::parser::symbol_type | "External" symbols: returned by the scanner |
Ctlyy::parser::by_kind | Type access provider for token (enum) based symbols |
Cspot::char_ptr_less_than | Strict Weak Ordering for char* |
Cspot::scc_stack::connected_component | |
Cspot::scc_stack_ta::connected_component | |
Cspot::internal::const_universal_dests | |
Choayy::parser::context | |
Ctlyy::parser::context | |
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 | |
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 wether the state will be compressed or not. This class aims to simplify this management |
Cspot::cstate | Class for thread-safe states |
Cspot::cubeset | |
►CData | |
Cspot::internal::boxed_label< Data, false > | |
Cspot::enumerate_cycles::dfs_entry | |
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 |
►CEdge_Data | |
Cspot::internal::edge_storage< StateIn, StateOut, Edge, Edge_Data > | |
►Cspot::internal::edge_iterator< Graph > | |
Cspot::internal::killer_edge_iterator< Graph > | |
Cspot::edge_separator | Separate edges so that their labels are disjoint |
Cspot::edge_separator_filter< subsumed > | |
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 | Compute a counter example from a spot::couvreur99_check_status |
►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::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< formula > | |
Cspot::taa_tgba_formula | |
►Cspot::taa_tgba_labelled< std::string > | |
Cspot::taa_tgba_string | |
Cspot::taa_tgba_labelled< label > | |
►Cspot::tgta | A Transition-based Generalized Testing Automaton (TGTA) |
Cspot::tgta_explicit | |
Cspot::twa_graph | Graph-based representation of a TωA |
►Cspot::twa_product | A lazy product. (States are computed on the fly.) |
Cspot::tgta_product | A lazy product. (States are computed on the fly.) |
Cspot::twa_product_init | A lazy product with different initial states |
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 | |
Cspot::internal::first_is_base_of< Of, Args > | |
Cspot::internal::first_is_base_of< Of, Arg1, Args... > | |
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::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 | |
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 | |
Cspot::game_relabeling_map | |
Cstd::hash< spot::acc_cond::mark_t > | |
Cstd::hash< spot::bitset< N > > | |
Cstd::hash< spot::formula > | |
Cspot::hoa_abort | |
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 | |
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 optimisations (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 check if the iterator has the good interface |
Cspot::is_a_mc_algorithm< T > | This class allows to ensure (at compile time) if a given parameter can be considered as a modelchecking algorithm (i.e., usable by instantiate) |
Cspot::isomorphism_checker | Check if two automata are isomorphic |
Cspot::iterable_uf< State, StateHash, StateEqual > | |
Cspot::iterable_uf_ec< State, StateHash, StateEqual > | |
Cspot::edge_separator_filter< subsumed >::iterator | |
Cspot::internal::keep_all | |
Cspot::internal::keep_inner_scc | |
Cspot::kripkecube< cspins_state, cspins_iterator > | |
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 | Check containment between LTL formulae |
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::ltsmin_model | |
Cspot::internal::mark_container | |
Cspot::internal::mark_iterator | |
Cspot::mark_tools | |
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 |
Cminmax_t | |
Cspot::multiple_size_pool | A multiple-size memory pool implementation |
Cspot::named_graph< Graph, State_Name, Name_Hash, Name_Equal > | |
Cnary | |
Cspot::nca_st_info | |
Cspot::random_formula::op_proba | |
Cspot::option_map | Manage a map of options |
Cspot::output_aborter | Helper object to specify when an algorithm should abort its construction |
Cspot::pair_hash | |
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 |
Choayy::parser | A Bison parser |
Ctlyy::parser | A Bison parser |
Cpnode | |
►Cspot::postprocessor | Wrap TGBA/BA/Monitor post-processing algorithms in an easy interface |
Cspot::translator | Translate an LTL formula into an optimized spot::tgba |
Cspot::power_map | |
►Cspot::printable | |
►Cspot::printable_value< formula > | |
Cspot::printable_formula | |
Cspot::printable_value< unsigned > | |
Cspot::printable_acc_cond | |
Cspot::printable_id | The default callback simply writes "%c" |
Cspot::printable_long_size | |
Cspot::printable_percent | Called by default for "%%" and "%\0" |
Cspot::printable_scc_info | |
Cspot::printable_size | |
Cspot::printable_value< 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 |
Choayy_support::result_::prop_info | |
Cspot::ptr_hash< T > | A hash function for pointers |
Cspot::randltlgenerator | |
►Cspot::random_formula | Base class for random formula generators |
Cspot::random_boolean | Generate random Boolean formulae |
►Cspot::random_ltl | Generate random LTL formulae |
Cspot::random_psl | Generate random PSL formulae |
Cspot::random_sere | Generate random SERE |
Cspot::realizability_simplifier | Simplify a reactive specification, preserving realizability |
Cspot::reduce_parity_data | Internal data computed by the reduce_parity function |
Cspot::remove_ap | |
Cresult_ | |
Choayy_support::result_ | |
Cspot::acc_cond::rs_pair | Rabin/streett pairs used by is_rabin_like and is_streett_like |
Cspot::rs_pairs_view | |
►Cstd::runtime_error | |
Choayy::parser::syntax_error | Syntax errors thrown from user actions |
Cspot::parse_error | |
Ctlyy::parser::syntax_error | Syntax errors thrown from user actions |
Cspot::satsolver | Interface with a SAT solver |
Cspot::scc_and_mark_filter | Create a filter for SCC and marks |
Cspot::internal::scc_edge_iterator< Graph, Filter > | |
Cspot::internal::scc_edges< Graph, Filter > | |
Cspot::scc_info | Compute an SCC map and gather assorted information |
Cspot::scc_info_node | Storage for SCC related information |
Cspot::scc_stack | |
Cspot::scc_stack_ta | |
Choayy::parser::stack< T, S >::slice | Present a slice of the top of a stack |
Ctlyy::parser::stack< T, S >::slice | Present a slice of the top of a stack |
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 whatever the input format considered |
Cspot::twa_reachable_iterator_depth_first::stack_item | |
►Cspot::state | Abstract class for states |
Cspot::kripke_graph_state | Concrete class for kripke_graph states |
Cspot::set_state | Set of states deriving from spot::state |
Cspot::state_product | A state for spot::twa_product |
Cspot::state_ta_explicit | |
Cspot::state_ta_product | A state for spot::ta_product |
Cspot::twa_graph_state | Graph-based representation of a TωA |
►CState_Data | |
Cspot::internal::distate_storage< Edge, State_Data > | |
Choayy_support::result_::state_info | |
Cspot::enumerate_cycles::state_info | |
Cspot::internal::state_out< Graph > | |
Cspot::state_ptr_equal | An Equivalence Relation for state* |
Cspot::state_ptr_hash | Hash Function for state* |
Cspot::state_ptr_less_than | Strict Weak Ordering for state* |
Cspot::state_shared_ptr_equal | An Equivalence Relation for shared_state (shared_ptr<const state*>) |
Cspot::state_shared_ptr_hash | Hash Function for shared_state (shared_ptr<const state*>) |
Cspot::state_shared_ptr_less_than | Strict Weak Ordering for shared_state (shared_ptr<const state*>) |
Cspot::state_unicity_table | Render state pointers unique via a hash table |
Cspot::twa_run::step | |
Cspot::stopwatch | A simple stopwatch |
Cspot::internal::succ_iterator | Helper structure to iterate over the successors of a state using the on-the-fly interface |
Cspot::couvreur99_check_shy::successor | |
Cspot::swarmed_bloemen< State, SuccIterator, StateHash, StateEqual > | 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 |
Cspot::swarmed_bloemen_ec< State, SuccIterator, StateHash, StateEqual > | 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 |
Cspot::swarmed_cndfs< State, SuccIterator, StateHash, StateEqual > | |
Cspot::swarmed_deadlock< State, SuccIterator, StateHash, StateEqual, 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 |
Choayy::parser::symbol_kind | Symbol kinds |
Ctlyy::parser::symbol_kind | Symbol kinds |
Cspot::synthesis_info | Benchmarking data and options for synthesis |
►Cspot::ta | A Testing Automaton |
Cspot::ta_explicit | |
Cspot::ta_product | A lazy product between a Testing automaton and a Kripke structure. (States are computed on the fly.) |
►Cspot::ta_reachable_iterator | Iterate over all reachable states of a spot::ta |
Cspot::ta_reachable_iterator_breadth_first | An implementation of spot::ta_reachable_iterator that browses states breadth first |
Cspot::ta_reachable_iterator_depth_first | An implementation of spot::ta_reachable_iterator that browses states depth first |
Cspot::ta_statistics | |
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 | |
Cspot::to_parity_data | |
Cspot::to_parity_options | Options to control various optimizations of to_parity() |
Cspot::kripkecube_to_twa< State, SuccIterator, StateHash, StateEqual >::todo__element | |
Cspot::couvreur99_check_shy::todo_item | |
Choayy::parser::token | Token kinds |
Ctlyy::parser::token | Token kinds |
Cspot::state_ta_explicit::transition | Explicit transitions |
Cspot::taa_tgba::transition | Explicit transitions |
Cspot::transition | Class for representing a transition |
Cspot::transition_info | |
Cspot::trival | A class implementing Kleene's three-valued logic |
►Cstd::tuple | |
Cspot::internal::boxed_label< void, true > | |
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 | |
Cspot::twa_sub_statistics | |
Cspot::internal::twa_succ_iterable | Helper class to iterate over the successors of a state using the on-the-fly interface |
►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 > | |
►Cspot::ta_succ_iterator | Iterate over the successors of a state |
Cspot::ta_explicit_succ_iterator | Successor iterators used by spot::ta_explicit |
►Cspot::ta_succ_iterator_product | Iterate over the successors of a product computed on the fly |
Cspot::ta_succ_iterator_product_by_changeset | |
Cspot::taa_succ_iterator | |
Cspot::tgta_succ_iterator_product | Iterate over the successors of a product computed on the fly |
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 | The hasher for the previous uf_element. Shortcut to ease shared map manipulation |
Cspot::iterable_uf_ec< State, StateHash, StateEqual >::uf_element_hasher | The hasher for the previous uf_element. Shortcut to ease shared map manipulation |
Cspot::unabbreviator | Clone and rewrite a formula to remove specified operators logical operators |
Cspot::internal::univ_dest_mapper< G > | |
►Cspot::unsigned_statistics | |
►Cspot::ars_statistics | Accepting Run Search statistics |
►Cspot::acss_statistics | Accepting Cycle Search Space statistics |
Cspot::couvreur99_check_result | Compute a counter example from a spot::couvreur99_check_status |
►Cspot::ec_statistics | Emptiness-check statistics |
Cspot::couvreur99_check | An implementation of the Couvreur99 emptiness-check algorithm |
Cspot::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) |
Choayy::parser::value_type | Symbol semantic values |
Ctlyy::parser::value_type | |
►Cstd::vector | |
Cspot::acc_cond::acc_code | An acceptance formula |
Cspot::zielonka_tree::zielonka_node | |
Cspot::zielonka_tree | Zielonka Tree implementation |