CIF documentation (Incubation)

CIF models consist of components. Each of the components represents the behavior of a part of the system. Components can be modeled as automata, which form the basis of CIF. The following CIF specification, or CIF model, shows a simple automaton:

The automaton is named lamp, and not surprisingly represents the (discrete) behavior of a lamp.

Automaton lamp declares two events, named turn_on and turn_off. Events model things that can happen in a system. They represent changes. For instance, the turn_on event indicates that the lamp is being turned on. It represents the change from the lamp being off to the lamp being on. The event declaration in the lamp automaton declares two events. The event declaration only indicates that these events exist, it does not yet indicate when they can happen, and what the result of them happening is.

All automata have one or more locations, which represent the mutually exclusive states of the automaton. The lamp automaton has two locations, named on and off. Automata have an active or current location. That is, for every automaton one of its location is the active location, and the automaton is said to be in that location. For instance, the lamp automaton is either in its on location, or in its off location.

Initially, the lamp is on, as indicated by the initial keyword in the on location. That is, the on location is the initial location of the lamp automaton. The initial location is the active location of the automaton, at the start of the system.

In each location, an automaton can have different behavior, specified using edges. An edge indicates how an automaton can change its state, by going from one location to another. Edges can be associated with events, that indicate what happened, and thus what caused the state change.

The lamp automaton has an edge with the turn_off event, in its on location, going to the off location. Whenever the lamp is on, the lamp automaton is in its on location. Whenever the lamp is turned off, the turn_off event happens. The edge with that event indicates what the result of that event is, for the on location. In this case the result is that the lamp will then be off, which is why the edge goes to the off location.

The lamp automaton can go from one location to another, as described by its edges. This is referred to as 'performing a transition', 'taking a transition', or 'taking an edge'. The lamp automaton can keep performing transitions. The lamp can be turned on, off, on again, off again, etc. This can go on forever.

The power of events is that they synchronize. To illustrate this, consider the following CIF specification:

The automaton represents a producer that produces products, to be consumed by a consumer. The producer automaton starts in its producing location, in which it produces a product. Once the product has been produced, indicated by the produce event, the automaton will be in its idle location, where it waits until it can provide the produced product to the consumer. Once it has provided the product to the consumer, it will once again be producing another product. Consider also the following continuation of the above specification:

This second automaton represents a consumer that consumes products. The consumer is initially idle, waiting for a product from the producer. Once the producer has provided a product, the consumer will be consuming. Once it has consumed the product, as indicated by the occurrence of the consume event, it will become idle again.

The specification has three events, the produce and provide events declared in the producer automaton, and the consume event declared in the consumer automaton. The consumer automaton, in its idle location, has an edge that refers to the provide event declared in the producer automaton. As such, that edge and the edge in the idle location of the producer automaton, refer to the same event.

Depending on the context in which it is used, non-determinism can mean different things. One definition is having multiple possible traces through the state space of a system. Another definition is having multiple possible transitions for a certain event, for a certain state. Different communities also use different definitions, and some communities only use one of the definitions, and use a different name to refer to the other concept.

The lesson on synchronizing events described how events that are used in multiple automata exhibit synchronizing behavior. That is, if the event is used in multiple automata, they must all enable that event in order for a transition to be possible. If one of them can not perform the event, the event is disabled, and none of the automata can perform a transition for that event.

Whether an automaton participates in the synchronization for a certain event, is determined by its alphabet. The alphabet of an automaton is the collection of events over which it synchronizes.

Consider the following CIF specification (the producer/consumer example from the lesson on synchronizing events):

The specification could also be specified as follows:

The consume event is now declared in the producer automaton rather than the consumer automaton, but the locations and edges have not changed. This modified specification exhibits the same behavior as the original.

It should be clear that while events can be declared in various places, it is best to declare them where they belong. That is, the consume event is only used by the consumer automaton, and is thus best declared in that automaton. Similarly, the produce event is only used by the producer automaton.

The provide event however is used by both automata. In such cases the event is usually declared where it is initiated. In the example above, the producer provides the product to the consumer, and not the other way around. Therefore, the provide event is declared in the producer automaton, rather than in the consumer automaton.

However, the modeler is free to choose the best place to declare the event. If no choice can be made between the automata, the event can also be declared outside the automata, as follows:

This specification also has the same behavior. Only the placement of the event declarations has changed.

The place where an event is declared is of no influence to the implicit (default) alphabets of the automata. The implicit alphabet of an automaton is determined solely based on the events that occur on the edges of that automaton.

This lessons explains several short notations, that can be used for easier modeling, can reduce the size of the specification, and make specifications easier to read. The following topics are discussed:

This lesson introduces discrete variables. Consider the following specification:

The counter automaton can be used to count certain things. The increment and decrement events are used to change the count. The count itself is stored in a variable named count. CIF has several different types of variables. Here, we use a discrete variable, as indicated by the disc keyword. The variable has an int data type, meaning it can have integer numbers as its value. It is initialized to value 3.

The automaton has two edges, one for the increment event, and one for the decrement event. The edge for the decrement event has a guard that indicates under which circumstances the event can take place. The condition is indicated using the when keyword. In this case, the guard ensures that the count can only be decremented if it is currently positive. The guard of the edge for the increment event indicates that the count can only be incremented as long as it is less than five. In general, a guard must hold in the source location of the edge, for the edge to be enabled, and a transition to be possible. If the guard is not specified, it defaults to true, which always holds and does not restrict the edge in any way.

Both edges also have updates, indicated using the do keyword. Updates can be used to specify the effect of the transition on variables. In this case, the updates assign a new value to the count variable that is one less or one more than the current value. That is the value of the count variable is decremented or incremented by one.

This specification represents a counter that can be repeatedly incremented and decremented by one, and ensures that the value of variable count is always at least zero and at most five.

The state space of the counter automaton is as follows:

Discrete variables can only change value by explicitly assigning them a new value in the do part of an edge. If an edge does not assign a value to a discrete variable, that variable keeps its current value. Consider the following CIF specification:

This is the same lamp automaton as used in the lesson on automata, but with a count variable added. This variable is used to count the number of times that the lamp has been turned on. The edge for the turn_on event increments the value of the variable by one, each time the lamp is turned on.

The edge for the turn_off event does not assign a value to a variable, so variable count keeps its value when the lamp is turned off.

The state space of this specification is:

The states are labeled with the name of the current location of automaton lamp and the current value of variable count.

The lesson that introduces discrete variables, uses an example of a counter. The actual count was modeled using a variable:

It is also possible to use multiple locations instead of a variable:

This alternate model has the same behavior, in that it models a counter that can be incremented an decremented in steps of one, and the value is kept at least zero, and at most five. The variant with the variable however, is shorter and more intuitive. It is also easier to change to the count < 5 guard to count < 100 than it is to add dozens of additional locations and edges. In this case, using a variable is preferable to using multiple locations.

The lesson that introduces automata, used an example of a lamp:

The automaton uses two locations to keep track of the current state of the lamp. Instead of two locations, it is also possible to use a variable:

This alternate automaton uses a single variable named on. The data type of the variable is bool, which means that the variable can only have one of two possible values: true or false. If variable on has value true, the lamp is on, and if it has value false it is off. Initially, the lamp is on, as the initial value of the variable is true. The automaton has only one location, with two edges. The first edge indicates that the lamp can be turned on (event turn_on), only when it is not currently on (guard not on), and then afterwards is on (variable on becomes true). Similarly, the second edge indicates that the lamp can be turned off, only when it is currently on, and then afterwards is on.

Both models represent a lamp that is initially on, and can be turned off, on, off again, on again, etc, repeating the behavior forever. Which approach is best depends on your preference, and on the rest of the model. It is however also possible to use both locations and a variable:

This automaton has the same behavior as the previous two automata. Variable on is renamed to on2, as a variable can not have the same name as a location of that same automaton.

While it is possible to model a lamp like this, this automaton duplicates the information about whether the lamp is on or off. This makes the automaton larger and more complex than it needs to be. In general, it is usually better to choose either a variable, or multiple locations, to express something, and not both. In several future lessons, we’ll see that combining multiple locations with variables is useful, but not to express the same thing. Furthermore, an other future lesson explains how to use a location as a variable.

Discrete variables can only be declared in automata, and may only be assigned (given a value, written) by that automaton. They may however be read globally. Consider the following CIF specification:

This specification models a supermarket, and features a customer and two queues. Customers arrive and enter either of the queues. Eventually customers leave the queue.

Both queues (automata queue1 and queue2) are identical, except for their names. They maintain the count, which represents the number of customers in the queue. A queues is full if it contains two customers. Customers can thus only enter a queue if less than two customers are present. Similarly, it is only possible for a customer to leave a queue if there is a customer in the queue.

Customers decide to which queue they go, based on the number of customers already present in those queues. A customer only enters the first queue if that queue has less than or the same number of customers as the second queue. Similarly, a customer only enters the second queue if that queue has less than or the same number of customers as the first queue. If the queues have the same number of customers, the customer can choose either queue.

The enter event declared in the first queue (queue1) is used by both the customer automaton and the queue1 automaton. The event is thus only possible (enabled) if both automata can participate. Both automata restrict the occurrence of the event using a guard. The event is thus only possible if both guards hold. That is, a custom never enters the first queue if it is full, but it also never enters that queue if it has more customers than the second queue.

