caching
SYNOPSIS
caching arg
DESCRIPTION
The "caching" command toggles whether or not transitions are cached during analysis. "arg" is either "on" or "off" When caching is on, the transitions of subterms of the parallel composition operator are cached as they are computed, which usually leads to impressive speedups since these are recomputed numerous times for a typical design. However, if the subterms of a parallel composition operator are automata (as is the case when doing component wise minimization) caching is unnecessary and wastes space, therefore should not be used.
cat
SYNOPSIS
cat identifier
DESCRIPTION
cat displays the item bound to "identifier". If "identifier" is bound
in more than one environment, each binding is displayed.
SEE ALSO
ls
cd
SYNOPSIS
cd directory
DESCRIPTION
cd sets the present working directory (the unix directory in which the
CWB-NC searches when the load command is executed). The initial working
directory is the one from which the CWB-NC was invoked.
EXAMPLE
cwb-nc> cd /usr/local/src/cwb-nc/examples/ccs Execution time (user,system,gc,real):(0.000,0.000,0.000,0.000) cwb-nc>SEE ALSO
load
chk
SYNOPSIS
chk agent formula
DESCRIPTION
chk invokes the model checker to determine whether or not "agent" satisfies
"formula". If the given formula is alternation-free then a global model
checker is invoked; otherwise, if the formula is in the L2 fragment of
the mu-calculus, then an on-the-fly model checker is invoked. Formulas
in neither of these fragments are not yet handled.
EXAMPLE
cwb-nc> load abp.ccs Execution time (user,system,gc,real):(0.120,0.010,0.000,0.161) cwb-nc> load abp.mu Execution time (user,system,gc,real):(0.010,0.000,0.000,0.014) cwb-nc> chk ABP-safe can_deadlock Building automaton... States: 49 Transitions: 74 Done building automaton. True, the agent satisfies the formula. Execution time (user,system,gc,real):(0.130,0.010,0.000,0.216)SEE ALSO
load
compile
SYNOPSIS
compile agent1 [ agent2 ... ]
DESCRIPTION
compile builds an automaton for the agents given as arguments and displays
a textual representation of the constructed automaton. In the example below,
the start state is 0 and this state has an "a" transition to state 1 and
a "c" transition to state 2.
EXAMPLE
cwb-nc> compile "a.b.nil | c.nil"
Building automaton...
States: 6
Transitions: 7
Done building automaton.
0: a {1}
c {2}
1: b {3}
c {4}
2: a {4}
3: c {5}
4: b {5}
5:
Start States: [0]
Execution time (user,system,gc,real):(0.010,0.020,0.000,0.082)
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)
es
SYNOPSIS
es filename1 [filename2]
DESCRIPTION
es executes the sequence of CWB-NC commands contained in filename1 and
directs the output to filename2 (stdout if second argument is not given).
Note that each command in filename1 (including the final command) must
end with a newline character.
EXAMPLE
Let the file abp.cws contain: load abp.ccs eq -S obseq Spec ABP-safe load abp.mu chk ABP-safe can_deadlock After, cwb-nc> es abp.cws abp.cws.output Executing CWB script file abp.cws, directing output to abp.cws.output. June 17, 1996 10:03 .................... cwb-nc> the file abp.cws.output contains: Executing CWB script file abp.cws, directing output to abp.cws.output. June 17, 1996 10:01 Execution time (user,system,gc,real):(0.010,0.000,0.000,0.120) cwb-nc> load abp.ccs Execution time (user,system,gc,real):(0.110,0.030,0.000,0.179) cwb-nc> eq -S obseq Spec ABP-safe Building automaton... States: 51 Transitions: 76 Done building automaton. Transforming automaton... Done transforming automaton. FALSE... Spec satisfies: [[send]]<<'receive>>tt ABP-safe does not. Execution time (user,system,gc,real):(0.240,0.010,0.010,0.259) cwb-nc> load abp.mu Execution time (user,system,gc,real):(0.020,0.000,0.000,0.018) cwb-nc> chk ABP-safe can_deadlock Building automaton... States: 49 Transitions: 74 Done building automaton. True, the agent satisfies the formula. Execution time (user,system,gc,real):(0.110,0.010,0.000,0.121) cwb-nc>
help
SYNOPSIS
help [command-name]
DESCRIPTION
help displays information about CWB-NC commands. If executed with no arguments, then a list of available commands is displayed. If given a command name as an argument, then information about the specific command is displayed.
le
SYNOPSIS
le [-S semantic-type] agent1 agent2
DESCRIPTION
le computes whether agent1 and agent2 are related by the behavioral preorder indicated by semantic-type. The currently available semantic-type arguments are may (may preorder) and must (must preorder).
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.
ls
SYNOPSIS
ls
DESCRIPTION
ls lists the names of variables bound in the various environments, i.e. agent variables, set variables, ...
min
SYNOPSIS
min [-S semantic-type] agent identifier
DESCRIPTION
min minimizes agent with respect to the equivalence relation indicated
by semantic-type (obseq by default) and binds the resulting agent to identifier.
The currently available semantic type arguments are obseq (observational
equivalence) and bisim (strong bisimulation equivalence).
EXAMPLE
cwb-nc> load abp.ccs Execution time (user,system,gc,real):(0.090,0.040,0.000,0.163) cwb-nc> min -S bisim ABP-lossy ABP-lossy-min Building automaton... States: 57 Transitions: 130 Done building automaton. Minimizing automaton... Computing bisimulation... Done computing bisimulation. Done minimizing automaton. Execution time (user,system,gc,real):(0.210,0.060,0.000,0.489) cwb-nc> size ABP-lossy-min Building automaton... States: 15 Transitions: 32 Done building automaton. 15 states 32 transitions Execution time (user,system,gc,real):(0.010,0.000,0.000,0.013)
quit
SYNOPSIS
quit
DESCRIPTION
quit ends the current CWB-NC session.
save
SYNOPSIS
save filename [ identifier ... ]
DESCRIPTION
The save command saves the bindings in the current environment, or selected
bindings, to a file. If one or more identifier arguments are given, then
the bindings for these identifiers are saved to filename. If no identifier
arguments are given, then all bindings in the environment are saved to
a file. The save command is useful for saving minimized automata for future
use.
SEE ALSO
load
search
SYNOPSIS
search agent formula
DESCRIPTION
search invokes the CWB-NC reachability analysis routine. Given an agent
and a formula the routine searches the set of reachable states in the agent
for a state satisfying the given formula. If such a state is found, the
simulator is invoked with a path to the state pre-loaded. The formula may
be any mu-calculus (or CTL) formula supported by the CWB-NC model checkers;
however, in most cases it will be a Hennessy-Milner Logic (HML) formula
that may be checked very quickly at each state. Note that a HML formula
is simply a mu-calculus formula that contains no fix point operators or
weak modalities.
EXAMPLE
cwb-nc> load abp.ccs
Execution time (user,system,gc,real):(0.140,0.020,0.020,0.212)
cwb-nc> load abp.mu
Execution time (user,system,gc,real):(0.030,0.000,0.000,0.035)
cwb-nc> search ABP-safe is_deadlocked
States explored: 8
State found satisfying is_deadlocked.
Path to state contains 8 states, invoking simulator.
1: ABP-safe -- send -->
2: (R0 | Msafe | S0')\Internals -- t -->
3: (R0 | 'r0.Msafe | (rack0.S1 + rack1.S0' + t.S0'))\Internals -- t -->
4: ('receive.'sack0.R1 | Msafe | (rack0.S1 + rack1.S0' + t.S0'))\
Internals -- t -->
5: ('receive.'sack0.R1 | Msafe | S0')\Internals -- t -->
6: ('receive.'sack0.R1 | 'r0.Msafe | (rack0.S1 + rack1.S0' + t.S0'))\
Internals -- t -->
7: ('receive.'sack0.R1 | 'r0.Msafe | S0')\Internals -- 'receive -->
8: ('sack0.R1 | 'r0.Msafe | S0')\Internals
cwb-nc-sim>
SEE ALSO
fd, chk, load
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
size
SYNOPSIS
size agent
DESCRIPTION
size builds an automaton which models the behavior of agent and displays
the number of states and transitions in the constructed automaton.
EXAMPLE
cwb-nc> size "a.b.nil | 'a.c.nil" Building automaton... States: 9 Transitions: 13 Done building automaton. Execution time (user,system,gc,real):(0.010,0.010,0.000,0.052)
sort
SYNOPSIS
sort agent
DESCRIPTION
sort displays the set of visible actions that agent may engage in.
EXAMPLE
cwb-nc> sort "a.b.nil | 'a.c.nil"
{ a, b, c, 'a }
Execution time (user,system,gc,real):(0.000,0.020,0.000,0.016)
trans
SYNOPSIS
trans agent
DESCRIPTION
trans displays the single step transitions which agent may perform.
EXAMPLE
Command: trans "a.nil + b.nil" -- b --> nil -- a --> nil Execution took 0.000 seconds.