Example Files¶

-- Introducing FDR4.0
-- Bill Roscoe, November 2013

-- A file to illustrate the functionality of FDR4.0.

-- Note that this file is necessarily basic and does not stretch the
-- capabilities of the tool.

-- To run FDR4 with this file just type "fdr4 intro.csp" in the directory
-- containing intro.csp, assuming that fdr4 is in your $PATH or has been aliased
-- to run the tool.

-- Alternatively run FDR4 and enter the command ":load intro.csp".

-- You will see that all the assertions included in this file appear on the RHS
-- of the window as prompts. This allows you to run them.

-- This file contains some examples based on playing a game of tennis between A
-- and B.

channel pointA, pointB, gameA, gameB

Scorepairs = {(x,y) | x  <- {0,15,30,40}, y <- {0,15,30,40}, (x,y) != (40,40)}

datatype scores = NUM.Scorepairs | Deuce | AdvantageA | AdvantageB

Game(p) = pointA -> IncA(p)
         [] pointB -> IncB(p)

IncA(AdvantageA) = gameA -> Game(NUM.(0,0))
IncA(NUM.(40,_)) = gameA -> Game(NUM.(0,0))
IncA(AdvantageB) = Game(Deuce)
IncA(Deuce) = Game(AdvantageA)
IncA(NUM.(30,40)) = Game(Deuce)
IncA(NUM.(x,y)) =  Game(NUM.(next(x),y))
IncB(AdvantageB) = gameB -> Game(NUM.(0,0))
IncB(NUM.(_,40)) = gameB -> Game(NUM.(0,0))
IncB(AdvantageA) = Game(Deuce)
IncB(Deuce) = Game(AdvantageB)
IncB(NUM.(40,30)) = Game(Deuce)
IncB(NUM.(x,y)) = Game(NUM.(x,next(y)))
-- If you uncomment the following line it will introduce a type error to
-- illustrate the typechecker.
-- IncB((x,y)) = Game(NUM.(next(x),y))

next(0) = 15
next(15) = 30
next(30) = 40

-- Note that you can check on non-process functions you have written. Try typing
-- next(15) at the command prompt of FDR4.

-- Game(NUM.(0,0)) thus represents a game which records when A and B win
-- successive games, we can abbreviate it as

Scorer = Game(NUM.(0,0))

-- Type ":probe Scorer" to animate this process.    
-- Type ":graph Scorer" to show the transition system of this process

-- We can compare this process with some others:

