Follow-эквивалентность

[TonitaN]

Определение follow-эквивалентности:

состояния follow-эквивалентны, если совпадает их follow-множество, и их финальность совпадает

То, что второе условие мы игнорируем при построении IlieYu, можно видеть по следующему отчёту:

rendered_report.pdf

Кстати, скорее всего, после исправления этого и с новым удалением эпсилон-правил гипотезу удастся верифицировать! (контрпример, который показывает нюанс с игнорированием финальности, как раз пришёл от верификатора)

Я воспользуюсь кое-чьим дедлайнерством и пожелаю, чтобы этот баг был исправлен до релиза :)

[TonitaN]

P.S. - Ну вот так алгоритм Брзозовски работает:

Verify (Equal (Minimize.Thompson *) (MergeBisim.Determinize.Reverse.Determinize.Reverse.Thompson *)) 100

Почему не работает без слияния, непонятно. Если верить стандартным алгоритмам детерминизации путём построения подмножеств, вроде как и не должен.

[TonitaN]

После расширения алфавита и исключения случая нескольких финальных состояний (введением "эндмаркеров" начала и конца регулярок в верифицируемых примерах) гипотеза про минимизацию Брзозовски даёт 100% результат для ДКА (на 1000 регулярок). Фишка в том, что варианты : (почти цитата) "безразлично, вводим ли мы несколько начальных состояний или новое начальное состояние с эпсилон-переходами во все бывшие финальные" после реверсирования - дают не эквивалентные результаты при стандартном алгоритме детерминизации (методом подмножеств). И у Брзозовски подразумевается симметричность: возможность введения нескольких начальных.

(попутно исправлена пара багов: один в методе Test с бесконечным парсингом по эпсилон-НКА, а другой традиционно с автоматами-ловушками, впрочем, это уже не сюда)