-
Notifications
You must be signed in to change notification settings - Fork 13
Synchronized_Operator
Synchronized Operator¶
Syntax¶
processBehaviour "||" processBehaviour
Semantics¶
process1 || process2
process1 and process2 are executed while synchronized over all channels, including EXIT.
When both processes have exited then the synchronized composition exits.
Examples¶
Communication¶
The statement
Channel1_Int ? x || Channel1_Int ? y
describes the process with two sub processes that are synchronized over all channels.
Since both sub processes want to communicate over Channel1_Int, communication is possible.
After that communication has occurred x and y contain the same value, and
since both communications have exited, the synchronized composition exits.
Constrained communication¶
The statement
Channel1_Int ? x [[ x >= 10 ]] || Channel1_Int ? y [[ y <= 20 ]]
describes the process with two sub processes that are synchronized over all channels.
Since both sub processes want to communicate over Channel1_Int and
both constraints can be simultaneously satisfied, communication is possible.
After that communication has occurred x and y contain the same value in the range [10,20]
and, since both communications have exited, the synchronized composition exits.
Deadlock¶
The statement
Channel1_Int ? x || Channel2_Int ? y
describes the process with two sub processes that are synchronized over all channels.
Since one sub process wants to communicate the variable x over Channel1_Int and
the other sub process wants to communicate the variable y over another channel, Channel2_Int,
communication under the synchronization constraint is not possible, i.e., the process is in deadlock.