CWB v7.1

Welcome to the Edinburgh Concurrency Workbench version 7.1!


Source code for SML-NJ 110
which is available for many more platforms than 0.93, so you can now compile the CWB on many different platforms, notably in the M*******t world.
Model checking by games: faster model checking, and the chance to debug models by playing games against the CWB.

(And more equivalence games coming soon, though the experimental strong bisimulation game has come out for now, pending being fitted into a more general games architecture.)

Colin Stirling's notes for a recent MathFit Summer School, Bisimulation, model checking and other games include an introduction to both kinds of games.

Various papers are available on the theory, including the model checking algorithm: see my papers page especially the TACAS paper with Colin Stirling.

Other advances
  • Various sanitisations and bug fixes. For example, the CWB now treats relabellings more intelligently. Milner's book, for example, refers always to relabelling functions, but the CWB used not to enforce this, and used to work blindly with lists of pairs of actions. The syntax for defining relabellings is unchanged, but the relabelling will be treated more like a function; for example, Of course, a list of pairs defines a set of simultaneous substitutions: A[a/b,b/a] behaves like A with a and b swapped, whereas (A[a/b])[b/a] behaves like A[b/a].

    Similar remarks apply to restriction sets: these now behave more like real sets, not lists.

    Again as a sanity improvement, formal parameters are now typed. This means that we eliminate a number of strange behaviours that could arise if you used a formal parameter both as an agent and as an action set. (Of course, sensible people other than destructive testers probably didn't do this anyway, but it might give you a nice warm feeling that now you can't!) The differences you may notice are:

  • Toggles for user options
  • Some new and changed commands:
  • A much improved Emacs mode, including better communication with daVinci


  • Incompatible changes

    Back to CWB home page