1.LMNtal実行フロントエンド †
エディタは編集中のLMNtalプログラムを解析し“int” などの予約語やコメントを色付けを行います。
また大量の出力が右画面に表示され可た場合でもそのままテキスト検索を行うことができます。
ボタンを押すとすぐにLMNtal 処理系で実行され、出力は機能部に表示されます。
どのような処理系の出力であってもこの1つの出力表示インターフェースにまとめて分かり易く表示されるので、
出力を確認しながらスムーズにプログラミングを行うことができます。
2.検証支援 †
命題記号定義の記述とNever Claimの記述を同時に行うことができます。
Never Claimを記述するためにはLTLをNever Claimに変換するLTL2BAが必要となりますが、
画面上からLTL2BAを呼び出すことができますのでNever Claimの記述を即座に行うことが可能です。
3.State Viewer †
State ViewerはLMNtalプログラムの実行経路を網羅的に探索した結果を解析し可視化を行います。
State Viewerでは仕様記述を必要としないため特別なモデル検査の準備が無くてもすぐに実行することができます。
4.State Profiler †
大きいモデルの探索が進行しているかわからない場合は、State Profilerで探索速度を評価することができます。
モデル検査器が探索した状態を逐一グラフにプロットを行います。
State Viewerのグラフ最適化機能 †
State Viewerには様々なオプションが備わっており、グラフをより見易くする機能が多数あります。
その中でも代表的な機能を紹介します。
Adjust Reset †
遷移を考慮したアルゴリズムによる配置を行います。
Set Dummy †
ダミーノードで折れ線を表現し、グラフの重なりを削減します。
Dynamic Modeling †
力学的アルゴリズムによってバランスのとれた配置を行います。
Adjacent Exchange †
Adjacent-Exchangeアルゴリズムによってグラフの交差数を減らします。
Attached files
- Attach file:
fan03.jpg 358 download
[Information]
fan04.gif 723 download
[Information]
sv03.jpg 709 download
[Information]
fan02.gif 667 download
[Information]
fan03.gif 645 download
[Information]
fan01.jpg 341 download
[Information]
sv04.jpg 653 download
[Information]
fan01.gif 701 download
[Information]
fan02.jpg 375 download
[Information]
sv01.jpg 727 download
[Information]
sv02.jpg 667 download
[Information]
