Feature #5586
closed[guarded-action] [extraction] Представление переходов в начальное состояние, выполняемых по сбросу
100%
Description
В EFSM, извлекаемом из b11, переходы по сбросу имеют пустой список чувствительности охранное выражение {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}.
Исходному коду больше бы соответствовал список чувствительности {clock, reset} и охранное выражение {(EQ RESET 1)}.
Updated by Igor Melnichenko almost 10 years ago
Также в 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}}}}
Updated by Sergey Smolov almost 10 years ago
- Status changed from Open to Resolved
- % Done changed from 0 to 100
- Published in build set to r1491
Поправил, теперь пустых списков чувствительности вроде не наблюдается.
Охранное условие имеет такой вид, потому что включает в себя инвариант на сигнал.
Updated by Igor Melnichenko over 9 years ago
- Status changed from Resolved to Verified
Updated by Sergey Smolov over 9 years ago
- Status changed from Verified to Closed
- Published in build changed from r1491 to 20150307