## Index of commands

actcl: see closure
actders: see derivatives
agent: change (or show) the definition of an agent identifier
basi: see set
bi: see agent
bpi: see prop
bpsi: see prop
branchingeq: are agents branching bisimilar?
bye: see quit
ccs: show CCS syntax
checkprop: model-checking: does an agent satisfy a formula?
checkpropold: DEPRECATED modelchecking using old algorithm
cl: see closure
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?
cp: see checkprop
cwb: mostly for internal use: set CWB options
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
df: see dfstrong
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
div: see diverges
diveq: are two agents divergence equivalent?
diverges: does the agent contain an unguarded occurrence of @?
dr: see derivatives
echo: print a string to whereever output's going
eq: are two agents observationally equivalent (weakly bisimilar)?
exit: see quit
findinit: find states with a given set of next observable actions
findinitobs: find states with a given set of next observable actions
freevariables: see freevars
freevars: list the free agent variables of an agent
fv: see freevars
game: play model-checking games
globalmc: DEPRECATED option for old modelchecking algorithm
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
localmc: DEPRECATED option for old modelchecking algorithm
logic: show logic syntax
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
obsders: see closure
output: control where CWB output is written
pae: see print
pase: see print
pasi: see set
pb: print largest weak bisimulation over the state-space of two agents
pe: see print
pf: see prefixform
pi: see agent
play: play strong bisimulation games
ppe: see print
ppi: see prop
ppsi: see prop
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
sccs: show SCCS syntax
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?
taucl: see closure
tauders: see derivatives
testeq: are two agents testing equivalent (i.e. failures equivalent)?
testpre: are two agents related by the testing preorder?
toggle: toggle various CWB user options
tr: see transitions
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

Edinburgh Concurrency Workbench (v7.1).
Page generated: Sat Jul 17 22:30:01 BST 1999