Backup diff of Nondeterministic Execution vs current(No. 2)

List of Backups
View the diff.
View the source.
View the backup.
Go to Nondeterministic Execution.
- 1 (2006-03-19 (Sun) 18:39:45)
- 2 (2006-03-19 (Sun) 19:06:40)
- 3 (2006-03-24 (Fri) 14:25:36)
- 4 (2009-11-30 (Mon) 16:13:03)
- 5 (2009-11-30 (Mon) 16:13:03)
- 6 (2010-05-28 (Fri) 14:17:18)

The added line is THIS COLOR.
The deleted line is THIS COLOR.

[[Documentation]]
//[[Documentation]]

*Nondeterministic Execution Mode
''NOTE:'' This page describes nondeterministic search using LMNtal Java.  Now LaViT and SLIM comes with a fuller implementation of nondeterministic state-space search.  The use of LaViT is strongly recommended because it significantly facilitates state-space search, model checking, and their visualization.  

(A fuller description will be available soon.)
*Nondeterministic Execution Mode in LMNtal Java

Version 0.8 (and up) supports nondeterministic execution mode
//(A fuller description will be available soon.)

Version 0.8 (and up) supports '''nondeterministic execution mode'''
that explores all possible reduction paths.

By giving the -nd option to lmnr(_cyg), the system computes all
By specifying the ''-nd'' option to ''lmnr(_cyg)'', the system computes all
possible reduction paths and displays the reduction graph (a graph
representing all possible states and state transition).
The nondeterministic execution mode will return a finite cyclic
graph for a diverging program as long as the set of possible
A powerful feature of the nondeterministic execution mode is that
it will return a '''finite''' cyclic
graph for a '''diverging''' program as long as the set of all possible
states is finite.

By giving the --interactive option in addition to the -nd option,
the system displays possible results of execution one by one
(as most Prolog systems do) in response to the ";" (semicolon) characters
entered by the user.
By specifying both the ''--interactive'' option and the ''-nd'' option,
the system displays possible results (= final states) of execution one by one in response to the "'';''" characters entered by the user (as
in Prolog systems).

The system comes also with the "all solutions" feature.  The process
The system comes also with the "'''all solutions'''" feature.  The process

 nd.exec{ { ... LMNtal program here ... }* }
>nd.exec{ { ... '''LMNtal program here''' ... }* }

will be reduced to a reduction graph of the (Flat) LMNtal program enclosed
by the double membranes.


** Restrictions

- Currently available only for Flat LMNtal programs, i.e.,
progrmas that do not use cells (membranes).
- Nondeterministic execution mode is currently applicable only to
'''Flat''' LMNtal programs, i.e., 
progrmas that do not use membranes.

- Nondeterministic execution cannot be used with the --interpret
option.
- Nondeterministic execution cannot be used with the ''--interpret''
option; the program must be compiled first (no ''--nd'' option need
at compile time) and then be run with the ''--nd'' option.

- Nondeterministic execution mode cannot be used with the ''-O3'' option.