assert Scorer [T= STOP
assert Scorer [F= Scorer
assert STOP [T= Scorer

-- The results of all these are all obvious.

-- Also, compare the states of this process

assert Scorer [T= Game(NUM.(15,0))
assert Game(NUM.(30,30)) [FD=  Game(Deuce)

-- The second of these gives a result you might not expect: can you explain why?
-- (Answer below....)

-- For the checks that fail, you can run the debugger, which illustrates why the
-- given implementation (right-hand side) of the check can behave in a way that
-- the specification (LHS) cannot.  Because the examples so far are all
-- sequential processes, you cannot subdivide the implementation behaviours into
-- sub-behaviours within the debugger.

-- One way of imagining the above process is as a scorer (hence the name) that
-- keeps track of the results of the points that A and B score.  We could put a
-- choice mechanism in parallel: the most obvious picks the winner of each point
-- nondeterministically:

ND = pointA -> ND |~| pointB -> ND

-- We can imagine one where B gets at least one point every time A gets one:

Bgood = pointA -> pointB -> Bgood |~| pointB -> Bgood

-- and one where B gets two points for every two that A get, so allowing A to
-- get two consecutive points:

Bg = pointA -> Bg1 |~| pointB -> Bg

Bg1 = pointA -> pointB ->  Bg1 |~| pointB -> Bg

assert Bg [FD= Bgood 
assert Bgood [FD= Bg 

-- We might ask what effect these choice mechanisms have on our game of tennis:
-- do you think that B can win a game in these two cases?

BgoodS = Bgood [|{pointA,pointB}|] Scorer
BgS = Bg [|{pointA,pointB}|] Scorer

assert STOP [T= BgoodS \diff(Events,{gameA})
assert STOP [T= BgS \diff(Events,{gameA})

-- You will find that A can in the second case, and in fact can win the very
-- first game.  You can now see how the debugger explains the behaviours inside
-- hiding and of different parallel components.

-- Do you think that in this case A can ever get two games ahead?  In order to
-- avoid an infinite-state specification, the following one actually says that A
-- can't get two games ahead when it has never been as many as 6 games behind:

Level = gameA -> Awinning(1)
        [] gameB -> Bwinning(1)

Awinning(1) = gameB -> Level -- A not permitted to win here

Bwinning(6) = gameA -> Bwinning(6) [] gameB -> Bwinning(6)
Bwinning(1) = gameA -> Level [] gameB -> Bwinning(2)
Bwinning(n) = gameA -> Bwinning(n-1) [] gameB -> Bwinning(n+1)

assert Level [T= BgS \{pointA,pointB}

-- Exercise for the interested: see how this result is affected by changing Bg
-- to become yet more liberal. Try Bgn(n) as n copies of Bgood in ||| parallel.

-- Games of tennis can of course go on for ever, as is illustrated by the check

assert BgS\{pointA,pointB} :[divergence-free]

-- Notice that here, for the infinite behaviour that is a divergence, the
-- debugger shows you a loop.

-- Finally, the answer to the question above about the similarity of
-- Game(NUM.(30,30)) and Game(Deuce).

-- Intuitively these processes represent different states in the game: notice
-- that 4 points have occurred in the first and at least 6 in the second. But
-- actually the meaning (semantics) of a state only depend on behaviour going
-- forward, and both 30-all and deuce are scores from which A or B win just when
-- they get two points ahead.  So these states are, in our formulation,
-- equivalent processes.

-- FDR has compression functions that try to cut the number of states of
-- processes: read the books for why this is a good idea. Perhaps the simplest
-- compression is strong bisimulation, and you can see the effect of this by
-- comparing the graphs of Scorer and

transparent sbisim, wbisim, diamond

BScorer = sbisim(Scorer)

-- Note that FDR automatically applies bisimulation in various places.

-- To see how effective compressions can sometimes be, but that
-- sometimes one compression is better than another compare 

NDS = (ND [|{pointA,pointB}|] Scorer)\{pointA,pointB}

wbNDS = wbisim(NDS)
sbNDS = sbisim(NDS)
nNDS = sbisim(diamond(NDS))

-- The five dining philosophers for FDR

-- Bill Roscoe

-- The most standard example of them all.  We can determine how many
-- (with the conventional number being 5):

N = 6

PHILNAMES= {0..N-1}
FORKNAMES = {0..N-1}

channel thinks, sits, eats, getsup:PHILNAMES
channel picks, putsdown:PHILNAMES.FORKNAMES

-- A philosopher thinks, sits down, picks up two forks, eats, puts down forks
-- and gets up, in an unending cycle.   

PHIL(i) = thinks.i -> sits!i -> picks!i!i -> picks!i!((i+1)%N) ->
          eats!i -> putsdown!i!((i+1)%N) -> putsdown!i!i -> getsup!i -> PHIL(i)

-- Of course the only events relevant to deadlock are the picks and putsdown
-- ones.  Try the alternative "stripped down" definition

PHILs(i) =  picks!i!i -> picks!i!((i+1)%N) ->
           putsdown!i!((i+1)%N) -> putsdown!i!i -> PHILs(i)



-- Its alphabet is

AlphaP(i) = {thinks.i, sits.i,picks.i.i,picks.i.(i+1)%N,eats.i,putsdown.i.i,
             putsdown.i.(i+1)%N,getsup.i}

-- A fork can only be picked up by one neighbour at once!

FORK(i) = picks!i!i -> putsdown!i!i -> FORK(i)
         []  picks!((i-1)%N)!i -> putsdown!((i-1)%N)!i -> FORK(i)

AlphaF(i) = {picks.i.i, picks.(i-1)%N.i, putsdown.i.i, putsdown.(i-1)%N.i}

-- We can build the system up in several ways, but certainly
-- have to use some form of parallel that allows us to
-- build a network parameterized by N.  The following uses
-- a composition of N philosopher/fork pairs, each individually
-- a parallel composition.

SYSTEM = || i:PHILNAMES@[union(AlphaP(i),AlphaF(i))] 
                       (PHIL(i)[AlphaP(i)|| AlphaF(i)] FORK(i))

-- or stripped down

SYSTEMs = || i:PHILNAMES@[union(AlphaP(i),AlphaF(i))] 
                       (PHILs(i)[AlphaP(i)|| AlphaF(i)] FORK(i))


-- As an alternative (see Section 2.3) we can create separate
-- collections of the philosophers and forks, each composed
-- using interleaving ||| since there is no communication inside
-- these groups.

PHILS = ||| i:PHILNAMES@ PHIL(i)
FORKS = ||| i:FORKNAMES@ FORK(i)

SYSTEM' = PHILS[|{|picks, putsdown|}|]FORKS

-- The potential for deadlock is illustrated by 

assert SYSTEM :[deadlock free [F]]

-- or equivalently in the stripped down
assert SYSTEMs :[deadlock free [F]]

-- which will find the same deadlock a lot faster.

-- There are several well-known solutions to the problem.  One involves a
-- butler who must co-operate on the sitting down and getting up events,
-- and always ensures that no more than four of the five
-- philosophers are seated.

BUTLER(j) = j>0 & getsup?i -> BUTLER(j-1)
            []j<N-1 & sits?i -> BUTLER(j+1)

BSYSTEM = SYSTEM [|{|sits, getsup|}|] BUTLER(0)

assert BSYSTEM :[deadlock free [F]]

-- We would have to reduce the amount of stripping down for this,
-- since it makes the sits and getsup events useful...try this.

-- A second solution involves replacing one of the above right-handed (say)
-- philosophers by a left-handed one:

LPHIL(i)= thinks.i -> sits.i -> picks.i.((i+1)%N) -> picks.i.i -> 
          eats.i -> putsdown.i.((i+1)%N) -> putsdown.i.i -> getsup.i -> LPHIL(i)

ASPHILS = ||| i:PHILNAMES @ if i==0 then LPHIL(i) else PHIL(i)

ASSYSTEM = ASPHILS[|{|picks, putsdown|}|]FORKS

-- This asymmetric system is deadlock free, as can be proved using Check.  

assert ASSYSTEM :[deadlock free [F]]

-- If you want to run a lot of dining philosophers, the best results will
-- probably be obtained by removing the events irrelevant to ASSYSTEM
-- (leaving only picks and putsdown) in:
LPHILs(i)=  picks.i.((i+1)%N) -> picks.i.i -> 
           putsdown.i.((i+1)%N) -> putsdown.i.i -> LPHILs(i)

ASPHILSs = ||| i:PHILNAMES @ if i==0 then LPHILs(i) else PHILs(i)

ASSYSTEMs = ASPHILSs[|{|picks, putsdown|}|]FORKS

assert ASSYSTEMs :[deadlock free [F]]

-- Setting N=10 will show the spectacular difference in running the
-- stripped down version.  Try to undertand why there is such an
-- enormous difference.

-- Compare the stripped down versions with the idea of "Leaf Compression"
-- discussed in Chapter 8.

-- compression09.csp

-- This DRAFT file supports various semi-automated compression techniques over
-- CSP networks for use with FDR.  

-- It it is designed to accompany the author's forthcoming book
-- "Understanding Concurrency"
-- and is an updated version of the 1997 file "compresion.csp" that
-- accompanied "Theory and Practice of Concurrency".

-- Bill Roscoe

-- We assume that networks are presented to us as 
-- structures comprising process/alphabet pairs arranged in list
-- arrangements,

-- or (09) as members of the structured datatype

datatype PStruct = PSLeaf.(Proc,Set(Events)) | PSNode.Seq(PStruct)

-- This can only be used with FDR 2.91 and up where processes (Proc) are allowed
-- as parts of user-defined types.

-- We may (subject to alterations to FDR) be able to support more complex
-- structured types over processes.

-- The alphabet of any such list is the union of the alphabets of
-- the component processes:

alphabet(ps) = Union(set(<A | (P,A) <- ps>))

-- The vocabulary of a list is the set of events that are synchronised
-- between at least two members:

vocabulary(ps) = if #ps<2 then {} else
                 let A = snd(head(ps))
             V = vocabulary(tail(ps))
             A' = alphabet(tail(ps))
         within
             union(V,inter(A,A'))

-- The following is a function 
-- that composes a process/alphabet list without any
-- compression:

ListPar(ps) = let N=#ps within
              || i:{0..N-1} @ [snd(cnth(i,ps))] fst(cnth(i,ps))

-- The most elementary transformation we can do on a network is to
-- hide all events in individual processes that are neither relevant to
-- the specification nor are required for higher synchronisation.
-- The following function takes as its (curried) arguments a compression
-- function to apply at the leaves, a process/alphabet list to compose
-- in parallel and a set of events which it is desired to hide (either
-- because they are genuinely internal events or irrelevant to the spec).
-- It hides as much as it can in the processes, but does not combine them

CompressLeaves(compress)(ps)(X) = let V = vocabulary(ps) 
                                    N = #ps
                    H = diff(X,V)
                within
          <(compress(P\inter(A,H)),diff(A,H)) | (P,A) <- ps>

-- The following uses this to produce a combined process

LeafCompress(compress)(ps)(X) = ListPar(CompressLeaves(compress)(ps)(X))\X

-- It is often advantageous to be able to apply lazy or mixed abstraction
-- operators in the same sort of way as the above does for hiding.  The
-- following are two functions that generalize the above: they take a
-- pair of event-sets (X,S): X is the set we want to abstract and S is
-- the set of signal events (which need not be a subset of X).  The
-- result is that inter(X,S) is hidden and diff(X,S) is lazily
-- abstracted.   Note that you can get the effect of pure hiding (eager
-- abstraction by setting S=Events) and pure lazy abstraction by setting
-- S={}.  Note also, however, that if you are trying to lazily abstract
-- a network with some natural hiding in it, that all these hidden events
-- should be treated as signals.

LeafMixedAbs(compress)(ps)(X,S) = 
                           let V = vocabulary(ps) 
                               N = #ps
                               D = diff(X,S)
                               H'= diff(X,V)
                           within
          <(compress((P[|inter(A,D)|] 
            compress(CHAOS(inter(A,D))))\inter(A,H')),diff(A,H')) 
                 | (P,A) <- ps>

-- The substantive function is then:

MixedAbsLeafCompress(compress)(ps)(X,S) = 
       ListPar(LeafMixedAbs(compress)(ps)(X,S))\X


-- The next transformation builds up a list network in the order defined
-- in the (reverse of) the list, applying a specified compression function
-- to each partially constructed unit.

InductiveCompress(compress)(ps)(X) = 
        compress(IComp(compress)(CompressLeaves(compress)(ps)(X))(X))

IComp(compress)(ps)(X) = let  p = head(ps)
                   P = fst(p)
                   A = snd(p)
                   A' = alphabet(ps')
                   ps' = tail(ps)
              within
                           if #ps == 1 then P\X
               else
               let Q = IComp(compress)(ps')(diff(X,A))
                           within
                   (P[A||A']compress(Q))\inter(X,A)

InductiveMixedAbs(compress)(ps)(X,S) = 
        compress(IComp(compress)(LeafMixedAbs(compress)(ps)(X,S))(X))

-- Sometimes compressed subnetworks grow to big to make the above
-- function conveniently applicable.  The following function allows you
-- to compress each of a list-of-lists of processes, and then
-- combine them all without trying to compress any further.

StructuredCompress(compress)(pss)(X) =
                         let N = #pss
             as = <alphabet(ps) | ps <- pss>
             ss = <Union({inter(cnth(i,as),cnth(j,as)) | 
                j <- {0..N-1}, j!=i}) | i <- <0..N-1>>  
             within
             (ListPar(<(compress(
                 InductiveCompress(compress)(cnth(i,
                      pss))(diff(X,cnth(i,ss)))
                         \(diff(X,cnth(i,ss)))),
                    cnth(i,as)) | i <- <0..N-1>>))\X

-- The analogue of ListPar

StructuredPar(pss) =  ListPar(<(ListPar(ps),alphabet(ps)) | ps <- pss>)

-- and the mixed abstraction analogue:

StructuredMixedAbs(compress)(pss)(X,S) =
                         let N = #pss
             as = <alphabet(ps) | ps <- pss>
             ss = <Union({inter(cnth(i,as),cnth(j,as)) | 
                j <- {0..N-1}, j!=i}) | i <- <0..N-1>>  
             within
             (ListPar(<(compress(
                 InductiveMixedAbs(compress)(cnth(i,
                      pss))(diff(X,cnth(i,ss)),S)
                         \(diff(X,cnth(i,ss)))),
                    cnth(i,as)) | i <- <0..N-1>>))\X

-- The following are some functional programming constructs used above

cnth(i,xs) = if i==0 then head(xs) 
                    else cnth(i-1,tail(xs))
        
fst((x,y)) = x
snd((x,y)) = y

-- The following function can be useful for partitioning a process list
-- into roughly equal-sized pieces for structured compression

groupsof(n)(xs) = let xl=#xs within
                  if xl==0 then <> else
                  if xl<=n or n==0 then <xs>
                  else let 
                         m=if (xl/n)*n==xl then n else (n+1)
                    within
                    <take(m)(xs)>^groupsof(n)(drop(m)(xs))

take(n)(xs) = if n==0 then <> else <head(xs)>^take(n-1)(tail(xs))

drop(n)(xs) = if n==0 then xs else drop(n-1)(tail(xs))

-- The following define some similar compression functions for PStruct


StructPar(t) = let (P,_) = SPA(t) within P

SPA(PSLeaf.(P,A)) = (P,A)

SPA(PSNode.ts) = let ps = <SPA(t) | t <- ts> 
                     A = Union(set(<a_ | (_,a_)  <- ps>))
                  within
                  (ListPar(ps),A)

PSmap(f,PSLeaf.p) = PSLeaf.(f(p))
PSmap(f,PSNode.ts) = PSNode.<PSmap(f,t) | t <- ts>

PSvocab(t) = let as = psalphas(t)
             within
               Union({inter(cnth(i,as),cnth(j,as)) |
                              i <- {1..(#as)-1}, j <- {0..i-1}})

psalphas(PSLeaf.(P,A)) = <A>
psalphas(PSNode.ts) = <A | u <- ts, A <- psalphas(u)>
--psalphas(PSNode.ts) = <>

CompressPSLeaves(compress)(t)(X) = let V = PSvocab(t)
                                       H = diff(X,V)
                                       f((P,A)) = (compress(P\H),A)
                                   within
                                   PSmap(f,t)


PSLeafCompress(compress)(t)(X) = let ct = CompressPSLeaves(compress)(t)(X)
                                 within
                                 StructPar(ct)\X

psalphabet(PSLeaf.(P,A)) = A
psalphabet(PSNode.ts) = let AS = <psalphabet(t) | t <- ts>
                            within Union(set(AS))


PSStructCompress(compress) =
      let G(PSLeaf.(P,A)) = let f(X) = P\X within f
          G(PSNode.ts) =  \X @
                             let as = <psalphabet(t) | t <- ts>
                                 tlv = Union({inter(cnth(i,as),cnth(j,as)) |
                                              i <- {1..#ts-1}, j <- {0..i-1}})

                                 ps = <(compress(PSStructCompress(compress)(t)(
                                       inter(psalphabet(t), diff(X,tlv)))), 
                                       psalphabet(t)) 
                                       | t <- ts >
                              within
                               ListPar(ps)\X
        within G