-- ring.csp
-- Deadlock-free messae passing ring
-- Bill Roscoe
-- This illustrates Example 13.2.5, again in a data-free way.
include "compression.csp"
transparent normal
transparent diamond, sbisim
channel ring,in,out:{0..100}
-- The deadlock of the simple version at the start of the example is
-- illustrated:
D1(N,i) = in.i -> D1'(N,i)
[] ring.i -> D1'(N,i)
D1'(N,i) = out.i -> D1(N,i)
|~| ring.(i+1)%N -> D1(N,i)
Alpha(N,i) = {in.i,out.i,ring.i,ring.(i+1)%N}
D1Ring(N) = <(D1(N,i),Alpha(N,i)) | i <- <0..N-1>>
assert LeafCompress(normal)(D1Ring(20))(Events) :[deadlock free [F]]
-- The inadequacy of simply adding further buffering is illustrated
-- by the following example, where each node has two spaces...
D2(N,i) = in.i -> D2'(N,i)
[] ring.i -> D2'(N,i)
D2'(N,i) = (out.i -> D2(N,i)
|~| ring.(i+1)%N -> D2(N,i))
[]
(in.i -> D2''(N,i)
[] ring.i -> D2''(N,i))
D2''(N,i) = (out.i -> D2'(N,i)
|~| ring.(i+1)%N -> D2'(N,i))
D2Ring(N) = <(D2(N,i),Alpha(N,i)) | i <- <0..N-1>>
assert LeafCompress(normal)(D2Ring(20))(Events) :[deadlock free [F]]
-- The example from the chapter in which the external user cannot fill
-- up a node is described:
DFN(N,i) = in.i -> DFN'(N,i)
[] ring.i -> DFN'(N,i)
DFN'(N,i) = (out.i -> DFN(N,i)
|~| ring.(i+1)%N -> DFN(N,i))
[]
(ring.i -> DFN''(N,i))
DFN''(N,i) = (out.i -> DFN'(N,i)
|~| ring.(i+1)%N -> DFN'(N,i))
DFRing(N) = <(DFN(N,i),Alpha(N,i)) | i <- <0..N-1>>
-- This does not collapse down quite as well under leaf compression,
-- as it still has 2^N states:
assert LeafCompress(normal)(DFRing(10))(Events) :[deadlock free [F]]
-- However, under inductive compression .....
assert InductiveCompress(normal)(DFRing(10))(Events) :[deadlock free [F]]
assert InductiveCompress(normal)(DFRing(50))(Events) :[deadlock free [F]]