Copyright (c) 1989, 1990, 1991, 1992, 1993
by Helsinki University of Technology, Digital Systems Laboratory.
All rights reserved.

Authors of probhelp: Jaakko Halme, Kari Hiekkanen,
                     and Kimmo Varpaaniemi

Current version:
    $Id$

Description:
    probhelp is the default help file of PROD's program "probe".
    When "probe" user calls help or "?" for the first time,
    probhelp is loaded if no other file has been specified
    by the "-h" option of "probe".

    Help file consists of subject lines, content blocks, and comment
    blocks. A line is an @-line if and only if its first character
    is @. (If the first character is a space or tabulator, the
    line is not a @-line.) An @-line is a subject line if and only
    if there is at least one string after the first @ on the line.
    (Spaces and tabulators separate strings from each other.
    No string contains a space or tabulator.) The strings after the
    first @ on a subject line form the key of a help subject. The
    lines after a subject line and before the next (if any) @-line
    form a content block. When "probe" user asks help or "?" about a
    subject, the content block of the subject is shown. If there
    is no string after the first @ on a @-line, the @-line starts
    a comment block which continues down to the next (if any) @-line.
    The lines before the first @-line in the file also form a comment
    block. "probe" skips all comment blocks.
    
Version history:
    $Log$

@Commands

"probe" accepts currently following commands:

	allcomps	build		calc		clear
	clearall	enabledfacts	goto		look
	next		pred		prev		query
	quit		sets		sgpred		sgsucc
	showends	shrink		statistics	succ
	termcomps

- Multiple commands can be typed to same command line by separating
  them with #. "probe" displays the results of commands in same order as
  they were on the command line.

  However this does not affect the use of literal commands.

  For example:
        define looksucc look#succ

  defines macro looksucc which expands to command sequence
  look # succ.

- Commands can be extented to multiple lines. This is done by typing
  "\" at end of each line. The command is executed when newline is
  pressed without preceding "\".

@Comments

Comments can be included in a command line simply by quoting them
between "/*"and "*/" as in C-language. Comments can be nested and can
extend to multiple lines without using the "\".

@Interrupt

User can interrupt the execution of a command by pressing
CTRL-C. In MS-DOS commands given with mute directive can
be interrupted only if "probe" was started with -. (dot) option.

@Literal commands

"probe" literal commands form a special set of commands in the sense
that they do not go through macro expansion, they cannot be used in
macro definitions, they must appear at the beginning of the line, and
they always continue to the end of the whole command line.

"probe" literal commands:
   - define		define macro or constant
   - defs	    	show defined macros and constants
   - undef		undefine macro or constant
   - undefall		undefine all macros and constants
   - help		on-line help
   - load		load and execute command file

@define

Syntax: define <name> <body>
        define <name> <(arguments)> <body>
	

Defines the macro (or constant) named <name>. The body of the
macro is given in <body> and possible arguments in <arguments>.

The body of the macro can be anything. The name of the macro cannot be
a reserved word in "probe".  After a macro has been defined, it can be
used as a part of any other command in "probe" simply by typing its
name to command line.

@defs

Syntax: defs name*

Displays the definition for named macros and constants. If abbreviations are
supplied, displays all possible completions. If no name is supplied, displays
definitions for all defined macros and constants.


@undef

Syntax: undef name*

Undefines named macros or constants.

@undefall

Undefines all defined macros and constants.

@help

Syntax: help subject
	?

On-line help on the subject. If abbreviation is supplied, lists all possible
completions. (If the abbreviation is complete but not unique, full description
of the complete subject is displayed.) The command help with no arguments
prints all possible subjects. The "?" is a shorthand for command
help.

@load

Syntax:	load name

Loads command file "name" and executes the commands in it.

If file "name" doesn't exist and PRODPATH environment variable has been
defined, "probe" looks for "$PRODPATH/name" ("%PRODPATH%\name" in MS-DOS).
"name" can contain directory parts (and a drive identifier in MS-DOS).

@prev

Syntax: prev

Returns to the previous node. The previous node is the node from which
we came to the current node by next -command.

@sgsucc

Syntax: sgsucc <stongcomp>

Displays information about the successor components of strongly
connected component <stongcomp>.

@sgpred

Syntax: sgpred <stongcomp>

Displays information about the predecessor components of strongly
connected component <stongcomp>.

@calc

Syntax: calc <expression>
	calc <marking>

Evaluates and displays the value of the expression or marking.

@clear

Syntax: clear <set>

Deletes the <set>.

@clearall

Deletes all non-special sets.

@termcomps

Syntax:	termcomps <preds,succs>

Displays information about the nontrivial terminal
strongly connected components in the reachability graph. (A terminal node
or a strongly connected reachability graph is a trivial terminal strongly
connected component.)

The <preds> option causes "probe" to display information about
the predecessor components for each component.

See also: allcomps

@allcomps

Syntax:	allcomps <preds,succs>

Displays information about all strongly connected
components in the reachability graph.

The <preds> option causes "probe" to display information about
the predecessor components for each component. Similary the
<succs> option causes "probe" to display information about the
successor components for each component.

See also: termcomps

@build

Syntax: build <set_operation> <volatile>

Calculates the <set_operation> and displays the result. If <volatile> option
is not supplied, makes a set from the result.

See also: sets

@goto

Syntax: goto <expression>

Sets current node to the node pointed by the <expression>.

@look

Syntax: look
	look <expression>

Displays the marking at the current node or the node pointed by
the <expression>.

@pred

Syntax: pred
	pred <expression>

Displays the information of predecessor arrows of the current node or
the node pointed by <expression>.

@query

