Во-первых, для MFA в проверке на бисимуляцию лучше возвращать OptionalBool, поскольку если есть циклические зависимости ссылок, то пока не ясно, что с этим делать.
Во-вторых, слабую (action-bisimilarity) и буквальную (ту, которую обсуждали в ТГ, с выносом действий над памятью в алфавит) тоже полезно иметь в интерфейсе интерпретатора для верификаторов гипотез и поиска контрпримеров.
[ ] - раскрашивать решающие действия в определённые цвета, причём сопоставленные друг другу action-бисимилярные действия после сужения по достижимости должны быть раскрашены в один и тот же цвет
[ ] - хорошо бы дополнительно выводить частичный порядок на решающих действиях, для начала в виде таблицы, или можно в форме автомата, где есть собственно только состояния с решающими действиями.
По базе:
[x] - добавить MergeBisim - для начала по symbolic bisimulation relation, а дальше уточним
Во-первых, для MFA в проверке на бисимуляцию лучше возвращать
OptionalBool
, поскольку если есть циклические зависимости ссылок, то пока не ясно, что с этим делать.Во-вторых, слабую (action-bisimilarity) и буквальную (ту, которую обсуждали в ТГ, с выносом действий над памятью в алфавит) тоже полезно иметь в интерфейсе интерпретатора для верификаторов гипотез и поиска контрпримеров.