Legend:
- The triangle is |>
- \sigma is just \sigma
- The reduction arrow is ---> p->q;0 ---> 0
- The downarrow evaluation operator is \eval
- Structural precongruence is <=
- Structural equivalence is ===
- The oplus is either \oplus or +
- Reductum: the right-hand side of a reduction. For example, in C -> C', C' is the reductum.
---
p -> q; r -> s; 0 ---> p -> q; 0
----------------------------------- Com
p -> q; r -> s; 0 <= r -> s; p -> q; 0 r -> s; p -> q; 0 ---> p -> q; 0 p -> q; 0 <= p -> q; 0
----------------------------------------------------------------------------------------------------------- Struct
p -> q; r -> s; 0 ---> 0
---
Write a (projectable) choreography for:
- p sends a product name to q;
- q replies with the price for the product;
- p decides whether the price is ok:
* if the price is ok:
- p sends some money (corresponding to the price) to b;
- q sends the product to p.
* if the prices is not ok:
- nothing happens.
You are free to insert selections as necessary to make the choreography projectable. You don't need to define the functions used by processes
in interactions.
p.prod -> q.x;
q.price(x) -> p.y;
if p.ok(y) then
p -> b[ok];
p -> q[ok];
p.money(y) -> b.m;
q.prod(x) -> p.yahoo;
0
else
p -> b[ko];
p -> q[ko];
0
---
Write a proceduce Buy(p,q,b) that implements the following:
- p sends a product name to q;
- q replies with the price for the product;
- p decides whether the price is ok:
* if the price is ok:
- p sends some money (corresponding to the price) to b;
- q sends the product to p.
* if the prices is not ok:
- p locally computes a new product it may wish to buy
- we invoke procedure Buy again.
You are free to insert selections as necessary to make the choreography projectable. You don't need to define the functions used by processes
in interactions.
Buy(p,q,b) =
p.prod -> q.x;
q.price(x) -> p.y;
if p.ok(y) then
p -> b[ok];
p -> q[ok];
p.money(y) -> b.m;
q.prod(x) -> p.yahoo;
0
else
p -> b[ko];
p -> q[ko];
p.anotherProduct;
Buy(p,q,b)
---
Show all reduction chains for the configuration , where
C =
p.f -> q.x;
if q.x then
q.g;
0
else
0
and \sigma is such that f(\sigma(p)) = true.
->
<
if q.x then
q.g;
0
else
0
,
\sigma'
>
->
->
<0,\sigma''>
where
\sigma' = \sigma[q |-> h'] and \sigma(q) = h and h'=h[x|->true]
\sigma'' = \sigma'[q |-> v] and g(\sigma'(q)) \eval v
---
Write the EPP of:
r -> s; s -> p; q -> b; 0
r |> s!;0 | s |> r?; p!;0 | p|> s?;0 | q |> b!;0 | b |> q?;0
---
Is this choreography
r -> s; s -> p; q -> b; 0
operationally correspondent to this network
r |> s!;0 | s |> r?; p!;0 | p|> s?;0 | q |> b!;0 | b |> q?;0
?
Yes, because:
(Completeness)
Choreography reduction:
r -> s; s -> p; q -> b; 0
--->
s -> p; q -> b; 0
corresponds to:
r |> s!;0 | s |> r?; p!;0 | p|> s?;0 | q |> b!;0 | b |> q?;0
--->
s |> p!;0 | p|> s?;0 | q |> b!;0 | b |> q?;0
which is the EPP of the reductum of the choreography.
Choreography reduction:
r -> s; s -> p; q -> b; 0
--->
r -> s; s -> p; 0
corresponds to:
r |> s!;0 | s |> r?; p!;0 | p|> s?;0 | q |> b!;0 | b |> q?;0
--->
r |> s!;0 | s |> r?; p!;0 | p|> s?;0
which is the EPP of the reductum of the choreography.
(Soundness)
Network reduction:
r |> s!;0 | s |> r?; p!;0 | p|> s?;0 | q |> b!;0 | b |> q?;0
--->
s |> p!;0 | p|> s?;0 | q |> b!;0 | b |> q?;0
Corresponding choreography reduction:
r -> s; s -> p; q -> b; 0
--->
s -> p; q -> b; 0
And the reductum of the network is the EPP of the reductum of the choreography.
Network reduction:
r |> s!;0 | s |> r?; p!;0 | p|> s?;0 | q |> b!;0 | b |> q?;0
--->
r |> s!;0 | s |> r?; p!;0 | p|> s?;0
Corresponding choreography reduction:
r -> s; s -> p; q -> b; 0
--->
r -> s; s -> p; 0
And the reductum of the network is the EPP of the reductum of the choreography.
---
Is this choreography
r -> s; s -> p; 0
operationally correspondent to this network
r |> s!;0 | s |> r?; p!;0 | p|> s?;0 | q |> b!;0 | b |> q?;0
?
No, because there is a network reduction that the choreography cannot match.
r |> s!;0 | s |> r?; p!;0 | p|> s?;0 | q |> b!;0 | b |> q?;0
--->
r |> s!;0 | s |> r?; p!;0 | p|> s?;0
---
Does procedure Buy, defined below, terminate?
Buy(p,q,b) =
p.prod -> q.x;
q.price(x) -> p.y;
if p.ok(y) then
p -> b[ok];
p -> q[ok];
p.money(y) -> b.m;
q.prod(x) -> p.yahoo;
0
else
p -> b[ko];
p -> q[ko];
p.anotherProduct;
Buy(p,q,b)
Yes, given that the price is eventually ok.
---
Is this network deadlock-free?
r |> s!;0 | s |> r?; p!;0 | p|> s?;0 | q |> b!;0 | b |> q?;0
Yes, because we can write a choreography whose EPP is exactly this network.
r -> s; s -> p; q -> b; 0
---
Does the following hold?
r -> s; p -> q; t -> w; 0 <= t -> w; p -> q; r -> s; 0
Yes, because
r -> s; p -> q; t -> w; 0
<=
r -> s; t -> w; p -> q; 0
<=
t -> w; r -> s; p -> q; 0
<=
t -> w; p -> q; r -> s; 0
and by transitivity of <=.