Retrascope

Sergey Smolov wrote:

In which parts of the extracted EFSMs did you find the redundant invariant conditions?

For example, the invariants map of b01: {STATO=(AND (GREATEREQ STATO 0) (LESSEQ STATO 7)), LINE1=(OR (EQ LINE1 1) (EQ LINE1 0)), LINE2=(OR (EQ LINE2 1) (EQ LINE2 0)), RESET=(OR (EQ RESET 1) (EQ RESET 0)), OUTP=(OR (EQ OUTP 1) (EQ OUTP 0)), OVERFLW=(OR (EQ OVERFLW 1) (EQ OVERFLW 0)), CLOCK=(OR (EQ CLOCK 1) (EQ CLOCK 0))}

So you mean that there is no need in invariants for Boolean and BIT_VECTOR(1) types, isn't it?

Of course I'm talking about the "general" invariants which cover all values of the specified type like "x true OR x false" for booleans.