問題タブ [alloy]

独自の API を合金で使用するにはどうすればよいでしょうか?

Alloy で API を開発しましたが、どのように使用すればよいかわかりません。

よろしく

ムーディー

私は現在、Alloy Analyzer API を使用してプログラムを作成していますが、奇妙な動作が発生しています。具体的には、ファイルを開いて解析し (CompUtil.parseEverything を使用)、新しいコマンドを作成し、解析したファイルに対して TranslateAlloyToKodkod.execute_command を呼び出し、MiniSat と UNSAT コアを使用して新しく作成したコマンドを呼び出すと、正常に動作します。ただし、後で実行すると、私のプログラムは 2 番目の入力ファイルを解析し (これも CompUtil.parseEverything を使用)、別の世界を取得し、新しいコマンドを作成してから、もう一度 TranslateAlloyToKodkod.execute_command を呼び出そうとすると、次のエラーがスローされます。

ERROR: class edu.mit.csail.sdg.alloy4.ErrorFatal: The required JNI library cannot be found: java.lang.UnsatisfiedLinkError: no minisatproverx5 in java.library.path edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod.execute_command(TranslateAlloyToKodkod.java:390)

なぜこれが2回目にスローされ、最初にスローされないのか、誰にも分かりますか?

要約すると、次のようなものがあります。

Alloy 4 文法では、署名宣言 (およびその他のいくつかのもの) にprivateキーワードを含めることができます。また、仕様に次の形式の列挙宣言を含めることもできます。

言語リファレンスには、(私が知る限り)privateキーワードまたはenum構成要素の意味が記述されていません。

利用可能なドキュメントはありますか? それとも、将来の仕様のために予約されている構文として文法にありますか?

ウィキでこれら2つの概念の定義を読みましたが、違いはまだ明らかではありません。誰かが例といくつかの簡単な説明を与えることができますか？

特定のセットに対して可能な限り最大の回答をAlloyに返すことができるかどうかを確認しようとしています。したがって、この例では、回答、、、x={}およびx=Aがx=Bモデルファインダーによって生成されないようにします。

私は次の線に沿って何かを試しました：

しかし、高次の定量化が必要なため、分析が不可能であるというエラーが発生します。

これを行うための可能な（またはより簡単な）方法があるかどうか疑問に思いましたか？

下限多重度someとone三項関係のセマンティクスは把握するのが困難です。Software Abstractions (Rev. ed.) pp.79-80 によると、関係は(p.97 も参照)addr: Book -> (Name -> some Addr)と同等である必要があります。all b: Book | b.addr in Name -> some Addrしかし、後者の式は正確には何を意味するのでしょうか? ここで私の想像力は失敗します。そのため、Alloy Analyzer 4.1.0 でいくつかの実験を行いました。このモデルでの含意:

成立します (反例は見つかりません)。そのため、Book が存在する場合、各 Name はそれらの Book の少なくとも 1 つに登録されている必要があります。文書化されていないアドレスは許可されており、ブックがなければ、文書化されていない名前も突然許可されているように見えます。

次のモデルでの含意:

再び保持します。これは以前のモデルの鏡像です: Book がまったくない場合を除き、文書化されていない Addrs は禁止されています。また、名前の文書化に関する制約はありません。

両方のモデルを組み合わせて、より簡潔に定式化できます。

したがって、Book がある場合、すべてのName がリレーション addr1 に参加し、すべてのAddr が addr2 に参加する必要があります。多重度は同様に動作します。one

下限制約に関する限り、ソフトウェア抽象化とアナライザーはR: A -> (B m -> n C)のような構造について同じ話をしていないようですが、何かを見落としている可能性があります。私が発見した意味は、私が期待していたものではありませんでした。私がまだ発見していない他の奇妙な意味があるかもしれません. ネストされた下限多重度はまったく意味をなさないとますます感じています。私はこれで正しいでしょうか？

avlTree.als に合金モデルがあります。このモデルは、整数演算、特にプラス関数とマイナス関数を使用します。このモデルにはいくつかのアサーションが含まれており、Alloy Analyzer GUI を使用してこれらを適切に実行できます。

test.als に別の合金モデルがあります。このモデルは、(「open avlTree」を使用して) avlTree をインポートし、avlTree モデルの関係についていくつかのアサーションを持ちます。しかし、Alloy Analyzer GUI でこれらのアサーションを実行しようとすると、次のメッセージが表示されます。

構文エラーが発生しました:

「プラス」という名前が見つかりません。

構文エラーへのリンクは、avlTree モデルに移動します。そのため、avlTree モデルの整数演算の使用は、そのモデルを単独で実行すると正常に機能するように見えますが、別のモデルにインポートしようとすると壊れます。これに対する修正はありますか？

Alloy 4.2を実行しています。

Alloy 4.2 のリリース ノートによると、整数に関連するセマンティクスの変更があります。これらの変更は、Alloy book の演習 A.1.6 に影響を与えるようです。

この演習では、次のコードがベースとして提供されます (問題を示すために最後に「Int」を追加しました)。「show」述語を実行すると、ビジュアライザーはインスタンスを表示しますが、このインスタンスには、整数に加えて、さらに 2 つのアトム「Univ0」と「Univ1」が含まれています。

この 2 つのアトム「Univ0」と「Univ1」の意味は何ですか? なぜ彼らはそこにいるのですか？これらは、Alloy 4.1.10 で実行された同じコードでは表示されません。

私には2つのクラスがAあり、それらBのクラスの追加データとの関係がありRます。

したがって、AとBはを介して相互に関連付けられていRます。

ここで、Boolは次のように定義されます。

今、私はAこのように拡張します：

これには、これとそれBの間に関係があり、データがタイプであるすべてのインスタンスが含まれます。ABTrue

次の論理ステートメントをAlloyファクトとして表現したいと思います。

_{（ソース：dropproxy.com）}

ここでTrue == 1、とは、とのすべてのインスタンスをそれぞれセットし、含むとFalse != 1仮定Aします。RAR

私がこれまでに試したことは、fun trueR(a : A)すべてRの'を返す必要があるR.a = a and r.data = Trueaとfact allbIsRTrue、それぞれに対して。によって返される'のA allb合計である必要があることを示すaを定義することです。R.btrueR

ただし、ここで行き詰まり、参照内のセットを合計するための適切な構成が見つからず、試行するとsum構文エラーが発生します。

正式な制約をAlloyファクトとして指定するにはどうすればよいですか？

私は合金にまったく慣れておらず、現在mitでチュートリアルを読んでいます。私は物事の論理に少し行き詰まりました。私がやろうとしている非常に基本的なことは以下のとおりです。

• 人はせいぜい 1 つのタスクしか実行できません
• タスクは最大 1 人で実行できます
• 人はできることしかできない

以下を実行すると、全員が同じスキル (すべてのスキル) を持ち、すべてのタスクに同じスキルが必要です (すべて)。少なくとも 1 つのタスクが割り当てられますが、同じタスクが割り当てられることもあります。

前もって感謝します