*LaViT: LMNtal Visual Tools [#ed6fa884]

The LMNtal system first compiles LMNtal source files into
intermediate code.  It then translates the intermediate code
into Java programs,
which is then compiled into Java bytecode and packaged into an
.jar (Java archive) file.  How to run the .jar file will be
described below.
The LaViT IDE should be quite easy to use.  

When invoked with the --interpret option, the second and subsequent
steps of compilation is skipped and the intermediate code will be
executed interpretively.

When invoked without specifying a source file, the LMNtal system
enters the REPL (read-eval-print loop) mode, in which case expressions
will be executed interpretively.
The upper-left pane is for
editing programs, while the upper-right pane shows system output.

The system comes with library APIs.  By default, the compiled version
of the APIs will be used (this works also when invoked
with the --interpret option).  In this case the .jar files of the library APIs
should be created beforehand and should be added to the classpath.
By using shellscripts in the bin directory, you can invoke LMNtal
after adding .jar files located in the lib directory.
Alternatively, you can use the source code of the APIs by specifying
the --use-source-library option, in which case .lmn files located
under the lib/src directory will be read and compiled on demand.
To run your program, use one of the buttons on the lower-left pane:

LMNtal programs transtaled into Java bytecode will run an order of
magnitude faster than the interpreted intermediate code.
:''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.

*How to Use
To model-check your program, click the ''LTL model check'' tab of the upper-right pane,

(Note to Cygwin users: The command names (lmnc, lmnr, lmntal) shown
below works on UNIX/Linux
and Windows.  On Cygwin, please use lmnc_cyg, lmnr_cyg, and lmntal_cyg

**Using shellscripts (Windows NT/2000/XP, Cygwin, UNIX/Linux)
and proceed as follows:

***Preparation (necessary only when using your own libraries)
- 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.

Prepare compiled libraries (how to make lirary .jar files will be
explained below) and put them in the lib directory.
Examples of propositional symbols and LTL formulas can be found by opening the programs under the ''demo/ltl'' directory of the distribution.

 $lmnc foo.lmn
--Compiler options can be specified before or after the file name.
 $ lmnc -O2 fool.lmn
 $ lmnc foo.lmn -d
 $ lmnr foo.jar
--Runtime options should be specified after the .jar file.
 (ok) $ lmnr foo.jar -g
 (no) $ lmnr -t foo.jar
***Interactive execution (Read-Eval-Print loop)
 $ lmntal
--(lmntal is an alias of lmnc.)
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. 

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.
For those who prefer starting execuition with one newline, the
--immediate option is provided.
For further details, see [[LaViT>http://www.ueda.info.waseda.ac.jp/lmntal/lavit/]] (in Japanese).

The following list shows some interactive-mode commands:
*LMNtal Java [#pbaad941]

 :q                - quit
 :h                - see help
 :trace | :notrace - set trace mode
 :verbose [0-9]    - set verbose level
 :shuffle [0-3]    - set shuffle level
The old page describing the use of LMNtal Java has been moved.
See [[How to Use LMNtal Java]] for details.

Here is an example of an interactive mode session:

 % lmntal [PRESS ENTER]
         LMNtal version 0.70.20060105
 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

**Doing manually (Windows 9x etc.)

++When standard or user-defined library APIs are used, add their
 .jar files into the classpath.
++Compile the source file:
 $ java runtime.FrontEnd foo.lmn
++foo.jar will be created.
++Add foo.jar into the classpath.
++When standard or user-defined library APIs are used, add their
 .jar files into the classpath.
++Invoke the Main class (in foo.jar) as:
 java Main

*Command-line options

 -t            - trace mode
 -v[0-9]       - set verbosity level ( -v = -v5 )
 -s[0-3]       - set shuffle level ( -s = -s3 )
 -g            - graphical mode (experimental)

There are many more options that can be specified.
To see what options are available, do:
  lmntal --help

***Verbosity Level

Expresses how verbosely an LMNtal process is displayed.

   0: silence
   2: default
   3: print `proxy atoms' and contents of rulesets
   4: expand operators
   5: expand atoms (default)
   6: expand rulesets

***Shuffle Level

Expresses how randomly the execution goes on.

   0: (default) use an atom stack for each membrane (atoms are selected in LIFO manner)
   1: 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

***Graphical Mode (experimental)

In the 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.

*How to create libraries
(to be supplied soon)

*Classes built by the translator
(to be supplied soon)

*System rulesets
(to be supplied soon)

(to be supplied soon)

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