class AM_INVARIANT_STMT < $AM_STMT |
---|
**** | Statement representing an invariant check. (If present, this type must define "invariant:BOOL"). |
$AM_STMT | $NEXT{_} | $AM | $PROG_ERR | AM_STMT | AM |
attr sig:SIG; |
---|
**** | Signature of the invariant. |
attr sig:SIG; |
---|
**** | Signature of the invariant. |
copy:$AM_STMT |
---|