The state space of this specification is as follows:

The states are labeled with the counts of the first and second queues.

The customer automaton uses the values of the variables of the queue automata, and thus reads variables of other automata. This is allowed, due to the global read concept of CIF. This concept allows for short guards, that directly and intuitively represent the condition under which an event may take place.

The global read concept should only be used when it is intuitive. In the supermarket example, the customer can physically see how many customers are in the queues. It is therefore intuitive to directly refer to the count variables of the queue automata. If however the customer would not be able to physically observer the queues, then the customer would not be able to directly base its decision of which queue to join, on that information. In that latter case, it may not be a good idea to model the guard in such way.

The local write concept means that discrete variables can only be written by the automata in which they are declared. It is not allowed for the customer and queue2 automata to write (change the value of) the count variable of the queue1 automaton. Only the queue1 automaton may write that variable. The local write concept prevents that multiple automata write to the same variable, as part of a synchronizing event, potentially causing conflicting values to be assigned to that variable. This leads to several benefits, most notably simpler semantics.

This lesson explains the concept of monitoring. It is explained using the following CIF specification:

The producer automaton represents a producer that can repeatedly produce a product, and provide it to either consumer 'a' (event provide_a) or consumer 'b' (event provide_b). The consumers are not modeled.

The detect_changeover automaton detects consumer changes. That is, it detects and counts how often the producer switching from providing consumer 'a' with products to providing consumer 'b' with products, and vice versa. Initially, the automaton waits for the first product to be provided. It goes to either location a or location b, depending on which consumer is provided that first product. Whenever a product is then provided to the other consumer, the count is incremented by one to account for the changeover taking place. This also switches the location to the location for the other consumer, where once again the automaton waits for a changeover.

This lesson explains old and new values of variables in assignments, multiple assignments, and the order of assignments.

Events allow for synchronization, allowing for interaction between automata based on events. If however an automaton has an edge that performs some internal processing, the event may not always be relevant. Consider for instance the following CIF specification:

The specification models two machines. Products enter the first machine, which processes them (event process) and assigns them an id. The machine them provides (event provide) them to the second machine. The second machine currently just accepts the products provided by the first machine, but would in reality likely perform its own processing as well. The state space of the specification is as follows:

The states are labeled with the names of the current locations of automaton machine1. Since automaton machine2 has only a single location, its current location does not change, and it is therefore not included in the state names.

The provide event synchronizes over both automata, while the process event is local to the first machine. The process event is not essential, and could be left out:

By omitting the event from an edge, the tau is used for that edge. The tau event is an event that is implicitly always present without declaring it. The state space of this modified specification is:

The tau event does not synchronize. You can think of this as each automaton having its own local tau event, and since then they are different events, they do not synchronize. If multiple automata can perform a transition for an edge with the tau event, this leads to potential transitions for each of those edges. Since they are all labeled with the tau event, it is impossible to distinguish them solely based on their label. This is a form of non-determinism.

Using the tau events saves having to declare a local event, and also saves having to put that event on the edge. It thus leads to smaller specifications. However, as explained above, if tau is used on multiple edges of multiple automata, the different tau transitions can no longer be distinguished from each other in the state space. The use of the tau event is thus always a trade-off.

It is also possible to explicitly use the tau event:

The tau event can thus be used instead of 'regular' events, and may even be combined with 'regular' events on the same edge:

Omitting the events from an edge defaults to a single tau event, as shown in one of the examples above.

Discrete variables can be given an initial value with their declaration:

The initial value may be omitted, leading to the default value of its data type being used:

The default value of integer typed variables is 0. The default value of boolean typed variables is false.

It is possible to indicate that a variable has more than one potential initial value:

This declares a variable x that has three potential initial values. Variables can only have one value at a time, so an initial value has to be chosen from the set of potential initial values. In other words, initially the value of variable x is either 1, 2, or 4. For information on how to store multiple values in a single variable, see the lessons on types and values, in particular those on tuples, lists, and sets.

It is also possible to indicate that a variable can have any arbitrary initial value:

Variable x can initially have any value. The only constraint is that the initial value must be an integer value, as it must conform to the integer type (int) of the variable. Examples of initial values include -1027, 0, 1, and 12345. Variable y can initially have any value, as long as that value is a boolean value, due to the variable having a boolean type (bool). There are only two boolean values, true and false.

Discrete variables with multiple potential initial values and arbitrary initial values essentially parametrize the specification. The exact initial value is to be chosen or configured later on. This allows a single specification to be used for various different combinations of initial values.

So far all examples used literal values to initialize the variables. However, it is also allowed to use expressions to compute initial values, for instance based on the initial values of other variables:

Variable x is explicitly initialized with value 1. Variable y is initialized to the initial value of x, multiplied by two. Variable z is initialized to the sum of the initial values of x and y. Using this kind of initialization is useful if the initial values must be kept consistent. Changing the initial value of x automatically also changes the initial values of y and z.

The order of the declaration of the variables does not matter. We could just as easily declare them as follows:

Variable y is still initialized using the initial value of variable x, which is now declared after variable y. It is not allowed to construct loops, where the initial values of variables depend on each other:

Variable x uses the value of variable y, which uses the value of variable z, which in turn uses the value of variable x again. This is not allowed in CIF, as it creates a cyclic dependency. However, since no restrictions are introduced on the initial values of variables x, y, and z, except that they must be equal to each other, we can declare them as follows:

Here, variable x is explicitly initialized to an arbitrary value. The other variables are initialized to be equal to whatever arbitrary value is chosen as initial value for variable x.

Initialization predicates can be used to specify the allowed initial locations of automata, as well as to restrict the allowed initial values of variables.

Consider the following CIF specification:

This specification models two machines, which produce products. The machines share a common resource, which may only be used by at most one of them, at any time (see mutual exclusion). Initially, the machines are idle. Then, they warm themselves up. Once they start processing, they set their boolean variable claimed to true to indicate that they claimed the shared resource. After processing, the machines release the resource, by setting claimed to false. They finish their processing cycle by cooling down, before starting the cycle for the next product. To ensure that a machine can not claim the resource if the other machine has already claimed it, the edges going to the processing locations have a guard that states that it is only allowed to claim the resource and start processing, if the other machine has not already claimed the resource. The state space of this specification is:

The states are labeled with the first letters of the names of the current locations of the automata.

The specification can alternatively be modeled as follows:

The claimed variables and corresponding updates have been removed, and the guards no longer use those variables. Instead, the edge for the start1 event now refers to the processing location of automaton machine2. The guard states that the first machine can perform the start1 event, only if the second machine is not currently in its processing location. In other words, the guard states that the first machine can start processing as long as the second machine is not currently busy processing (and thus using the shared resource).

The processing location of automaton machine2 is used as a boolean variable. Using the location as a variable saves having to declare another variable (claimed) that essentially holds the same information, and needs to be explicitly updated (on two separate edges) to the correct value.

The lesson on discrete variables used the following CIF specification:

The counter can repeatedly be incremented and decremented by one, as long as the count remains at least one and at most five. To keep the count in the allowed range of values, guards were used to limit the occurrence of the increment and decrement events.

Instead of using guards, it is also possible to use state (exclusion) invariants, also called state invariants, or just invariants:

The guards on the edges have been replaced by the two invariants. The first invariant specifies that the value of variable count must always be at least zero. The second invariant specifies that the value must also be at most five.

Invariants specify conditions that must always hold. Invariants must hold in the initial state, and all states reached via transitions. If a transition results in a state where an invariant doesn’t hold, the transition is not allowed and can’t be taken.

For the counter example, initially the count is 3. The edge for the increment event can be taken, leading to a state where the count is 4. Taking another transition for the increment event leads to a state where the count is 5. If we then were to take another transition for the increment event, the count would then become 6. However, that violates the invariant. Therefore, in the state where the count is 5, no transition for the increment event is possible. In other words, the invariant disables the transition for the increment event for that state.

The two invariants can be specified in various ways:

Each of these variants leads to the exact same behavior, and which variant to use depends mostly on the modeler’s own preference.

The benefit of guards over invariants is that they more explicitly state the condition under which an edge can lead to a transition. If a guard doesn’t hold, the edge can’t be part of a transition. It is thus immediately clear when the edge can lead to a transition. For invariants, the update has to be calculated first, after which the invariants can be evaluated for the state resulting from the transition. If one of the invariants doesn’t hold, the transition is not allowed. In the case of the invariants, it is not as immediately clear from the edge alone, when that specific edge can or can not lead to a transition.

The benefit of invariants over guards is that they apply to all edges. If several edges in an automaton have updates to the same variable, then the invariants need to be specified only once, and apply to all transitions, for all edges. Using guards, all the edges that modify the variable would need their own guards, and if the updates are different, the different edges usually require different guards. Furthermore, if new edges with updates to the same variables are added, the invariant is already present, but guards have to be added, which can easily be forgotten. In those cases, invariants can thus help keep the specification consistent.

Another benefit of invariants is that they explicitly state the conditions that must hold in relation to the variables, while guards specify the condition under which the update is allowed. Consider the following CIF specification:

