Module 4.4: Modeling for synthesis

Now that you know about requirement automata and invariants, it is time to see how they can be modeled in CIF. Besides that, we will discuss some other aspects related to modeling for synthesis using CIF. That is, we will discuss limitations for data types of variables when using synthesis, and how that affects modeling and the synthesis algorithm. And, we will discuss the concept of monitors, which can be useful when modeling requirements, as well as how to model monitors in CIF.

Modeling requirements in CIF

In the third module, you learned that plant and supervisor automata are regular automata that are indicated as either being part of the plant or the supervisor, using the plant and supervisor keywords, respectively. Such a keyword can be placed before the automaton keyword, or can be used instead of it. Automata can also be indicated as being a requirement, by similarly using the requirement keyword.

Earlier in this module, you learned about requirement invariants. Requirement invariants are indicated either by the requirement keyword, or by the requirement invariant keywords, whichever you prefer.

The requirement automaton from the bridge deck and traffic light example from earlier in this module can be modeled in CIF as follows:

                        
                            requirement ClosedWhenGreen:
                                location ClosedGreen:
                                    initial;
                                    marked;
                                    edge to_red           goto ClosedRed;

                                location ClosedRed:
                                    edge to_green         goto ClosedGreen;
                                    edge partially_opened goto PartiallyOpenRed;

                                location PartiallyOpenRed:
                                    edge opened           goto OpenRed;
                                    edge closed           goto ClosedRed;

                                location OpenRed:
                                    edge partially_opened goto PartiallyOpenRed;
                            end
                        
                    

The 10 different requirement invariants from that same example, two state requirements and eight state/event exclusion requirements, can be modeled in CIF as follows:

                        
                            requirement not ((BridgeDeck.PartiallyOpen or BridgeDeck.Open) and TrafficLight.Green);
                            requirement (BridgeDeck.Closed and TrafficLight.Green) or TrafficLight.Red;

                            requirement BridgeDeck.Closed and TrafficLight.Green disables partially_opened;
                            requirement BridgeDeck.PartiallyOpen or BridgeDeck.Open disables to_green;
                            requirement TrafficLight.Green disables partially_opened;
                            requirement BridgeDeck.PartiallyOpen or BridgeDeck.Open disables to_green;
                            requirement not TrafficLight.Red disables partially_opened;
                            requirement not BridgeDeck.Closed disables to_green;
                            requirement partially_opened needs TrafficLight.Red;
                            requirement to_green needs BridgeDeck.Closed;
                        
                    

Sometimes, you may write the same state/event exclusion requirement for multiple events. For instance, if the emergency mode of a system is activated by an operator pressing the emergency button, none of the system's motors may be started. In CIF, you can combine these requirements into a single requirement, by simply listing multiple events for the state/event exclusion requirement. For instance, the following example gives three separate state/event exclusion requirements, and their combination into a single requirement:

                        
                            requirement EmergencyMode.On disables Motor1.c_start;
                            requirement EmergencyMode.On disables Motor2.c_start;
                            requirement EmergencyMode.On disables Motor3.c_start;

                            requirement EmergencyMode.On disables {Motor1.c_start, Motor2.c_start, Motor3.c_start};
                        
                    

Similarly, multiple events can be given for needs state/event exclusion requirements.

For traceability and readability, requirement invariants can be given a name. This applies to both state requirement invariants and state/event exclusion requirement invariants. Here is an example of the latter:

                        
                            requirement RQ1: EmergencyMode.On disables Motor1.c_start;
                            requirement RQ2: EmergencyMode.On disables Motor2.c_start;
                            requirement RQ3: EmergencyMode.On disables Motor3.c_start;
                        
                    

State/event exclusion requirements with multiple events are a shorter form for writing multiple requirements, and since requirement names must be unique, state/event exclusion requirements with multiple events can not be given a name.

Synthesis requires finite data types

You learned previously that automata may declare discrete variables that hold a value of a certain type. These variables can then be used in among others guards of edges and conditions of requirement invariants, and be updated on edges. There are different data types, that indicate the possible values that a variable can have. For instance, a boolean variable (keyword bool) can have values true and false. And an integer variable (keyword int) can have whole numbers as its values, such as 1 or 32.

To allow for synthesis, the data type must be finite, so that variables can only have a finite number of possible values. For booleans, this is already the case, as with true and false it only allows two different values. But, for integers, you must explicitly limit the allowed values, using ranged integer types. For instance, if a variable can only have the values 1 through 5, 1 and 5 included, you'd use the type int[1..5] instead of int.

If you the same bounds for integer types multiple times, you can define a constant for that bound, and use it multiple times, like this:

                        
                            const int MAX = 3;
                            disc int[0..MAX] count1;
                            disc int[0..MAX] count2;
                        
                    

Although, if the variables are declared in the same automaton, and have the exact same type, you could also combine their declarations:

                        
                            const int MAX = 3;
                            disc int[0..MAX] count1, count2;
                        
                    

And, if you use the same type multiple times, you can also give it a name, and reuse it many times:

                        
                            const int MAX = 3;
                            type t = int[0..MAX];
                            disc t count1;
                            disc t count2;
                        
                    

Here a type definition named t is defined as being equal to the type int[0..MAX]. Type definition t can then be used in place of a type.

Staying within integer bounds

When a variable has a ranged integer type, it can only have the values that are part of the range. That is, assigning it a value outside that range is invalid. For instance, for a variable x with type int[0..3], the assignment x := 4 is invalid, as 4 is larger than the integer type's upper bound of 3. Assignments like this are invalid in CIF.

