[[Documentation]] ''NOTE:'' This page describes nondeterministic search using LMNtal Java. Now LMNtalEditor and SLIM comes with a fuller implementation of nondeterministic state-space search. The use of LMNtalEditor 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.