spot 2.12.2
|
Classes | |
class | acc_cond |
An acceptance condition. More... | |
class | acd |
Alternating Cycle Decomposition implementation. More... | |
class | acss_statistics |
Accepting Cycle Search Space statistics. More... | |
class | aig |
A class representing AIG circuits. More... | |
class | ars_statistics |
Accepting Run Search statistics. More... | |
struct | automaton_parser_options |
class | automaton_stream_parser |
Parse a stream of automata. More... | |
class | barand |
Compute pseudo-random integer value between 0 and n included, following a binomial distribution with probability p. More... | |
class | bdd_dict |
Map BDD variables to formulae. More... | |
struct | bdd_hash |
Hash functor for BDDs. More... | |
struct | bdd_less_than |
Comparison functor for BDDs. More... | |
struct | bdd_less_than_stable |
Comparison functor for BDDs. More... | |
class | bfs_steps |
Make a BFS in a spot::tgba to compute a twa_run::steps. More... | |
class | bitset |
class | bitvect |
A bit vector. More... | |
class | bitvect_array |
struct | char_ptr_less_than |
Strict Weak Ordering for char* . More... | |
class | couvreur99_check |
An implementation of the Couvreur99 emptiness-check algorithm. More... | |
class | couvreur99_check_result |
Compute a counter example from a spot::couvreur99_check_status. More... | |
class | couvreur99_check_shy |
A version of spot::couvreur99_check that tries to visit known states first. More... | |
class | couvreur99_check_status |
The status of the emptiness-check on success. More... | |
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... | |
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... | |
class | cstate |
Class for thread-safe states. More... | |
class | cubeset |
class | declarative_environment |
A declarative environment. More... | |
class | default_environment |
A laxist environment. More... | |
class | digraph |
A directed graph. More... | |
class | ec_statistics |
Emptiness-check statistics. More... | |
struct | ec_stats |
This structure contains, for each thread, the collected information during the traversal. More... | |
class | edge_separator |
separate edges so that their labels are disjoint More... | |
struct | edge_separator_filter |
class | emptiness_check |
Common interface to emptiness check algorithms. More... | |
class | emptiness_check_instantiator |
Dynamically create emptiness checks. Given their name and options. More... | |
class | emptiness_check_result |
The result of an emptiness check. More... | |
class | enumerate_cycles |
Enumerate elementary cycles in a SCC. More... | |
class | environment |
An environment that describes atomic propositions. More... | |
class | exclusive_ap |
class | fair_kripke |
Interface for a Fair Kripke structure. More... | |
class | fair_kripke_succ_iterator |
Iterator code for a Fair Kripke structure. More... | |
class | fixed_size_pool |
A fixed-size memory pool implementation. More... | |
class | fnode |
Actual storage for formula nodes. More... | |
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... | |
class | formater |
class | formula |
Main class for temporal logic formula. More... | |
struct | formula_ptr_less_than_bool_first |
struct | game_relabeling_map |
struct | hoa_abort |
class | hoa_alias_formater |
Help printing BDDs as text, using aliases. More... | |
struct | identity_hash |
A hash function that returns identity. More... | |
struct | inner_callback_parameters |
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 | 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 | is_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) More... | |
class | isomorphism_checker |
Check if two automata are isomorphic. More... | |
class | iterable_uf |
class | iterable_uf_ec |
class | kripke |
Interface for a Kripke structure. More... | |
class | kripke_graph |
Kripke Structure. More... | |
struct | kripke_graph_state |
Concrete class for kripke_graph states. More... | |
class | kripke_graph_succ_iterator |
class | kripke_succ_iterator |
Iterator code for 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 | kripkecube< cspins_state, cspins_iterator > |
class | kripkecube_to_twa |
convert a (cube) model into a twa. Note that this algorithm cannot be run in parallel but could. More... | |
class | language_containment_checker |
Check containment between LTL formulae. 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... | |
class | ltsmin_model |
class | mark_tools |
struct | mealy_like |
A struct that represents different types of mealy like objects. 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 | named_graph |
struct | nca_st_info |
class | open_temporary_file |
Open temporary file. More... | |
class | option_map |
Manage a map of options. More... | |
class | output_aborter |
Helper object to specify when an algorithm should abort its construction. More... | |
struct | pair_hash |
class | parallel_policy |
This class is used to tell parallel algorithms what resources they may use. More... | |
struct | parse_error |
struct | parsed_aut |
Result of the automaton parser. More... | |
struct | parsed_formula |
The result of a formula parser. More... | |
class | postprocessor |
Wrap TGBA/BA/Monitor post-processing algorithms in an easy interface. More... | |
struct | power_map |
class | printable |
class | printable_acc_cond |
class | printable_formula |
class | printable_id |
The default callback simply writes "%c". More... | |
class | printable_long_size |
class | printable_percent |
Called by default for "%%" and "%\0". More... | |
class | printable_scc_info |
class | printable_size |
class | printable_value |
struct | process_timer |
Struct used to start and stop both timer and stopwatch clocks. More... | |
class | product_to_twa |
convert a (cube) product automaton into a twa Note that this algorithm cannot be run in parallel. More... | |
struct | ptr_hash |
A hash function for pointers. More... | |
class | randltlgenerator |
class | random_boolean |
Generate random Boolean formulae. More... | |
class | random_formula |
Base class for random formula generators. More... | |
class | random_ltl |
Generate random LTL formulae. More... | |
class | random_psl |
Generate random PSL formulae. More... | |
class | random_sere |
Generate random SERE. More... | |
class | realizability_simplifier |
Simplify a reactive specification, preserving realizability. More... | |
struct | reduce_parity_data |
Internal data computed by the reduce_parity function. More... | |
class | remove_ap |
struct | rs_pairs_view |
class | satsolver |
Interface with a SAT solver. More... | |
class | satsolver_command |
Interface with a given sat solver. More... | |
class | scc_and_mark_filter |
Create a filter for SCC and marks. More... | |
class | scc_info |
Compute an SCC map and gather assorted information. More... | |
class | scc_info_node |
Storage for SCC related information. More... | |
class | scc_stack |
class | scc_stack_ta |
class | set_state |
Set of states deriving from spot::state. More... | |
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 manipulated transparently whatever the input format considered. More... | |
class | stat_printer |
prints various statistics about a TGBA More... | |
class | state |
Abstract class for states. More... | |
class | state_product |
A state for spot::twa_product. More... | |
struct | state_ptr_equal |
An Equivalence Relation for state* . More... | |
struct | state_ptr_hash |
Hash Function for state* . More... | |
struct | state_ptr_less_than |
Strict Weak Ordering for 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... | |
struct | state_shared_ptr_less_than |
Strict Weak Ordering for shared_state (shared_ptr<const state*>). More... | |
class | state_ta_explicit |
class | state_ta_product |
A state for spot::ta_product. More... | |
class | state_unicity_table |
Render state pointers unique via a hash table. More... | |
struct | stopwatch |
A simple stopwatch. More... | |
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 | 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 deadlock algorithm, otherwise perform a simple reachability. More... | |
struct | synthesis_info |
Benchmarking data and options for synthesis. More... | |
class | ta |
A Testing Automaton. 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_explicit |
class | ta_explicit_succ_iterator |
Successor iterators used by spot::ta_explicit. More... | |
class | ta_product |
A lazy product between a Testing automaton and a Kripke structure. (States are computed on the fly.) More... | |
class | ta_reachable_iterator |
Iterate over all reachable states of a spot::ta. More... | |
class | ta_reachable_iterator_breadth_first |
An implementation of spot::ta_reachable_iterator that browses states breadth first. More... | |
class | ta_reachable_iterator_depth_first |
An implementation of spot::ta_reachable_iterator that browses states depth first. More... | |
struct | ta_statistics |
class | ta_succ_iterator |
Iterate over the successors of a state. More... | |
class | ta_succ_iterator_product |
Iterate over the successors of a product computed on the fly. More... | |
class | ta_succ_iterator_product_by_changeset |
class | taa_succ_iterator |
class | taa_tgba |
A self-loop Transition-based Alternating Automaton (TAA) which is seen as a TGBA (abstract class, see below). More... | |
class | taa_tgba_formula |
class | taa_tgba_labelled |
class | taa_tgba_string |
class | temporary_file |
Temporary file name. More... | |
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... | |
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... | |
class | tl_simplifier |
Rewrite or simplify f in various ways. More... | |
class | tl_simplifier_options |
struct | to_parity_data |
struct | to_parity_options |
Options to control various optimizations of to_parity(). More... | |
class | trans_index |
Class for iterators over transitions. More... | |
class | transition |
Class for representing a transition. More... | |
struct | transition_info |
class | translator |
Translate an LTL formula into an optimized spot::tgba. More... | |
class | trival |
A class implementing Kleene's three-valued logic. More... | |
class | twa |
A Transition-based ω-Automaton. More... | |
class | twa_graph |
Graph-based representation of a TωA. More... | |
struct | twa_graph_edge_data |
Data attached to edges of a twa_graph. More... | |
struct | twa_graph_state |
Graph-based representation of a TωA. More... | |
class | twa_graph_succ_iterator |
Iterator used by the on-the-fly interface of twa_graph. 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 | 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... | |
struct | twa_run |
An accepted run, for a twa. More... | |
struct | twa_statistics |
struct | twa_sub_statistics |
class | twa_succ_iterator |
Iterate over the successors of a state. More... | |
struct | twa_word |
An infinite word stored as a lasso. More... | |
class | twacube |
Class for representing a thread-safe twa. More... | |
class | unabbreviator |
Clone and rewrite a formula to remove specified operators logical operators. More... | |
struct | unsigned_statistics |
class | zielonka_tree |
Zielonka Tree implementation. 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< const twa_word > | const_twa_word_ptr |
typedef std::shared_ptr< twa_word > | twa_word_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::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 { op::ff , op::tt , op::eword , op::ap , op::Not , op::X , op::F , op::G , op::Closure , op::NegClosure , op::NegClosureMarked , op::Xor , op::Implies , op::Equiv , op::U , op::R , op::W , op::M , op::EConcat , op::EConcatMarked , op::UConcat , op::Or , op::OrRat , op::And , op::AndRat , op::AndNLM , op::Concat , op::Fusion , op::Star , op::FStar , op::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 { scc_info_options::NONE = 0 , scc_info_options::STOP_ON_ACC = 1 , scc_info_options::TRACK_STATES = 2 , scc_info_options::TRACK_SUCCS = 4 , scc_info_options::TRACK_STATES_IF_FIN_USED = 8 , scc_info_options::PROCESS_UNREACHABLE_STATES = 16 , scc_info_options::ALL = TRACK_STATES | TRACK_SUCCS } |
Options to alter the behavior of scc_info. More... | |
enum class | zielonka_tree_options { zielonka_tree_options::NONE = 0 , zielonka_tree_options::CHECK_RABIN = 1 , zielonka_tree_options::CHECK_STREETT = 2 , zielonka_tree_options::CHECK_PARITY = CHECK_RABIN | CHECK_STREETT , zielonka_tree_options::ABORT_WRONG_SHAPE = 4 , zielonka_tree_options::MERGE_SUBTREES = 8 } |
Options to alter the behavior of acd. More... | |
enum class | acd_options { acd_options::NONE = 0 , acd_options::CHECK_RABIN = 1 , acd_options::CHECK_STREETT = 2 , acd_options::CHECK_PARITY = CHECK_RABIN | CHECK_STREETT , acd_options::ABORT_WRONG_SHAPE = 4 , acd_options::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... | |
atomic_prop_set | collect_literals (formula f) |
Collect the literals occurring in f. More... | |
std::vector< std::vector< spot::formula > > | collect_equivalent_literals (formula f) |
Collect equivalent APs. 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 <l_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 <l_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 <l_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 <l_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 | 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... | |
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 | reduce_buchi_acceptance_set_here (twa_graph_ptr &aut, bool preserve_sbacc=false) |
Reduce the acceptance set of a Büchi automaton. More... | |
twa_graph_ptr | enlarge_buchi_acceptance_set_here (twa_graph_ptr &aut, bool preserve_sbacc=false) |
Enlarge the acceptance set of a Büchi automaton. 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... | |
int | containment_select_version (const char *version=nullptr) |
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, const 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... | |
twa_word_ptr | difference_word_forq (const_twa_graph_ptr left, const_twa_graph_ptr right) |
Returns a word accepted by left that is rejected by right, or nullptr. More... | |
bool | contains_forq (const_twa_graph_ptr left, const_twa_graph_ptr right) |
Returns a boolean value indicating whether the language of left includes in the language of right. 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, bool solve_globally=false) |
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 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 const_twa_graph_ptr &arena, unsigned state) |
Get the winner of a state. 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, const std::vector< std::pair< std::string, bdd > > &aliases) |
Define all aliases used in the HOA format. More... | |
void | create_alias_basis (const twa_graph_ptr &aut) |
Create an alias basis. 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_guaranteed_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... | |
relabeling_map | partitioned_relabel_here (twa_graph_ptr &aut, bool split=false, unsigned max_letter=-1u, unsigned max_letter_mult=-1u, const bdd &concerned_ap=bddtrue, std::string var_prefix="__nv") |
Replace conditions in aut with non-overlapping conditions over fresh variables. More... | |
bool | rabin_is_buchi_realizable (const const_twa_graph_ptr &aut) |
Check if aut is Rabin-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, bool keep_one_color=false) |
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_graph_ptr | separate_edges (const const_twa_graph_ptr &aut) |
Make edge labels disjoints. 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 transitions, even unreachable ones. More... | |
bool | is_terminal_automaton (const const_twa_graph_ptr &aut, scc_info *sm=nullptr) |
Check whether an automaton is terminal. More... | |
SPOT_DEPRECATED ("is third argument of is_terminal_automaton()" " is now ignored") bool is_terminal_automaton(const const_twa_graph_ptr &aut | |
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... | |
game_relabeling_map | partitioned_game_relabel_here (twa_graph_ptr &arena, bool relabel_env, bool relabel_play, bool split_env=false, bool split_play=false, unsigned max_letter=-1u, unsigned max_letter_mult=-1u) |
Tries to relabel a SPLIT game arena using fresh propositions. Can be applied to env or player depending on relabel_env and relabel_play. The arguments split_env and split_play determine whether or not env and player edges are to be split into several transitions labelled by letters not conditions. More... | |
void | relabel_game_here (twa_graph_ptr &arena, game_relabeling_map &rel_maps) |
Undoes a relabeling done by partitioned_game_relabel_here. A dedicated function is necessary in order to remove the variables tagging env and player conditions. 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 appearance 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) |
formula | relabel_bse (formula f, relabeling_style style, relabeling_map *m=nullptr) |
Relabel Boolean subexpressions in a formula using atomic propositions. More... | |
formula | relabel_overlapping_bse (formula f, relabeling_style style, relabeling_map *m) |
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... | |
std::ostream & | operator<< (std::ostream &os, const acc_cond &acc) |
prints the acceptance formula as text More... | |
std::ostream & | operator<< (std::ostream &os, acc_cond::mark_t m) |
prints the acceptance formula as text More... | |
std::ostream & | operator<< (std::ostream &os, const acc_cond::acc_code &code) |
prints the acceptance formula as text More... | |
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... | |
formula | bdd_to_formula (bdd f, const bdd_dict_ptr d) |
Convert a BDD into a formula. More... | |
formula | bdd_to_cnf_formula (bdd f, const bdd_dict_ptr d) |
Convert a BDD into a formula. 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, const realizability_simplifier *rs=nullptr) |
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, const realizability_simplifier *rs=nullptr) |
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, const realizability_simplifier *rs=nullptr) |
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, const realizability_simplifier *rs=nullptr) |
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... | |
const region_t & | get_state_winners (const const_twa_graph_ptr &arena) |
Get the winner of all states. More... | |
const region_t & | get_state_winners (twa_graph_ptr &arena) |
Get the winner of all 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_independent_formulas (formula f, const std::vector< std::string > &outs) |
Seeks to decompose a formula into independently synthetizable sub-parts. The conjunction of all sub-parts then satisfies the specification. More... | |
std::pair< std::vector< formula >, std::vector< std::set< formula > > > | split_independent_formulas (const std::string &f, const std::vector< std::string > &outs) |
Seeks to decompose a formula into independently synthetizable 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^" |
scc_info * | sm |
scc_info | bool |
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... | |
This file aggregates all classes and typedefs necessary to build a kripke that is thread safe
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
using spot::cube = typedef unsigned* |
A cube is only a set of bits in memory.
This set can be seen as two bitsets
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 represented by:
To represent free variables such as in (a & !b) | (a & b) (which is equivalent to (a) with b free)
To be memory efficient, these two bitsets are contigious 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
typedef std::shared_ptr<spot::kripkecube<spot::cspins_state, spot::cspins_iterator> > spot::ltsmin_kripkecube_ptr |
shortcut to manipulate the kripke below
typedef struct spot::process_timer spot::process_timer |
Struct used to start and stop both timer and stopwatch clocks.
typedef std::vector<std::pair<unsigned, unsigned> > spot::product_states |
Automata constructed by product() contain a property named "product-states" with this type.
typedef std::unordered_set<shared_state, state_shared_ptr_hash, state_shared_ptr_equal> spot::shared_state_set |
Unordered set of shared states.
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.
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.
|
strong |
The list of parallel model-checking algorithms available.
|
strong |
|
strong |
Enum used to change the behavior of is_obligation().
|
strong |
A enum class to define the policy of the fixed_sized_pool. We propose 2 policies for the pool:
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.
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.
dict | The dictionary to use, to lookup variables. |
b | The BDD to print. |
std::string spot::bdd_format_formula | ( | const bdd_dict_ptr & | dict, |
bdd | b | ||
) |
Format a BDD as a formula.
dict | The dictionary to use, to lookup variables. |
b | The BDD to print. |
std::string spot::bdd_format_isop | ( | const bdd_dict_ptr & | dict, |
bdd | b | ||
) |
Format a BDD as an irredundant sum of product.
dict | The dictionary to use, to lookup variables. |
b | The BDD to print. |
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.
dict | The dictionary to use, to lookup variables. |
b | The BDD to print. |
std::string spot::bdd_format_set | ( | const bdd_dict_ptr & | dict, |
bdd | b | ||
) |
Format a BDD as a set.
dict | The dictionary to use, to lookup variables. |
b | The BDD to print. |
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.
os | The output stream. |
dict | The dictionary to use, to lookup variables. |
b | The BDD to print. |
std::ostream & spot::bdd_print_formula | ( | std::ostream & | os, |
const bdd_dict_ptr & | dict, | ||
bdd | b | ||
) |
Print a BDD as a formula.
os | The output stream. |
dict | The dictionary to use, to lookup variables. |
b | The BDD to print. |
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.
os | The output stream. |
dict | The dictionary to use, to lookup variables. |
b | The BDD to print. |
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.
os | The output stream. |
dict | The dictionary to use, to lookup variables. |
b | The BDD to print. |
std::ostream & spot::bdd_print_set | ( | std::ostream & | os, |
const bdd_dict_ptr & | dict, | ||
bdd | b | ||
) |
Print a BDD as a set.
os | The output stream. |
dict | The dictionary to use, to lookup variables. |
b | The BDD to print. |
formula spot::bdd_to_cnf_formula | ( | bdd | f, |
const bdd_dict_ptr | d | ||
) |
Convert a BDD into a formula.
Format the BDD as a Boolean spot::formula object. 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.
The bdd_to_formula() version produces an irredundant sum of product (see the minato_isop class for details) and map the BDD variables back into their atomic propositions.
The bdd_to_cnf_formula() version produces an irredundant product of sum, using the dual construction.
formula spot::bdd_to_formula | ( | bdd | f, |
const bdd_dict_ptr | d | ||
) |
Convert a BDD into a formula.
Format the BDD as a Boolean spot::formula object. 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.
The bdd_to_formula() version produces an irredundant sum of product (see the minato_isop class for details) and map the BDD variables back into their atomic propositions.
The bdd_to_cnf_formula() version produces an irredundant product of sum, using the dual construction.
void spot::check_determinism | ( | twa_graph_ptr | aut | ) |
Set the deterministic and semi-deterministic properties appropriately.
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.
aut | the automaton to check |
sm | an scc_info object for the automaton if available (it will be built otherwise). |
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.
aut | the input automaton |
keep_style | whether the style of the parity acc is kept. |
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.
aut | the input automaton |
keep_style | whether the style of the parity acc is kept. |
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.
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.
aut | the input automaton |
keep_style | whether the style of the parity acc is kept. |
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.
aut | the input automaton |
keep_style | whether the style of the parity acc is kept. |
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.
If an output_aborter is supplied, it is used to abort the construction of larger automata.
complement_semidet() is not yet used, as it is not always better when the input is semi-deterministic.
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]
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.
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.
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.
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().
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.
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.
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.
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:
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). [47]
aut | the automaton to decompose |
keep | a string specifying the strengths/SCCs to keep |
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.
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).
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 |
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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_synthetize() 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.
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.
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.
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.
void spot::enable_utf8 | ( | ) |
Enable UTF-8 output for bdd printers.
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.
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().
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().
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.
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.
std::set< const state * > spot::get_states_set | ( | const const_ta_ptr & | t | ) |
Compute states set for an automaton.
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.
void spot::highlight_languages | ( | twa_graph_ptr & | aut | ) |
Color state that recognize identical language.
State that recognize a unique language will not be colored.
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.
si | the SCC information of the automaton to process |
color | the color to give to states reachable from accepting SCCs. |
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.
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.
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.
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).
m | The automaton to be verified |
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.
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.
acc_cond::mark_t spot::is_partially_degeneralizable | ( | const const_twa_graph_ptr & | aut, |
bool | allow_inf = true , |
||
bool | allow_fin = true , |
||
const 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.
If you need to disallow certain marks from being returned, pass them in the forbid vector.
bool spot::is_safety_automaton | ( | const const_twa_graph_ptr & | aut, |
scc_info * | sm = nullptr |
||
) |
Check whether an automaton is a safety automaton.
An automaton is a safety automaton if its acceptance condition can be changed to "true" without changing its language.
The test performed by this function differs depending on the nature of the input aut.
If aut is an automaton with t
acceptance, it is necessarily a safety automaton.
Else we check for the absence of rejecting cycle in the useful part of the automaton. This absence is only a sufficient condition in the non-deterministic case, because a rejecting run might correspond to a word that is accepted by another run.
If the previous test could not conclude, we build the automaton B that is a copy of aut with acceptance set to true, and we check that aut contains all words of B. This last test requires complementing aut.
aut | the automaton to check |
sm | an scc_info object for the automaton if available (it will be built otherwise). |
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.
bool spot::is_terminal_automaton | ( | const const_twa_graph_ptr & | aut, |
scc_info * | sm = nullptr |
||
) |
Check whether an automaton is terminal.
An automaton is terminal if it is weak, all its accepting SCCs are complete, and no accepting SCC may lead to a non-accepting SCC.
This property guarantees that a word is accepted if it has some prefix that reaches an accepting transition.
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.
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.
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.
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.
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.
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 total number of recognized languages, states recognizing the same language have the same value.
The given automaton must be deterministic.
std::list< std::string > spot::list_formula_props | ( | const formula & | f | ) |
List the properties of formula f.
bitvect * spot::make_bitvect | ( | size_t | bitcount | ) |
Allocate a bit-vector of bitcount bits.
The resulting object should be released with delete
.
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
.
|
inline |
|
inline |
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.
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.
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.
int spot::memusage | ( | ) |
Total number of pages in use by the program.
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 ']'.
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.
Compute the nesting depth of an operator.
Return the maximum number of occurrence of oper among all branches of the AST of f.
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.
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.
std::ostream & spot::operator<< | ( | std::ostream & | os, |
acc_cond::mark_t | m | ||
) |
prints the acceptance formula as text
std::ostream & spot::operator<< | ( | std::ostream & | os, |
const acc_cond & | acc | ||
) |
prints the acceptance formula as text
std::ostream & spot::operator<< | ( | std::ostream & | os, |
const acc_cond::acc_code & | code | ||
) |
prints the acceptance formula as text
std::ostream & spot::operator<< | ( | std::ostream & | os, |
const formula & | f | ||
) |
Print a formula.
|
inline |
Struct used to start and stop both timer and stopwatch clocks.
|
inline |
on-the-fly TGBA product
|
inline |
on-the-fly TGBA product with forced initial states
twa_word_ptr spot::parse_word | ( | const std::string & | word, |
const bdd_dict_ptr & | dict | ||
) |
relabeling_map spot::partitioned_relabel_here | ( | twa_graph_ptr & | aut, |
bool | split = false , |
||
unsigned | max_letter = -1u , |
||
unsigned | max_letter_mult = -1u , |
||
const bdd & | concerned_ap = bddtrue , |
||
std::string | var_prefix = "__nv" |
||
) |
Replace conditions in aut with non-overlapping conditions over fresh variables.
Partitions the conditions in the automaton, then (binary) encodes them using fresh propositions. This can lead to an exponential explosion in the number of conditions. The operations is aborted if either the number of new letters (subsets of the partition) exceeds max_letter OR max_letter_mult times the number of conditions in the original automaton. The argument concerned_ap can be used to filter out transitions. If given, only the transitions whose support intersects the concerned_ap (or whose condition is T) are taken into account. The fresh aps will be enumerated and prefixed by var_prefix. These variables need to be fresh, i.e. may not exist yet (not checked)
std::ostream & spot::print_formula_props | ( | std::ostream & | out, |
const formula & | f, | ||
bool | abbreviated = false |
||
) |
Print the properties of formula f on stream out.
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().
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().
acc_cond::acc_code spot::random_acceptance | ( | unsigned | n_accs | ) |
Build a random acceptance where each acceptance sets is used once.
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.
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 example), 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.
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 example), 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.
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().
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"
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.
twa_graph_ptr spot::scc_filter | ( | const const_twa_graph_ptr & | aut, |
bool | remove_all_useless = false , |
||
scc_info * | given_si = nullptr , |
||
bool | keep_one_color = false |
||
) |
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. If the automaton had no rejecting SCC, the acceptance condition is set to "t". Otherwise, the acceptance condition is set to Büchi unless the input was co-Büchi (in which case we keep this acceptance).
If given_si is supplied, the function will use its result without computing a map of its own.
If keep_one_color is set, the output will keep at least color if the input had colors. Normally scc_filter removes as many colors as possible.
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.
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.
std::vector< bool > spot::semidet_sccs | ( | scc_info & | si | ) |
Whether an SCC is in the deterministic part of an automaton.
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.
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.
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 |
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.
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.
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.
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: [35] , [37] .
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.
aut | the automaton to convert to weak |
less | whether to activate the optimization on the number of transitions or not, disabled by default |
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.
init | The optional new initial state. |
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 transitions will be processed.
init | The optional new initial state. |
twacube_ptr spot::twa_to_twacube | ( | spot::const_twa_graph_ptr | aut | ) |
Convert a twa into a twacube.
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.