The Concurrency Workbench (CWB) is a tool used to model concurrent systems. Actually, there are two versions of the CWB -- the "North Carolina" version and the "Edinburgh" version, which were developed at North Carolina State University and the University of Edinburgh, respectively. The commands used to control the CWB vary between the two systems, but they both allow us to simulate systems described by CCS. We have the North Carolina version installed on departmental DEC Alphas (such as csgrad, fir, etc.).
The first thing to do is, as always, add something to your path. The usual way to do this is in your .tcshrc, .cshrc, or .login file; this is so that every time you log in, your path will be modified to include the proper directory. If you don't modify your path in one of these files, and instead modify your path on the command line, then the modification will only be held until you exit your current shell (or you log out). It seems that on the Alphas, at least, the .login file is processed after the shell configuration file, so you may want to make the modification in there; it couldn't really hurt to put it in both places, just to be safe. So, add the following to the end of your .tcshrc, .cshrc, or .login files:
set path=($path /usr/local/CWB/cwb-nc/bin)Then, when you log in, your shell will process its configuration file and your .login file; it will see the modification you've made (which was to just add
/usr/local/CWB/cwb-nc/bin to your path)
every time. If you don't want to add this to your path permanently, you
can type the above command at the shell prompt, but remember, the next
time you log in, you'll have to type it again.
When you actually want to run the CWB, then assuming the above directory is in your path, type:
cwb-nc ccsThis will start the CWB interpreter that understands CCS.
load
SYNOPSIS
load filename
DESCRIPTION
This command loads a file into the current CWB-NC session.
The file suffix indicates the type of file to be loaded:
.ccs files contain a sequence of ccs process definitions.
.mu files contain a sequence of mu-calculus formulas.
eq
SYNOPSIS
eq [-S semantic-type] agent1 agent2
DESCRIPTION
eq computes whether agent1 and agent2 are related by the
equivalence relation indicated by semantic-type (obseq by
default). The currently available semantic-type arguments
are obseq (observational equivalence), bisim (strong
bisimulation equivalence), trace (trace equivalence),
may (may equivalence), and must (must equivalence).
EXAMPLE
cwb-nc> load abp.ccs
Execution time (user,system,gc,real):(0.080,0.070,0.000,0.198)
cwb-nc> eq Spec ABP-lossy
Building automaton...
States: 59
Transitions: 132
Done building automaton.
Transforming automaton...
Done transforming automaton.
TRUE
Execution time (user,system,gc,real):(0.250,0.010,0.000,0.423)
cwb-nc> eq -S bisim Spec ABP-lossy
Building automaton...
States: 59
Transitions: 132
Done building automaton.
FALSE...
Spec satisfies:
[t]ff
ABP-lossy does not.
Execution time (user,system,gc,real):(0.190,0.050,0.010,0.343)
quit
SYNOPSIS
quit
DESCRIPTION
quit ends the current CWB-NC session.
sim
SYNOPSIS
sim agent
DESCRIPTION
sim allows user-directed or random simulation of agent.
After invoking the simulator the following commands are
available: help [command], current, transition-num,
random [num], break [-a][-d][-l] [act list], back [num],
history, trace, goto num, !!, quit,
More information on each of these commands is available
via the simulator's help command.
EXAMPLE
cwb-nc> sim "a.b.nil + c.nil"
a.b.nil + c.nil
1: -- c --> nil
2: -- a --> b.nil
sim: 2
b.nil
1: -- b --> nil
sim: 1
nil
The agent has no transitions
sim: history
1: a.b.nil + c.nil -- a -->
2: b.nil -- b -->
3: nil
sim: trace
a b
sim: goto 2
Current state moved 1 step back.
sim: current
b.nil
1: -- b --> nil
history
SYNOPSIS
history
DESCRIPTION
Simulator command that prints the history of the current
simulator session. Note that backtracking with the back
command removes transitions from the history; thus, the
path displayed by the history command represents a path
from the initial agent to the current agent. The states
through which the path progresses are numbered starting
with 1.
EXAMPLE
cwb-nc> sim "a.b.c.nil | d.e.nil"
a.b.c.nil | d.e.nil
1: -- d --> a.b.c.nil | e.nil
2: -- a --> b.c.nil | d.e.nil
cwb-nc-sim> 2
b.c.nil | d.e.nil
1: -- d --> b.c.nil | e.nil
2: -- b --> c.nil | d.e.nil
cwb-nc-sim> 1
b.c.nil | e.nil
1: -- e --> b.c.nil | nil
2: -- b --> c.nil | e.nil
cwb-nc-sim> 1
b.c.nil | nil
1: -- b --> c.nil | nil
cwb-nc-sim> history
1: a.b.c.nil | d.e.nil -- a -->
2: b.c.nil | d.e.nil -- d -->
3: b.c.nil | e.nil -- e -->
4: b.c.nil | nil
SEE ALSO
trace, goto
random
SYNOPSIS
random [num]
DESCRIPTION
Simulator command that simulates num random execution steps
of an agent. The default value for num is 1.
EXAMPLE
cwb-nc> sim "a.b.c.nil | d.e.nil"
a.b.c.nil | d.e.nil
1: -- d --> a.b.c.nil | e.nil
2: -- a --> b.c.nil | d.e.nil
cwb-nc-sim> random
b.c.nil | d.e.nil
1: -- d --> b.c.nil | e.nil
2: -- b --> c.nil | d.e.nil
cwb-nc-sim> random 3
c.nil | d.e.nil
1: -- d --> c.nil | e.nil
2: -- c --> nil | d.e.nil
nil | d.e.nil
1: -- d --> nil | e.nil
nil | e.nil
1: -- e --> nil | nil
cwb-nc-sim> history
1: a.b.c.nil | d.e.nil -- a -->
2: b.c.nil | d.e.nil -- b -->
3: c.nil | d.e.nil -- c -->
4: nil | d.e.nil -- d -->
5: nil | e.nil
quit
SYNOPSIS
quit
DESCRIPTION
Simulator command that ends the current simulator session.
Suppose we have a CCS description of a vending machine that's stored in
a file named vending.ccs. A
session (user commands in bold) with the North Carolina CWB might
look like:
fir.cs.vt.edu:[b-nc/examples/ccs/cs5204] -> cwb-nc ccs The Concurrency Workbench of North Carolina (Version 1.0 --- September, 1996) cwb-nc> load vending.ccs Execution time (user,system,gc,real):(0.014,0.003,0.000,0.021) cwb-nc> ls ===Agent=== VM ===Set=== ===Formula=== Execution time (user,system,gc,real):(0.001,0.005,0.000,0.007) cwb-nc> sim VM VM 1: -- twop --> big.collect.VM 2: -- onep --> little.collect.VM cwb-nc-sim> 2 little.collect.VM 1: -- little --> collect.VM cwb-nc-sim> 1 collect.VM 1: -- collect --> VM cwb-nc-sim> 1 VM 1: -- twop --> big.collect.VM 2: -- onep --> little.collect.VM cwb-nc-sim> random 6 little.collect.VM 1: -- little --> collect.VM collect.VM 1: -- collect --> VM VM 1: -- twop --> big.collect.VM 2: -- onep --> little.collect.VM big.collect.VM 1: -- big --> collect.VM collect.VM 1: -- collect --> VM VM 1: -- twop --> big.collect.VM 2: -- onep --> little.collect.VM cwb-nc-sim> quit Execution time (user,system,gc,real):(0.028,0.014,0.000,18.650) cwb-nc> quit
When we typed the command sim VM, we started simulating the
vending machine. Note how the prompt changed from
cwb-nc> to cwb-nc-sim> when we did this;
this indicates that we are in simulation mode. Note that the command
set is different between the simulation mode and the top-level (see the
references for help with these two classes of
commands). When we entered the simulator, we were given two choices: to
perform a "twop" or a "onep"; typing "2" selected a "onep", and the
simulation proceeded from there. The random command lets the
simulator make a certain number of random choices from those possible at
every successive state in the simulation.