*How to Use
 java -jar lmntal.jar [options...]                 --> start interactive mode
 java -jar lmntal.jar [options...] [filenames...]  --> load from files and run
 java -jar lmntal.jar [options...] -e 'program'    --> run a one-liner program
*LaViT: LMNtal Visual Tools [#ed6fa884]

**Interactive Mode
The LaViT IDE should be quite easy to use.  

Interactive mode will start when filenames are not specified in the command line.
The process to be executed can be given in multiple lines.
Press the enter key twice to finish the process and execute it.

The following list shows some interactive-mode commands:
The upper-left pane is for
editing programs, while the upper-right pane shows system output.

 q             - quit
 h             - see help
 trace|notrace - set trace mode
 verbose [0-9] - set verbose level
 shuffle [0-3] - set shuffle level
To run your program, use one of the buttons on the lower-left pane:

Here is an example of an interactive mode session:
:''Compile'':|  Invoke the LMNtal compiler to generate intermediate code.
:''UNYO(2G)'', ''UNYO(3G)'':|  Invoke the 3rd-generation UNYO-UNYO visualizer.  (UNYO-UNYO internally uses the Java runtime.)
:''SLIM'':|  Run the program (LMNtal source or intermediate code) using the SLIM runtime.
:''StateViewer'':|  Visualize the state-space of the program.  StateViewer internally runs SLIM with the --nd (nondeterministic execution) option.

 % java -jar lmntal.jar [PRESS ENTER]
         LMNtal version 0.64.20040611
 Type h to see help.
 Type q to quit.
 Enter an empty line to run the input.
 # A=f(f(f(f(f(A))))), c,c, ( c, X=f(Y) :- X=g(Y) ) [PRESS ENTER]
 f(g(g(f(f(_4)))),_4), @601
 # A=f(f(f(f(f(A))))), c,c, ( c, X=f(Y) :- X=g(Y) ) [PRESS ENTER]
 g(f(f(f(g(_24)))),_24), @604
To model-check your program, click the ''LTL model check'' tab of the upper-right pane,


 -t            - trace mode
 -v[0-9]       - set verbose level ( -v = -v5 )
 -s[0-3]       - set shuffle level ( -s = -s3 )
 -g            - graphical mode (experimental)
and proceed as follows:

***Verbose Level
- Define propositional symbols that represent properties of states (using the syntax of the left-hand sides of rewrite rules). 
- Specify an LTL formula representing the property you wish to check.
- Press the ''Translate'' button to compile the formula to a Buchi automaton.
- Press the ''slim --ltl'' (or ''slim --ltl-all'' or ''LTL StateViewer'') button to check the specified property.

Expresses how verbosely an LMNtal process is displayed.
Examples of propositional symbols and LTL formulas can be found by opening the programs under the ''demo/ltl'' directory of the distribution.

   0: silence
   2: default
   3: print `proxy atoms' and contents of rulesets
   4: expand operators
   5: expand atoms (default)
   6: expand rulesets
You can save and load the set of propositional symbols and a LTL formula (that can be numbered from 0 to 9) using the "LTL File" feature on the lower-right. 

***Shuffle Level
For further details, see [[LaViT>http://www.ueda.info.waseda.ac.jp/lmntal/lavit/]] (in Japanese).

Expresses how randomly the execution goes on.
*LMNtal Java [#pbaad941]

   0: use an atom stack for each membrane (atoms are selected in LIFO manner)
   1: default (atoms are selected in some arbitrary manner, not random nor LIFO)
   2: select atoms and membranes randomly from a membrane
   3: select atoms, membranes and rules randomly from a membrane
The old page describing the use of LMNtal Java has been moved.
See [[How to Use LMNtal Java]] for details.

***Graphical Mode (experimental)

In graphical mode, a window is displayed that visualizes
the content of the atoms and links at the root (top-level) membrane.
Pressing space bar or clicking on 'Go ahead' button
will proceed the computation step by step.
Atoms can be dragged to arbitrary positions so that the graph
can be viewed better.
To terminate the execution, please close the window manually.

Front page List of pages Search Recent changes Backup   Help   RSS of recent changes