spot 2.13.1.dev
Loading...
Searching...
No Matches
Public Member Functions | Public Attributes | List of all members
spot::mtdfa Struct Reference

a DFA represented using shared multi-terminal BDDs More...

#include <spot/twaalgos/ltlf2dfa.hh>

Inheritance diagram for spot::mtdfa:
Collaboration diagram for spot::mtdfa:

Public Member Functions

 mtdfa (const bdd_dict_ptr &dict) noexcept
 create an empty mtdfa
 
unsigned num_roots () const
 the number of MTBDDs roots
 
unsigned num_states () const
 The number of states in the automaton.
 
bool is_empty () const
 
std::ostream & print_dot (std::ostream &os, int index=-1, bool labels=true) const
 Print the states array of MTBDD in graphviz format.
 
twa_graph_ptr as_twa (bool state_based=false, bool labels=true) const
 Convert this automaton to a spot::twa_graph.
 
mtdfa_stats get_stats (bool nodes, bool paths) const
 compute some statistics about the automaton
 
bdd_dict_ptr get_dict () const
 get the bdd_dict associated to this automaton
 
bdd get_controllable_variables () const
 Returns the conjunction of controllable variables.
 
void set_controllable_variables (const std::vector< std::string > &vars, bool ignore_non_registered_ap=false)
 declare a list of controllable variables
 
void set_controllable_variables (bdd vars)
 declare a list of controllable variables
 

Public Attributes

std::vector< bdd > states
 
std::vector< formulanames
 
std::vector< formulaaps
 The list of atomic propositions possibly used by the automaton.
 

Detailed Description

a DFA represented using shared multi-terminal BDDs

Such a DFA is represented by a vector a BDDs: one BDD per state. Each BDD encodes set of outgoing transitions of a state. The of the transitions encoded naturally using BDD decision variables, and the destination state is stored as a "terminal" node.

Those DFA use transition-based acceptance, and that acceptance is represented by the last bit of the value stored in the terminal.

If a transition should reach state V, the terminal stores the value 2*V if the transition is rejecting, or 2*V+1 if the transition is accepting.

Constructor & Destructor Documentation

◆ mtdfa()

spot::mtdfa::mtdfa ( const bdd_dict_ptr &  dict)
inlinenoexcept

create an empty mtdfa

The dict is used to record how BDD variables map to atomic propositions.

Member Function Documentation

◆ as_twa()

twa_graph_ptr spot::mtdfa::as_twa ( bool  state_based = false,
bool  labels = true 
) const

Convert this automaton to a spot::twa_graph.

The twa_graph is not meant to represent finite automata, so this will actually abuse the twa_graph class by creating a deterministic Büchi automaton in which accepting transitions should be interpreted as final transitions. If state_based is set, then a DBA with state-based acceptance is created instead.

The conversion can be costly, since it requires creating BDD-labeled transitions for each path between a root and a leave of the state array. However it can be useful to explain the MTDBA semantics.

By default the created automaton will have its states named using the LTLf formula for the original state if available. Set labels to false if you do not want that.

◆ get_controllable_variables()

bdd spot::mtdfa::get_controllable_variables ( ) const
inline

Returns the conjunction of controllable variables.

◆ get_dict()

bdd_dict_ptr spot::mtdfa::get_dict ( ) const
inline

get the bdd_dict associated to this automaton

◆ get_stats()

mtdfa_stats spot::mtdfa::get_stats ( bool  nodes,
bool  paths 
) const

compute some statistics about the automaton

By default, only fetch statistics that are available in constant time.

If nodes is true, this will additionally count the number of internal nodes and leaves. It requires scanning the BDDs for the entire array of states, so this is linear in what the number of nodes involved.

If paths is true, this will additionally count the number of paths from roots to leaves. This is potentially exponential in the number of atomic propositions.

◆ num_roots()

unsigned spot::mtdfa::num_roots ( ) const
inline

the number of MTBDDs roots

This is the size of the states array. It does not account for any false or true state.

◆ num_states()

unsigned spot::mtdfa::num_states ( ) const
inline

The number of states in the automaton.

This counts the number of roots, plus one if the true state is reachable. This is therefore the size that the transition-based output of as_twa() would have.

◆ print_dot()

std::ostream & spot::mtdfa::print_dot ( std::ostream &  os,
int  index = -1,
bool  labels = true 
) const

Print the states array of MTBDD in graphviz format.

If index is non-negative, print only a single state.

By default states will be named according to the formulas given in the names array, if available. Set labels is false (or clear names) if you prefer states to by numbered.

◆ set_controllable_variables() [1/2]

void spot::mtdfa::set_controllable_variables ( bdd  vars)

declare a list of controllable variables

Doing so affect the way the automaton is printed in dot format, but this is also a prerequisite for interpreting the automaton as a game.

This function should only be called after the state have been registered by the automaton. If ignore_non_registered_ap is set, variable listed as output but not registered by the automaton will be dropped. Else, an exception will be raised for those variables.

◆ set_controllable_variables() [2/2]

void spot::mtdfa::set_controllable_variables ( const std::vector< std::string > &  vars,
bool  ignore_non_registered_ap = false 
)

declare a list of controllable variables

Doing so affect the way the automaton is printed in dot format, but this is also a prerequisite for interpreting the automaton as a game.

This function should only be called after the state have been registered by the automaton. If ignore_non_registered_ap is set, variable listed as output but not registered by the automaton will be dropped. Else, an exception will be raised for those variables.

Member Data Documentation

◆ aps

std::vector<formula> spot::mtdfa::aps

The list of atomic propositions possibly used by the automaton.

This is actually the list of atomic propositions that appeared in the formulas/automata that were used to build this automaton. The automaton itself may use fewer atomic propositions in cases some of them canceled each other.

This vector is sorted by formula ID, to make it easy to merge with another sorted vector.


The documentation for this struct was generated from the following file:

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.8