Backup diff of How to Use(No. 17)

The added line is THIS COLOR.
The deleted line is THIS COLOR.
#author("2017-03-02T14:03:59+09:00","default:LMNtal","LMNtal")
//[[Documentation]]

*LaViT: LMNtal Visual Tools
*LaViT: LMNtal Visual Tools [#ed6fa884]

The LaViT IDE should be quite easy to use.  

>>&ref(editor1.png,60%,around);
>>&ref(./editor1.png,60%,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.
:''State&#86;iewer'':|  Visualize the state-space of the program.  State&#86;iewer 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(editor2.png,70%,around);
>>&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 State&#86;iewer'') 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>http://www.ueda.info.waseda.ac.jp/lmntal/lavit/]] (in Japanese).

*LMNtal Java
*LMNtal Java [#pbaad941]

The old page describing the use of LMNtal Java has been moved.
See [[How to Use LMNtal Java]] for details.
Backup diff of How to Use (No. 17)