The goal is to keep the value of in the range [0..100]. The invariant is simple and direct. The guard however, has to state the condition under which the update does not violate the goal. That is, the upper bound has to be decreased by three, and the result has to be divided by two, to get the highest value (48) for which the update is still within the valid range of values. That is, for value 48 the update results in value 99 (2 * 48 + 3 = 99), and for value 49 the update results in value 101 (2 * 48 + 3 = 99). The more complex the update, the harder it is to figure out the guard to use to keep satisfy the goal.

You can of course also use 2 * x + 3 <= 100 as guard, instead of x <= 48. However, this duplicates part of the update in the guard.

So far, all invariants have been specified in automata. They may however also be specified outside of the automata, similar to initialization predicates. It is generally recommended to place an invariant inside an automaton if the condition only applies to declarations from that automaton, and to place it outside of the automata if the condition applies to declarations of multiple automata.

Furthermore, invariants can be placed in a location. Such an invariant only has to hold while the location in which it is specified is the current location of its automaton.

Consider an elevator, consisting of three parts: a motor to make the elevator move up and down, a door that can be opened and closed to let passengers enter and exit, and an emergency button that can be used to stop the elevator in case of an emergency. The following CIF specification models the three parts:

Each part is modeled by an automaton. Since the automata don’t share any events, they operate independently. What is missing, is a controller that links the different automata, and controls them in a safe manner. Such a controller restricts the behavior of the individual automata, allowing only the combined behavior that is deemed desired. There are several ways to restrict events, including introducing synchronization between the different automata, and adding guards. The downside of these approaches it that they require modification of the automata. What if we wanted to specify the controller separately from the behavior of the physical system? We could introduce an additional automaton, that synchronizes with the existing automata. For instance, we could add the following to the CIF specification:

This controller introduces restrictions for the turn_on event of the motor. In this particular case, the controller ensures that the motor may only be turned on when both the door is closed and the emergency button is released. By restricting the event, the controller prohibits the event from taking place in certain states, ensuring that only the desired behavior remains.

It is nice that we can separate the description of the physical behavior of the elevator from the controller that controls it. This separation of concerns may make it easier to reason about the behavior, it may make it easier to adapt the controller when the physical system doesn’t change, and it may make it easier to reuse the model of the physical system for other purposes.

However, modeling an automaton with a single location that must then also be initial requires quite some syntax. State/event exclusion invariants can serve the same purpose, but are often easier to use, shorter to write, and more intuitive to read. Instead of the controller automaton, we can also use the following:

Each state/event exclusion invariant restricts an event, preventing it from happening in certain states. That is, the event is excluded from taking place in certain states. In this case, the turn_on event of the motor automaton needs the door to be in its closed location and the emergency_button to be in its released location, for the event to be allowed/enabled. For the states in which that condition doesn’t hold, the event is disabled.

The invariant consists of two conditions. It can also be written as two separate state/event exclusion invariants, one for each condition:

The second and third invariants lead to the same behavior as the first combined invariant. The second invariant ensures that the event can only take place when the door is closed, while the third invariant ensures that the event can only take place when the emergency button is released. The second and third invariants each indicate a necessary condition that must hold for the event to be allowed/enabled. Together, they require that both conditions hold, for the event to be allowed/enabled. If one of the conditions doesn’t hold, the event will be disabled.

The door is either opened or closed. So far, we’ve required that the door is closed to allow the motor to be turned on. We can also specify it the other way around: to disallow the motor to be turned on, while the door is opened:

Both invariants have the exact same effect. The first invariant only allows the motor to be turned on while the door is closed, which means that it disallows the motor to be turned on in all other situations, namely when the door is opened. And that is exactly what is specified by the second invariant: when the door is opened, turning the motor on is disallowed/disabled. In general, state/event exclusion invariants can always be specified as a positive form (allowed/enabled) and a negative form (disallowed/disabled). It is up to the modeler to choose, based on considerations such as personal preference and readability. Consider the following four alternative forms:

Each of the four forms has the exact same effect, but is written in a different way.

We already saw earlier that for state/event exclusion invariants that introduce necessary conditions for an event to be enabled (the needs variant), the conditions can be combined using an and operator to form a combined condition, for a single invariant.

Here, we also see how in a similar way, state/event exclusion invariants that introduce sufficient conditions for an event to be disabled (the disabled variant) can be combined. Each of them individually has a condition, that if satisfied disables the event, regardless of the other invariants. So, if one of them disables the event, the event is disabled. To combine such invariants into a single invariant, the conditions need to be combined using an or operator, as shown above.

It may occur that multiple events need to be disabled for the same conditions. Instead of writing multiple invariants with the same conditions, one for each event, they can also be combined:

The first two invariants have the same condition, but restrict different events. The third invariant has the same condition, but restricts both events. In general, for all state/event invariants, multiple events may be given, if they share the same condition. The events must then be separated by spaces and be enclosed in curly brackets ({...}).

This lesson explains the difference between types, values, and expressions. These concepts have already been used in previous lessons, but this lesson names them explicitly, and also explains the relations between them. Furthermore, this lesson serves as an introduction for the coming lessons, which rely heavily on these concepts. Consider the following declarations of discrete variables:

The first declaration declares a discrete variable named x, and the second declaration declares a discrete variable named y. Both variables have an int data type. A data type is usually just called a type, if there is no confusion with other kinds of types. The type of a variable indicates the potential or allowed values of the variable. Variable x is initialized to value 1. Variable y is initialized to twice the value of x, meaning it is initialized to value 2.

Both 1 and 2 * x are expressions. Expressions are combinations of among others literal values (e.g. 1), variables (e.g. x), and operations (e.g. *) on them. Expressions can be computed, resulting in a value. This is called evaluation of the expression.

Expression 2 * x can be evaluated. Evaluating the expression results in value 2 if the value of x is 1, and in value 4 if the value of x is 2. Expressions can thus be evaluated to different values, depending on the values of the variables that occur in them.

Expression 1 consists of only a single value, called a literal value expression. Evaluation always results in that single value. Expression 1 + 3 evaluates to value 4. Even though it does not consist of only just a literal, the value is the same for each evaluation. The expression represents a constant value.

The values of CIF (and their types) can be categorized into different categories: elementary values, container values, and miscellaneous values. Elementary values represent single values, such as a single number. Container values represent multiple values. The different container values combine or store the values in different ways. The elementary and container values are described in the remainder of this part of the tutorial. The miscellaneous values are special, and are explained later in the tutorial. The remainder of this lesson gives an overview of the values available per category, along with short descriptions of each of the different kinds of values.

Elementary values

Container values

Miscellaneous values

Integers are whole numbers, numbers without a fractional part. Examples include -123 and 5. The default value of integers (int type) is 0. Several standard arithmetic operators and functions are available to work with integers, including the following:

Integer values can be compared to other integer values:

CIF can only represent integer numbers (type int) in the range -2,147,483,648 (= -2³¹) to 2,147,483,647 (= 2³¹ - 1). Using values outside that range results in the CIF model being invalid, and leads to runtime errors:

It is possible in CIF to explicitly specify that only a sub range of the integer values are allowed:

This variable x can only have integer values that are at least 3 and at most 7. Assigning any other value to x is not allowed. The default value is not 0 but 3, as that is the value closest to 0 that is in the allowed range of values.

Reals or real numbers are numbers with a fractional part. Examples include 1.56 and -2.7e6 (scientific notation for 2.7 million). Real numbers must either have a fraction or use the scientific notation, to distinguish them from integer numbers. The default value of reals (real type) is 0.0. Several standard arithmetic operators and functions are available to work with reals, including the following:

Real values can be compared to other real values, as well as to integer values:

Integer numbers can often be written where real numbers are expected. Real values and integer values can also often be combined using arithmetic operators and functions. Furthermore, it is possible to convert between them, e.g as follows:

Booleans represents truth values of for instance guards and other conditions and properties. The only two possible values are true (condition or property holds) and false (condition or property does not hold). The default value of booleans (bool type) is false. Several standard logical operators are available to work with booleans, including the following:

The condition x < 3 evaluates to true if x is less than 3 and to false if x is 3 or larger than 3. The result is thus a boolean value.

Conditions can be combined. x >= 3 and x <= 9 means that the value of x must be both at least 3 and at most 9. x >= 3 or x <= 9 means that the value of x must be at least 3, at most 9, or both. Since the condition is always satisfied (it always evaluates to true), condition true can be used instead of x >= 3 or x <= 9.

Strings represent textual values, as a sequence of characters. String values are always written between double quotes. An example is "hello world". The default value of strings (string type) is the empty string "".

Strings can be composed using the + operator. The expression "hello" + " " + "world" evaluates to "hello world". For advanced text formatting, see the text formatting tutorial.

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:

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:

The TrafficColor enumeration is used as 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.

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. The edge as a whole models that if the light is currently RED, it may change color (event change_color) and become GREEN.

Tuples are used for keeping several (related) kinds of data together in one variable, e.g. the identification number and weight of a box. A tuple consists of a number of fields, where the types of these fields may be different. The number of fields is fixed. For instance, consider the following:

Variable box has a tuple type, consisting of two fields, an integer typed field with name nr and real typed field with name weight. The box variable has essentially two values, an integer typed value, and a real typed value.

If multiple consecutive fields have the same type, the type need not be repeated for each of them. In the following example, variables x1 and x2 have the same type:

Literal values exist for tuple types:

