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.