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:
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:
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 LaViT for details (Japanese only).
The old page describing the use of LMNtal Java has been moved. See How to Use LMNtal Java for details.