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