Backup of How to Use (No. 20)

[ Front page | List of pages | Search | Recent changes | Backup | Help ]

• List of Backups
• View the diff.
• View the diff current.
• View the source.
• Go to How to Use.
  • 1 (2006-01-08 (Sun) 07:52:55)
  • 2 (2006-01-19 (Thu) 13:59:56)
  • 3 (2006-03-24 (Fri) 14:50:48)
  • 4 (2006-06-13 (Tue) 15:59:26)
  • 5 (2006-11-30 (Thu) 17:16:12)
  • 6 (2006-12-01 (Fri) 16:29:26)
  • 7 (2006-12-18 (Mon) 16:59:22)
  • 8 (2009-12-07 (Mon) 06:53:40)
  • 9 (2009-12-07 (Mon) 10:38:20)
  • 10 (2010-02-11 (Thu) 15:45:09)
  • 11 (2010-02-11 (Thu) 15:45:09)
  • 12 (2010-05-28 (Fri) 14:05:18)
  • 13 (2011-06-12 (Sun) 03:44:34)
  • 14 (2012-05-10 (Thu) 06:30:26)
  • 15 (2014-06-01 (Sun) 14:38:04)
  • 16 (2017-03-02 (Thu) 03:32:49)
  • 17 (2017-03-02 (Thu) 05:03:59)
  • 18 (2019-04-29 (Mon) 07:59:42)
  • 19 (2019-05-26 (Sun) 13:19:39)
  • 20 (2019-05-27 (Mon) 01:33:56)

---

LaViT: LMNtal Visual Tools †

The LaViT IDE should be quite easy to use.

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.

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

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.

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

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

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.

   

Modified by uedalab LMNtal group

PukiWiki 1.5.1 © 2001-2016 PukiWiki Development Team
Powered by PHP 7.4.33

HTML convert time to 0.008 sec.