Do transitions need a label or source?

[mtf90]

Do Transitions actually need a reference to their label and source location? Given that transitions are typically accessed when a source location and input symbol is available (its a transition system after all) this seems like unnecessary clutter in the type definition. The only related usages that I have found for these fields were in, e.g., RegisterAutomaton#getInputTransitions and RegisterAutomaton#getInputStates which themselves are only used in utility System.outs.

[pfg666]

As you say, RA transitions do not need a reference to the source location/label. However, I can see situations when it is convenient to have this information (e.g., if you are doing a backwards BFS from some location to initial location). Having this information is also in line with the formal definition of an RA transition. Ultimately, however, for RAs to be incorporated into AutomataLib, AutomataLib principles should be used, which include minimal redundancy. Hence, I would be in favor or removing label/input. However, I would like others to comment (e.g., @FredrikTaquist ).

[mtf90]

We could go with a hybrid approach. On an interface level, the transition type only needs to implement some form of GuardedTransition interface which allows one to access the transition's assignment and guard and the current (default) implementation could stick with the existing Transition class. This way, if you decide to link against the concrete implementation, you still have all the information available but we don't enforce it on any custom implementations.

[pfg666]

Seems reasonable to me!