In some situations, the assignment itself is valid, but may in certain situations lead to the variable getting a value outside its range. For instance, if for the same variable x, we have an assignment x := x + 1, then x can safely be incremented from 0 to 1, 1 to 2, and 2 to 3. But, if x has the value 3, incrementing it by one will lead to it getting value 4, which is outside its valid range. Such a model is not flagged as being an invalid model when you edit it. But, if you simulate the model, and x gets value 4, this will lead to a runtime error. The model is thus still an invalid model.

One way to make it a valid model, is to add a guard to the edge. By adding guard x < 3, x can only be incremented by one if x is less than 3. It can thus never get to value 4 any more, and thus the variable stays within its range.

While you should always ensure that your integer variables can't go out of range, you can also use synthesis for this. That is, synthesis will also ensure, besides safety, non-blockingness, controllability and maximally permissiveness, that all variables remain with their ranges. So, if you forget to add the x < 3 guard, synthesis will compute it for you, and still ensure that variables can't go out of range.

In the synthesis algorithm, preventing runtime errors is another preparation step. That is, for every edge, a extra condition is computed for every integer variable that is assigned on the edge, and the guard of the edge is strengthened with that condition. Furthermore, for a variable x with type int[a..b], state requirement invariant a <= x and x <= b is added. You'd think that either of these is sufficient, and theoretically that's correct. But, due to some rather technical reasons related to how predicates are represented and manipulated during synthesis, which are beyond the scope of this course, the synthesis algorithm does both.

The updated synthesis algorithm

The synthesis algorithm still takes the uncontrolled plant and requirements as input, but now performs the following steps:

1. For each edge of each automaton, compute the extra condition for every integer variable that is assigned on the edge, and the add it to the guard of the edge.
2. For each integer-typed variable x with type int[a..b], add a state requirement invariant a <= x and x <= b.
3. Plantify the requirement automata to plant automata and state/event exclusion requirement invariants.
4. Determine all states where state requirement invariants don't hold. Mark them as bad states and remove them.
5. Disable all transitions for controllable events in states where they violate a state/event exclusion requirement invariant.
6. Disable all transitions for uncontrollable events in states where they violate a state/event exclusion requirement invariant. Additionally, mark their source states as bad states and remove them.

7. Determine all blocking states. Mark them as bad states and remove them.
8. Determine all non-controllable states, the states from which an uncontrollable-event transition is possible to a bad state. Mark them as bad states and remove them.
9. Optionally, determine all unreachable states. Mark them as bad states and remove them.
10. Disable all transitions for controllable events in states where they lead to a bad state.
11. If any of the previous steps led to removing any states or disabling any transitions, repeat the steps again, starting from step 7.

The first four steps are preparation steps that are only performed once. The remaining steps are repeated as often as is necessary, until no more behavior is removed.

Enumerations

For synthesis, CIF supports only a few data types. Besides booleans and ranged integers, it also supports enumerations.

Enumerations represent collections of related entities, such as types of products, types of available resources, available machine types, different countries, different colors, different genders, and so on. It is possible to use numbers to represent the different entities, for instance 0 for red, 1 for orange, and 2 for green, to represent the different colors of a traffic light. However, these numbers are rather arbitrary. Furthermore, they don’t actually represent numbers, but rather they represent one of the entities (red, orange, green). Enumerations allow giving each entity a name, and to use those names instead of numbers. This usually makes the model easier to read and understand. For instance, consider the following:

                        
                            enum TrafficColor = RED, ORANGE, GREEN;
                        
                    

The enum keyword is used to declare an enumeration. The TrafficColor enumeration has three possible values or literals. The literals are named RED, ORANGE, and GREEN. An enumeration can be used as data type, and the enumeration literals can be used as values:

                        
                            disc TrafficColor light = RED;
                        
                    

The TrafficColor enumeration is used as the type of the light variable. The light variable is given value RED as its initial value. The default value of an enumeration type is its first literal (RED in this case). However, it is usually preferred to explicitly initialize variables with enumeration types, for readability.

Variables with an enumeration type can be compared and assigned, similar to boolean and integer variables:

                        
                            edge change_color when light = RED do light := GREEN;
                        
                    

This edge has a guard that compares the value of the light variable to enumeration literal RED. Only if the light is currently RED, may this edge be taken. The edge further assigns enumeration literal GREEN as the new value of variable light.

Monitors

You previously learned that requirement automata are taken into account during synthesis by plantifying them to non-restrictive plant automata, and state/event exclusion requirement invariants. Such a plantified requirement automaton essentially monitors the state of the plant, but does not restrict it. The restrictions are moved to state/event exclusion requirement invariants, that can then be expressed over the locations of the plantified automaton. Such a plantified automaton can be expressed in CIF as a monitor automaton, also simply called a monitor. For instance, the plantified version of the requirement automaton from the railway crossing example from earlier in this module, can be modeled in CIF as a monitor automaton as follows:

                        
                            requirement RailwayCrossingOrder2:
                                monitor open, close, turn_on, turn_off;

                                location OffOpen:
                                    initial;
                                    marked;
                                    edge turn_on  goto OnOpen;

                                location OnOpen:
                                    edge close    goto OnClosed;

                                location OnClosed:
                                    edge turn_off goto OffClosed;

                                location OffClosed:
                                    edge open     goto OffOpen;
                            end
                        
                    

This automaton monitors four of the events in its alphabet: open, close, turn_on and turn_off. This essentially means self-loop edges are automatically added to ensure that this automaton does not disable these events in any state. Since in this case the automaton monitors all of the events in its alphabet, we may also shorten the monitor declaration to simply monitor;.

Quiz