The box variable is initialized to a tuple value consisting of integer value 5 (identification number) and real value 2.7 (weight). The entire value of the variable is reassigned in the assignment. That is, both fields are given new values.

It is also possible to refer to a specific field of a tuple, using projection:

The first edge uses projection to obtain the value of the integer nr field, and assign it to integer variable i (i becomes 5). The second edge performs a similar operation for the weight field (r becomes 2.7). The third edge assigns the value of integer variable i to the integer field nr of the box variable. This changes only the value of the nr field. The value of the weight field of the box variable is not affected by this assignment. The third edge increments the value of the nr field of the box variable by one, leaving the weight of the box as is. Besides projection using field names, it is also possible to do projection using 0-based indices:

Index 0 refers to the first field, in this case field nr. Index 1 refers to the second field, etc. Projection using indices is also called indexing. For tuples, it is usually preferred to use field names, rather than indices, for readability.

It is possible to create a tuple from separate values, each stored in a variable:

The right hand side of the assignment is a tuple literal value, as used before. The field values however, are obtained by evaluation of variables, rather than using literal integer and real values. This kind of assignment, where there is tuple variable at the left hand side, and values for each of the fields of that tuple at the right hand side, is called packing a tuple.

It is possible to obtain the values of the fields of a tuple into separate variables:

The first edge uses projection on the variable box to obtain the values of the individual fields, and assigns those extracted values to two separate variables. The second edge does the same thing as the first edge, and is preferred in this case, because of its simple and short notation. This kind of use, where at the left hand side of the assignment you see variables for each of the fields of the tuple, and on the right hand side you see only one variable that has a tuple type, is called unpacking a tuple.

A list is an ordered collection of values (called elements) of a same type. Lists can be used to model anything where duplicate values may occur or where order of the values is significant. Examples are customers waiting in a shop, process steps in a recipe, or products stored in a warehouse. Consider the following:

Variable x has a list of integers as its value. In this case, its initial value is a literal list with three integer elements. Lists are ordered collections of elements. [7, 8, 3] is thus a different list as [8, 7, 3]. Lists are empty by default, and they may have duplicate elements:

Since lists are ordered, there is a first element and a last element (unless the list is empty). An element can be obtained by projection, usually called indexing for lists:

The first three edges obtain specific elements of the list, and assign them to variable i. The first element is obtained using index or offset 0, the second element using index 1, etc. The index of the last element is the length of the list (the number of elements in the list), minus one. Indexing does not change the value of variable x. The fourth edge is invalid, as the fourth element (index 3) of variable x is used, which does not exist. The fifth edge replaces only the first element (index 0) of list x, while keeping the remaining elements as they are. It is also allowed to use negative indices:

Negative indices start from the back of the list, rather than from the front. Index -1 thus always refers to the last element, -2 to the second to last element, etc. As with the non-negative indices, using a negative index that is out of range of available elements, results in an error. To obtain a non-negative index from a negative index, add the negative index to the length of the list: 3 + -1 = 2, 3 + -2 = 1, and 3 + -3 = 0. The following figure visualizes a list, with non-negative indexing (at the top) and negative indexing (at the bottom):

Besides obtaining a single element from a list, it is also possible to obtain a sub-range of the elements of a list, called a slice. Slicing also does not change the contents of the list. It results in a copy of a contiguous sub-sequence of the list. The result of a slice operation is again a list, even if the slice contains just one element, or no elements at all. Slicing requires two indices: the index of the first element of the sub-range (inclusive), and the index of the last element of the sub-range (exclusive). Both indices may be omitted. If the start index is omitted, it defaults to zero. If the end index is omitted it defaults to the length of the list. If the begin index is equal to or larger than the end index, the slice is empty. Similar to indexing, negative indices may be used, which are relative to the end of the list rather than the start of the list. Indices that are out of bounds saturate to those bounds. Some examples:

The first slice takes the third (index 2) and fourth (index 3) elements. The begin index (2) is thus included, the end index (4) is not. The second slice starts at the same index, but extends to the sixth element (index 7). Since there are only five elements, the index is saturated (or clamped) to the end of the list. The results is that all but the first two elements are included. The third slice excludes the first element (index 0), by starting at index 1. It omits the end index, meaning that the entire remainder of the list is kept, and only the first element is not included. The fourth slice begins at the beginning of the list, as the begin index is omitted. It continues until the last element of list, which it excludes. It thus excludes a single element from the end of the list. The fifth slice includes all elements, as both the begin and end index are omitted. The slice is thus identical to the list in x. The following figure graphically represents the slices:

Lists can be combined into new lists. They are essentially 'glued' together. This is called concatenation. This can also be used to add a single element to the front or back of the list. For instance:

Several other standard operators and functions are available to work with lists, including the following:

CIF can only represent lists (type list) with at most 2,147,483,647 (= 2³¹ - 1) elements. Using lists with more elements results in the CIF model being invalid, and leads to runtime errors. For instance, consider the following CIF specification:

Each time the edge is taken, another element is added to list x. As soon as an attempt is made to add the 2,147,483,648^th element, a runtime error occurs.

It is possible to explicitly restrict the number of elements that may be contained in a list:

Variable y can only have lists as its value that have at least 3 and at most 7 elements. Assigning a list with any other number of elements is not allowed. Lists with size restrictions are called bounded lists. They can also be called size restricted lists or ranged lists. The default value for y is [0, 0, 0]. That is, the default value has the least amount of elements that is allowed by the bounded list, and the default value (0) of the element type (int).

Lists with a fixed length are called arrays:

By giving a bounded list the same lower and upper bound, the bounded list has a fixed number of elements, and can be called an array. Arrays also have a shorter and more convenient notation, where the number of elements is only given once. Both notations for arrays are equivalent.

Both bounded lists and arrays support the same operations as regular lists, and can be modified (assigned) the same way as regular lists, as long as their size restrictions are not violated.

A set is an unordered collection of values (called elements) of a same type. Each element value either exists in a set, or it does not exist in a set. Each element value is unique, as duplicate elements are silently discarded. Consider the following:

Variable x1 has a set of integers as its value. In this case, its initial value is a literal set with three integer elements. As sets are unordered collections of elements, {3, 7, 8} is the same set as {8, 3, 7}, and thus variables x1 and x2 have the same initial values. Since elements in a set are unique, set {8, 3, 7} is equal to the set {8, 3, 7, 3}, and thus variables x2 and x3 have the same initial values. For readability, elements in a set are normally written in increasing order, for example {3, 7, 8}. Variable x4 has an empty set as initial value, which is also the default initial value for sets.

The union of two sets results in a set that contains the combined elements of both sets. You can think of the resulting set containing the elements that are in the one set or in the other set (or in both of them). Since sets never contain duplicates, common elements are present only once in the resulting set:

Since sets are unordered, both answers are possible, and represent the same set. Since the order is irrelevant, there are 24 different ways to represent that same set. In the remainder of this lesson, we’ll use increasing order, for readability.

The intersection of two sets results in a set that contains the elements that are present in both sets. You can think of the resulting set containing the elements that are in the one set and in the other set. In other words, the result contains the elements common to both sets:

The difference of two sets results in a set that contains the elements of the first set that are not present in the second set. You can think of the resulting set containing the elements of the first set, with the elements of the second set subtracted or removed from it:

Several other standard operators and functions are available to work with sets, including the following:

A dictionary is an unordered collection of keys and associated values. A key with its associated value is called a key/value pair. Consider the following:

Variable age has as value a dictionary consisting of pairs of strings (the keys) and integers (the values). In this example, each string represents a person’s name, and each integer represents the age of that person. Variable age is initialized with a literal dictionary, containing three key/value pairs. You can think of the dictionary as storing the information that eve is 32 years old, or that the age of eve is 32.

As with sets, dictionaries are unordered. The order of the key/value pairs is irrelevant, {"eve": 32, "adam": 25} is the same dictionary as {"adam": 25, "eve": 32}. For readability, key/value pairs of dictionary literals are normally written in increasing order of their keys. {"adam": 25, "eve": 32} is thus preferred over {"eve": 32, "adam": 25}, as adam goes before eve in a phone book.

Dictionary literals are often written using multiple lines, to get two 'columns' for the keys and values, which can improve readability:

The default value for dictionary types, is an empty dictionary. The following two variables thus have the same initial value:

Every key of a dictionary is unique, but they may be associated with the same value. For the above example with ages, the names (keys) are used to uniquely identify people, but multiple people may have the same age (values). It is not allowed to have the same key twice, in a dictionary literal, regardless of whether they map to the same value or to different values:

The values of a dictionary can be obtained by projection on that dictionary, using the keys:

Projection using a key that exists in the dictionary, results in the associated value. Projection using a key that does not exist in the dictionary, leads to a runtime error.

It is possible to modify single elements of a dictionary, as follows:

The age of eve is changed from 32 to 33. The age is thus replaced by a new age. The age of bob is set to 47. Since there was no key/value pair for that person in the dictionary, a new key/value pair is added. After the updates of both edges, the value of variable age is {"adam": 25, "bob": 47, "eve": 33, "john": 34}.

Several other standard operators and functions are available to work with dictionaries, including the following:

Values of different types can usually be arbitrarily combined. For instance, consider the following example:

