add fja_checker for hsExprTest

41b36c4f · Kateřina Sloupová · 59bf694e · 41b36c4f · 41b36c4f · 41b36c4f
Commit 41b36c4f authored Mar 05, 2020 by Kateřina Sloupová
--- a/DFA_grammar.g4
+++ b/DFA_grammar.g4
@@ -23,7 +23,7 @@ RIGHT_PARENTHESIS : ')';
 LEFT_BRACKET      : '{';
 RIGHT_BRACKET     : '}';
 COMMA             : ',';
-FINAL             : 'final';
+FINAL             : ('final' | 'F');
 STATE             : [a-zA-Z0-9]+;

 /* Characters to be ignored */

--- a/DFA_grammar.interp
+++ b/DFA_grammar.interp
@@ -7,7 +7,7 @@ null
 '{'
 '}'
 ','
-'final'
+null
 null
 null


--- a/DFA_grammar.tokens
+++ b/DFA_grammar.tokens
@@ -15,4 +15,3 @@ WS=10
 '{'=5
 '}'=6
 ','=7
-'final'=8
--- a/DFA_grammarLexer.interp
+++ b/DFA_grammarLexer.interp
@@ -7,7 +7,7 @@ null
 '{'
 '}'
 ','
-'final'
+null
 null
 null

@@ -44,4 +44,4 @@ mode names:
 DEFAULT_MODE

 atn:
