CWB v7.1
Welcome to the Edinburgh Concurrency Workbench version 7.1!
Benefits
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.
Games
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,
- pairs will be put into a standard order
- redundant a/a pairs will be eliminated
- successive literal relabellings combined
- the identity relabelling eliminated
- nonsensical relabellings like [a/b, c/b] are now forbidden
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:
- when the CWB reports the binding of a parameterised agent, it will
tell you what the type of the parameter is. For example
Command: agent A(X) = X + a.0;
Command: agent A;
agent A(X : agent) = X + a.0;
The syntax the workbench uses to report types is also legal input syntax:
you may use it yourself if you prefer. If the CWB cannot infer the type of
a parameter from the body of the definition it will ask you. Remember that
everything is still dynamic: so in particular there's no static checking
outside the body of the single definition you're making.
Toggles for user options
Some new and changed commands:
- checkprop
: modelchecking using new game
algorithm, offers to play games (unless you toggle "hateGames"!)
- checkpropold
: modelchecking using old algorithm
- cwb
: mostly for internal use: set CWB options
- echo
: print a string to whereever output's going
- game
: play model-checking games
- graph
: list the transition graph of an agent
- toggle
: toggle various CWB user options
A much improved
Emacs mode,
including better communication with daVinci
Caveats
- There are various
cosmetic changes,
which you probably won't care about
unless you've produced tutorial material or something including CWB output
which you want to be exactly as the CWB produces it.
- Value-passing CCS: is closer than you think, but not there yet.
Incompatible changes
- formal parameters to propositions or agents must now
be identifiers (previously you could use 'a, for example, as a formal
parameter). I hope this won't upset anybody!
- The Emacs mode has changed the names of the CWB modes to cwb-mode and
cwb-file-mode. If you have set up autoloads etc. you will need to make
minor changes. See the CWB emacs mode
documentation for details.
Back to CWB home page