Skip to content

Commit

Permalink
ensure correctness of bisimilar and compare_automata if you pass same…
Browse files Browse the repository at this point in the history
… object twice
  • Loading branch information
emuskardin committed Jun 22, 2024
1 parent 7957455 commit f7693b5
Showing 1 changed file with 9 additions and 1 deletion.
10 changes: 9 additions & 1 deletion aalpy/utils/ModelChecking.py
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand Down Expand Up @@ -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
Expand Down

0 comments on commit f7693b5

Please sign in to comment.