-- express.csp
-- Illustrating full abstraction results for CSP
-- Part 1: expressibility
-- Bill Roscoe
-- This file, and its companion,
-- illustrate the constructions used in Section 9.3 on
-- expressibility and full abstraction for CSP. The concepts
-- illustrated are sophisticated and remote from direct practical
-- applications. You are strongly advised not to try to follow these
-- files without studying the relevant section of the book!
-- BASICS
-- For simplicity and efficiency, we will deal only with the
-- case of a small fixed alphabet
channel a,b,c,fail,tick
-- The role of the event fail will be as in the text.
-- It is not permitted to refer to the actual tick event of CSP (written
-- as _tick when you see it in debuggers, etc) in
-- CSP scripts (because of the special role it has, only introduced via
-- SKIP), but we do need a way of referring to it in the semantic values
-- we manipulate in this script. Therefore the declared event tick
-- is included so we can handle semantic objects involving it. The
-- intention is that when it comes to mapping one of these (say the trace
-- ) to a real CSP process, that the corresponding behaviour of
-- that process would replace all tick's by the "real" event _tick
-- (i.e, this trace would become ).
-- The automatically-supported set Events equals {a,b,c,fail,tick}, of
-- course, but at the modelling level we want a set of communications
-- that doesn't include tick as an ordinary one
Sigma = diff(Events,{tick})
-- and an augmented one that does:
Sigmatick = Events
-- so the range of possible refusal sets (at the modelling level) is
RefSets = Set(Sigmatick)
--^~-^~-^~-^~-^~-^~-^~-^~-^~-^~-^~-^~-^~-^~-^~-^~-^~-^~-^~-^~-^~-^~-^~-^~-^~-
-- EXPRESSIBILITY
-- Here we are showing how the constructions in the book map a member
-- of one of the semantic models to a CSP term that has the right value,
-- in each of the models in turn. In each case we can only handle finite
-- semantic values, simply because FDR can only handle finite sets in
-- its functional language.
-- Traces model
-- The following are as defined in the book
-- A process that performs any given trace
TT(<>) = STOP
TT() = SKIP
TT(^s) = x -> TT(s)
-- and one that performs any nonempty, prefix-closed set of traces
TINT(P) = |~| s:P @ TT(s)
-- Here are some simple examples of pairs of objects, each being
-- an element of the traces model and a CSP process that corresponds to it:
TP1 = {<>,,,,}
TQ1 = (a -> a -> STOP) [] (b -> b -> STOP)
TP2 = {<>,,,}
TQ2 = (a -> STOP) [] (b -> SKIP)
-- That the expressibility construction works in these examples is
-- demonstrated:
assert TINT(TP1) [T= TQ1
assert TQ1 [T= TINT(TP1)
assert TINT(TP2) [T= TQ2
assert TQ2 [T= TINT(TP2)
---+--+--+--+--+--+--+--+--+--+--+--+--+--+--+--+--+--+--+--+--+--+--+--+--+-
-- Stable failures model
-- The simply divergent process plays an important role in the
-- constructions for this model
DIV = SKIP;DIV
-- for example in the creation of modified trace processes that are
-- minimally stable (only around ticks)
TT'(<>) = DIV
TT'() = SKIP
TT'(^s) = DIV [] x -> TT'(s)
-- a modified trace interpretation is thus
TINT'(P) = |~| s:P @ TT'(s)
-- this works just as well as the earlier one for the trace model:
assert TINT'(TP2) [T= TQ2
assert TQ2 [T= TINT'(TP2)
-- but we need to be able to handle failures as well for the stable
-- failures model. The following is as defined in the book
FF(<>,X) = [] x:diff(Sigma,X) @ x -> DIV
FF(^s,X) = DIV[] x -> FF(s,X)
-- it assumes that the trace has no tick and that X does contain tick,
-- and also that this is a failure of the underlying process that refuses
-- all events impossible after the given trace.
-- The following functions all manipulate semantic values: pairs (T,F) where
-- T is a set of traces and F a set of failures:
TFafter(s,(T,F)) = let n = #s within
({drop(n,t) | t <- T, s<=t},
{(drop(n,t),X) | (t,X) <- F, s<=t})
Refusalsafter(s,(T,F)) = {X | (t,X) <- F, s==t}
RefMax(XX) = diff(XX,{X| X<-XX, Y<-XX, X | s^ <- T})
-- The complete representation of an arbitrary process is thus
SFINT(P) = let FS = RepFail(P)
(T,F) = P
within
if FS == {} then TINT'(T)
else TINT'(T) |~| (|~| (s,X):FS @ FF(s,X))
-- We can again test out the construction with a few examples:
SFP1 = (TP1,
union({(<>,X) | X<-RefSets, not({a,b} <= X)},{(,X) | X <- RefSets}))
SFQ1 = (a -> (DIV [] a -> STOP))
|~| (b -> (DIV ||| b -> STOP))
-- The following function extracts the failures for mapping any appropriate
-- member of the traces model (as discussed in Section 9.1) to either the
-- stable failures, or failures/divergences, models
detF(T) = {(s,X) | s <- T, X <- RefSets,
inter(X,{x | x <-Sigmatick, member(s^,T)})=={}}
-- Thus the following function maps any member of T^d (described in Lemma
-- 9.1.2) to the appropriate member of the stable failures model:
detSFM(T) = (T,detF(T))
-- so we can get another example from
SFP2 = detSFM(TP2)
SFQ2 = TQ2
assert SFQ1 [F= SFINT(SFP1)
assert SFINT(SFP1) [F= SFQ1
assert SFQ2 [F= SFINT(SFP2)
assert SFINT(SFP2) [F= SFQ2
--\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-\/-
-- Failures/Divergences model
-- Here a member of the semantic model is represented as a pair consisting
-- of failures and divergences. For finiteness we will not record all
-- of a divergent process's divergences and failures: only the ones up to
-- minimal divergence traces.
FDinitials((F,D)) = {x | (,X) <- F}
FDafter(s,(F,D)) = let n = #s within
({(drop(n,t),X) | (t,X) <- F, s<=t},
{drop(n,t) | t <- D, s<=t})
drop(0,s) = s
drop(n,^s) = drop(n-1,s)
-- The expressibility construction for the failures/divergences model
-- behaves differently depending on whether:
-- The process is immediately divergent and, if not
-- if the process can perform tick immediately,
-- has maximal refusals containing tick
-- or both of the last two
FDINT(P) = let (F,D) = P
MR = {X | X <- RefMax({X | (<>,X) <- F}), member(tick,X)}
within
if member(<>,D) then DIV
else
if not member(tick,FDinitials(P))
then
(([] x:FDinitials(P) @ x -> FDINT(FDafter(,P)))
|~|
(|~| X:MR @
([] x:diff(Sigma,X) @ x -> FDINT(FDafter(,P)))))
else
if MR == {} then
(([] x:diff(FDinitials(P),{tick}) @ x -> FDINT(FDafter(,P)))
[> SKIP)
else
(([] x:diff(FDinitials(P),{tick}) @ x -> FDINT(FDafter(,P)))
|~|
(|~| X:MR @
([] x:diff(Sigma,X) @ x -> FDINT(FDafter(,P)))))
FDP1 = ({(s,X) | s <- {<>,,,}, X <- RefSets,
(#s>1 or not member(a,X))},{})
FDQ1 = a -> a -> (STOP |~| a -> DIV)
assert FDINT(FDP1) [FD= FDQ1
assert FDQ1 [FD= FDINT(FDP1)
-- The analogue of the determinism construction used for the previous model:
detFDM(T) = (detF(T),{})
-- and the corresponding example:
FDP2 = detFDM(TP2)
FDQ2 = TQ2
assert FDINT(FDP2) [FD= FDQ2
assert FDQ2 [FD= FDINT(FDP2)
FDP3 = (union({(,X),(,X) | X <- RefSets},
{(<>,X) | X <- RefSets, not member(tick,X)}),
{})
FDQ3 = a -> STOP [> SKIP
assert FDINT(FDP3) [FD= FDQ3
assert FDQ3 [FD= FDINT(FDP3)