#author("2019-04-29T16:59:42+09:00","default:LMNtal","LMNtal") //[[Documentation]] *LaViT: LMNtal Visual Tools [#ed6fa884] The LaViT IDE should be quite easy to use. >>&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. :''SLIM'':| Run the program (LMNtal source or intermediate code) using the SLIM runtime. :''UNYO & Graphene'':| Invoke the UNYO-UNYO visualizer (using the Java runtime) and Graphene :''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(./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 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>http://www.ueda.info.waseda.ac.jp/lmntal/lavit/]] (in Japanese). *LMNtal Java [#pbaad941] The old page describing the use of LMNtal Java has been moved. See [[How to Use LMNtal Java]] for details.