Task #5551
closed
[efsm] [extraction] Избыточные условия в состояниях
Added by Igor Melnichenko over 9 years ago.
Updated over 9 years ago.
Description
На примере b11:
Все извлечённые состояния включают в себя предикат (AND (GREATEREQ STATO 0) (LESSEQ STATO 8)) в дополнение к предикатам вида (EQ STATO const). Также некоторые дополнительно включают условия вида (NOT (EQ STATO const)).
Упрощение таких условий существенно облегчило бы отладку.
- Status changed from New to Feedback
1. Предикат вида (AND (GREATEREQ STATO 0) (LESSEQ STATO 8)) в b11 - это т.н. инвариант типа, полученный путем преобразования декларации:
variable stato: integer range 8 downto 0;
2. Предикаты вида (NOT (EQ STATO const)) в состояниях - следствие работы процедуры канонизации, которая для списка выражений вида {x == a_i}, i=1,N возвращает такие попарно несовместные конъюнкции:
(x == a_1) && !(x == a_2) && ... && !(x == a_n)
...
NOT(x == a_1) && !(x == a_2) && ... && (x == a_n)
Процедуру "упрощения вообще" для таких выражений я придумать затрудняюсь, если есть конкретная идея реализации, просьба её указать. В таком случае задача будет перенесена в проект Fortress и будет решаться там. Вот примеры уже реализованных в Fortress процедур упрощения выражений: http://forge.ispras.ru/issues/5424, http://forge.ispras.ru/issues/5419
- Target version set to 0.1
- Status changed from Feedback to Closed
Создал задачу в Fortress по простому случаю второго пункта.
Also available in: Atom
PDF