How to Use
[
Front page
|
List of pages
|
Search
|
Recent changes
|
Backup
|
Help
]
Start:
//[[Documentation]]
*LaViT: LMNtal Visual Tools [#ed6fa884]
The LaViT IDE should be quite easy to use.
>>&ref(./editor1.png,50%,around);
The upper-left pane is for
editing programs, while the upper-right pane shows system...
To run your program, use one of the following buttons on ...
Before writing your own program, it is recommended to sta...
:''SLIM'':| Run the program (LMNtal source or intermedia...
-- ''--nd'': nondeterministic execution mode for state sp...
-- ''-t'': trace mode: In ordinary execution mode, prints...
-- ''--use-builtin-rule'': enables arithmetic in the righ...
-- ''--hl'': use hyperlinks
:|Details of all SLIM options can be viewed by specifying...
:''UNYO & Graphene'':| Invoke the UNYO-UNYO visualizer (...
:''StateViewer'':| Visualize and browse the state space ...
StateViewer internally runs SLIM with the ''--nd'' (nonde...
:''Compile'':| Invoke the LMNtal compiler to generate in...
**LTL Model Checking [#c35deaf4]
To model-check your program, click the ''LTL model check'...
>>&ref(./editor2.png,70%,right,around);
and proceed as follows:
- Define propositional symbols that represent properties ...
- Specify an LTL formula representing the property you wi...
- Press the ''Translate'' button to compile the formula t...
(Note: for this to work, ltl2ba must have been installed,...
- Press the ''slim --ltl'' (or ''slim --ltl-all'' or ''LT...
- Options given to SLIM for LTL model checking can be spe...
Examples of propositional symbols and LTL formulas can be...
You can save and load the set of propositional symbols an...
For further details, see [[LaViT>http://www.ueda.info.was...
*LMNtal Java [#pbaad941]
The old page describing the use of LMNtal Java has been m...
See [[How to Use LMNtal Java]] for details.
End:
//[[Documentation]]
*LaViT: LMNtal Visual Tools [#ed6fa884]
The LaViT IDE should be quite easy to use.
>>&ref(./editor1.png,50%,around);
The upper-left pane is for
editing programs, while the upper-right pane shows system...
To run your program, use one of the following buttons on ...
Before writing your own program, it is recommended to sta...
:''SLIM'':| Run the program (LMNtal source or intermedia...
-- ''--nd'': nondeterministic execution mode for state sp...
-- ''-t'': trace mode: In ordinary execution mode, prints...
-- ''--use-builtin-rule'': enables arithmetic in the righ...
-- ''--hl'': use hyperlinks
:|Details of all SLIM options can be viewed by specifying...
:''UNYO & Graphene'':| Invoke the UNYO-UNYO visualizer (...
:''StateViewer'':| Visualize and browse the state space ...
StateViewer internally runs SLIM with the ''--nd'' (nonde...
:''Compile'':| Invoke the LMNtal compiler to generate in...
**LTL Model Checking [#c35deaf4]
To model-check your program, click the ''LTL model check'...
>>&ref(./editor2.png,70%,right,around);
and proceed as follows:
- Define propositional symbols that represent properties ...
- Specify an LTL formula representing the property you wi...
- Press the ''Translate'' button to compile the formula t...
(Note: for this to work, ltl2ba must have been installed,...
- Press the ''slim --ltl'' (or ''slim --ltl-all'' or ''LT...
- Options given to SLIM for LTL model checking can be spe...
Examples of propositional symbols and LTL formulas can be...
You can save and load the set of propositional symbols an...
For further details, see [[LaViT>http://www.ueda.info.was...
*LMNtal Java [#pbaad941]
The old page describing the use of LMNtal Java has been m...
See [[How to Use LMNtal Java]] for details.
Page: