Fix to_state_setup() with unreachable states

[MaxiSchwindler]

The method to_state_setup() of multiple automata types (DFA, Mealy, Moore) fails when the automaton contains an unreachable state (i.e. the state's prefix is None - not an empty tuple!). This also means that we cannot copy such an automaton if it contains an unreachable state, since copy() uses to_state_setup():

from aalpy.utils import moore_from_state_setup, dfa_from_state_setup, mealy_from_state_setup

# DFA
dfa = dfa_from_state_setup({
    "a": (True, {"x": "b1", "y": "a"}),
    "b1": (False, {"x": "b2", "y": "a"}),
    "b2": (True, {"x": "b3", "y": "a"}),
    "b3": (False, {"x": "b4", "y": "a"}),
    "b4": (False, {"x": "c", "y": "a"}),
    "c": (True, {"x": "a", "y": "a"}),
    "unreachable": (True, {"x": "a", "y": "a"}),
})
dfa.visualize("dfa", file_type="png")
dfa_copy = dfa.copy()
dfa_copy.visualize("dfa_copy", file_type="png")

# Moore Machine
moore = moore_from_state_setup({
    "a": ("a", {"x": "b1", "y": "a"}),
    "b1": ("b", {"x": "b2", "y": "a"}),
    "b2": ("b", {"x": "b3", "y": "a"}),
    "b3": ("b", {"x": "b4", "y": "a"}),
    "b4": ("b", {"x": "c", "y": "a"}),
    "c": ("c", {"x": "a", "y": "a"}),
    "unreachable": ("d", {"x": "a", "y": "a"}),
})
moore.visualize("moore", file_type="png")
moore_copy = moore.copy()
moore_copy.visualize("moore_copy", file_type="png")

# Mealy Machine
mealy = mealy_from_state_setup({
    "a": {"x": ("o1", "b1"), "y": ("o2", "a")},
    "b1": {"x": ("o3", "b2"), "y": ("o1", "a")},
    "b2": {"x": ("o1", "b3"), "y": ("o2", "a")},
    "b3": {"x": ("o3", "b4"), "y": ("o1", "a")},
    "b4": {"x": ("o1", "c"), "y": ("o4", "a")},
    "c": {"x": ("o3", "a"), "y": ("o5", "a")},
    "unreachable": {"x": ("o3", "a"), "y": ("o5", "a")},
})
mealy.visualize("mealy", file_type="png")
mealy_copy = mealy.copy()
mealy_copy.visualize("mealy_copy", file_type="png")

[emuskardin]

Hi,

good catch, thank you!
I would rather ignore the unreachable state, since it is unreachable anyways, and keeping it there adds to the confusion (imo).

In other words, if a state is unreachable, it might as well not exist.

Will fix tomorrow

[MaxiSchwindler]

Hm, I get your point, but in my opinion, ignoring the unreachable state is more confusing... For example, since copy() depends on to_state_setup()/from_state_setup(), copying a model with unreachable states produces a model without those unreachable states - i.e., the copy is not an exact copy. This is more confusing in my eyes - I would expect a copy to be exact.

A possible (admittedly contrived) usecase could be, creating a model with only states (no transitions yet), copying it, and then adding different transitions to both models. If the copy-operation removed unreachable states, this would not be possible.

Also, there might be learning algorithms, which (perhaps on accident) produce unreachable states - then ignoring these states during copy might hide the bug sometimes (if copy() is used) but not other times...

[emuskardin]

I will see still, need to sleep it over :p

I would still consider all of these in some way or another improper handling of states.
Automaton contains behavior that can be reached by it, unreachable states might as well not exist. Abstractly this could be seen as a memory leak even.

[emuskardin]

@MaxiSchwindler
Did you find this bug in a natural use of AALpy or were you experimenting?
As if the former is the case, I also need to fix this :)

[MaxiSchwindler]

@MaxiSchwindler
Did you find this bug in a natural use of AALpy or were you experimenting?

Not during natural use of AALpy, no, but during use of the PMSAT-Inference algorithm - which uses Partial Max-SAT-solving to learn an automaton with exactly the given number of states... So there it can happen that the returned hypothesis has unreachable states (and it makes some sense not to do pruning directly in that algorithm, otherwise you'd e.g. request an automaton with 5 states but receive one with 4).

[MaxiSchwindler]

...but I don't think that algorithm is the best argument for keeping the unreachable states on copy(). I'd still simply argue that "copy()" should mean "exact copy", regardless of anything else. If there is an unreachable state in the original, it would make sense to me for it to be also in the copy.