ツールの準備 - Alloy Analyzer で形式仕様記述

ここでは、Alloy のセットアップと簡単な使い方について説明します。

1. 対応 OS

---

Java が動く OS

2. ツールのダウンロード

---

Alloy は公式ページ ( http://alloy.mit.edu/community/ ) からダウンロードすることができます。
上のメニューから Software を選択するとダウンロードのページが表示されます。

3. ツールのインストール

---

あらかじめ Java をインストールしてください。
必要な Java のバージョンは、公式ページで確認してください。

Java がインストールされていれば、ダウンロードしたファイルをそのまま実行することができます。
Alloy を起動すると、以下のような画面が表示されます。

3. 画面の各部名称

---

3.1. メイン画面

• 1
  • ここに様々な条件を Alloy 言語で記述します。
• 2
  • ここに探索結果やエラーなどが表示されます。
• 3
  • 指定した条件の例 (インスタンス) を探します。
  • 指定したい条件は、メニューの [Execute] から選択することができます。
• 4
  • 3 の Execute でインスタンスが見つかったら、以下の [インスタンス画面] で、見つかったインスタンスが表示されます。

3.2. インスタンス画面

• 1
  • 見つかったインスタンスが図で表示されます。
• 2
  • インスタンスの表示形式を図以外に切り替えることができます。
• 3
  • 以下の [テーマ画面] で、図の表示 (色や形) をカスタマイズすることができます。
  • 詳しくは説明しませんが、細かくカスタマイズできます。色々触ってみてください。
• 4
  • 図の表示を自動で調整してくれます。
• 5
  • 式を書いてインスタンスを評価することができます。
• 6
  • 別のインスタンスを探すことができます。
• 7
  • 指定した型の要素ごとに、インスタンスを表示することができます。
  • 詳しくは別のページで説明します。

4. 初期設定

---

メイン画面のメニューの [Options] - [Font] で日本語が使えるフォントを選択しておいたほうがよいでしょう。
それ以外は初期設定のままでかまわないと思います。

---