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)

Public Attributes
unsigned	clause_num
unsigned	state_num
bitvect *	all_dst

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)

---

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

• spot/twaalgos/cobuchi.hh