-- virtroute.csp
-- Bill Roscoe
-- This file illustrates Example 13.2.1, Yantchev's virtual routeing or
-- "mad postman" network.
-- It is configured mainly as an exercise in determining the effectiveness
-- of compression functions:
include "compression.csp"
transparent normal
H = 20
W = 20
-- We give here the "data-free" nondeterministic version of the network
-- discussed in section 13.6.1. The coding of the original version
-- (which would be the natural one to run on ProBE; either being suitable
-- for the deadlock checker) is left as an exercise.
channel u,d,l,r,over,in,out:{0..W+1}.{0..H+1}
-- Each physical node has two parallel processes, I and O. When each
-- inputs a value it selects (here nondeterministically) where to send it.
I(i,j) = in.i.j -> I'(i,j)
[] d.i.j -> I'(i,j)
[] r.i.j -> I'(i,j)
-- I selects between sending right,down and over to O
I'(i,j) = let
S = Union({{over.i.j},
{d.i.j+1},
{r.i+1.j}})
within
|~| x:S @ x -> I(i,j)
AI(i,j) = {in.i.j,over.i.j,
d.i.j, r.i.j,
d.i.j+1, r.i+1.j}
O(i,j) = over.i.j -> O'(i,j)
[] u.i.j -> O'(i,j)
[] l.i.j -> O'(i,j)
-- O selects between sending left,up and out to its user
O'(i,j) = let
S = Union({{out.i.j},
{u.i.j-1},
{l.i-1.j}})
within
|~| x:S @ x -> O(i,j)
AO(i,j) = {out.i.j, over.i.j,
u.i.j, l.i.j,
u.i.j-1, l.i-1.j}
-- So the complete node is
N(i,j) = (I(i,j)[AI(i,j)||AO(i,j)]O(i,j))\{over.i.j}
AN(i,j) = diff(union(AI(i,j),AO(i,j)),{over.i.j})
NetList(W',H') = <(N(i,j),AN(i,j)) | i <- <1..W'>, j<-<1..H'>>
-- We give here three different compression strategies: note the
-- incremental network sizes given to them
-- None
assert ListPar(NetList(2,2)):[deadlock free [F]]
assert ListPar(NetList(2,3)):[deadlock free [F]]
-- Simply compressing the individual node processes without using
-- the abstraction of external communications. You will find this
-- gives a lot less states but runs very slowly per state. This
-- is because there are lots of refusal sets to calculuate for
-- each state
assert LeafCompress(normal)(NetList(2,2))({}) :[deadlock free [F]]
assert LeafCompress(normal)(NetList(2,3))({}) :[deadlock free [F]]
-- and using the abstraction:
assert LeafCompress(normal)(NetList(2,3))(Events) :[deadlock free [F]]
assert LeafCompress(normal)(NetList(4,4))(Events) :[deadlock free [F]]
assert LeafCompress(normal)(NetList(10,10))(Events) :[deadlock free [F]]
-- You will notice that this always gets the network down to one
-- state, but that it still takes impossibly long for the 10x10
-- network. This is again because of multiplication of refusal sets.
-- This can be eliminated by building up the network
-- a row at a time.
RowList(W',H') = <<(N(i,j),AN(i,j)) | i <- <1..W'>> | j<-<1..H'>>
assert StructuredCompress(normal)(RowList(10,10))(Events) :[deadlock free [F]]