Revision history [back]

The problem of side effects error occurs when using the Promela cexpr primitive with the SPIN model checker because cexpr allows for arbitrary C expressions to be evaluated within a Promela process. If the C expression contains side effects such as modifying global variables, accessing external resources, or invoking functions with side effects, it can lead to non-deterministic behavior and make the verification of the system incorrect. These side effects can also cause the model checking process to become more complex and time-consuming. To avoid this problem, it is recommended to avoid using c_expr and instead use Promela's built-in constructs for expressing system behavior.