Developers' Corner

In the past the structure of the CWB code hasn't made it easy to modify it, and indeed, it is still less clear than it might be. I'm working on this, slowly. In the meantime, let me give some pointers that may be helpful. This document describes the CWB as it is, not as it should be! Both are constantly changing, probably for the better ;-)

1 Licensing and conditions of use of CWB source code

You are welcome to make your own changes or additions to your own copies of the CWB; indeed, one of the purposes of the CWB is to be a test-bed for new theories and ideas. I'd just like to remind you of the clauses in the
licence which say that if you do this, you must offer me your changes, for possible inclusion in future versions of the CWB; also, that you may not distribute the CWB, either modified or not, without permission.

2 Architecture

By architecture we mean the things you have to know in order to replace or add a component. This includes both the architectural structure of the CWB, and the standard ways of doing things, that is, the architectural decisions about how a component should interact with the rest of the CWB.

2.1 High level structure

Roughly like this, where higher things depend on interfaces to lower things:

The diagram shows component types, not component instances: there are many equivalence checking modules, and several process algebras, for example. Instances of the same component type have the same interface.

You might want to add a component at either of the higher two levels.

2.1.1 Using the common facilities
See common.ml, which defines a few useful pervasives (i.e. functions you can call as though they were part of the language) and the structure Lib which contains a few more useful things.

Globally accessible structures are:

2.1.2 Using a process algebra
If you want to add or alter something that's specific to a particular process algebra, you do it inside that process algebra's module, so that you can take advantage of the PA's protected interface. Otherwise, do it by writing a component that depends on the public interface to process algebras as described in
Agent.sig. For example, you might write a functor that takes a structure of signature AGENT.

2.2 Non-structural architectural guidelines

That is, "how things are done in the CWB". You should follow this style -- that is, abide by these architectural decisions -- to maintain the integrity of the architecture. If there's a good reason why you can't, it may be that the decision needs to be revisited: in that case please let me know.
2.2.1 Exceptions
Exceptions you might want to raise
Uncaught exceptions are one of the commonest sorts of ML bug. So I ask you NOT to add any more globally visible exceptions. By all means use exceptions internally to your module, but take care to catch any exceptions you raise, plus any that may be produced by any library modules you use. Some global exceptions are handled at the top level by the CWB. You can raise these from your own code when appropriate. Do NOT override them by putting statements like "exception Parse of string" in your own code: it prevents the CWB top level code from handling them.

See common.ml. In summary:

Exceptions you might have to handle
See the interfaces concerned. Exceptions currently in signatures:
2.2.2 Public and protected interfaces
Many structures have two signatures, giving a permissive "protected" interface and a more restricted "public" interface. This is not as easy as it might be in ML to do without duplicating things in several signatures, because although you can include one signature in another, you can't then override what was a type with a datatype, or override a structure that matched a restricted signature with the same thing matching a more permissive signature. However, we can achieve the same effect using sharing.

To illustrate the way we do this, here's how it is for Act.

If any ML experts out there would like to tell me a better way to do this I'd be grateful! I'm pleased with this because at least it stops me having to duplicate things in several signatures, which I used to do.

3 Common tasks and how to achieve them

3.1 I want to add a new command to work with existing PAs and/or logics

For example, suppose you'd like to implement your newly-invented equivalence, or that you want a command to say whether there's a Z in the process definition, or whatever.

You obviously need to write a component that does the work, making use of appropriate interfaces. Your component should compile under Standard ML of New Jersey v110 and it should have empty interface, sig end.

Your component must register your new command, together with some information about what your component is, what process algebras it works with, the documentation, name and any aliases for the command. See the comments on registerCommand[s] and registerAlias in DynamicCommands.sig for how to do this. You call these functions via the global structure UI (whose signature includes DYNAMIC_COMMANDS).

Your command is implemented by a function of type unit -> unit, say myFunction. It will only be called if the user gives a command line which starts with its registered name (or one of its aliases). Probably, then, the first thing myFunction needs to do is to read its arguments. If they are simply some types that the CWB already knows about -- variable, string, natural number, agent of some already defined process algebra, formula of some already defined logic -- you can probably use already existing utility functions like readAgent to do this. For example, here's a case that would work if myCommand were to take a natural number and a CCS agent, being invoked like this:

Command: myCommand (6, (a.b.0 | b.c.0)\a); functor myFunctor (Ag : AGENT_WRAPPER) : sig end = struct ... fun myFunction _ = let val n = readNumber() val ag = Ag.readAgent() val answer = doTheRightThing (n, ag) in UI.print (makeString answer) end val _ = UI.registerCommand ("myCommand", "Do some stuff", myFunction) ... end

3.2 I want to add another process algebra

Your process algebra can be used by the other CWB modules if you construct your agent structure to match
Agent.sig, where the A : ACT refers to signature Act.sig.

Note: Although this makes the CWB modules syntactically able to work with your process algebra, what if any semantic sense this makes is not guaranteed! As a rough guide, provided that "has the same transition system as" is a congruence, you're probably OK provided that your implementations of the signature functions "make sense". If not, you're on your own!


3.3 I want to try out my model-checking algorithm.

For which logic? If for a new logic -- not the mu-calculus -- see the next point first. If for the mu-calculus, you have a choice about whether you want the version without negation or the version with negation and with only positive operators (box, and, no diamond, or). The CWB provides translators to either of these logics from the complex user-level logic.

The easiest thing to do is probably just to have a look at the existing model checking algorithm and imitate the way it fits into the CWB. See GameCheck.sig and GameCheck.str.


3.4 I want to add another logic.

Best to wait until I've reorganised the logic module properly, or else just have a look at the contents of
the logic directory and do what you can. The main reason why the current set up is complicated is that the user level uses a complex mu calculus with parameters, weak modalities etc., whereas the underlying model checking algorithms use simpler logics without these features. So a user level proposition has to be translated into the lower level logic before model-checking is done. The way this is organised needs a thorough overhaul, and is currently a bit confusing.

Back to CWB home page


Perdita.Stevens@ed.ac.uk