Enumerations are a kind of custom data type. Each enumeration is composed of a finite list of discrete values. A new enumeration can be created by selecting. An enumeration type can be used by constraining a variable to the desired type, or by using one of the enumeration-related primitive components.
Why use enumerations¶
Enumerations behave like all other data types in CertSAFE. As such, CertSAFE will generate errors if you accidentally mix values from two different enumeration types. For example, suppose there were two variables in the system, one that represented months and one that represented colors. If both variables were defined as integer-typed, it would be possible to assign values from the colors variable to the months variable without CertSAFE showing an error or warning. However, using enumerations would result in CertSAFE informing the user that there is a type mismatch if a variable of type color was being assigned to a variable of type month.
Enumerations are made up of discrete user-defined values. This is useful for variables that can only hold a specific list of values, and no more. For example, the states that a finite-state system can be in might be a good use of enumerations. Another example might be various commands that could be executed on a subsystem. This is also important when simulating the model, as using an enumeration prevents the variable from being set to values not explicitly defined by the enumeration. For the purposes of robustness testing, it may be beneficial to add an “Invalid” entry to some enumeration types so that the model can explicitly describe the behavior if an illegal value is received.
Operations on enumeration values¶
By default, variables that have been set to an enumeration type can be compared to other variables of the same enumeration type. As CertSAFE has no knowledge of enumeration ordinal values, greater than and less than comparisons cannot be done on an enumeration. If that is required, it is advised that the enumeration be converted to some numeric type first, and then compared.
CertSAFE also provides an inline enumeration comparator primitive, and a primitive that detects when enumeration variables transition from one value to another.