spot::fm_simple_edge Struct Reference

A simplified successor edge without condition. More...

#include <spot/twaalgos/ltl2tgba_fm.hh>

Collaboration diagram for spot::fm_simple_edge:

Public Attributes
acc_cond::mark_t	acc
	Acceptance marks, using negated-Inf semantics.
formula	dst
	Destination formula-state.

Detailed Description

A simplified successor edge without condition.

This is a lighter variant of fm_edge that omits the BDD condition on atomic propositions. It is useful for on-the-fly emptiness checks where the condition is known to be bddtrue (e.g., after realizability simplification has removed all atomic propositions).

Member Data Documentation

acc

acc_cond::mark_t spot::fm_simple_edge::acc

Acceptance marks, using negated-Inf semantics.

dst

formula spot::fm_simple_edge::dst

Destination formula-state.

---

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

• spot/twaalgos/ltl2tgba_fm.hh