Version:
[release notes]

Module 5: Hybrid simulation models

In Module 4, you learned that:

  • That user-specified requirements capture system-specific requirements that are essential to ensure a safe and productive system.
  • Synthesized supervisors ensure that the controlled system adheres to all user-specified requirements, in every reachable state.
  • Requirements can be specified as requirement automata, state requirement invariants and state/event exclusion requirement invariants.
  • Requirements are dealt with in the synthesis algorithm by preparation steps, and the different kinds of requirements are each dealt with in a different way.
  • State/event exclusion requirement invariants come in two forms: needs and disables.
  • Depending on the system being modeled, and the kinds of requirements that are expressed, different kinds of requirements may be easier to understand or more succinct.
  • Requirement automata can be modeled in CIF similarly as plant automata, using the requirement keyword instead of the plant keyword.
  • Requirement invariants can be modeled in CIF using dedicated syntax.
  • CIF allows to combine multiple state/event exclusion requirement invariants for different events, to avoid having to duplicate the condition predicates.
  • Synthesis requires that all variables have a finite data type, with only booleans, ranged integers and enumerations being supported.
  • CIF features type declarations to make it easier to reuse types, such as ranged integer types, in multiple places, and to keep them consistent when the model is adapted.
  • It is a runtime error for an integer variable to go outside of its defined range.
  • Synthesis prevents out-of-range runtime errors, but it is generally preferred to make sure the plant doesn't have runtime errors if they are not physically possible.
  • CIF features enumerations, collections that consist of literals representing named entities, and using them leads to more readable models compared to encoding the entities as integer numbers.
  • The CIF monitor concept can be used to prevent automata from blocking certain events, and essentially prevents having to specify many self-loop edges.
  • If no supervisor can be computed for the given plants and requirements, synthesis will give an 'empty supervisor' error.
  • CIF models can be connected to Scalable Vector Graphics (SVG) images, to allow visualizing the state of the system in a way that gives better overview than for instance the CIF simulator's state visualizer.
  • An SVG image is connected to a CIF model by using an svgfile declaration.
  • The attributes of elements of SVG images can be changed based on the state of the system, by using SVG output mappings.
  • The use of if and switch expressions is useful when using different values depending on the state of the system, for instance for SVG output mappings.
  • SVG images can also be used for interaction, by adding SVG input mappings that connect clicks on elements of images to enabling events in the model.

Interactive simulation with SVG images is powerful. But, so far, we used discrete event models for this. This means that actions that the system can perform, like opening a gate, are completed instantaneously. In a real system, such actions take time. Validation through simulation with a discrete event model is thus not fully representative of the behavior of the real system.

In this module, you learn the concepts of timed and hybrid systems, and how to model them in CIF. You extend discrete event models with continuous behavior, to create a hybrid model for the water lock case. You use the improved simulation model to validate the final supervisory controller, making sure it operates as intended.

This module is divided into the following sub-modules: