Backup of How to Use(No. 13)

LaViT: LMNtal Visual Tools

The LaViT IDE should be quite easy to use.

&ref(): The style ref(filename,pagename) is ambiguous and become obsolete. Please try ref(pagename/filename);

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):: Run the program using the Java runtime.
UNYO(2G):: Invoke the 2nd-generation UNYO-UNYO visualizer.
UNYO(3G):: Invoke the 3rd-generation UNYO-UNYO visualizer. (UNYO-UNYO internally uses the Java runtime.)
SLIM:: Run the program using the C runtime.
StateViewer:: Visualize the state-space of the program. StateViewer internally runs SLIM with the --nd (nondeterministic execution) option.

To model-check your program, click the LTL model check tab of the upper-right pane,

&ref(): The style ref(filename,pagename) is ambiguous and become obsolete. Please try ref(pagename/filename);

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.

For further details, see LaViT (in Japanese).

↑

LMNtal Java

The old page describing the use of LMNtal Java has been moved. See How to Use LMNtal Java for details.

Backup of How to Use (No. 13)

LaViT: LMNtal Visual Tools

LMNtal Java