- 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
//(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 ... }* }
>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.