DFA equality

[bennn]

Is there a way to compare two minimized DFAs for equality?

What I really want to do is compare two LTLf terms. I'm hoping to parse them with logaut, minimize them, and check for DFA equality.

[marcofavorito]

For SimpleDFA it should already work:

from pythomata import SimpleDFA
alphabet = {"a", "b", "c"}
states = {"s1", "s2", "s3"}
initial_state = "s1"
accepting_states = {"s3"}
transition_function = {
    "s1": {
        "b" : "s1",
        "a" : "s2"
    },
    "s2": {
        "a" : "s3",
        "b" : "s1"
    },
    "s3":{
        "c" : "s3"
    }
}
dfa = SimpleDFA(states, alphabet, initial_state, accepting_states, transition_function)

x = dfa.minimize()
y = dfa.minimize()

assert x == y

For SymbolicDFA currently it is not supported:

from pythomata.impl.symbolic import SymbolicDFA

dfa = SymbolicDFA()
s0 = dfa.initial_state
s1 = dfa.create_state()
dfa.add_transition((s0, 'a', s1))
dfa_1 = dfa.minimize()
dfa_2 = dfa.minimize()
assert dfa_1 == dfa_2  # it fails, since it uses the default __eq__ method of Python objects

However, a workaround could be to access all the relevant attributes and compare them:

def eq_symbolic_dfa(arg_1: SymbolicDFA, arg_2: SymbolicDFA) -> bool:
    return arg_1.states == arg_2.states and\
            arg_1.initial_state == arg_2.initial_state and\
            arg_1.accepting_states == arg_2.accepting_states and\
            arg_1._transition_function == arg_2._transition_function

eq_symbolic_dfa(dfa_1, dfa_2)  # returns True

Having this function (as SymbolicAutomaton.__eq__) included in the library is surely a nice-to-have feature! But hopefully, the workaround above should already help you.

[bennn]

Excellent, thank you!!