Project

General

Profile

Task #5551

[efsm] [extraction] Избыточные условия в состояниях

Added by Igor Melnichenko over 4 years ago. Updated over 4 years ago.

Status:
Closed
Priority:
Normal
Assignee:
Category:
-
Target version:
Start date:
01/12/2015
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Published in build:

Description

На примере b11:
Все извлечённые состояния включают в себя предикат (AND (GREATEREQ STATO 0) (LESSEQ STATO 8)) в дополнение к предикатам вида (EQ STATO const). Также некоторые дополнительно включают условия вида (NOT (EQ STATO const)).
Упрощение таких условий существенно облегчило бы отладку.

History

#1

Updated by Sergey Smolov over 4 years ago

  • 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

#2

Updated by Sergey Smolov over 4 years ago

  • Target version set to 0.1
#3

Updated by Igor Melnichenko over 4 years ago

  • Status changed from Feedback to Closed

Создал задачу в Fortress по простому случаю второго пункта.

Also available in: Atom PDF