CWB-NC Top-Level Commands


NAME

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.


NAME

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


NAME

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


NAME

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


NAME

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)


NAME

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)


NAME

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>        


NAME

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.


NAME

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).


NAME

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.


NAME

ls

SYNOPSIS

ls

DESCRIPTION

ls lists the names of variables bound in the various environments, i.e. agent variables, set variables, ...


NAME

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)


NAME

quit

SYNOPSIS

quit

DESCRIPTION

quit ends the current CWB-NC session.


NAME

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


NAME

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


NAME

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


NAME

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)


NAME

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)


NAME

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.