Back to Verification Homepage Back to Tool page

Using CWB with Emacs and daVinci (on harald)

  Installation   Usage   Pitfalls   Commands

Step by Step Installation

  1. Set some environment variables:
    $PATH must contain /users/btools/CWB-7.1:/users/btools/CWB-7.1/daVinci_V2.0/
    $DAVINCIHOME must be /users/btools/CWB-7.1/daVinci_V2.0

    E.g. in bash shell you can do this by

    bash$ export DAVINCIHOME=/users/btools/CWB-7.1/daVinci_V2.0
    bash$ export PATH=$PATH:/users/btools/CWB-7.1:/users/btools/CWB-7.1/daVinci_V2.0/

  2. Install the emacs cwb package
    copy the file /users/btools/CWB-7.1/cwb.el to a place emacs can find it
    usually this is ~/emacs

    You should byte-compile this file, e.g. from command line:
    bash$ emacs -batch --funcall batch-byte-compile cwb.el

  3. Set up emacs to use the packages:
    Copy the following into your ~/.emacs file

    (autoload 'cwb "cwb" "Run a CWB process." t)
    (autoload 'cwb-file-mode "cwb" "Major mode for editing CWB source." t)
    (add-hook 'cwb-load-hook
                  (lambda ()
                    (setq cwb-program-name "/users/btools/CWB-7.1/cwb")))) 
    (setq auto-mode-alist
          (append '(
    		("\\.cwb$" . cwb-file-mode)      ; Concurrency Workbench mode
    (add-hook 'daVinci-load-hook
               (lambda ()
                 (setq cwb-program-name "/users/btools/CWB-7.1/daVinci_V2.0/daVinci"))))

  4. Set up the daVinci translation script:
    Copy the modified perl script cwb2daVinci in a directory that occurs earlier in your $PATH than /users/btools/CWB-7.1
    Now the temporary files are labeled by your username, i.e. they look like /tmp/CWB_{your user name}_something. This makes it possible for more than one user on harald to run the CWB with daVinci.

  5. Run it:
    If you are working on working on a Silicon Graphics, log in on harald:
            bash$  xhost harald
            bash$  rlogin harald
     harald:bash$  export DISPLAY={yourTerminal}:0.0
    Note: If harald is very occupied, you could use other machines like e.g. gorm

    Restart emacs and enter       M-x cwb
    With C-c C-x you can start the daVinci backend now and view the processes you defined as graphics (use the menu-bar to steer this).
    The first time you will be asked for a registration, but this is free of any legal trapdoors.


Some Pitfalls

  1. Formulas in the modal µ-Calculus are sometimes hard to interpret. Important ones are
    max(Z.PHI & [-]Z) AG PHI    (Safety: Allways PHI)
    max(Z.[a]F & [-]Z) AG [a]F    (Safety: action a never enabled)
    max(Z.PHI & <->Z) EG PHI    (Potentially Allways PHI)
    min(Z.<a>T | <->Z) EF <a>T    (Eventually a, i.e. possibility)
    min(Z.[-a]F | ( <->T &[-]Z )) AF (<a>T & [-a]F)    (Inevitably a)
    min(Z.Q | (P & <->T & [-]Z)) P Until Q    (strong until)
    max(Z.Q | (P & [-]Z)) P Wuntil Q    (weak until)
    max(Z.[a]min(Y.<->T & [-b]Y)&[-]Z if a happens, eventually b follows (Response)

    For a more elaborate description refer to Colin Stirling 1997: Bisimulation, Model Checking and other Games.

  2. The daVinci interface is not perfectly clean, i.e. if you modify your definitions in the CWB, the exported graphics sometimes recycle outdated pictures. Fix: sometimes erase temporary graphic files in /tmp:
          bash$  rm /tmp/CWB_${USER}_*

The list of commands

Important ones are coloured pink.
agent change (or show) the definition of an agent identifier
branchingeq are agents branching bisimilar?
checkprop modelchecking: does agent satisfy formula?
clear removes all bindings (a fresh start)
closure find the weak derivatives of an agent via a trace
cong are two agents observationally congruent (equal)?
contraction are agents related by the contraction pre-order?
deadlocks find dead- or live-locked states and traces leading to them
deadlocksobs find dead- or live-locked states with observations
derivatives find the derivatives of an agent via a given action
dfstrong find a strong HML formula distinguishing two agents
dftrace find a trace distinguishing two agents
dfweak find a weak HML formula distinguishing two agents
diveq are two agents divergence equivalent?
diverges does the agent contain an unguarded occurrence of @?
eq are two agents observationally equivalent (weakly bisimilar)?
findinit find states with a given set of initial observable actions
findinitobs find states with a given set of initial observable actions
freevars list the free agent variables of an agent
graph list the transition graph of an agent
help provide on-line help
init find the observable actions an agent can perform immediately
input execute the CWB commands in the given file
inputfc2 execute the given FC2 file
mayeq are two agents may equivalent, i.e. trace equivalent?
maypre are two agents related by the may preorder?
min minimise an agent with respect to weak bisimulation
musteq are two agents must equivalent?
mustpre are two agents related by the must preorder?
normalform print an agent in normal form
obs find observations of a given length, and their results
output send CWB output to a file, or to the terminal
pb print largest weak bisimulation over the state-space of two agents
pre are two agents related by the (weak) bisimulation preorder?
precong are two agents related by the bisimulation precongruence?
prefixform print an agent in prefix form
print show the definitions of all identifiers
prop change (or show) the definition of a proposition identifier
quit terminates the workbench session
random give a pseudo-random observation of at most a given length
relabel change (or show) the definition of a relabelling identifier
save save the current environment in a file
savefc2 save an agent in FC2 format in a file
savemeije save an agent in Meije format in a file
set change (or show) the definition of a set identifier
sim simulate an agent interactively
size find the number of states of a finite-state agent
sort find the syntactic sort of the agent
stable is the agent stable?
states list the state-space of a finite-state agent
statesexp list the state-space, and a trace leading to each state
statesobs list the state-space and an observation leading to each state
strongeq are two agents strongly bisimilar?
strongpre are two agents related by the strong bisimulation preorder?
testeq are two agents testing equivalent (i.e. failures equivalent)?
testpre are two agents related by the testing preorder?
transitions list the (single-step) transitions of an agent
twothirdseq are agents related both ways by 2/3 bisimulation preorder?
twothirdspre are two agents related by the 2/3 bisimulation preorder?
vs find observations of a given length

Back to Verification Homepage Back to Tool page Back to top of this page   Oliver Möller - Last modified: Fri Apr 28 21:05:33 2000