LaViT: LMNtal Visual Tools

The LaViT IDE should be quite easy to use.

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:

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.

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

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.

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.


Attach file: fileeditor1.png 1049 download [Information] filesv_dtp.png 58 download [Information] fileeditor2.png 1007 download [Information]

Reload   New Edit Freeze Diff Upload Copy Rename   Front page List of pages Search Recent changes Backup   Help   RSS of recent changes
Last-modified: 2017-03-02 (Thu) 05:03:59 (290d)