spot::mtdfa_stats Struct Reference

statistics about an mtdfa instance More...

#include <spot/twaalgos/ltlf2dfa.hh>

Collaboration diagram for spot::mtdfa_stats:

Public Attributes
unsigned	states
	number of roots More...
unsigned	aps
	number of atomic propositions More...
unsigned	nodes
	Number of internal nodes (or decision nodes) More...
unsigned	terminals
	Number of terminal nodes. More...
unsigned long long	paths
	Number of paths between a root and a leaf (terminal or constant) More...
unsigned long long	edges
	Number of pairs (root, leaf) for which a path exists. More...
bool	has_true
	Whether the true and false constants are used. More...
bool	has_false
	Whether the true and false constants are used. More...

Detailed Description

statistics about an mtdfa instance

$ to indicate whether the transition is accepting (i.e., the evaluation can stop after reading the last letter). The bddfalse and bddtrue nodes are kept to represent rejecting and accepting sinks; using them helps some to shortcut some BDD operations.

[20]

This holds the result of a call to mtdfa::get_stats().

Member Data Documentation

aps

unsigned spot::mtdfa_stats::aps

number of atomic propositions

This are the number of atomic proposition used in the original formula. The proposition actually used in the automaton may be less.

edges

unsigned long long spot::mtdfa_stats::edges

Number of pairs (root, leaf) for which a path exists.

Only filled if mtdfa::get_stats() was passed the edges option.

has_false

bool spot::mtdfa_stats::has_false

Whether the true and false constants are used.

Only filled if mtdfa::get_stats() was passed the nodes option.

has_true

bool spot::mtdfa_stats::has_true

Whether the true and false constants are used.

Only filled if mtdfa::get_stats() was passed the nodes option.

nodes

unsigned spot::mtdfa_stats::nodes

Number of internal nodes (or decision nodes)

Only filled if mtdfa::get_stats() was passed the nodes option.

paths

unsigned long long spot::mtdfa_stats::paths

Number of paths between a root and a leaf (terminal or constant)

Only filled if mtdfa::get_stats() was passed the edges option.

states

unsigned spot::mtdfa_stats::states

number of roots

This excludes true and false, that are never listed as roots.

terminals

unsigned spot::mtdfa_stats::terminals

Number of terminal nodes.

This excludes the true and false, constant nodes.

Only filled if mtdfa::get_stats() was passed the nodes option.

---

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

• spot/twaalgos/ltlf2dfa.hh