From f7693b5609e38d37e74f29a57fb5af2dad273102 Mon Sep 17 00:00:00 2001 From: Edi Muskardin Date: Sat, 22 Jun 2024 20:20:55 +0200 Subject: [PATCH] ensure correctness of bisimilar and compare_automata if you pass same object twice --- aalpy/utils/ModelChecking.py | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/aalpy/utils/ModelChecking.py b/aalpy/utils/ModelChecking.py index 230fcaf29c6..31992500768 100644 --- a/aalpy/utils/ModelChecking.py +++ b/aalpy/utils/ModelChecking.py @@ -247,6 +247,10 @@ def bisimilar(a1: DeterministicAutomaton, a2: DeterministicAutomaton, return_cex # TODO allow states as inputs instead of automata if a1.__class__ != a2.__class__: raise ValueError("tried to check bisimilarity of different automaton types") + # if you use this function with the same object (does not make sense anyway) + if a1 is a2: + a2 = a1.copy() + supported_automaton_types = (Dfa, MooreMachine, MealyMachine) if not isinstance(a1, supported_automaton_types): raise NotImplementedError( @@ -302,8 +306,12 @@ def compare_automata(aut_1: DeterministicAutomaton, aut_2: DeterministicAutomato """ # from aalpy.oracles import RandomWMethodEqOracle + # if you use this function with the same object (does not make sense anyway) + if aut_1 is aut_2: + aut_2 = aut_1.copy() - assert set(aut_1.get_input_alphabet()) == set(aut_2.get_input_alphabet()) + if set(aut_1.get_input_alphabet()) != set(aut_2.get_input_alphabet()): + assert False, "Cannot compare automata with different input alphabets" input_al = aut_1.get_input_alphabet() # larger automaton is used as hypothesis, as then test-cases will contain prefixes leading to states