Add nonblocking under control check to CIF controller checker

The controller checker implements various checks. These come from a PhD thesis (Chapter 4). Currently, we have implemented the 'finite response' and 'confluence' checks, but not yet the 'nonblocking under control' check. We should add that as well.

Steps

• Add non-blocking under control check to the CIF controller properties checker, based on the algorithm from the paper. (!931 (merged))
  • The CIF PLC code generator (new version, PLCgen) refers to the CIF controller checker as implementing two checks. This needs to be updated.
• Further improvements:
  • Consider whether to also check uncontrollable-complete paths. See #410 (comment 2406373).
  • Report details in case the model is blocking under control. The debug output can serve as inspiration. At least include whether there are marked states without controllable events enabled, and which initial states are bad.
  • See follow-ups in #621, as several of them could also apply here.

Related issues

• Issue #695 discusses the performance of the confluence check, which relates closely to this issue.

Addresses #892