Nondeterministic Execution

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

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.