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
                (function
                 (lambda ()
                   (setq cwb-program-name "/users/btools/CWB-7.1/cwb")))) 
   
   (setq auto-mode-alist
         (append '(
   		("\\.cwb$" . cwb-file-mode)      ; Concurrency Workbench mode
   		)
                 auto-mode-alist))
   
   (add-hook 'daVinci-load-hook
             (function
              (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
   
   • If you have e.g. ~/bin direcory in your directory, copy it there.
   • Else, create ~/bin, copy it the perl script there and modify the export line above: Instead of

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

     It should be

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

   You should set the permissions of this script right, so it does not create /tmp/CWB... files that can confuse others:

   bash$  chmod 0700 $HOME/bin/cwb2daVinci
   	    

   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.
   
   
• If you just want to use Emacs:
  Just omit everything containing 'daVinci' in the description above.
  
  
• If you don't like Emacs...
  Just include /users/btools/CWB-7.1 in your $PATH, then run CWB by the command line argument

        bash$  cwb
        

  I advise against it. You don't have to like Emacs in order to use it where it helps you.

Usage

• the buffer *cwb* contains your primary interface.
  Define some processes here, e.g.:
  

        set S = {a,b,c};
        agent A = a.A;
        agent X = b.A + c.A;
        print;
        

• Very useful Emacs commands:

  C-return	word completion
  C-up	last commands toggle
  C-down	next command toggle
  M-s [regexp]	toggle to last command matching some regular expression
  C-c C-l	load file

  
  
• You can display agents graphically via daVinci:
  
  M-x cwb-graph-add-graph [Ret] X [Ret]
  (or use the menu bar, I haven't figured out a better method).
  
  Unfortunately, the editing commands in the GUI do not work, so you can merely display agents. But this is still better than having only the naked definitions.
  
  
• There are some predefined .cwb examples avaliable (load in *cwb* with C-c C-l )
  
  
  • Alternating Bit Protocol
  • Basic Example
  • Basic checking of a proposition
  • Demo (from 11/04/2000)
  • Jobshop
  • Mailsystem (Gordon Brebner)
  • Parametrized Agents
  • Parametrized Propositions

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

Oliver Möller - Last modified: Fri Apr 28 21:05:33 2000