Syntax:	query <formula> <volatile>
	query node <formula> <volatile>

Issues a query about the reachability graph.
If <volatile> option is not supplied, makes a set from the answer.

query returns paths starting from the current node. query node returns paths
starting from any node. An atomic <formula> is evaluated either to an empty
set or a set consisting of a path of length 0. A recursive <formula> is
evaluated to a set of path concatenations.

The program displays paths simultaneously while searching.

See also: Formula, Interrupt

@quit

Syntax:	quit

Quits "probe". Returns control back to calling programs.

@showends

Syntax: showends <set_operation>
	showends all

Displays the information of the last nodes of paths on the set of
paths pointed by <set_operation>. The showends all command displays
the information of all nodes in the graph.

The showends command can be used with options <preds>,
<succs> and <factarrows>.

The <preds> option causes "probe" to display information about the
predecessor nodes and arrows for each node. Similary the <succs>
option causes "probe" to display information about the successor nodes
and arrows for each node. The <factarrows> option causes "probe" to
display information about the fact arrows from each node.

Options can be combined and they can be typed before or after the
actual command.

@shrink

Syntax:	shrink <set>

Shrinks <set> so that only the path end nodes remain.

@statistics

Syntax:	statistics

Displays the statistical information on the reachability graph. The
statistical information contains the number of nodes, arrows, fact arrow
source nodes, fact arrows, terminal nodes, handled nodes, strongly
connected components and nontrivial terminal strongly connected
components.

@next

Syntax: next <expression>

Moves from current node to the target node of arrow pointed by
<expression>. The target node becomes the new current node.

@succ

Syntax: succ
	succ <expression>
	succ <node> arrow <number>
	succ arrow <expression>

Displays the information about the successor arrows of the current
node or the node pointed by <expression>.

succ <node> arrow <number> displays the information about the defined
arrow from defined node.  The node is defined by <node> and the arrow
by <number>.  Both <node> and <number> must be valid expressions.

succ arrow <expression> displays the information about the arrow from the
current node. The number of arrow is defined by <expression>.
 
@sets

Syntax: sets

Displays sets and operations (query or set operation) which
resulted them.

@enabledfacts

Syntax: enabledfacts <expression>
	enabledfacts <node> arrow <number>

enabledfacts <expression> displays information about all fact arrows
from node pointed by expression. If expression is omitted, displays
information about fact arrows from current node.

enabledfacts <node> arrow <number> displays information about defined
fact arrows from defined node.  The node is given by <node> and the
arrow number by <number>.  If <node> is omitted then current
node will be used. Both <node> and <number> must be valid
expressions.

@Verbosity

The user can define the verbosity level of commands. Verbosity options
are <mute>, <verbose> and <superverbose>. The number of verbosity levels
is four because the default verbosity level is distinct. The default is
more than <mute> but less than <verbose>.

@Formula

Simplified syntax of formula is 

	(x)			false			true
	not x			step x			bpath (x,y) z
	dpath (x,y) z		bspan (x) y		dspan (x,y) z
	@ expression  		set_operation		expression
	x and y			x  or y			fire (firing_class) x

where x, y and z are formulas.

The exact syntax and semantics of formulas can be found in the manual.

See : Expression, Sets

@Expressions

The syntax of expression if similar to the expression syntax of
C-language. Operators are the same.

See: Expression syntax, Expression operators

@Expression syntax

 simple_expression ::=
   	variable                Value of variable of the transition
                                in question. (See firing_class.)
        preclass                Precedence class of the transition
                                in question. (See firing_class.)
	card(marking)	        The cardinality of a marking.
	(expression)
	field[expression]	The value of defined field in a marking.
				The number of the field is determined by
				expression. 
	integer			The type of integer is long.
	.			The number of current node in the
				reachability graph.

See also: Expressions operators

@Expression operators

Expressions can be combined with following operators - (unary minus),
! (negation), ~ , *, /, % (modulus), +, -- (minus), >> (shift right),
<< (shift left)), <, <=, >, >=, ==, !=, & (bitwise and), | (bitwise
or), ^ (bitwise xor), && (logical and), \\ (logical or), ? : (selection)
Also comparation of markings with <, <=, > >=, == and != operator are
expressions.

The value of expression is integer (long).

See also: Expression syntax

@Marking

 simple_marking :: =
	  place name 		The name of the place in a net as defined
				  in a net description file.
	  empty			Empty marking.
	 <.rangelist.>		
  	 <. .>
  	 (marking)

 marking :: =
	  simple_marking
	  marking & marking	intersection
  	  marking + marking 	sum
	  marking - marking 	difference
  	  simple_marking : simple_expression
				The submarking of simple_marking for which
				the simple_expression is true (not equal to
				zero).
  	  simple_expression simple_marking
				; The simple_marking multiplied by
                                  the simple_expression.

See also: Expression syntax
@Range

 rangelist :=
	  range
	  rangelist , range

 range ::=
	  expression
	  expression ..  expression
	  (range)

See also: Expression syntax

@firing_class

 firing_class ::=
  transition name(expression)         Transition instances satisfying
                                      expression.
  (firing_class)
  !firing_class
  firing_class || firing_class
  firing_class && firing_class


@Sets

 set_operation :: =
	  (set_operation)
  	  set
  	  scomp
	  set_operation | set_operation		; union
	  set_operation + set_operation		; union
	  set_operation & set_operation		; intersection
	  set_operation - set_operation 	; set difference

 set :: =
	 $simple_expression
	 (set)

See also: Expression syntax, Strongly connected components

@Strongly connected components

 scomp ::=
 	  $$simple_expression
	  (scomp)

See also: Expression syntax
