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
2 Architecture of the CWB
- 2.1 High level structure
  - 2.1.1 Using the common facilities
  - 2.1.2 Using a process algebra
- 2.2 Non-structural architectural guidelines
  - 2.2.1 Exceptions: handling and raising
  - 2.2.2 Public and protected interfaces
3 Common tasks and how to achieve them
4 Draft paper A Verification Tool Developer's Vade Mecum

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:

Lib, defined in common.ml
UI, with signature UI.sig. Provides functions to do things like giving the user various kinds of messages, asking questions, etc. UI.sig includes the signature DynamicCommands.sig which provides the functions by which a component may register a command: see below for more on this.
Registry, which is concerned with the maintenance of environments, which bind things to variables. Read on if your component maintains an environment. The Registry (global structure, matching signature Registry.sig ) provides a place where you can register certain functions for use when your module won't know when a piece of functionality is required, but does know how to provide it. You register the unit -> unit function together with a descriptive string for debugging purposes.
- The CWB commands print; and save "filename"; are intended to show the contents of all environments, in the form of CWB commands which would recreate the CWB state. The basic function UI.message prints a string to the appropriate place (screen or file) but the component writer has to use this basic function to show the environment as appropriate.
  For example one component has a function printAgentEnv to show the environment, and is registered thus:
  val _ = Registry.registerPrinter ("CCS Agent's agent environment printer", printAgentEnv)
  Tip It's a good idea if your printing function prints the entries in some predictable order, e.g. alphabetical by identifier. This helps you write automatic tests, as well as helping the user! The function listAlphabetical in Env may be useful.
- The CWB command clear; is intended to clear all environments, unbinding all variables. Register your environment-emptier thus: val _ = Registry.registerForgetter ("CCS Agent's agent environment forgetter", forgetAgents)
- Read this if your component has a signature whose behaviour may depend on mutable state, for example. the user-defined bindings of variables. If your component alters something that may invalidate someone else's cached information -- typically, you change a variable's binding -- you must cause the registry to call all the resetters by calling Registry.resetTables().
  If on the other hand your internal state may get invalidated if someone else changes something, read on:
Resetting yourself when things get into a bad state
If your module caches any information which could become out of date for reasons outwith your control, you should register a function for returning the cached information to a consistent state, e.g. by forgetting it. For example, PolyGraph caches graphs which it calculates, but the cached information may become wrong if the binding of any identifier is changed. It may also become inconsistent if an interrupt happens at a bad moment. These functions get called when either of these things happens. Register thus: val _ = Registry.registerTableResetter ("CCS Agent's knowledge and timestep knowledge", forgetall)
Lexing, a structure that helps with lexing (and hence parsing). Apology The situation here is a bit suboptimal: I haven't worked out a really good way to do distributed lexing and parsing in a sensible way. (I want to call a function meaning "here's my lexer, now please read a foo off it and give me the foo." But the lexer is a structure, and so ML's 2 layer set up gets in the way. Again.) Anyway, suggestions welcome, and in the mean time:
There is a global lexer which lexes the user's input. The CWB's parsers are hand-built: for historical reasons, reinforced by the difficulties I later had understanding MLYacc's documentation (and its relation with reality!) The most useful structure is Lexing : LEXING. The normal, global token set can be seen in cwb.lex: although in fact internally the CWB uses a couple of different lexers, both happen to be built on the same token set, which makes it easy to use a few instances of the Lexing structure throughout.
Suppose you want the user to input things in your syntax: say, to describe processes in your PA or formulae in your logic. You need to make sure that you use no tokens which will be rejected by the global tokeniser. You will probably want to do your own tokenising, lexing and parsing on relevant bits of input, e.g. on process descriptions in your PA. If the CWB's token set and lexing will do for you, just use them together with Lexing functions as need be. Otherwise, you can use global Lexing functions (e.g. getRest, toRBrack) to get hold of the string you need to deal with. Then you can deal with the string however you like. You may or may not find the CWB's functor Lexing a useful starting point. If you can make MLYacc work for you, feel free.
The main confusion is that the CWB is schizophrenic at the moment between saying "here is a stream, read a Foo from it" and working out what string must contain the Foo, and saying "here is a string, make a Foo out of it".
The existing process algebras work using two lexers, both on the same set of tokens but separately initialisable. One is used by top-level command parsing; you should open and use this one when you implement user commands. The other is private for use by the agent syntax parsing only. See the CCS Agent.str for an example.

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:

exception Error of string for a (non-syntactic) user error: the string will be shown to the user as an error message.
exception Parse of string for a parsing error: the string will be shown to the user as an error message.
exception PanicNoisily of string for something that shouldn't happen, i.e. a bug in your code. The user will be told that this is a bug, and the string argument will be used in "Found in" your string.

Exceptions you might have to handle

See the interfaces concerned. Exceptions currently in signatures:

Env.sig: Unbound
MaybeVar.sig: Unbound of V.var
PolyGraph.sig: LookUp
SortedList.sig: Retrieve
Trie.sig: Already_in_trie
Trie.sig: Not_in_trie
UI.sig: Picked of string
logic/ModalityComplex.sig: Dunno (defunct, in fact)

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.

Act.str contains a functor whose result matches ACT_PROTECTED.
Act.sig defines the public interface
ActProtected defines the protected interface like this: signature ACT_PROTECTED = sig include ACT structure Value' : VALUE_PROTECTED sharing Value = Value' [the rest of the signature then refers to Value']
Act.str must define both Value and Value', like this: structure Value' = [param] structure Value = Value'
Unfortunately anything using ACT_PROTECTED that wants to use things about VALUE_PROTECTED that only occur in the protected sig has to refer to Value' not to Value. Hence lines line structure A = A' at the top of functors. This is ugly: is it unacceptable? I don't think so, for now.
The analogous trick works for things which should be datatypes in the protected interface and types in the public interface.

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