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