This directory contains examples of workbench environments created by
various people using the workbench. Each file can be loaded into a
workbench session by issuing the command "input" with the appropriate
parameter.
For version 7, several more examples have been added. They are mostly very
simple, and may serve to demonstrate the use of the new version 7
facilities. In many cases they are slight adaptations of test scripts, but
in most cases the lines which do calculations (as opposed to setting up
environments) have been commented out. The new files are not described
here. You may find it useful to browse the directory.
Briefly, the contents of the main files are as follows.
abp
---
Author: Rance Cleaveland
This file contains a development of the Alternating Bit Protocol. The
specification of the protocol is represented by the agent "Spec", and there
are two implementations, "ABP-lossy" and "ABP-safe", that differ only in that
the former uses a lossy medium ("Mlossy") while the second uses a safe medium
("Msafe"). "ABP-lossy" is correct in the sense that it is observation
equivalent to "Spec", while "ABP-safe" is not. There are several ways to see
why this is the case:
o Use the "deadlocks" ("find deadlocks") command to note that "ABP-safe" may
deadlock.
o Use the "checkprop" ("check proposition") command on "ABP-safe" and the
proposition "Bx (<<send>>T | <<receive>>T)" to note that it is not
always the case that "ABP-safe" can either send or receive. The
parameterised proposition "Bx" (for the temporal logic operator "Box")
takes one proposition P as a parameter, and holds of a state if P holds
of every state reachable from the state.
NOTE: In the implementations of the sender (S0, S0', S1, S1') and the receiver
(R0 and R1), tau actions are used to model time-outs.
csma
----
Author: Joachim Parrow
This file contains a development of the "Carrier Sense/Multiple Access with
Collision Detection" protocol. The specification is the agent "SSCS", and the
implementation is "CSPROT". A complete description of this development of the
protocol can be found in the Edinburgh University technical report
ECS-LFCS-86-18 by Joachim Parrow, entitled "Verifying a CSMA/CD Protocol with
CCS".
dekker-2
--------
Author: David Walker
This file contains a development of Dekker's mutual exclusion algorithm for two
processes. The specification is the agent "Spec", and the implementation is
"Dekker-2". A complete description of this development of the algorithm can be
found in the Edinburgh University technical report ECS-LFCS-88-45 by David
Walker, entitled "Analysing mutual exclusion algorithms using CCS".
jobshop
-------
Author: Faron Moller
This file contains a specification of the "Jobshop" system, described in
Milner's book. The value-passing system has been suitably translated into
the pure calculus.
mailsystem
----------
Author: Gordon Brebner
This file contains the specification of a simple mail system.
peterson-2
----------
Author: David Walker
This file contains a development of Peterson's mutual exclusion algorithm for
two processes. The specification is the agent "Spec", and the implementation
is "Peterson-2". A complete description of this development of the algorithm
can be found in the Edinburgh University technical report ECS-LFCS-88-45 by
David Walker, entitled "Analysing mutual exclusion algorithms using CCS".
tl.macros
---------
Author: Rance Cleaveland
This file contains parameterised propositions that define some of the
standard (branching time) temporal logic operators. Those included
are the following.
Bx - the "Box" (or "always") operator.
Ev - the "eventuality" operator; "Ev P" holds of a state if P is true
of the state or if "Ev P" holds true of each derivative of the
state, and there is at least one derivative.
StrongUntil - the "strong until" operator". "Until P Q" holds of a state if P
holds until "Q" does along every computation starting from the
state; furthermore, Q must hold at some point.
WeakUntil - the "weak until" operator. "Until* P Q" holds of a state if P
holds until "Q" does along every computation starting from the
state; however, Q need not ever become true.
Poss - the "possibility" operator. This is the dual of the "always"
operator. "Poss P" holds of a state if P holds of the state or
if it is possible to evolve from the state to another state in
which P holds.
vending-machine
---------------
Author: Faron Moller
This is a specification of the "user friendly" vending machine as described
on pages 23-24 of Milner's book. The machine "VM" will accept 1p and 2p
coins (actions "in1" and "in2") and deliver either little chocolates
(worth 1p) or big chocolates (worth 2p) under the following constraints:
# the machine can never make a profit nor a loss;
# the machine cannot hold a credit of more than 4p;
# a chocolate cannot be requested if one has previously
been delivered but not yet collected.
The last of these constraints can be confirmed using the hiding of coin
inputs to see that what remains repeatedly does a request for a chocolate
followed by the collection of the chocolate (which is given by the agents
"VMnew" and "VMnewSpec").
Name Last modified Size Description
UsefulProps.cwb 2004-06-28 15:38 2.0K
abp.cwb 2004-06-28 15:38 5.0K
basic.cwb 2004-06-28 15:38 448
basicparamprop.cwb 2004-06-28 15:38 328
csma.cwb 2004-06-28 15:38 1.3K
dekker-2.cwb 2004-06-28 15:38 1.3K
jobshop.cwb 2004-06-28 15:38 3.5K
mailsystem.cwb 2004-06-28 15:38 1.5K
paramagent.cwb 2004-06-28 15:38 773
paramprop.cwb 2004-06-28 15:38 968
peterson-2.cwb 2004-06-28 15:38 1.2K
sched.cwb 2004-06-28 15:38 2.0K
tl.macros.cwb 2004-06-28 15:38 2.0K
vending-machine.cwb 2004-06-28 15:38 1.7K