-- 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))