Added by Igor Melnichenko almost 10 years ago. Updated over 9 years ago.
100%
Description
Необходимо извлекать ограничения на значения всех переменных из их объявлений (как сейчас делается для переменных состояния).
Дополнительно предлагаю вынести такие ограничения из состояний в отдельное поле класса VariableData.
Действительно, сейчас инварианты на переменные учитываются только при построении состояний. Будет исправлено.
Помещать инвариант в объект VariableData, который потом кладется в ту же Node Variable - это решение порождает рекурсию (в поле userData объекта NodeVariable будет лежать выражение, которое исопльзует ту же самую переменную). Предлагаю в архитектурном плане оставить все как есть, т.е. хранить инварианты на переменные в ассоциированных с ними объектах VariableDeclaration.
А VariableDeclaration существует только на уровне CFG?
Нужно как-то передать эту информацию в EFSM, чтобы генератор тестов и симулятор могли ей пользоваться.
Да, только на уровне CFG.
Если нужно, можно хранить инварианты на переменные также и в EFSM.
Но тикет-то носит префикс "[efsm][extraction]". То, что ты предлагаешь, я сделать могу, но на это лучше бы другой тикет создать.