Backup diff of How to Use vs current(No. 11)

The added line is THIS COLOR.
The deleted line is THIS COLOR.
#author("2019-05-27T22:51:52+09:00","default:LMNtal","LMNtal")
//[[Documentation]]

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

The LMNtalEditor IDE should be quite easy to use.  
The LaViT IDE should be quite easy to use.  

>>&ref(editor1.png,70%,around);
>>&ref(./editor1.png,50%,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 following buttons on the lower-left pane.~
Before writing your own program, it is recommended to start with examples in the 'demo' folder found in the explorer menu on the left.

To run your program, use one of the buttons on the lower-left pane:
:''SLIM'':|  Run the program (LMNtal source or intermediate code) using the SLIM runtime.  Options can be specified by clicking the '' 'Option' '' tab and choosing options under '' 'SLIM Options' ''.  Options most commonly used include:
-- ''--nd'': nondeterministic execution mode for state space construction
-- ''-t'': trace mode: In ordinary execution mode, prints execution steps.  In nondeterministic execution mode, prints individual states and state transitions of the state space
-- ''--use-builtin-rule'': enables arithmetic in the right-hand side of rules
-- ''--hl'': use hyperlinks

- ''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.
:|Details of all SLIM options can be viewed by specifying the ''--help'' option in the text box under '' 'SLIM Options' '' and running SLIM.

:''UNYO & Graphene'':|  Invoke the UNYO-UNYO visualizer (using the Java runtime) and Graphene visualizer (using SLIM).

:''StateViewer'':|  Visualize and browse the state space of the program.  States and state transitions can be browsed by clicking the state transition diagram and specifying appropriate options in the lower-right pane.~
StateViewer internally runs SLIM with the ''--nd'' (nondeterministic execution) option.  Other options given to SLIM can be specified by clicking the 'Option' tab and choosing options under '' 'StateViewer SLIM Options' ''.

:''Compile'':|  Invoke the LMNtal compiler to generate intermediate code.  Used when you wish to view the intermediate code.

**LTL Model Checking [#c35deaf4]

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%,right,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.
- Press the ''Translate'' button to compile the formula to a Buchi automaton.~
(Note: for this to work, ltl2ba must have been installed, as described in the [[Download page>http://www.ueda.info.waseda.ac.jp/lmntal/lavit/index.php?Download]].)
- Press the ''slim --ltl'' (or ''slim --ltl-all'' or ''LTL State&#86;iewer'') button to check the specified property.
- Options given to SLIM for LTL model checking can be specified by clicking the 'Option' tab and choosing options under '' 'LTL Model Check SLIM Options' ''.

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)
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.