現在の位置
backup プラグインを使用中
- List of Backups
- View the diff.
- View the diff current.
- View the source.
- Go to LaViTの使い方.
- 1 (2009-11-24 (Tue) 08:12:35)
- 2 (2009-12-30 (Wed) 15:03:45)
- 3 (2009-12-30 (Wed) 16:07:38)
- 4 (2009-12-30 (Wed) 16:07:38)
- 5 (2017-03-02 (Thu) 05:38:19)
Windowsでの使い方を紹介します。
1.起動 †
cygwin等のインストールが終了した後、run.batをダブルクリックしてLMNtalEditor?を起動して下さい。
2.ロゴ表示 †
起動が始まるとロゴが表示されます。
既に手順3~手順7のインストールが終了している場合は手順8の画面に飛びます。
3.言語の設定 †
LMNtalEditor?内で表示する言語を「英語」か「日本語」のどちらか選択して下さい。
4.cygwinへのパス設定 †
インストールしたcygwinへのパスを設定して下さい。
デフォルトでcygwinをインストールした場合は「C:\cygwin」となります。
5.SLIMへのパス設定 †
モデル検査器SLIMへのパスを設定します。
SLIMを別の方法でインストールしていない場合は「インストール」を選択して下さい。
6.SLIMインストール開始 †
SLIMのインストールを選択するとインストールが開始されます。
長いと5分~10分かかりますのでしばらくお待ちください。
7.SLIMインストール終了 †
インストールが終了したらボタンをクリックしてインストール画面を閉じてください。
正しくSLIMがインストールされれば手順3~手順7の設定は次回からスキップされます。
8.エディタ †
左の画面でLMNtalプログラムを書くことができます。
ここでは1,2,3を足し算するプログラムを書いています。
9.LMNtalプログラム実行 †
下の「LMNtal(java)」ボタンを押すと右の画面に実行結果が表示されます。
10.UNYO UNYO(3G)実行 †
「UNYO UNYO(3G)」ボタンを押すと実行の様子が図で表示されます。
UNYO UNYO内の「Go Ahead」ボタンを押すと処理を1ステップ勧めることができます。
11.SLIM実行 †
「SLIM」ボタンを押すとモデル検査器SLIMで通常実行されます。
LMNtal(java)処理系と同じ結果になっていることが分かります。
もしここで正しく実行されない場合はcygwinのインストールが正しく出来ていない、またはSLIMのインストールが正しく出来ていない可能性があります。
12.StateViewer?実行 †
「StateViewer?」ボタンを押すと実行経路が表示されます。(SLIMが実行できないとStateViewer?も実行できません。)
1,2,3の足し算の結果は1通りですが、その途中の経路は3通りあることが分かります。
13.状態表示 †
例えばその途中の状態をクリックする3,3となっていることが分かります。
他の状態もクリックすることで1,5と2,4となっていることが分かります。
14.複雑化 †
今度は足し算だけでなく、掛け算のルールも追加しました。
またそれぞれのルールにadd,mulというルール名をつけました。
このプログラムの実行経路を見てみると計算結果が5つあることが分かります。
15.ルール名の表示(1) †
StateViewer?のウィンドウ上で右クリックし、「Graph View」⇒「Show Rule」を選択すると適用ルールの表示がされます。
16.ルール名の表示(2) †
計算方法の組み合わせで計算結果が異なることが分かります。
このほかにも引き算や割り算を加えることで、例えば「4つの数字を四則演算して10にする」経路を見つけたりすることもできます。
17.ファイルの選択 †
保存されている他のLMNtalプログラムを開く場合はメニューから選択します。
18.起動 †
フォルダdemoの中には様々なLMNtalプログラムが入っています。
19.起動 †
「phi.lmn」は「食事する哲学者」の問題をLMNtalでモデル化したプログラムになっています。
20.起動 †
StateViewer?を起動して実行経路を表示すると、最終状態(赤い状態)が存在しプログラムが停止する可能性があることが分かります。
この様に停止しないつもり(仕様)で書いたプログラムでも停止する可能性(バグ)を発見することができます。