Inconsistency between "Refinement" and safety property
Steps to reproduce the issue:
- Compile CHECK_REFINEMENT
- Check "MTS->Refinement" between TV_CONTROLLER_NO_DET and CONTROLLER_CHECK_COMP
The output is:
When checking the following safety properties (expected to be equivalent to verifying Refinement): property ||SAFETY_1 = TV_CONTROLLER_NO_DET. || CHECK_SAFETY_1 = (SAFETY_1 || CONTROLLER_CHECK_COMP).
property ||SAFETY_2 = CONTROLLER_CHECK_COMP. || CHECK_SAFETY_2 = (SAFETY_2 || TV_CONTROLLER_NO_DET).
Verifying safety over CHECK_SAFETY_1 throws "No deadlock/errors", but verifying CHECK_SAFETY_2 throws:
