Feature #5586
closed
[guarded-action] [extraction] Представление переходов в начальное состояние, выполняемых по сбросу
Added by Igor Melnichenko over 9 years ago.
Updated about 9 years ago.
Published in build:
20150307
Description
В EFSM, извлекаемом из b11, переходы по сбросу имеют пустой список чувствительности охранное выражение {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}.
Исходному коду больше бы соответствовал список чувствительности {clock, reset} и охранное выражение {(EQ RESET 1)}.
Также в EFSM b11 есть ещё несколько переходов с пустым списком чувствительности, хотя они должны происходит про фронту сигнала clock. Например:
{source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 8)) (AND (AND (GREATEREQ CONT 0) (LESSEQ CONT 63)) (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2)) (LESS CONT 25)))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 8)) (AND (NOT (EQ STATO 0)) (EQ STATO 1))); guarded action: {{}: {predicate: (AND (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)))) (AND (AND (GREATEREQ R_IN 0) (LESSEQ R_IN 63)) (OR (EQ RESET 1) (EQ RESET 0))))}->{{assignment: STATO:= 1}}}}
- Status changed from New to Open
- Status changed from Open to Resolved
- % Done changed from 0 to 100
- Published in build set to r1491
Поправил, теперь пустых списков чувствительности вроде не наблюдается.
Охранное условие имеет такой вид, потому что включает в себя инвариант на сигнал.
- Status changed from Resolved to Verified
- Status changed from Verified to Closed
- Published in build changed from r1491 to 20150307
Also available in: Atom
PDF