-[3, 24715, 42794, 33075, 47597, 16764, 15335, 30598, 22884, 2, 12, 58, 8, 1, 4, 2, 9, 2, 4, 3, 9, 3, 4, 4, 9, 4, 4, 5, 9, 5, 4, 6, 9, 6, 4, 7, 9, 7, 4, 8, 9, 8, 4, 9, 9, 9, 4, 10, 9, 10, 4, 11, 9, 11, 3, 2, 3, 2, 3, 2, 3, 2, 3, 2, 3, 3, 3, 3, 3, 4, 3, 4, 3, 5, 3, 5, 3, 6, 3, 6, 3, 7, 3, 7, 3, 8, 3, 8, 3, 9, 3, 9, 3, 9, 3, 9, 3, 9, 3, 9, 3, 10, 6, 10, 48, 10, 10, 13, 10, 14, 10, 49, 3, 11, 6, 11, 53, 10, 11, 13, 11, 14, 11, 54, 3, 11, 3, 11, 2, 2, 12, 3, 3, 5, 4, 7, 5, 9, 6, 11, 7, 13, 8, 15, 9, 17, 10, 19, 11, 21, 12, 3, 2, 4, 5, 2, 50, 59, 67, 92, 99, 124, 5, 2, 11, 12, 15, 15, 34, 34, 2, 59, 2, 3, 3, 2, 2, 2, 2, 5, 3, 2, 2, 2, 2, 7, 3, 2, 2, 2, 2, 9, 3, 2, 2, 2, 2, 11, 3, 2, 2, 2, 2, 13, 3, 2, 2, 2, 2, 15, 3, 2, 2, 2, 2, 17, 3, 2, 2, 2, 2, 19, 3, 2, 2, 2, 2, 21, 3, 2, 2, 2, 3, 23, 3, 2, 2, 2, 5, 28, 3, 2, 2, 2, 7, 30, 3, 2, 2, 2, 9, 32, 3, 2, 2, 2, 11, 34, 3, 2, 2, 2, 13, 36, 3, 2, 2, 2, 15, 38, 3, 2, 2, 2, 17, 40, 3, 2, 2, 2, 19, 47, 3, 2, 2, 2, 21, 52, 3, 2, 2, 2, 23, 24, 7, 107, 2, 2, 24, 25, 7, 112, 2, 2, 25, 26, 7, 107, 2, 2, 26, 27, 7, 118, 2, 2, 27, 4, 3, 2, 2, 2, 28, 29, 7, 63, 2, 2, 29, 6, 3, 2, 2, 2, 30, 31, 7, 42, 2, 2, 31, 8, 3, 2, 2, 2, 32, 33, 7, 43, 2, 2, 33, 10, 3, 2, 2, 2, 34, 35, 7, 125, 2, 2, 35, 12, 3, 2, 2, 2, 36, 37, 7, 127, 2, 2, 37, 14, 3, 2, 2, 2, 38, 39, 7, 46, 2, 2, 39, 16, 3, 2, 2, 2, 40, 41, 7, 104, 2, 2, 41, 42, 7, 107, 2, 2, 42, 43, 7, 112, 2, 2, 43, 44, 7, 99, 2, 2, 44, 45, 7, 110, 2, 2, 45, 18, 3, 2, 2, 2, 46, 48, 9, 2, 2, 2, 47, 46, 3, 2, 2, 2, 48, 49, 3, 2, 2, 2, 49, 47, 3, 2, 2, 2, 49, 50, 3, 2, 2, 2, 50, 20, 3, 2, 2, 2, 51, 53, 9, 3, 2, 2, 52, 51, 3, 2, 2, 2, 53, 54, 3, 2, 2, 2, 54, 52, 3, 2, 2, 2, 54, 55, 3, 2, 2, 2, 55, 56, 3, 2, 2, 2, 56, 57, 8, 11, 2, 2, 57, 22, 3, 2, 2, 2, 5, 2, 49, 54, 3, 8, 2, 2]
\ No newline at end of file
+[3, 24715, 42794, 33075, 47597, 16764, 15335, 30598, 22884, 2, 12, 60, 8, 1, 4, 2, 9, 2, 4, 3, 9, 3, 4, 4, 9, 4, 4, 5, 9, 5, 4, 6, 9, 6, 4, 7, 9, 7, 4, 8, 9, 8, 4, 9, 9, 9, 4, 10, 9, 10, 4, 11, 9, 11, 3, 2, 3, 2, 3, 2, 3, 2, 3, 2, 3, 3, 3, 3, 3, 4, 3, 4, 3, 5, 3, 5, 3, 6, 3, 6, 3, 7, 3, 7, 3, 8, 3, 8, 3, 9, 3, 9, 3, 9, 3, 9, 3, 9, 3, 9, 5, 9, 47, 10, 9, 3, 10, 6, 10, 50, 10, 10, 13, 10, 14, 10, 51, 3, 11, 6, 11, 55, 10, 11, 13, 11, 14, 11, 56, 3, 11, 3, 11, 2, 2, 12, 3, 3, 5, 4, 7, 5, 9, 6, 11, 7, 13, 8, 15, 9, 17, 10, 19, 11, 21, 12, 3, 2, 4, 5, 2, 50, 59, 67, 92, 99, 124, 5, 2, 11, 12, 15, 15, 34, 34, 2, 62, 2, 3, 3, 2, 2, 2, 2, 5, 3, 2, 2, 2, 2, 7, 3, 2, 2, 2, 2, 9, 3, 2, 2, 2, 2, 11, 3, 2, 2, 2, 2, 13, 3, 2, 2, 2, 2, 15, 3, 2, 2, 2, 2, 17, 3, 2, 2, 2, 2, 19, 3, 2, 2, 2, 2, 21, 3, 2, 2, 2, 3, 23, 3, 2, 2, 2, 5, 28, 3, 2, 2, 2, 7, 30, 3, 2, 2, 2, 9, 32, 3, 2, 2, 2, 11, 34, 3, 2, 2, 2, 13, 36, 3, 2, 2, 2, 15, 38, 3, 2, 2, 2, 17, 46, 3, 2, 2, 2, 19, 49, 3, 2, 2, 2, 21, 54, 3, 2, 2, 2, 23, 24, 7, 107, 2, 2, 24, 25, 7, 112, 2, 2, 25, 26, 7, 107, 2, 2, 26, 27, 7, 118, 2, 2, 27, 4, 3, 2, 2, 2, 28, 29, 7, 63, 2, 2, 29, 6, 3, 2, 2, 2, 30, 31, 7, 42, 2, 2, 31, 8, 3, 2, 2, 2, 32, 33, 7, 43, 2, 2, 33, 10, 3, 2, 2, 2, 34, 35, 7, 125, 2, 2, 35, 12, 3, 2, 2, 2, 36, 37, 7, 127, 2, 2, 37, 14, 3, 2, 2, 2, 38, 39, 7, 46, 2, 2, 39, 16, 3, 2, 2, 2, 40, 41, 7, 104, 2, 2, 41, 42, 7, 107, 2, 2, 42, 43, 7, 112, 2, 2, 43, 44, 7, 99, 2, 2, 44, 47, 7, 110, 2, 2, 45, 47, 7, 72, 2, 2, 46, 40, 3, 2, 2, 2, 46, 45, 3, 2, 2, 2, 47, 18, 3, 2, 2, 2, 48, 50, 9, 2, 2, 2, 49, 48, 3, 2, 2, 2, 50, 51, 3, 2, 2, 2, 51, 49, 3, 2, 2, 2, 51, 52, 3, 2, 2, 2, 52, 20, 3, 2, 2, 2, 53, 55, 9, 3, 2, 2, 54, 53, 3, 2, 2, 2, 55, 56, 3, 2, 2, 2, 56, 54, 3, 2, 2, 2, 56, 57, 3, 2, 2, 2, 57, 58, 3, 2, 2, 2, 58, 59, 8, 11, 2, 2, 59, 22, 3, 2, 2, 2, 6, 2, 46, 51, 56, 3, 8, 2, 2]
\ No newline at end of file
--- a/DFA_grammarLexer.py
+++ b/DFA_grammarLexer.py
 # Generated from DFA_grammar.g4 by ANTLR 4.8
