packageSafeStateGraphs

Safe StateGraphs

Information

In this section it will be discussed in which sense "StateGraph2" models are "safe". This section consists of the following sub-sections:

  1. "Valid Graph Structures" discusses that only valid graph structures of a StateGraph2 model will be accepted by a Modelica tool.
  2. "Single Assignment Rule" discusses that a variable must always be defined by exactly one equation and therefore non-determinism as in other state machine formalisms cannot occur (especially, it is not possible to assign the same variable twice in parallel executing branches).
  3. "Bounded Event Iterations" discusses that infinite event looping is not possible, because it is required that every "loop" in a StateGraph2 model must have at least one delayed Transition.

Contents

NameDescription
ValidGraphStructuresValid Graph Structures
SingleAssignmentRuleSingle Assignment Rule
BoundedEventIterationsBounded Event Iterations