Project

General

Profile

Feature #5586

[guarded-action] [extraction] Представление переходов в начальное состояние, выполняемых по сбросу

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

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

100%

Estimated time:
Published in build:
20150307

Description

В EFSM, извлекаемом из b11, переходы по сбросу имеют пустой список чувствительности охранное выражение {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}.

Исходному коду больше бы соответствовал список чувствительности {clock, reset} и охранное выражение {(EQ RESET 1)}.

History

#1

Updated by Igor Melnichenko over 5 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}}}}

#2

Updated by Sergey Smolov over 5 years ago

  • Status changed from New to Open
#3

Updated by Sergey Smolov over 5 years ago

  • Status changed from Open to Resolved
  • % Done changed from 0 to 100
  • Published in build set to r1491

Поправил, теперь пустых списков чувствительности вроде не наблюдается.
Охранное условие имеет такой вид, потому что включает в себя инвариант на сигнал.

#4

Updated by Igor Melnichenko over 5 years ago

  • Status changed from Resolved to Verified
#5

Updated by Sergey Smolov over 5 years ago

  • Status changed from Verified to Closed
  • Published in build changed from r1491 to 20150307

Also available in: Atom PDF