//[[Documentation]]

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

*Nondeterministic Execution Mode in LMNtal Java

//(A fuller description will be available soon.)

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

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

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

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


** Restrictions

- 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; 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.
Front page List of pages Search Recent changes Backup   Help   RSS of recent changes