g?var: T \(\rightarrow\) an input of type T is expected through the gate g.
g! constant \(\rightarrow\) an output (constant) is exposed through the gate g.
Additional operators allow building more complex processes:
Sequential composition (;)
Several events can occur in a sequence. For example, g? x: int; g!x+1 represent two events (at two different instants of time). In the first one, it is expected to synchronize on an integer input, while in the second one it is expected to synchronize on the output that is the value received plus one.
We can now define a process P with a gate g that it always receives a value and exposes the value incremented:
process P[g] =
g?x:int ; g!x+1; P[g]
The last element in the sequential composition (P[g]) indicates that a new instance of the process starts when reaching to this point.
Choice ([])
The operator Choice ([]) allows representing the choice between two (or more) paths.
For example,
g! "hello"
[]
g! "world"
allows either exposing "hello" or "world" through the gate g.
Guards ([condition] \(\rightarrow\))
In general, choice conditions are non-deterministic (or more precisely, dependent on the environment). To add conditions, we can use guards combined with the choice operator:
[condition1] \(\rightarrow\) behavior1
[]
[condition2] \(\rightarrow\) behavior2
Then, the behaviors enabled depend on the conditions. For example, let P be a process having been instantiated with a variable x
P[g](x: int)
[x <0] \(\rightarrow\) g! -x; g? y: int; P[g](y)
[]
[x >= 0] \(\rightarrow\) g! x; g? y: int; P[g](y)
This process has an if-else like behavior. It exposes the absolute value of x, receives a new value from the environment (y), and creates a new instance of the process with this value.
No comments:
Post a Comment