Compassion constraint. More...
#include <nuxmv.h>
Collaboration diagram for nuxmv_compassion:
Data Fields | |
| nuxmv_expr | p |
| nuxmv_expr | q |
Detailed Description
Compassion constraint.
A compassion constraint consists of a pair of formulas (p, q); if property p is true infinitely often in a fair path, then also formula q has to be true infinitely often in the fair path.
Field Documentation
◆ p
| nuxmv_expr nuxmv_compassion::p |
The first formula of the compassion constraint.
◆ q
| nuxmv_expr nuxmv_compassion::q |
The second formula of the compassion constraint.
The documentation for this struct was generated from the following file:
- Code/include/nuxmv.h
