spot::nca_st_info Struct Reference

#include <spot/twaalgos/cobuchi.hh>

Collaboration diagram for spot::nca_st_info:

Public Member Functions
	nca_st_info (unsigned clause, unsigned st, bitvect *dst)
	Construct an nca_st_info entry.

Public Attributes
unsigned	clause_num
	Index of the NCA clause for this state.
unsigned	state_num
	State number in the NCA.
bitvect *	all_dst
	Bit vector of all successor states.

Detailed Description

A vector of nca_st_info is given as argument to nsa_to_nca() or dnf_to_nca(). Each nca_st_info has information about a state that must be seen infinitely often. For a state 's' visited infinitely often by a run, the information provided is:

• the clause number satisfied by the run (from left to right)
• the state number of 's'
• destinations of all outgoing edges of 's' (represented as a bitvect)

Constructor & Destructor Documentation

nca_st_info()

spot::nca_st_info::nca_st_info ( unsigned  clause, unsigned  st, bitvect *  dst  )

inline

Construct an nca_st_info entry.

Parameters

clause	clause index
st	state number
dst	bitvector of successor states (ownership taken)

References all_dst, clause_num, and state_num.

Member Data Documentation

all_dst

bitvect* spot::nca_st_info::all_dst

Bit vector of all successor states.

Referenced by nca_st_info().

clause_num

unsigned spot::nca_st_info::clause_num

Index of the NCA clause for this state.

Referenced by nca_st_info().

state_num

unsigned spot::nca_st_info::state_num

State number in the NCA.

Referenced by nca_st_info().

---

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

• spot/twaalgos/cobuchi.hh