Project

General

Profile

Developer Request #5632

Избыточные переходы в b11

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

Status:
Closed
Priority:
Normal
Assignee:
Category:
Engine (Transformer)
Target version:
Start date:
02/15/2015
Due date:
% Done:

100%

Estimated time:
Published in build:

Description

Автомат b11 был бы проще, если бы в качестве переменной состояния извлекалась только STATO. Например, код
when s_spazio=>
if r_in=0 or r_in=63 then
if cont<25 then
cont:=cont+1;
else
cont:=0;
end if;
cont1:=r_in;
stato:=s_dataout;
elsif r_in<=26 then
stato:=s_mul;
else
stato:=s_datain;
end if;

сейчас преобразуется в два состояния:
(AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2)) (LESS CONT 25))
(AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2)) (NOT (LESS CONT 25)))

и десять переходов: {source state: (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2)) (LESS CONT 25)); destination state: (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (EQ STATO 8)) (NOT (LESS CONT1 0))); guarded action: {{posedge of CLOCK}: {predicate: (AND (OR (EQ R_IN 0) (EQ R_IN 63)) (NOT (LESS R_IN 0)) (NOT (EQ RESET 1)))}->{{assignment: CONT := (ADD CONT 1); assignment: CONT1 := R_IN; assignment: STATO := 8}}}} {source state: (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2)) (NOT (LESS CONT 25))); destination state: (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (EQ STATO 8)) (NOT (LESS CONT1 0))); guarded action: {{posedge of CLOCK}: {predicate: (AND (OR (EQ R_IN 0) (EQ R_IN 63)) (NOT (LESS R_IN 0)) (NOT (EQ RESET 1)))}->{{assignment: CONT := 0; assignment: CONT1 := R_IN; assignment: STATO := 8}}}}

{source state: (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2)) (LESS CONT 25)); destination state: (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (EQ STATO 3)); guarded action: {{posedge of CLOCK}: {predicate: (AND (NOT (EQ RESET 1)) (NOT (OR (EQ R_IN 0) (EQ R_IN 63))) (OR (LESS R_IN 26) (EQ R_IN 26)))}->{{assignment: STATO := 3}}}} {source state: (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2)) (NOT (LESS CONT 25))); destination state: (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (EQ STATO 3)); guarded action: {{posedge of CLOCK}: {predicate: (AND (NOT (EQ RESET 1)) (NOT (OR (EQ R_IN 0) (EQ R_IN 63))) (OR (LESS R_IN 26) (EQ R_IN 26)))}->{{assignment: STATO := 3}}}}

{source state: (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2)) (LESS CONT 25)); destination state: (AND (NOT (EQ STATO 0)) (EQ STATO 1)); guarded action: {{posedge of CLOCK}: {predicate: (AND (NOT (EQ RESET 1)) (NOT (OR (EQ R_IN 0) (EQ R_IN 63))) (NOT (OR (LESS R_IN 26) (EQ R_IN 26))))}->{{assignment: STATO := 1}}}} {source state: (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2)) (NOT (LESS CONT 25))); destination state: (AND (NOT (EQ STATO 0)) (EQ STATO 1)); guarded action: {{posedge of CLOCK}: {predicate: (AND (NOT (EQ RESET 1)) (NOT (OR (EQ R_IN 0) (EQ R_IN 63))) (NOT (OR (LESS R_IN 26) (EQ R_IN 26))))}->{{assignment: STATO := 1}}}}

{source state: (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2)) (LESS CONT 25)); state: (EQ STATO 0); guarded action: {{CLOCK,RESET}: {predicate: (EQ RESET 1)}->{{assignment: STATO := 0; assignment: R_IN := 0; assignment: CONT := 0; assignment: CONT1 := 0; assignment: X_OUT := 0}}}} {source state: (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2)) (NOT (LESS CONT 25))); destination state: (EQ STATO 0); guarded action: {{CLOCK,RESET}: {predicate: (EQ RESET 1)}->{{assignment: STATO := 0; assignment: R_IN := 0; assignment: CONT := 0; assignment: CONT1 := 0; assignment: X_OUT := 0}}}}

{source state: (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2)) (NOT (LESS CONT 25))); destination state: (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (EQ STATO 8)) (LESS CONT1 0)); guarded action: {{posedge of CLOCK}: {predicate: (AND (OR (EQ R_IN 0) (EQ R_IN 63)) (LESS R_IN 0) (NOT (EQ RESET 1)))}->{{assignment: CONT := 0; assignment: CONT1 := R_IN; assignment: STATO := 8}}}} {source state: (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2)) (LESS CONT 25)); destination state: (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (EQ STATO 8)) (LESS CONT1 0)); guarded action: {{posedge of CLOCK}: {predicate: (AND (OR (EQ R_IN 0) (EQ R_IN 63)) (LESS R_IN 0) (NOT (EQ RESET 1)))}->{{assignment: CONT := (ADD CONT 1); assignment: CONT1 := R_IN; assignment: STATO := 8}}}}

При этом среди них есть три пары переходов с совпадающими GA и конечными состояниями. То есть исключение переменной CONT из числа переменных состояния позволило бы сократить количество переходов в данном случае с десяти до семи без потери информации и с сопутствующим упрощением обхода. Ещё два перехода можно было бы убрать, исключив CONT1
Я не знаю, какая эвристика используется для определения переменных состояния, поэтому конкретных предложений дать не могу. Возможно, стоит попробовать повысить минимальный порог по количеству вхождений переменной-кандидата в охранные выражения: кажется, для отсечения переменной cont этого будет достаточно (она встречается только в двух условиях).

History

#1

Updated by Sergey Smolov over 4 years ago

  • Subject changed from [efsm] [transition] Избыточные переходы в b11 to Избыточные переходы в b11
  • Category set to Engine (Transformer)
#2

Updated by Sergey Smolov about 4 years ago

  • Status changed from New to Resolved
  • % Done changed from 0 to 100

For user-defined state-like variables you may use "--state-vars" option of cgaa-efsm-transformer engine.
As for b11 design, run the tool with "--state-vars STATO" for the result you want.

#3

Updated by Sergey Smolov about 4 years ago

I've implemented B11CgaaEfsmTransformerTestCase which illustrated this option.

#4

Updated by Igor Melnichenko almost 4 years ago

  • Status changed from Resolved to Verified
#5

Updated by Sergey Smolov over 3 years ago

  • Status changed from Verified to Closed

Also available in: Atom PDF