class AM_INVARIANT_STMT < $AM_STMT
****
Statement representing an invariant check. (If present, this type must define "invariant:BOOL").


Flattened version is here

Ancestors
$AM_STMT $NEXT{_} $AM $PROG_ERR
AM_STMT AM



Public


Readable Attributes
attr sig:SIG;
**** Signature of the invariant.

Writable Attributes
attr sig:SIG;
**** Signature of the invariant.

Features
copy:$AM_STMT