Variable boxes stores data about multiple boxes, in a dictionary with unique identification numbers (1, 2, and 3) used as keys. For each box, the position (pos) and weight are stored as a tuple. Initially, there are three boxes. The first box has identification number 1, position 0.0, and weight 2.5. The second box has identification number 2, position 3.0, and weight 1.7. Also consider the following example, where the data of that variable is manipulated:

The first edge changes the weight of the box 1 (the box with identification number 1), from 2.5 to 3.5. The second edge increases the position (pos) of box 2 from 3.0 to 4.0. The third edge adds data for a new box with identification number 4.

Through the use of constants, fixed values can be given a name. Using constants, it is easy to change certain fixed values. If the constant is used consistently throughout the model, the value needs to be changed only in one place. Constants can thus make it easier to keep the model consistent.

Consider the following CIF specification:

In this example, the movement automaton keeps track of the position of an object. The object starts at position 0. It can move until it reaches its target position. The target position is 100. Rather than using position < 100 as guard, the value 100 is stored in a constant named TARGET. The constant can then be used instead the value 100. Similarly, the step size of the object is stored in a constant named STEP.

Constants have a name, which by contention is usually written using upper case letters. Using a constant instead of a fixed value makes it more clear what that value represents. For instance, by using position < TARGET rather than position < 100, the intention of the guard condition is more clear. Using a constant can thus enhance readability.

Another benefit of constants, is that they can be used multiple times in the same model:

In this modified example it is possible for the object to perform forward as well as backward movements. The step size is the same for both movements, making it possible to use the STEP constant in the updates of both edges. Since a constant is used, the speed of both movements can be changed by changing the value of the constant. Without using a constant, the speed would have to be changed separately for each edge.

Constants are not limited to integer values. Consider the following example, where a more complex value is used:

This example declares a ProductType enumeration, with three different product types: A, B, and C. The DURATION constant indicates for each product type, how long it takes to produce a product of that type. Products of type A can be produced in 3.5 hours, products of type B in 5.7 hours, etc. To get the production duration of products of type C, expression DURATION[C] can be used. For more information, see the lessons on enumerations and dictionaries.

Consider a conveyor belt with a product on it:

The product starts at the left side, at position 0. There is a sensor that can detect the product between positions 13 and 14. The product exits the conveyor at position 18. The following CIF specification models the conveyor, product, and sensor:

The conveyor automaton models the conveyor, with a product on it. The product is modeled by means of the position of the left side of the product, relative to the left side of the conveyor. As the conveyor starts to move, the product moves as well, and its position on the conveyor is updated. The product moves in steps of 0.1.

The width of the product is 6. The sensor is on whenever the product, which spans from position to position + width, is within the sensor range, which spans from 13 to 14. An algebraic variable named sensor is used here, to represent the value of the sensor.

An algebraic variable is a variable whose value is determined by its definition. For the sensor variable, its value is determined from a calculation involving variable position and constant width. Unlike discrete variables, algebraic variables can not be assigned a new value. The value of algebraic variable sensor changes automatically as the value of discrete variable position changes. The value of algebraic variable sensor is true whenever the product is over the sensor, and it is false otherwise.

If we had modeled the value of the sensor as a discrete variable, we would have had to update the variable for every edge where the value of variable position is updated. In this example, that is only one edge. However, if the variable would have been updated on multiple edges, the sensor value would also have to be updated for all those edges. Furthermore, when adding another edge that updates the position variable, the edge needs to be adapted to also update the sensor discrete variable, which can easily be forgotten. Using an algebraic variable, the value computation needs to be specified only once, and no changes to its value are needed, as the value always remains consistent with its definition.

Algebraic variables can be used to give an expression (computations) a name, similar to how constants can be used to give fixed values a name. The benefits of using an algebraic variable are similar to the benefits of using constants. Both can be used to improve readability, and to make it easier to consistently change the model.

Algebraic variables can also be used as an abstraction. Consider the following extension of the specification:

The idea is to have a light turn on when a product is detected by the sensor, and have it turn off when the sensor no longer detects the product. The algebraic variable sensor is used in the guard conditions of the light automaton, to determine when the light should be turned on or off.

In the example, the light automaton only uses the sensor variable from automaton conveyor. It does not matter how the value of that variable is defined. Currently, it is defined in terms of variable position and constant width. However, if the conveyor automaton were modeled differently, the expression that defines the value of the algebraic variable could be changed, without the need to change the use of the variable in automaton light.

Consider the following CIF specification:

The car is initially idle. Once you start driving, the car is moving. Once you stop driving, the car is idle again. While moving it is possible for a breakdown to occur, meaning the car is broken. Once a mechanic starts the repair (start_repair), the mechanic is repairing the car. Once it is repaired, the car is idle, and you can start driving it again, etc.

Algebraic variable can_drive indicates whether you can currently drive the car. As the value calculation indicates, the car can be driven whenever it is idle or moving. That is, it can’t be driven if the car is broken or a mechanic is repairing it.

In the example above, the value of the algebraic variable is defined with the declaration, as was already explained in the lesson that introduced algebraic variables. However, it also possible to specify the value separately, using an equation:

This allows for separation of variable declarations and equations. Both variants have the same algebraic variable with the same value. An equation of an algebraic variable must be placed in the same component as where the algebraic variable is declared. In the example above, the equation for algebraic variable can_drive must be placed in automaton car, as that is where the algebraic variable is declared.

For algebraic variables declared in automata, it is also possible to specify the value using an equation per location of the automaton:

Every algebraic variable must have a unique value in every situation. Algebraic variables must thus have a value with their declaration, a single equation in the same component, or an equation in every location of the automaton. For every algebraic variable, one of the three variants must be chosen. It is allowed to choose a different variant for different algebraic variables, but it is not allowed to use multiple variants for the same algebraic variable.

Which variant fits best for a specific algebraic variable, depends on the situation. One of the benefits of using an equation per location, is that the equations are checked for completeness. If you add a new location, you must add an equation to that location as well, as otherwise the model is invalid (incomplete). This means you can’t forget to specify the value of the algebraic variable for that new location. If you use a value with the declaration or a single equation in the component, you might forget to update the value for the changes you made to the automaton.

Consider this slightly modified version of an example from the lesson on constants:

This example declares a ProductType enumeration, with three different product types: A, B, and C. The M1_DURATION constant indicates for each product type, how long it takes to produce a product of that type, on machine 1. Products of type A can be produced in 3.5 hours, products of type B in 5.7 hours, etc. Constant M2_DURATION is similar, but for machine 2.

The type of both constants is the same. To avoid having to repeat complex types in multiple places, a type declaration can be used:

A type declaration with name Durations is introduced, and Durations can then be used wherever a type is expected, instead of dict(ProductType:real). In the example above, Durations is used as type of the two constants. The original specification and the one with the type declaration have the same constants, with effectively the same type. That is, in both specification the value of constant M1_DURATION is a dictionary with three key/value pairs.

Type declarations can be used to give a type a name, similar to how constants can be used to give fixed values a name, and algebraic variables can be used to give computations a name. The benefits are also similar, as type declarations can be used to make specifications more concise, to increase readability, and to make it easier to consistently change types throughout the specification.

So far, the tutorial has only used discrete event models as examples, which are all untimed. This lesson introduces the concept of timing.

In CIF, time starts at zero (0.0). Time can progress continuously. That is, after one unit of time has passed, the model time is 1.0. After an additional one and a half time units have passed, the model time is 2.5, etc. By default, one time unit corresponds to one second. However, you can decide to use another unit, and tools such as the simulator can be configured to speed up or slow down the simulation accordingly.

In the lesson that introduced timing, variable time was used. Variable time uses absolute model time, i.e. the total amount of time that has passed since the start of the simulation. It is usually easier to use relative model time, i.e. a certain amount of time passes after a certain event. This is where continuous variables are ideal. A continuous variable is a variable that changes value automatically, as time progresses. Consider the following CIF specification:

This specification models a machine that is initially idle. The machine can start to produce a product. After a while, it is done producing. Due to having finished the product, it becomes idle again, until it is starts to product the next product.

Continuous variable t is declared to initially have value 0. Its derivative is 1, meaning that every unit of time that passes, the value of t increases by 1. Every time the start event happens, the value of continuous variable t is reset to 0 using an assignment. As a result of this reset, t will be 0 when the automaton enters the producing location. The edge for the finished event indicates that the event can only happen when t >= 3 holds. This condition will hold after three time units. This means that automaton machine remains in the producing location for three time units, before going to the idle location. It will thus always take three units after entering the producing location, before the guard becomes enabled, and the finished event can take place. The state space is as follows:

The states are labeled with the first letters of the names of the current locations of automaton machine and the current values of variables time and t.

Continuous variables always have real values. Similar to discrete variables, if their initial value is not specified, it is 0.0:

The derivative of a continuous variable can be used as a variable as well. The derivative of continuous variable t is t'. A derivative is read only; it can not be assigned. Similar to algebraic variables, it is always equal to its definition. In the case of variable t, its derivative is always 1. The values of variables time, t, and t' as time progresses are:

Consider the following CIF specification:

This specification models a person walking back and forth. Every time that the person has walked 10 time units, (s)he will turn around, walking in the other direction.

In the example above, the derivative of the continuous variable is defined with the declaration, as was already explained in the lesson that introduced continuous variables. However, it also possible to specify the derivative separately, using an equation:

