- The added line is THIS COLOR.
- The deleted line is THIS COLOR.
//[[Documentation]]
*LMNtalEditor
*LaViT: LMNtal Visual Tools
The LMNtalEditor IDE should be quite easy to use.
The LaViT IDE should be quite easy to use.
>>&ref(editor1.png,70%,around);
The upper-left pane is for
editing programs, while the upper-right pane shows system output.
To run your program, use one of the buttons on the lower-left pane:
- ''LMNtal(Java)'' to run the program using the Java runtime,
- ''UNYO(2G)'' to invoke the 2nd-generation UNYO-UNYO visualizer,
- ''UNYO(3G)'' to invoke the 3rd-generation UNYO-UNYO visualizer,
- ''SLIM'' to run the program using the C runtime, and
- ''StateViewer'' to visualize the state-space of the program.
To model-check your program, click the ''LTL model check'' tab of the upper-right pane,
>>&ref(editor2.png,70%,around);
and proceed as follows:
- 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.
Examples of propositional symbols and LTL formulas can be found by opening the programs under the ''demo/ltl'' directory of the distribution.
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.
See [[LMNtalEditor>http://www.ueda.info.waseda.ac.jp/lmntal/lmntaleditor/]] for details.(Japanese only)
See [[LaViT>http://www.ueda.info.waseda.ac.jp/lmntal/lavit/]] for details (Japanese only).
*LMNtal Java
The old page describing the use of LMNtal Java has been moved.
See [[How to Use LMNtal Java]] for details.