else-based eges

[adl]

(Joachim's suggestion)

For the boolean-edge-label format one idea I had a while ago but never researched in practice is the following. For a deterministic automaton, the edge definitions are read in order. However, the boolean formulas are interpreted with an implicit "successor state for label is not yet defined". E.g,

State: 0 [1 & 2] 1 [t] 2

The second edge definition would be interpreted as "t & !(1 & 2)". When the edge information is internally stored in a BDD I imagine such a scheme could potentially result in a smaller encoding, as the latter edge defs can use more "don't cares". So, this is a more speculative idea :)

Jan S suggests that we implement some e (short for "else") constant that can be used as:

State: 0
[1 & 2] 1
[e]     2

and the semantic of e would be either the complement of every thing we have seen so far (my view), or the complement of all other transitions (his).

In all cases, this can be useful to complete automata, and this does not require changing the semantic of t.

[JanKretinsky]

I like the idea of "e", but to make its usage clear, I'd enforce to use it as the last case in the switch for each state (both semantics collide and it looks more standard and less wild). However, it's kind of a feature that can be put in the let's-see-if-we-can-implement-this-nice-idea-at-some-point bag

[kleinj]

Ok, let's postpone for a later version.

[JanKretinsky]

yes, let's do this in v2