-from antlr4 import * # type: ignore
+from antlr4 import *
 from io import StringIO
 from typing.io import TextIO
 import sys
@@ -9,26 +9,27 @@ import sys
 def serializedATN():
    with StringIO() as buf:
        buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2\f")
-        buf.write(":\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7")
+        buf.write("<\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7")
        buf.write("\4\b\t\b\4\t\t\t\4\n\t\n\4\13\t\13\3\2\3\2\3\2\3\2\3\2")
        buf.write("\3\3\3\3\3\4\3\4\3\5\3\5\3\6\3\6\3\7\3\7\3\b\3\b\3\t\3")
-        buf.write("\t\3\t\3\t\3\t\3\t\3\n\6\n\60\n\n\r\n\16\n\61\3\13\6\13")
-        buf.write("\65\n\13\r\13\16\13\66\3\13\3\13\2\2\f\3\3\5\4\7\5\t\6")
-        buf.write("\13\7\r\b\17\t\21\n\23\13\25\f\3\2\4\5\2\62;C\\c|\5\2")
-        buf.write("\13\f\17\17\"\"\2;\2\3\3\2\2\2\2\5\3\2\2\2\2\7\3\2\2\2")
-        buf.write("\2\t\3\2\2\2\2\13\3\2\2\2\2\r\3\2\2\2\2\17\3\2\2\2\2\21")
-        buf.write("\3\2\2\2\2\23\3\2\2\2\2\25\3\2\2\2\3\27\3\2\2\2\5\34\3")
-        buf.write("\2\2\2\7\36\3\2\2\2\t \3\2\2\2\13\"\3\2\2\2\r$\3\2\2\2")
-        buf.write("\17&\3\2\2\2\21(\3\2\2\2\23/\3\2\2\2\25\64\3\2\2\2\27")
-        buf.write("\30\7k\2\2\30\31\7p\2\2\31\32\7k\2\2\32\33\7v\2\2\33\4")
-        buf.write("\3\2\2\2\34\35\7?\2\2\35\6\3\2\2\2\36\37\7*\2\2\37\b\3")
-        buf.write("\2\2\2 !\7+\2\2!\n\3\2\2\2\"#\7}\2\2#\f\3\2\2\2$%\7\177")
-        buf.write("\2\2%\16\3\2\2\2&\'\7.\2\2\'\20\3\2\2\2()\7h\2\2)*\7k")
-        buf.write("\2\2*+\7p\2\2+,\7c\2\2,-\7n\2\2-\22\3\2\2\2.\60\t\2\2")
-        buf.write("\2/.\3\2\2\2\60\61\3\2\2\2\61/\3\2\2\2\61\62\3\2\2\2\62")
-        buf.write("\24\3\2\2\2\63\65\t\3\2\2\64\63\3\2\2\2\65\66\3\2\2\2")
-        buf.write("\66\64\3\2\2\2\66\67\3\2\2\2\678\3\2\2\289\b\13\2\29\26")
-        buf.write("\3\2\2\2\5\2\61\66\3\b\2\2")
+        buf.write("\t\3\t\3\t\3\t\3\t\5\t/\n\t\3\n\6\n\62\n\n\r\n\16\n\63")
+        buf.write("\3\13\6\13\67\n\13\r\13\16\138\3\13\3\13\2\2\f\3\3\5\4")
+        buf.write("\7\5\t\6\13\7\r\b\17\t\21\n\23\13\25\f\3\2\4\5\2\62;C")
+        buf.write("\\c|\5\2\13\f\17\17\"\"\2>\2\3\3\2\2\2\2\5\3\2\2\2\2\7")
+        buf.write("\3\2\2\2\2\t\3\2\2\2\2\13\3\2\2\2\2\r\3\2\2\2\2\17\3\2")
+        buf.write("\2\2\2\21\3\2\2\2\2\23\3\2\2\2\2\25\3\2\2\2\3\27\3\2\2")
+        buf.write("\2\5\34\3\2\2\2\7\36\3\2\2\2\t \3\2\2\2\13\"\3\2\2\2\r")
+        buf.write("$\3\2\2\2\17&\3\2\2\2\21.\3\2\2\2\23\61\3\2\2\2\25\66")
+        buf.write("\3\2\2\2\27\30\7k\2\2\30\31\7p\2\2\31\32\7k\2\2\32\33")
+        buf.write("\7v\2\2\33\4\3\2\2\2\34\35\7?\2\2\35\6\3\2\2\2\36\37\7")
+        buf.write("*\2\2\37\b\3\2\2\2 !\7+\2\2!\n\3\2\2\2\"#\7}\2\2#\f\3")
+        buf.write("\2\2\2$%\7\177\2\2%\16\3\2\2\2&\'\7.\2\2\'\20\3\2\2\2")
+        buf.write("()\7h\2\2)*\7k\2\2*+\7p\2\2+,\7c\2\2,/\7n\2\2-/\7H\2\2")
+        buf.write(".(\3\2\2\2.-\3\2\2\2/\22\3\2\2\2\60\62\t\2\2\2\61\60\3")
+        buf.write("\2\2\2\62\63\3\2\2\2\63\61\3\2\2\2\63\64\3\2\2\2\64\24")
+        buf.write("\3\2\2\2\65\67\t\3\2\2\66\65\3\2\2\2\678\3\2\2\28\66\3")
+        buf.write("\2\2\289\3\2\2\29:\3\2\2\2:;\b\13\2\2;\26\3\2\2\2\6\2")
+        buf.write(".\638\3\b\2\2")
        return buf.getvalue()


