Version:
v7.0
[release notes]

# Module 2.4: Shared variables

Besides interaction through synchronization on events, automata can also interact by sharing discrete variables. Discrete variables must be declared in automata, and only the automaton that declares a variable can change its value through updates on edges. Variables can thus only be 'written' locally, by the automata that declare them. Other automata can however access the values of the variables, and use them in for instance guards or assign them to their own variables. Variables can thus be 'read' globally, by all automata. This principle is called 'global read, local write'. This prevents that multiple automata write different, conflicting values, when they synchronize on a shared event.

## Example

Consider for instance the following example, with four automata. The first automaton is the `buffer`:

The second one is a `decision_unit`:

The third and fourth are the `even_packer` and `odd_packer`, respectively:

The four automata together model a production line. The `buffer` automaton represents a buffer that can take products (event `take_product`) from a production process. The variable `products` represents the number of products in the buffer. At most 10 products can be stored in the buffer and the products are sold in batches of 5 to 10 products. The operator executes the `send_batch` event when the next batch has reached the desired size.

There are two types of packages in which the batches are sold, even and odd ones, each packaged by a different packaging machine. The `decision_unit` automaton represents a decision unit that decides whether a batch is to be sent to the even or odd packaging machine, once the batch is made available by the operator. The `even_packer` automaton represents the packer for even batches. Similarly, the `odd_packer` automaton represents the packer for odd batches.

The `products` variable is declared in the `buffer` automaton, and all updates to that variable are therefore done in that same automaton. Due to the 'global read, local write' principle, other automata can not update the value of this variable, but they can read it. The guards on edges of the `decision_unit` automaton use the value of the `products` variable declared in the `buffer` automaton. To access the variable of another automaton, the variable name is prefixed with the name of that other automaton and a period, to form `buffer.products`. This is similar to how in the previous sub-module an event declared in another automaton was used.

Remember that it is possible to label one edge with multiple events, as is used here in the `buffer` automaton. The automaton can go from location `Sending` to location `Receiving` by either the `batch_to_even` event or the `batch_to_odd` event, but not both for the same batch. Such an edge is essentially an abbreviation for multiple separate edges, each labeled with one of the events, but with the same source location, target location, guards and updates. This improves the readability of the model, by not having to include many very similar edges.

## Quiz

[ { type: 'single-choice', question: "Can the `even_packer` automaton change the value of the `products` variable?", answers: [ "No, because the variable is declared in the `buffer` automaton and the 'local write' concept states that it can only be changed in the automaton where it is declared.", "Yes, an update can assign new values to variables. It does not matter in which automaton this update is located, because of the 'global read' concept." ], correctAnswer: '1' }, { type: 'single-choice', question: "If the `odd_packer` automaton would have declared the variable `packages` and the `decision_unit` would like to use this variable in one of its guards, would this be possible, and if so, how should the `decision_unit` refer to this variable in its guard?", answers: [ "Yes, this is possible by referring to the variable with `packages.odd_packer`.", "Yes, this is possible by referring to the variable with `odd_packer.packages`.", "No, this is not possible because of the 'local read' concept." ], correctAnswer: '2' }, { type: 'single-choice', question: "What are the shared events in the production line model?", answers: [ "Events `batch_to_even` and `batch_to_odd`.", "Events `batch_to_even`, `batch_to_odd` and `send_batch`.", "Events `batch_to_odd`, `finish_even` and `finish_odd`." ], correctAnswer: '2' }, { type: 'single-choice', question: ` When the `send_batch` event occurs, is then the batch also physically sent? What do you think?`, answers: [ `Yes, the `send_batch` event takes the `buffer` to its `Sending` location and the `decision_unit` to its `Deciding` location. The `send_batch` event is executed when the batch has the desired size according to the operator. So, this event must start the sending process.`, `This depends on the situation. If the decision unit is very fast, the actual sending that happens when the `batch_to_even` or `batch_to_odd` event is executed will almost coincide with the `send_batch` event. When the decision unit is slow, this will not coincide, and the `send_batch` event does not physically send the batch.`, `No, the `send_batch` event synchronizes the `buffer` and `decision_unit`. The `send_batch` event makes sure the decision unit only evaluates the batch size (variable `buffer.products`) on whether it is even or odd when the batch is ready to be sent. The physical sending happens with the `batch_to_even` or `batch_to_odd` event. These events cause the `products` variable to be reset to `0` in the `buffer` automaton, and change the locations of the packaging machines using synchronization.` ], correctAnswer: '3' }, { type: 'single-choice', question: "Would it be possible to add the update `buffer.products := 0` to the edges with the `batch_to_even` and `batch_to_odd` events in the `decision_unit` automaton, instead of the update `products := 0` of the edge labeled with both the `batch_to_even` and `batch_to_odd` events in the `buffer` automaton?", answers: [ "No, because then you try to change a variable in a different automaton than in which it was declared. This is not possible according to the 'local write' concept.", "No, because then you try to change a variable in a different automaton than in which it was declared. This is not possible according to the 'global read' concept.", "Yes, an update can assign variables a new value. It does not matter in which automaton this update is declared because of the 'global write' concept." ], correctAnswer: '1' }, { type: 'single-choice', question: ` The packing machines can only pack one batch at a time. Is this restriction properly modeled? In other words, is it never the case that the packing machine receives another batch while it is still packing?`, answers: [ `This restriction is properly modeled. A machine can only receive a batch when the buffer, decision unit and packaging machine are in location `Sending`, `Deciding` and `Idle`, respectively, because in these three locations, an edge with event `batch_to_even` or `batch_to_odd` is present. This means that a machine first needs to finish a batch (event `finish_even` or `finish_odd`) to go back to its `Idle` location, before the three automata can synchronize on `batch_to_even` or `batch_to_odd` again, for a new batch.`, `This is not properly modeled. When the decision unit executes the `batch_to_even` or `batch_to_odd` event, the corresponding packaging machine will be sent a new batch without looking whether it is already busy.` ], correctAnswer: '1' }, { type: 'single-choice', question: "If the even packer would like to know how many products it received from the buffer, how could that be achieved?", answers: [ "This is not possible, due to the 'local write' principle.", "This is not possible, due to the 'global read' principle.", "It could perform the `products := buffer.products` assignment, to assign its own local variable named `products`." ], correctAnswer: '3' } ]