assert p;
where p is a temporal formula, means that every execution of the program
must satisfy the formula p. An execution that does not satisfy the formula
is called a failure of the program.
An assertion may be given a name. For example:
foo : assert p;
This does not change the semantics of the program, but provides an identifier
``foo'' for referring to the given assertion. The code
foo : assert p;
foo : assert q;
is equivalent to
foo : assert p & q;