Example Files¶

FDR4 Introduction¶

Download

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 -- 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)) 

Dining Philosophers¶

Download

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 -- 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 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. 

Inductive Compression¶

Download

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 -- 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()) -- 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 = ss = > 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 = ss = > 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 else let m=if (xl/n)*n==xl then n else (n+1) within ^groupsof(n)(drop(m)(xs)) take(n)(xs) = if n==0 then <> else ^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 = A = Union(set()) within (ListPar(ps),A) PSmap(f,PSLeaf.p) = PSLeaf.(f(p)) PSmap(f,PSNode.ts) = PSNode. 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)) = psalphas(PSNode.ts) = --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 = within Union(set(AS)) PSStructCompress(compress) = let G(PSLeaf.(P,A)) = let f(X) = P\X within f G(PSNode.ts) = \X @ let as = 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