#424 Event-based toolset: use CIF precondition checker framework

• Best to understand per commit. Some things change again a bit in later commits, I think, but not too much.
• Changes:
  • All event-based tools now use the new precondition checking framework.
  • General event-based toolset precondition changes:
    • Unused channels are now also not allowed.
    • Allow non-restrictive invariants in components.
    • Allow non-restrictive state/event exclusion invariants in locations.
    • Check for non-restrictive state invariants in locations now allows multiple state invariants per location.
    • Check for non-restrictive state invariants in locations now allows any non-restrictive state invariant, not only boolean literal true.
    • Having multiple initialization/marker predicates in a location is now supported.
    • Initialization/marker predicates in locations are now supported if they can be statically evaluated, rather than having to be boolean literals.
    • Having multiple guards on an edge of a location is now supported.
    • Guards on edges of locations are now supported if they can be statically evaluated, rather than having to be boolean literals.
  • Specific event-based toolset precondition changes:
    • The controllability check no longer supports unused events that are not controllable/uncontrollable.
    • The supervisory synthesis tool no longer supports unused events that are not controllable/uncontrollable.
    • The supervisory synthesis tool no longer checks for no marking during precondition checking, but as a first step during synthesis. It still results in an empty supervisor.
  • Documentation improvements:
    • General preconditions have improved order.
    • Improved consistency for the different tools.
    • Some small textual improvements.
    • Automaton abstraction: lists missing preconditions.
    • Controllability check: also unused events must be (un)controllable.
    • Supervisor synthesis: also unused events must be (un)controllable.
  • New local checks:
    • New AutOnlyDeterministicCheck check. Not as generally implemented as it could be, so is as local check.
    • New AutOnlyMarkedAndNonMarkedLocsCheck check. Rather specific, and not as generally implemented as it could be, so is as local check.
  • General check changes:
    • Generalized AutOnlyWithOneInitLocCheck to AutOnlyWithCertainNumberOfInitLocsCheck (currently with 'at most one' or 'exactly one').
    • Generalized AutOnlySpecificSupKindsCheck constructors.
    • New EdgeNoUpdatesCheck check.
    • New EdgeOnlyStaticEvalGuardPredsCheck check.
    • New EventOnlyReqSubsetPlantAlphabetCheck check.

Addresses #424 (closed)