spot 2.12.2
|
Classes | |
class | spot::scc_info_node |
Storage for SCC related information. More... | |
class | spot::scc_info |
Compute an SCC map and gather assorted information. More... | |
class | spot::edge_separator |
separate edges so that their labels are disjoint More... | |
struct | spot::twa_statistics |
struct | spot::twa_sub_statistics |
class | spot::printable_formula |
class | spot::printable_acc_cond |
class | spot::printable_scc_info |
class | spot::printable_size |
class | spot::printable_long_size |
class | spot::stat_printer |
prints various statistics about a TGBA More... | |
Enumerations | |
enum class | spot::scc_info_options { spot::scc_info_options::NONE = 0 , spot::scc_info_options::STOP_ON_ACC = 1 , spot::scc_info_options::TRACK_STATES = 2 , spot::scc_info_options::TRACK_SUCCS = 4 , spot::scc_info_options::TRACK_STATES_IF_FIN_USED = 8 , spot::scc_info_options::PROCESS_UNREACHABLE_STATES = 16 , spot::scc_info_options::ALL = TRACK_STATES | TRACK_SUCCS } |
Options to alter the behavior of scc_info. More... | |
Functions | |
bool | spot::isomorphism_checker::is_isomorphic (const const_twa_graph_ptr aut) |
Check whether an automaton is isomorphic to the one passed to the constructor. More... | |
static bool | spot::isomorphism_checker::are_isomorphic (const const_twa_graph_ptr ref, const const_twa_graph_ptr aut) |
Check whether two automata are isomorphic. More... | |
twa_graph_ptr | spot::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 | spot::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... | |
twa_graph_ptr | spot::dualize (const const_twa_graph_ptr &aut) |
Complement an automaton by dualizing it. More... | |
twa_graph_ptr | spot::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... | |
unsigned | spot::count_nondet_states (const const_twa_graph_ptr &aut) |
Count the number of states with non-deterministic branching in aut. More... | |
bool | spot::is_universal (const const_twa_graph_ptr &aut) |
Return true iff aut is universal. More... | |
bool | spot::is_deterministic (const const_twa_graph_ptr &aut) |
Return true iff aut is deterministic. More... | |
void | spot::highlight_nondet_states (twa_graph_ptr &aut, unsigned color) |
Highlight nondeterministic states. More... | |
void | spot::highlight_nondet_edges (twa_graph_ptr &aut, unsigned color) |
Highlight nondeterministic edges. More... | |
bool | spot::is_unambiguous (const const_twa_graph_ptr &aut) |
Whether the automaton aut is unambiguous. More... | |
bool | spot::check_unambiguous (const twa_graph_ptr &aut) |
Like is_unambiguous(), but also sets the property in the twa. More... | |
bool | spot::scc_has_rejecting_cycle (scc_info &map, unsigned scc) |
Whether the SCC number scc in map has a rejecting cycle. More... | |
bool | spot::is_inherently_weak_scc (scc_info &map, unsigned scc) |
Whether the SCC number scc in map is inherently weak. More... | |
bool | spot::is_weak_scc (scc_info &map, unsigned scc) |
Whether the SCC number scc in map is weak. More... | |
bool | spot::is_complete_scc (scc_info &map, unsigned scc) |
Whether the SCC number scc in map is complete. More... | |
bool | spot::is_terminal_scc (scc_info &map, unsigned scc) |
Whether the SCC number scc in map is terminal. More... | |
twa_graph_ptr | spot::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 | spot::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... | |
twa_graph_ptr | spot::split_edges (const const_twa_graph_ptr &aut) |
transform edges into transitions More... | |
twa_graph_ptr | spot::separate_edges (const const_twa_graph_ptr &aut) |
Make edge labels disjoints. More... | |
twa_statistics | spot::stats_reachable (const const_twa_ptr &g) |
Compute statistics for an automaton. More... | |
twa_sub_statistics | spot::sub_stats_reachable (const const_twa_ptr &g) |
Compute sub statistics for an automaton. More... | |
unsigned long long | spot::count_all_transitions (const const_twa_graph_ptr &g) |
Count all transitions, even unreachable ones. More... | |
void | spot::strip_acceptance_here (twa_graph_ptr a) |
Remove all acceptance sets from a twa_graph. More... | |
enum class | spot::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(* | spot::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 edge_filter_choice(* spot::edge_filter) (const twa_graph::edge_storage_t &e, unsigned dst, void *filter_data) |
#include <spot/twaalgos/sccinfo.hh>
An edge_filter may be called on each edge to decide what to do with it.
The edge filter is called with an edge and a destination. (In existential automata the destination is already given by the edge, but in alternating automata, one edge may have several destinations, and in this case the filter will be called for each destination.) The filter should return a value from edge_filter_choice.
keep
means to use the edge normally, as if no filter had been given. ignore
means to pretend the edge does not exist (if the destination is only reachable through this edge, it will not be visited). cut
also ignores the edge, but it remembers to visit the destination state (as if it were an initial state) in case it is not reachable otherwise.
Note that successors between SCCs can only be maintained for edges that are kept. If some edges are ignored or cut, the SCC graph that you can explore with scc_info::initial() and scc_info::succ() will be restricted to the portion reachable with "keep" edges. Additionally, SCCs might be created when edges are cut, but those will not be reachable from scc_info::initial()..
|
strong |
#include <spot/twaalgos/sccinfo.hh>
An edge_filter may be called on each edge to decide what to do with it.
The edge filter is called with an edge and a destination. (In existential automata the destination is already given by the edge, but in alternating automata, one edge may have several destinations, and in this case the filter will be called for each destination.) The filter should return a value from edge_filter_choice.
keep
means to use the edge normally, as if no filter had been given. ignore
means to pretend the edge does not exist (if the destination is only reachable through this edge, it will not be visited). cut
also ignores the edge, but it remembers to visit the destination state (as if it were an initial state) in case it is not reachable otherwise.
Note that successors between SCCs can only be maintained for edges that are kept. If some edges are ignored or cut, the SCC graph that you can explore with scc_info::initial() and scc_info::succ() will be restricted to the portion reachable with "keep" edges. Additionally, SCCs might be created when edges are cut, but those will not be reachable from scc_info::initial()..
|
strong |
#include <spot/twaalgos/sccinfo.hh>
Options to alter the behavior of scc_info.
|
static |
#include <spot/twaalgos/are_isomorphic.hh>
Check whether two automata are isomorphic.
twa_graph_ptr spot::canonicalize | ( | twa_graph_ptr | aut | ) |
#include <spot/twaalgos/canonicalize.hh>
Reorder the states and transitions of aut in a way that will be the same for every isomorphic automata.
bool spot::check_unambiguous | ( | const twa_graph_ptr & | aut | ) |
#include <spot/twaalgos/isunamb.hh>
Like is_unambiguous(), but also sets the property in the twa.
|
inline |
#include <spot/twaalgos/copy.hh>
Build an explicit automaton from all states of aut,.
This function was deprecated in Spot 2.4. Use the function make_twa_graph() instead.
References spot::make_twa_graph().
unsigned long long spot::count_all_transitions | ( | const const_twa_graph_ptr & | g | ) |
#include <spot/twaalgos/stats.hh>
Count all transitions, even unreachable ones.
unsigned spot::count_nondet_states | ( | const const_twa_graph_ptr & | aut | ) |
#include <spot/twaalgos/isdet.hh>
Count the number of states with non-deterministic branching in aut.
The automaton is universal if it has 0 states with non-deterministic branching but it is more efficient to call is_universal() if you do not care about the number of non-deterministic states.
twa_graph_ptr spot::dualize | ( | const const_twa_graph_ptr & | aut | ) |
#include <spot/twaalgos/dualize.hh>
Complement an automaton by dualizing it.
Given an automaton aut of any type, produces the dual as output. Before dualization, the automaton will be completed if it isn't already, but any sink state in the output might then be removed.
Dualizing the automaton is done by interpreting the outgoing transitions of a state as a Boolean function, and then swapping operators ∧ and ̇∨. This first step does not have to be done on deterministic automata. Additionally, the acceptance condition is dualized by swapping operators ∧ and ̇∨, and swapping Inf and Fin.
For instance, the dual of a generalized Büchi automaton will be a generalized co-Büchi automaton.
If the input acceptance condition accepts every infinite path (such as "t" or "Inf(0)|Fin(0)") and the automaton is not complete, then the input automaton will be assumed to have Büchi acceptance in order to complete it, and the output will then have co-Büchi acceptance.
Due to a defect in the way transition-based alternating automata are represented in Spot and in the HOA format, existential automata with transition-based acceptance will be converted to use state-based acceptance before dualization. See https://github.com/adl/hoaf/issues/68 for more information.
If the input automaton is deterministic, the output will be deterministic. If the input automaton is existential, the output will be universal. If the input automaton is universal, the output will be existential. Finally, if the input automaton is alternating, the result is alternating. More can be found on page 22 (Definition 1.6) of [40] .
Functions like to_generalized_buchi() or remove_fin() are frequently called on existential automata after dualize() to obtain an easier acceptance condition, but maybe at the cost of losing determinism.
Up to version 2.11.6, this function used to call cleanup_acceptance_here() to simplify the acceptance condition after dualization. This caused some surprizes, users expected the dual of a Büchi automaton to be a co-Büchi automaton, but cleanup_acceptance_here() sometimes reduced the condition to t
when all states where accepting. This function is not called anymore since version 2.12.
twa_graph_ptr spot::g_f_terminal_inplace | ( | twa_graph_ptr | f_terminal, |
bool | state_based = false |
||
) |
#include <spot/twaalgos/gfguarantee.hh>
Given a terminal automaton f_terminal recognizing some formula F(φ), modify it to recognize GF(φ).
If state_based is set, the automaton's terminal states are all replaced by a unique accepting state that has the same outgoing transitions as the initial state, and the initial state is actually relocated to that accepting state. The latter point is not necessary, but it favors shorter accepting cycles.
If state_based is not set, all transition going to terminal states are made accepting and redirected to the initial state.
This construction is inspired by a similar construction in the LICS'18 paper by Esparza et al. [20]
void spot::highlight_nondet_edges | ( | twa_graph_ptr & | aut, |
unsigned | color | ||
) |
#include <spot/twaalgos/isdet.hh>
Highlight nondeterministic edges.
An edge is nondeterministic if there exist another edge leaving the same source state, with a compatible label (i.e., the conjunction of the two labels is not false).
aut | the automaton to process |
color | the color to give to nondeterministic edges. |
void spot::highlight_nondet_states | ( | twa_graph_ptr & | aut, |
unsigned | color | ||
) |
#include <spot/twaalgos/isdet.hh>
Highlight nondeterministic states.
A state is nondeterministic if it has two outgoing edges whose labels are not incompatibles.
aut | the automaton to process |
color | the color to give to nondeterministic states. |
bool spot::is_complete_scc | ( | scc_info & | map, |
unsigned | scc | ||
) |
#include <spot/twaalgos/isweakscc.hh>
Whether the SCC number scc in map is complete.
An SCC is complete iff for all states and all label there exists a transition that stays into this SCC. For this function, universal transitions are considered in the SCC if all there destination are into the SCC.
bool spot::is_deterministic | ( | const const_twa_graph_ptr & | aut | ) |
#include <spot/twaalgos/isdet.hh>
Return true iff aut is deterministic.
An automaton is called deterministic if it is both universal and existential.
bool spot::is_inherently_weak_scc | ( | scc_info & | map, |
unsigned | scc | ||
) |
#include <spot/twaalgos/isweakscc.hh>
Whether the SCC number scc in map is inherently weak.
An SCC is inherently weak if either its cycles are all accepting, or they are all non-accepting.
Note the terminal SCCs are also inherently weak with that definition.
bool spot::isomorphism_checker::is_isomorphic | ( | const const_twa_graph_ptr | aut | ) |
#include <spot/twaalgos/are_isomorphic.hh>
Check whether an automaton is isomorphic to the one passed to the constructor.
Two automata are considered isomorphic if there exists a bijection f between the states of a1 and the states of a2 such that for any pair of states (s1, s2) of a1, there is a transition from s1 to s2 with condition c and acceptance set A iff there is a transition with condition c and acceptance set A between f(s1) and f(s2) in a2. This can be done simply by checking if canonicalize(aut1) == canonicalize(aut2), but is_isomorphic can do some optimizations in some cases.
bool spot::is_terminal_scc | ( | scc_info & | map, |
unsigned | scc | ||
) |
#include <spot/twaalgos/isweakscc.hh>
Whether the SCC number scc in map is terminal.
An SCC is terminal if it is weak, complete, and accepting.
bool spot::is_unambiguous | ( | const const_twa_graph_ptr & | aut | ) |
#include <spot/twaalgos/isunamb.hh>
Whether the automaton aut is unambiguous.
An automaton is unambiguous if each accepted word is recognized by only one path.
We check unambiguousity by synchronizing the automaton with itself, and then making sure that the co-reachable part of the squared automaton has the same size as the co-reachable part of the original automaton.
bool spot::is_universal | ( | const const_twa_graph_ptr & | aut | ) |
#include <spot/twaalgos/isdet.hh>
Return true iff aut is universal.
This function is more efficient than count_nondet_states() when the automaton is nondeterministic, because it can return before the entire automaton has been explored.
In addition to returning the result as a Boolean, this will set the prop_universal() property of the automaton as a side-effect, so further calls will return in constant-time.
bool spot::is_weak_scc | ( | scc_info & | map, |
unsigned | scc | ||
) |
#include <spot/twaalgos/isweakscc.hh>
Whether the SCC number scc in map is weak.
An SCC is weak if its non-accepting, or if all its transition are fully accepting (i.e., the belong to all acceptance sets).
Note that terminal SCCs are also weak with that definition.
twa_graph_ptr spot::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 |
||
) |
#include <spot/twaalgos/randomgraph.hh>
Construct a twa randomly.
n | The number of states wanted in the automata (>0). All states will be connected, and there will be no dead state. |
d | The density of the automata. This is the probability (between 0.0 and 1.0), to add a transition between two states. All states have at least one outgoing transition, so d is considered only when adding the remaining transition. A density of 1 means all states will be connected to each other. |
ap | The list of atomic property that should label the transition. |
dict | The bdd_dict to used for this automata. |
n_accs | The number of acceptance sets to use. If this number is non null, then there is no guarantee that the generated graph contains an accepting cycle (raise the value of a to improve the chances). |
a | The probability (between 0.0 and 1.0) that a transition belongs to an acceptance set. |
t | The probability (between 0.0 and 1.0) that an atomic proposition is true. |
deterministic | build a complete and deterministic automaton |
state_acc | build an automaton with state-based acceptance |
colored | build an automaton in which each transition (or state) belongs to a single acceptance set. |
This algorithms is adapted from the one in Fig 6.2 page 48 of [55] .
Although the intent is similar, there are some differences between the above published algorithm and this implementation. First labels are on transitions, and acceptance conditions are generated too. Second, the number of successors of a node is chosen in following a normal distribution with mean
and variance
. (This is less accurate, but faster than considering all possible n successors one by one.)
Note that while this constructs an automaton with random acceptance sets, this does not set the acceptance condition.
bool spot::scc_has_rejecting_cycle | ( | scc_info & | map, |
unsigned | scc | ||
) |
#include <spot/twaalgos/isweakscc.hh>
Whether the SCC number scc in map has a rejecting cycle.
twa_graph_ptr spot::separate_edges | ( | const const_twa_graph_ptr & | aut | ) |
#include <spot/twaalgos/split.hh>
Make edge labels disjoints.
Create a new version of the automaton where all edges are split in such a way that two labels are either equal or disjoint.
For instance if the automaton uses only {a,b,!a&!b&c} as labels, the result should have label among {a&!b,a&b,!a&b,!a&!b&c}.
Using split_edges() also creates an automaton with separated labels, but the separation will be much finer since it will result in a much involves all atomic proposition.
twa_graph_ptr spot::split_edges | ( | const const_twa_graph_ptr & | aut | ) |
#include <spot/twaalgos/split.hh>
transform edges into transitions
Create a new version of the automaton where all edges are split so that they are all labeled by a conjunction of all atomic propositions.
So if an edge is labeled by "true", it will be split into $2^{AP}$ distinct edges.
After this we can consider that each edge of the automaton is a transition labeled by one of $2^{AP}$ letters.
twa_statistics spot::stats_reachable | ( | const const_twa_ptr & | g | ) |
#include <spot/twaalgos/stats.hh>
Compute statistics for an automaton.
void spot::strip_acceptance_here | ( | twa_graph_ptr | a | ) |
#include <spot/twaalgos/stripacc.hh>
Remove all acceptance sets from a twa_graph.
This will also set the acceptance condition to true, and mark the automaton as weak. Doing so obviously makes all recognized infinite runs accepting.
twa_sub_statistics spot::sub_stats_reachable | ( | const const_twa_ptr & | g | ) |
#include <spot/twaalgos/stats.hh>
Compute sub statistics for an automaton.
twa_graph_ptr spot::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 |
||
) |
#include <spot/twaalgos/powerset.hh>
Build a deterministic automaton, ignoring acceptance conditions.
This create a deterministic automaton that recognizes the same language as aut would if its acceptance conditions were ignored. This is the classical powerset algorithm.
If pm is supplied it will be filled with the set of original states associated to each state of the deterministic automaton. The merge argument can be set to false to prevent merging of transitions.
If ab aborter is given, abort the construction whenever it would build an automaton that is too large, and return nullptr.
If a vector of accepting sinks is given, all power-state that contains any accepting sink will be merged into a single state with number 0.