This allows for separation of variable declarations and equations. Both variants have the same continuous variable with the same derivative. An equation of a derivative of a continuous variable must be placed in the same component as where the continuous variable is declared. In the example above, the equation for t' must be placed in automaton person, as that is where t is declared.

We could extend this specification to keep track of the direction that the person is moving:

For continuous variables declared in automata, it is also possible to specify the derivative using an equation per location of the automaton. This allows us to keep track of the exact position of the person:

Here, the continuous variable t has been renamed to pos, to make it more clear that it indicates the position of the person. As long as the person is moving away, the derivative of pos is 1, and the person moves away, one place every time unit. When the person reaches position 10, the position is not reset to zero. Instead, only the location is changed to the back location. In that location, the derivative of pos is -2. This means that every time unit, the position decreases by 2. That is, the person back to the original position, but at twice the speed. The values of variables time, pos, and pos' as time progresses are:

As with algebraic variables, every continuous variable must have a unique derivative in every situation. Continuous variables must thus have a derivative with their declaration, a single equation in the same component, or an equation in every location of the automaton. For every continuous variable, one of the three variants must be chosen. It is allowed to choose a different variant for different continuous variables, but it is not allowed to use multiple variants for the same continuous variable.

Consider the following non-linear system:

Variable V models the water volume of a tank. The water volume of the tank changes based on the incoming flow of water Qi and outgoing flow of water Qo. The tank can be modeled using the following CIF specification:

Initially, the tank is filled with 5 liters of water. The incoming flow is constant at 1 liter per second. The outgoing flow increases as the water volume of the tank increases.

By separating the declarations of the three variables from their equations, the specification becomes more readable:

The values of the variables as time passes are shown in the following figure:

CIF features different kinds of variables, that have different functionality. Each is better suited for a particular purpose. The following table gives an overview:

Discrete variables can only change value when given an explicit new value by means of an assignment. They don’t change automatically as time progresses.

Algebraic variables can’t be assigned. Instead, their values depend on their declarations or equation(s). If the computations that result in their values depend on a variable that can change value as time progresses, then so can the values of the algebraic variables. Algebraic variables are used as named shorthand notations for computations, for readability, reuse, consistency, and abstraction.

Continuous variables automatically change value as time progresses, as specified by their derivatives. They can also be assigned new values, from which they then automatically change again, based on the current values of their derivatives.

The derivatives of the continuous variables can be seen as variables themselves. Their values depend on their declaration or equation(s). If the computations that result in their values depend on a variable that can change value as time progresses, then so can the values of the derivatives.

In CIF, urgency indicates whether or not time may progress. CIF has three forms of urgency: event urgency, location urgency, and edge urgency. Edge urgency should be avoided, and is not explained here.

This lesson explains the concepts of deadlock and livelock.

Consider the following figure of a producer and two consumers, where rectangles represent entities and the arrows represent the data that is communicated:

The producer creates products, identified by a unique identification number. Each product produced by the producer, is provided either to the first or to the second consumer. Consider the following CIF specification:

The producer keeps track of the identification number (variable nr) of the current product, and provides products to either the first consumer (event provide1) or the second consumer (provide2). Both consumers have an identification number of their current product as well (variable nr in the consumer automata). Initially, the consumers don’t have a product, as indicated by value -1. When a consumer gets a new product, it looks up the identification number of the product at the producer, and stores it locally. The producer then moves on to the next product, by increasing its current identification number.

We can identify two problems in this model.

The first problem is that we need two events in order for the producer to provide products to either the one consumer or the other consumer. If we used only one event, both consumers would need to use that event, have the event in their alphabet, and would thus have to simultaneously participate in the synchronization. A consequence of having an event per consumer, is that the producer automaton has both events on its edge. Adding a third consumer entails having to add another event, as well as having to modify the edge of the producer automaton. This is not a nice scalable solution.

The second problem is that the consumer refers directly to the nr variable of the producer automaton. This introduces a very tight coupling between the producer and the consumers. It exposes the nr variable of the producer to the consumers, making it more difficult to change the producer without changing the consumers.

Both these problems can be solved by using channels. Channels are a special form of events, that can be used to communicate or transmit data from a sender to a receiver. In our example, data that is communicated are the identification numbers of the products, the producer is the sender, and the consumers are the receivers.

Channels require one or more potential senders, and one or more potential receivers. Automata cannot be both sender and receiver for a single channel. They may however be a sender for one channel, and a receiver for another channel. For every transition, exactly one of the senders and exactly one of the receivers participate. The sender sends a value, and the receiver receives that value. This type of communication is often called channel communication or point-to-point communication, as the data is communicated from one point (the sender) to another point (the receiver).

Multiple automata that synchronize over the same event perform a transition together. Similarly, a sender and receiver that together perform a channel communication, perform a transition together. In both cases, all automata involved take their respective edges synchronously (simultaneously).

Channels are ideally suited for modeling product flows, or more generally the movement of physical entities through a system. Physical objects usually don’t duplicate themselves or spontaneously stop to exist. This fits nicely with channels, where data is communicated or passed along from exactly one sender to one receiver. In our example, product produced by the producer are physically provided to one of the consumers.

The following CIF specification models the above example using channels:

The provide1 and provide2 events have been replaced by a single channel named provide. Channels are declared similar to events, but have a data type that indicates the type of values that are communicated over the channel. In this case integers are communicated.

The producer now uses the channel on its edge, instead of the two events. The exclamation mark (!) after the channel name means that the producer is sending over the channel. After the exclamation mark, the value that the producer sends is given. In this case, the producer sends the identification number of its current product.

The edges of the consumers have been modified as well. The channel is used with a question mark (?) after the channel name, indicating that the consumers receive over the channel. The received value, which is available as the ? variable in the update, is directly assigned to the nr variable of the consumer.

By using channels, we no longer need multiple events, and the producer does not need to be modified if another consumer is added. This makes the model scalable to varying amount of consumers. Furthermore, the consumers now use the ? variable to obtain the received value, and no longer need direct access to the variables of the producer. This makes it easier to modify the producer without having to also modify the consumers.

To conclude this lesson, we’ll extend the example with a second producer:

The producer automaton has been renamed to producer1, and a producer2 has been added. Both producers independently produce products and provide them to the consumers. Both consumers can receive products from either producer. At all times, four transitions are possible: producer1 communicates with consumer1, producer1 communicates with consumer2, producer2 communicates with consumer1, or producer2 communicates with consumer2.

Besides channels that communicate data, it is also possible to use dataless channels. A channel that does not communicate any data, is declared with the void type. Dataless channels are also called void channels. When using dataless channels, the sender does not provide a value to send over the channel. Also, the receiver cannot use the received value (variable ?) since no data is communicated.

Dataless channels are used in the same situations as 'normal' channels, for instance when physical product flow is modeled. If products don’t have an identification number, and can not be distinguished based on color or some other property, all products are essentially equal. It is then sufficient to communicate that a product is being 'transferred'. No further data is needed. While it is possible to communicate dummy values, dataless channels provide a better solution in such cases.

Consider again the producer/consumer example from the previous lesson, with one producer and two consumers, but without identification numbers for the products:

The producer still produces products and provides them to either the first or the second consumer.

Consider again the producer/consumer example with two producers and two consumers, from a previous lesson:

Now assume we want to restrict communication to allow at most five products in total to be provided to the consumers. We could adapt both producers, as follows:

Each producer gets an additional guard condition whether it may provide a product to one of the consumers. If the total number of products provided by both providers does not exceed five, they may still provide a product. Having to adapt both producers is less than ideal.

As an alternative solution, we can add an additional automaton, instead of adapting the producers:

This controller automaton (together with the original producer automata) keeps track of the number of products provided to consumers, by counting them in variable cnt. It only allows the provide event when less than five products have been provided. If five or more products have been provided, it disables the provide event.

In the controller automaton, the provide channel is used as an event rather than a channel. When one of the producers and one of the consumers together perform a channel communication, the controller automaton that has the provide event in its alphabet, must synchronize with it. This allows the controller to impose additional restrictions on the channel communication, allowing or forbidding it in certain cases. The controller is added as a separate process, which improves scalability.

In general, every automaton may either send over a channel, receive over a channel, or synchronize with a channel. An automaton may not take on more than one of these roles, for a single event. It may however send over one channel, receive over another channel, and synchronize with yet another one.

Every event transition for a channel requires exactly one automaton that participates as sender, and exactly one automaton that participates as receiver. Furthermore, all automata that have the channel in their alphabet, must additionally participate as well, by synchronizing together with the sender and receiver. Automata that send or receive over a channel, do not have that channel in their alphabet. Only automata that synchronize with an event or channel have that event or channel in their alphabet.

Automata that synchronize over a channel can be used to further restrict the allowed channel communications, as shown in the above example. It is however also possible for the additional synchronizing automata to monitor (observe) the channel communication.

Functions can be used to compute values from other values. CIF has many built-in functions, called standard library functions. An example is the size function, which takes a list and returns the number of elements of the list. Another example is the abs function, which takes an integer or real number and computes the absolute value of that number.

While many built-in functions are available, they may not always suffice. User-defined functions can be added to CIF models, to allow custom computations needed by the model. By putting the calculation in a user-defined function, the calculation can be used in several places, allowing for reuse. Furthermore, functions allow for more complex computations than would otherwise be possible.