@@ -54,7 +55,7 @@ class DFA_grammarLexer(Lexer):
    modeNames = [ "DEFAULT_MODE" ]

    literalNames = [ "<INVALID>",
-            "'init'", "'='", "'('", "')'", "'{'", "'}'", "','", "'final'" ]
+            "'init'", "'='", "'('", "')'", "'{'", "'}'", "','" ]

    symbolicNames = [ "<INVALID>",
            "INIT", "EQUALS", "LEFT_PARENTHESIS", "RIGHT_PARENTHESIS", "LEFT_BRACKET", 

--- a/DFA_grammarLexer.tokens
+++ b/DFA_grammarLexer.tokens
@@ -15,4 +15,3 @@ WS=10
 '{'=5
 '}'=6
 ','=7
-'final'=8
--- a/DFA_grammarListener.py
+++ b/DFA_grammarListener.py
 # Generated from DFA_grammar.g4 by ANTLR 4.8
-from antlr4 import * # type: ignore
+from antlr4 import *
 if __name__ is not None and "." in __name__:
    from .DFA_grammarParser import DFA_grammarParser
 else:

--- a/DFA_grammarParser.py
+++ b/DFA_grammarParser.py
 # Generated from DFA_grammar.g4 by ANTLR 4.8
 # encoding: utf-8
-from antlr4 import * # type: ignore
+from antlr4 import *
 from io import StringIO
 import sys
 if sys.version_info[1] > 5:
@@ -42,7 +42,7 @@ class DFA_grammarParser ( Parser ):
    sharedContextCache = PredictionContextCache()

    literalNames = [ "<INVALID>", "'init'", "'='", "'('", "')'", "'{'", 
-                     "'}'", "','", "'final'" ]
+                     "'}'", "','" ]

    symbolicNames = [ "<INVALID>", "INIT", "EQUALS", "LEFT_PARENTHESIS", 
                      "RIGHT_PARENTHESIS", "LEFT_BRACKET", "RIGHT_BRACKET", 

--- a/demo.py
+++ b/demo.py
@@ -4,6 +4,7 @@ from reg_automata import Composition as comp
 from reg_grammars import REG, Terminal, Nonterminal
 from typing import Set, Dict, Tuple, Union
 from copy import deepcopy
+from antlr4 import RecognitionException


 def make_dfa(states: Set[str], characters: Set[str],
@@ -84,6 +85,18 @@ def nfa_e():
    nfae = NFAE({q0, q1, q2, q3, q4}, {a, b, c, d}, transition, q0, {q2})
    return nfae

+def dfa_eq(str1, str2):
+    try:
+        parser = Parser()
+        dfa1 = parser.str_to_dfa(str1)
+        print(parser.dfa_to_str(dfa1))
+        dfa2 = parser.str_to_dfa(str2)
+        print(parser.dfa_to_str(dfa2))
+        return dfa1.is_equivalent(dfa2)
+
+    except RecognitionException as re:
+        print(re)
+

 def main():
    dfa_1 = make_dfa({"q_0", "q_1"}, {"a"}, {("q_0", "a"): "q_1", ("q_1", "a"): "q_1"}, "q_0", {"q_1"})
@@ -234,15 +247,20 @@ def main():
    print(parser.nfa_to_str(nfae))
    print()
    nfa_elim = nfae.eliminate_epsilon()
-    print(parser.nfa_to_str(nfa_elim, True))
+    print(parser.nfa_to_str(nfa_elim))

    print("__________________________________")
-    print("Parsers")
+    print("Testing parsers")
    print("Input of parser.str_to_dfa:")
    print("init=0 (0,x)=1 (0,y)=2 (1,x)=1 (1,y)=1 (2,x)=0 (2,y)=4 (3,x)=2 (3,y)=5 (4,x)=3 (4,y)=0 (5,x)=5 (5,y)=5 final={4,5}")
    dfa_p = parser.str_to_dfa("init=0 (0,x)=1 (0,y)=2 (1,x)=1 (1,y)=1 (2,x)=0 (2,y)=4 (3,x)=2 (3,y)=5 (4,x)=3 (4,y)=0 (5,x)=5 (5,y)=5 final={4,5}")
    print("Output of parser.dfa_to_str should be identical:")
    print(parser.dfa_to_str(dfa_p))
+    print()
+    print("Try equality of automata from strings:")
+    str1 = "init=0 (0, a)=1 (0, b)=2 (1, a)=1 (2,b)=2 F={1,2}"
+    str2 = "init=q1 (q1, a)=q2 (q1, b)=q3 (q2,a)=q2 (q3,b)=q4 (q4,b)=q4 final={q3,q4,q2}"
+    print(dfa_eq(str1, str2))


 main()
\ No newline at end of file
--- a/fja_checker.py
+++ b/fja_checker.py
+from parser import Parser
+from reg_automata import DFA
+from antlr4 import RecognitionException # type: ignore
+import sys
+
+
+def transformation(solution: str, solution_type: str) -> DFA:
+    if solution_type == "DFA":
+        parser = Parser()
+        return parser.str_to_dfa(solution)
+    elif solution_type == "NFA":
+        parser = Parser()
+        nfa = parser.str_to_nfa(solution)
+        return nfa.determinize()
+    #elif solution_type == "EFA":
+    #    parser = Parser()
+    #    efa = parser.str_to_efa(solution)
+    #    return efa.eliminate_epsilon.determinize()
+
+def main():
+    with open(sys.argv[1]) as student_file:
+        student_solution = student_file.read()
+
+    for argument in sys.argv:
+        if argument[:2] == "-o":
+            teacher_solution = argument[2:]
+
+    task, teacher_solution = teacher_solution.split(":", 1)
+    student_type, teacher_type = task.split("-", 1)
+    student_dfa = transformation(student_solution, student_type)
+    teacher_dfa = transformation(teacher_solution, teacher_type[:3])
+
+    try:
+        parser = Parser()
+        result = student_dfa.is_equivalent(teacher_dfa)
+        if result:
+            exit(0)
+        else:
+            student_word, teacher_word = result.left_counterexample, result.right_counterexample
+            print("Hláška, že to není správně.")
+            print("Příklad slova, které je ve studentově řešení a není v zadaném jazyce: ", student_word)
+            print("Příklad slova, které chybí ve studentově řešení a je v zadaném jazyce: ", teacher_word)
+            exit(1)
+
+    except RecognitionException as ex:
+        print(ex)
+
+main()
\ No newline at end of file
--- a/parser.py
+++ b/parser.py
@@ -6,8 +6,11 @@ import antlr4 # type: ignore
 from DFA_grammarLexer import DFA_grammarLexer
 from DFA_grammarParser import DFA_grammarParser
 from DFA_grammarListener import DFA_grammarListener
+from NFA_grammarLexer import NFA_grammarLexer
+from NFA_grammarParser import NFA_grammarParser
+from NFA_grammarListener import NFA_grammarListener
+

-# TODO ask: commas at the ends of lines or not?
 class Parser:
    def __init__(self):
        pass
@@ -86,7 +89,7 @@ class Parser:
            elif isinstance(character, Character) and isinstance(nfa, NFA):
                dest_states = nfa.transition[state, character]
            transition += "(" + state.name + "," + char + ")={" + \
-                          ','.join(set(map(lambda x: x.name, dest_states))) + "}\n"
+                          ','.join(set(map(lambda x: x.name, dest_states))) + "} "

        init = "init=" + nfa.init.name
        final = "final={" + ','.join(set(map(lambda x: x.name, nfa.final))) + "}"
@@ -96,24 +99,37 @@ class Parser:
                   init + ", " + final + ")\n" + transition

        else:
-            return transition + "\n" + final
+            return init + " " + transition + " " + final


-    def str_to_dfa(self, input: str):
-        input = "init=0 (0,x)=1 (0,y)=2 (1,x)=1 (1,y)=1 (2,x)=0 (2,y)=4 (3,x)=2 (3,y)=5 (4,x)=3 (4,y)=0 (5,x)=5 (5,y)=5 final={4,5}"
-        chars = antlr4.InputStream(input)
+    def str_to_dfa(self, string: str) -> DFA:
+        chars = antlr4.InputStream(string)
        lexer = DFA_grammarLexer(chars)
        tokens = antlr4.CommonTokenStream(lexer)
        parser = DFA_grammarParser(tokens)

        tree = parser.start()
-        printer = StatenamePrinter()
+        printer = DFAPrinter()
        walker = antlr4.ParseTreeWalker()
        walker.walk(printer, tree)
        dfa = DFA(printer.states, printer.characters, printer.transition, printer.init, printer.final)
        return dfa

-class StatenamePrinter(DFA_grammarListener):
+    def str_to_nfa(self, string: str) -> NFA:
+        chars = antlr4.InputStream(string)
+        lexer = NFA_grammarLexer(chars)
+        tokens = antlr4.CommonTokenStream(lexer)
+        parser = NFA_grammarParser(tokens)
+
+        tree = parser.start()
+        printer = NFAPrinter()
+        walker = antlr4.ParseTreeWalker()
+        walker.walk(printer, tree)
+        nfa = NFA(printer.states, printer.characters, printer.transition, printer.init, printer.final)
+        return nfa
+
+
+class DFAPrinter(DFA_grammarListener):
    def __init__(self):
        self.states = set()
        self.characters = set()
@@ -142,3 +158,37 @@ class StatenamePrinter(DFA_grammarListener):
            self.states.add(state)
            self.final.add(state)
            i += 1
+
+class NFAPrinter(NFA_grammarListener):
+    def __init__(self):
+        self.states = set()
+        self.characters = set()
+        self.transition = {}
+        self.init = State("")
+        self.final = set()
+
+    def exitInit(self, ctx):
+        state = State(str(ctx.statename().STATE()))
+        self.init = state
+        self.states.add(state)
+
+    def exitProduction(self, ctx):
+        state = State(str(ctx.statename(0).STATE()))
+        character = Character(str(ctx.statename(1).STATE()))
+        self.states.add(state)
+        self.characters.add(character)
+
+        i = 0
+        while ctx.stateset().statename(i) is not None:
+            state = State(str(ctx.stateset().statename(i).STATE()))
+            self.states.add(state)
+            self.final.add(state)
+            i += 1
+
+    def exitFinal(self, ctx):
+        i = 0
+        while ctx.statename(i) is not None:
+            state = State(str(ctx.statename(i).STATE()))
+            self.states.add(state)
+            self.final.add(state)
+            i += 1
\ No newline at end of file
--- a/reg_automata.py
+++ b/reg_automata.py
@@ -12,6 +12,21 @@ class Composition(Enum):
    Subtraction = enum.auto()


+class IsEmptyResult:
+  def __init__(self, counterexample : Optional[...] = None):
+    self.counterexample = counterexample
+
+  def __bool__(self):
+    return self.counterexample is None
+
+class IsEquivalentResult:
+  def __init__(self, left_counterexample : Optional[...] = None, right_counterexample : Optional[...] = None):
+    self.left_counterexample = left_counterexample
+    self.right_counterexample = right_counterexample
+
+  def __bool__(self):
+    return self.left_counterexample is None and self.right_counterexample is None
+
 class Character:
    def __init__(self, name: str):
        self.name = name
@@ -63,7 +78,7 @@ class DFA:
        self.transition = transition
        self.init = init
        self.final = final
-        #assert self.check()
+        assert self.check()

    def check(self) -> bool:
        assert len(self.states) > 0, "empty automaton"
@@ -391,7 +406,7 @@ class DFA:
                        predecessor[dest_state] = (actual, character)

        if len(reachable.intersection(self.final)) == 0:
-            return True
+            return IsEmptyResult()
        else:
            word = []
            state = reachable.intersection(self.final).pop()
@@ -399,16 +414,23 @@ class DFA:
                word.append(predecessor[state][1].name)
                state = predecessor[state][0]

-            counterexample = ''.join(reversed(word))
-            return False
+            counterexample = IsEmptyResult(''.join(reversed(word)))
+            return counterexample

    # Ha!
    def is_universal(self):
        return self.complement().is_empty()

+    # returns: True or (1. what IS in first language (self) and NOT in second (dfa), 2. analogically)
    def is_equivalent(self, dfa: DFA) -> bool:
-        return self.intersection(self, dfa.complement()).is_empty() and \
-               self.intersection(self.complement(), dfa).is_empty()
+        left_empty = self.intersection(self, dfa.complement()).is_empty()
+        right_empty = self.intersection(self.complement(), dfa).is_empty()
+        if left_empty and right_empty:
+            result = IsEquivalentResult()
+        else:
+            result = IsEquivalentResult(left_empty.counterexample, right_empty.counterexample)
+        return result
+

    def is_part_identical(self, dfa: DFA) -> bool:
        return self.states == dfa.states and self.characters == dfa.characters and \