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
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'
}
]