CIF features two kinds of user-defined functions: internal ones and external ones. Internal user-defined functions are fully defined within the CIF model. External user-defined functions declare only a header which indicates the existence of the function, while the actual implementation is obtained from an external source. The lessons of this category only explain internal user-defined functions. The language reference documentation gives more information on external user-defined functions.

The most commonly used kind of user-defined functions are the internal user-defined functions. Consider the following CIF specification:

This specification defines a function (keyword func) named mean. After the name of the function, between the parentheses, the parameters are listed. The parameters are the input values, which the function can use to compute its result. In this example, the function takes a list of real values as its only parameter. Parameter name vs can be used in the body of the function to refer to this input value. Just after the func keyword, the type of the result of the computation is specified. In this case, the function results in a real typed value. The mean function takes a list of integer values and produces a single real value as result.

In the body of the function, local variables can be declared. The mean function declares three variables: length, index, and sum. Local variables of functions are very similar to discrete variables. The main difference is that they are declared without the disc keyword. In the example, length is set to the number of elements in list vs. Variables index and sum are both initialized to 0.

After the local variables (if any), the statements of the body are given. The statements implement the algorithm, the actual computation of the function. Statements are executed one after another, in the order they are given. In the mean function, the while statement is executed before the return statement. The mean function first calculates the sum of the input values, and then returns the mean value. The details of the statements are discussed in the next lesson.

A function can be called (or applied) on concrete input values, to obtain the computation result for those specific input values. For instance, consider the following extension to the above CIF specification:

Algebraic variable m is given the value that results from calling function mean on a single argument, a list with four values. Each argument of a function call must match with the corresponding parameter of the function being called. In this case, the list of four real values matches with the vs parameter of the mean function, which has type list real. Variable m becomes 7.1, as the mean of those four values is 7.1 ((1.5 + 3.2 + 7.9 + 15.8) / 4).

The edge in automaton a assigns a value to variable x. The mean of a list of three values is calculated, and multiplied by two, to obtain the new value of x. The mean of 0.4, 1.5, and 6.8 is (0.4 + 1.5 + 6.8) / 3, which is 2.9. Variable x gets 5.8 (2.9 * 2) as its new value.

Function mean is called in two places in the example, showing reuse of calculations.

Functions in CIF are mathematical functions. That is, the result of a function is the same for the same input values, and functions have no side effects. Functions can not directly access variables outside their body. For example, they cannot access discrete, continuous, and algebraic variables. They can also not use variable time. To use the values of those variables in a function, they have to to be passed in through parameters.

This lesson explains the different statements that can be used in internal user-defined functions:

Functions can be used as values. By treating them as data, they can be stored in variables, and passed to other functions. This lesson shows one example of how that can be useful.

Consider the following list of numbers:

Now assume we wanted to sort these numbers both in increasing and in decreasing order, using a single sorting function:

Variable inc contains the same numbers as nrs, but sorted in increasing order, while dec contains them in decreasing order. We use the same sort function in both cases, but with different comparison functions:

Function cmp_inc takes two real numbers and returns true only if the first number is smaller than the second one (a and b are in increasing order). Function cmp_dec has the same parameters, but returns true only if the first number is larger than the second one (a and b are in decreasing order). The sort function is defined as follows:

The sort function has two parameters. The first parameter is xs, which contains the values to sort. The second parameter is cmp, the compare function to use to determine whether two numbers are correctly ordered. The cmp parameter has type func bool (real, real), which means that a function that has two real parameters and a boolean return value is required. The cmp_inc and cmp_dec functions satisfy these requirements, and can be used as second argument when the function is called to determine the values of algebraic variables inc and dec.

The sort function implements a standard insertion sort algorithm. The cmp parameter is used in the sort function to compare two consecutive values in xs, and swap them if they are not correctly ordered.

The cmp parameter of the sort function has a function type, allowing compare functions to be passed to the sort function, as data. This allows the sort function to sort lists of numbers in different orders, depending on the compare function that is provided.

Parts of a system that are nearly identical, are often modeled as nearly identical automata. Having to specify them multiple times can be burdensome. It can also hinder scalability, as changes to one of them usually need to be applied to the others as well. Consider again the producer/consumer example from the lesson that introduced channels:

The producer provides products either to the first consumer or to the second consumer. The consumers are modeled using identical automata. Only the names of the consumer1 and consumer2 automata differ. Ideally, we would have a sort of consumer template, and use that template twice, once for each of the actual consumers. This can be achieved in CIF using an automaton definition (the template) and two automaton instantiations (the uses of the template):

The Consumer automaton definition is identical to the original consumers, except that it is an automaton definition rather than an automaton. An automaton definition can be identified by the def keyword between the automaton keyword and the name of the automaton definition, as well as by the parentheses after its name. As a convention, names of automaton definitions start with an upper case letter (Consumer rather than consumer).

An automaton definition by itself is not an automaton. The instantiations of the automaton definition (consumer1 and consumer2) however, are automata. Before the colon (:), the name of the instantiation is given. This name is also the name of the actual automaton. After the colon, the name of the automaton definition that is instantiated is given.

Using an automaton definition, the above example models the behavior of a consumer only once. Adding a third consumer is as easy as adding another automaton instantiation, which takes only one line of code (consumer3: Consumer();). Changing the behavior of all consumers only requires changes to the common automaton definition. Automaton definition/instantiation allows for scalability and reuse, and also improves maintainability.

Automaton definition/instantiation can be eliminated, by replacing all automaton instantiations by the automaton definitions that they instantiate, and changing the automaton definition header (automaton def Consumer():) by an automaton header (automaton consumer1:). If we do that for the example above, we obtain the original specification from the beginning of this lesson. The two specifications are functionally equivalent. Automaton instantiation consumer1 is also often referred to as automaton consumer1, when there is no confusion.

In the previous lesson, automaton definition/instantiation was used to obtain two identical automata, while only having to specify their behavior once. What we have seen so far, is enough for exactly identical automata, but not for nearly identical automata. Consider the following two nearly identical consumers:

The consumers can accept products that the producer provides (channel provide). They store the identification numbers of those products in a buffer. The two consumers are identical except for the number of products that they can accept: the first consumer can accept two products, the second producer can accept three products. We can still use automaton definition and instantiation to model the consumer only once, but we need to parametrize the automaton definition:

The Consumer automaton definition now has a parameter named capacity that indicates how many identification numbers can be stored in its buffer. The automaton instantiations consumer1 and consumer2 provide an argument (2 and 3 respectively) to match the parameter of Consumer. That is, the instantiations indicate their capacity. Using parameters, the Consumer automaton definition models the behavior of both automata consumer1 and consumer2, even though they have different capacities.

The details of the different kind of parameters of automaton definitions are explained in the next lesson.

In the previous lesson, an automaton definition with parameter was used. The parameter was an algebraic parameter, which is only one of the different kinds of automaton definition parameters. This lesson explains each of them:

This lesson also explains how to use multiple parameters.

For large CIF specifications with many automata, it can be beneficial to add more structure to the specification. For this purpose, CIF has groups. Groups are named collections of automata and other declarations. For instance, consider the following CIF specification:

This specifications features four automata that model the behavior of machines. The details of the actual automata are omitted, as they are irrelevant for this lesson. All four machines are in the same factory, but they are divided into two halls. This physical subdivision is expressed in the CIF specification using groups named factory, hall1, and hall2. While in this case the subdivision into a hierarchical specification structure is based on the physical subdivision of the actual system, the modeler is free to base the specification structure on other criteria.

Consider also the following partial CIF specification:

The configuration group is used to group together several configuration values, modeled by constants. By grouping these constants together, it is more clear that they together are the configuration settings of the system, and that they belong together.

Finally, consider the following CIF specification, based on the non-linear system from the lesson on equations.

By grouping the declarations and their equations together, it is becomes clear that together they model a tank. This is especially useful if other parts of the specification model something different.

Similar to how automaton definitions can be used for reuse of automata, group definitions can be used for reuse of groups:

Automaton definition Machine models a machine, but most of the details are omitted here, as they are not relevant for this lesson. Group definition Hall models that each hall has two machines. Similarly, group definition Factory models that each factory has two halls.

Automata and groups are both components in CIF. Automaton definitions and group definitions can together be called component definitions. If we eliminate all component definitions and their instantiations, by replacing instantiations by their definitions, we get the following CIF specification:

Group definitions may be parametrized using the same kinds of parameters as automaton definitions.

For large systems, having to model the entire system in a single CIF file can lead to long CIF specifications. Being able to split that single CIF file into multiple CIF files can help. Consider the following two CIF specifications in CIF files producer.cif and consumer.cif respectively:

The two CIF specifications together form a simplified producer/consumer system. The producer.cif file declares the provide event and the producer automaton. The producer can provide a product.

The consumer.cif file declares the consumer automaton, that can accept products provided by a producer. The provide event is not declared in that CIF specification. However, the producer.cif file is imported, which does declare that event. By importing another CIF specification, all declarations from that imported CIF specification (producer.cif in the example) become available in the importing CIF specification, i.e. in the specification that does the import (consumer.cif in the example).

The result of the import in consumer.cif is:

You can think of an import as being replaced by the content of the imported file. The producer.cif file contains only its own content, while the consumer.cif file contains the contents of both files, due to the use of the import.

