The documentation states:
If one state has no label, and no labeled edges, then there should be exactly $2^a$ edges listed, where $a$ is the number of atomic propositions. In this case, each edge corresponds to a transition, with the same order as in ltl2dstar. If a transition $t$ is the $i$-th transition of a state (starting with 0), then the label of $t$ can be deduced by interpreting $i$ as a bitset. The label is a set of atomic propositions such that the atomic proposition $j$ is in the set if the $j$-th least significant bit of $i$ is set to 1.
So it seems if one would like to specify a state with no exit arcs, the seemingly obvious code with no state label and no outgoing arcs is in fact incorrect, as 2^a arcs are necessary. So it looks like the only way to do that is to have the label [f] on the state, which is awkward for automata where only transitions carry labels.
The documentation states:
If one state has no label, and no labeled edges, then there should be exactly $2^a$ edges listed, where $a$ is the number of atomic propositions. In this case, each edge corresponds to a transition, with the same order as in ltl2dstar. If a transition $t$ is the $i$-th transition of a state (starting with 0), then the label of $t$ can be deduced by interpreting $i$ as a bitset. The label is a set of atomic propositions such that the atomic proposition $j$ is in the set if the $j$-th least significant bit of $i$ is set to 1.So it seems if one would like to specify a state with no exit arcs, the seemingly obvious code with no state label and no outgoing arcs is in fact incorrect, as 2^a arcs are necessary. So it looks like the only way to do that is to have the label [f] on the state, which is awkward for automata where only transitions carry labels.