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
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:
unit function together with a descriptive string for debugging
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:
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.
clear; is intended to clear all
environments, unbinding all variables. Register your environment-emptier
If on the other hand your internal state may get invalidated if someone else changes something, read on:
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.
See common.ml. In summary:
To illustrate the way we do this, here's how it is for Act.
structure A = A' at
the top of functors. This is ugly: is it unacceptable? I don't think so,
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
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
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:
A : ACT refers to signature
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!
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.
Back to CWB home page