If one CIF specification is merged into another CIF specification, the names of the declarations in both CIF specifications must be different. It is not allowed to have declarations with the same name in multiple CIF specifications. For instance, in the example above, if the provide event were declared in both CIF specifications, the imports would be invalid. Exceptions to this rule are discussed in one of the next lessons, which explains the relation between imports and groups.

Using imports, it is possible to make libraries that can be used by multiple CIF specifications. For instance, consider the following CIF specification in file math.cif:

This CIF specification declares a single function inc that takes an integer number and returns that number incremented by one. Now also consider the following CIF specification in file counter.cif:

By importing the math.cif file, the counter automaton can use the inc function. Other CIF files could similarly import the math.cif file, essentially turning math.cif into a library.

It is possible to make a function library, consisting of commonly used functions, a constant library, with commonly used constants, or an automaton definition library, with automaton definitions. As libraries are just CIF files, they can contain anything as long as they are valid CIF files. Essentially, every CIF file that is imported in more than one other CIF file can be considered a library.

The import as used above, only works if both CIF files are in the same directory. Library files however, are often placed in a different directory. Consider the same two CIF files, but organized into directories (or folders) as follows:

Directory system contains a sub-directories named libraries, which contains the math.cif library. The system directory also contains the counter.cif file. The import in the counter.cif file needs to be adapted to refer to the math.cif file in the libraries directory:

Large systems can be hierarchically modeled using groups. When using imports, two specifications may not have declarations with the same name. Groups however, are the exception to this rule. Consider a factory with two machines, each consisting of two parts. We can model this using five files, one for each of the parts of the machines, and one for the factory as a whole. The following CIF specifications show the contents of the five CIF files, where the comment at the first line indicates which file it is:

The four CIF specifications for the machine parts differ only in their group and automaton names. Their implementations are kept identical for simplicity. The factory.cif file imports all four part specifications, which together form the full factory. The effect of the imports in factory.cif is the following:

For groups with the same name, the contents of the groups is merged together. That is, automaton part1 in the machine1 group from one CIF file, and the automaton part2 in that same machine1 group from another CIF file, end up in a single machine1 group after eliminating the imports.

In general, contents of groups with the same name are merged into a single group. This works also for groups in groups, groups in groups in groups, etc. If two CIF files that are imported both contain a group a and in both CIF files those groups contain a group b, then the contents of both a groups are merged, and also the contents of both b groups are merged. It is not allowed for different CIF files to have declarations with the same name in the same group. It is allowed to have declarations with the same name in different groups. The file itself (the top level) can be considered a group as well.

When using imports and groups to model large hierarchical systems, it is a common pattern to have groups around the entire specification:

The groups around the entire specification lead to additional indentation. As this is a common pattern, the CIF language provides namespaces to reduce the impact of large numbers of top level groups:

The factory.machine1.part1 namespace has exactly the same effect as the original three groups. Both specifications can thus be considered identical.

Input variables can be used to model that some data exists, without specifying the value or how or when the value changes. Input variables are used in cases where the CIF model is to be connected something else that provides the values.

For many things in the world, the behavior is not the same every time. An example is a coin toss, where the result can be either heads or tails. Tossing a coin exhibits randomness. It is possible to model the different variants in a CIF model without specifying the likelihood of each of the outcomes. This approach was used in the lesson on non-determinism.

It is however also possible to explicitly specify the likelihood of each of the outcomes in the CIF model, using a stochastic distribution (also called probability distribution). A stochastic distribution describes how likely the different outcomes are. There are many different stochastic distributions. The Bernoulli distribution for instance, can be used to model things with two potential outcomes, such as a coin toss.

Consider the following CIF specification:

Variable d holds a stochastic distribution that produces boolean values (true or false), as indicated by its dist bool type. In this case it holds a Bernoulli distribution, with a probability of 0.5 (or chance of 50%) for true, and thus also the same probability/chance for false (the only other possible outcome).

The bernoulli function is used to create a Bernoulli distribution with the proper parameter (probability of 0.5 for true). Different distributions have different parameters. See the language reference documentation for further details. Distribution functions, such as the bernoulli function can be used to create distributions with specific parameters, and may only be used to initialize discrete variables.

Initially, the automaton is in its toss location, where the coin can be tossed. The edge uses the sample operator to get a sample from the bernoulli distribution. Each time the distribution is sampled, the outcome is either a true value or a false value. As we used a probability of 0.5 for both outcomes, half of the times true will be the outcome, and the other half of the times false will be the outcome, if we were to sample infinitely many times.

Sampling does not only result in the outcome, but also the distribution itself. This is further explained in one of the next lessons, which explains pseudo-randomness.

The result of sampling is stored in the outcome variable. In the result location, the sampling result is used to make a decision to go to either the heads location (true outcome) or the tails location (false outcome). From there, it is possible to go back to the toss location, to proceed with the next coin toss.

CIF features over a dozen different stochastic distributions. These distributions can be categorized into three categories: discrete, continuous, and constant distributions. Discrete distributions can result in only a limited number of possible values. Examples include tossing a coin (heads and tails) and throwing a dice (six possible outcomes). Continuous distributions can result in all values from a certain range. Examples include the time it takes for a machine to produce a single product (positive amount of time), and the purity of produced medicine (0% to 100%). Constant distributions are discrete distributions that always result in the same sampled value. They are useful during the development of a model, or for debugging. The remainder of this lesson further explains these three categories, and illustrates them using some examples.

So far, the lessons on stochastics used the mathematical notion of stochastic distribution to describe how to model stochastic behavior. Simulating a model with stochastic behavior using a computer is however not stochastic at all. Computer systems are deterministic machines, and have no notion of varying results.

Supervisory controller synthesis (or supervisor synthesis, or just synthesis) is a generative technique, where one derives a supervisory controller from a collection of plants and requirements. Synthesis allows to focus on the what, i.e. which requirements should hold, rather than on the how, i.e. how to implement this in a controller.

The plants describe capabilities or behavior of a physical system 'as is', without any integrated control. They represent the available behavior of the uncontrolled system. Requirements model (a part of) the functions a system is supposed to perform. They represents behavior that is allowed in the controlled system, or more precisely, they specify the behavior that is not allowed in the controlled system. In other words, requirements restrict the behavior of the plants, to ensure that only the desired behavior remains. The goal of supervisory controller synthesis is to compute a supervisory controller (or supervisor) that enforces the requirements, assuming the behavior of the plants, additionally preventing deadlock and livelock, and without restricting the system any further than is required.

It is beyond the scope of the CIF language tutorial to go into the details of supervisory controller synthesis. However, CIF has several features that are used solely of modeling systems for the purpose of supervisory controller synthesis:

These concepts are explained below. When a model is not used for supervisory controller synthesis, e.g. for simulation, these concepts are usually ignored.

Language keywords

Trigonometric functions

General functions

Distributions

Expression operators

Besides the keyword terminals listed above, CIF features several other terminals:

CIF supports spaces, tabs, and new line characters as whitespace. Whitespace is ignored (except in string literals), but can be used to separate tokens as well as for layout purposes. The use of tab characters is allowed, but should be avoided if possible, as layout will be different for text editors with different tab settings. You may generally format a CIF script as you see fit, and start on a new line when desired.

Examples:

CIF features two types of comments. Single line comments start with // and end at end of the line. Multi line comments start with /* and end at */. Comments are ignored.

Examples:

Part of the CIF tooling is a textual editor for CIF specifications. This editor is part of the Eclipse IDE. Below is a list of some of the more notable features of this text editor:

The CIF to yEd transformer can be used to transform CIF specifications to yEd diagrams. Several kinds of diagrams can be generated. These diagrams can be used to better understand the specification, to communicate the specification to other, or to be included in reports.

The yEd Graph Editor is an application that can be used to view, create, edit, arrange, import and export various kinds of diagrams. It is freely available and runs on Windows, Linux, and macOS.

The yEd diagrams are generated as GraphML files (*.graphml files), using yEd specific extensions to specify the graphical representation.

The data-based supervisory controller synthesis tool performs data-based supervisory controller synthesis, or simply data-based synthesis. It can be used to synthesize a supervisor for an untimed CIF specification, with data (e.g. discrete variables). For a CIF specification with plants and requirements, the tool computes a supervisor. The supervisor restricts the plants in such a way that the resulting controlled system satisfies the following properties:

Note that deadlock is not prevented for marked states.

The synthesis algorithm is based on the following paper: Lucien Ouedraogo, Ratnesh Kumar, Robi Malik, and Knut Åkesson: Nonblocking and Safe Control of Discrete-Event Systems Modeled as Extended Finite Automata, IEEE Transactions on Automation Science and Engineering, Volume 8, Issue 3, Pages 560-569, July 2011.

Synthesis, 'supervisor synthesis', or 'supervisory controller synthesis', is a generative technique, where one derives a (supervisor) automaton from a collection of plants and requirements. The resulting supervisor is maximally permissive under the conditions of being free of deadlocks, and always having the option of reaching a marked state.

While there is only one true synthesis tool (the tool that actually derives a supervisor automaton from a collection of plant and requirement automata), other tools exist to support the process. These tools together form the event-based synthesis toolset.

These tools use and modify the sequences of events that can be performed. This in contrast to state-based tools, which operate primarily on the state of the system. Event sequences directly hook into language theory, which places these tools firmly in the language theory mathematical framework.