問題タブ [alloy]

私はしばらくの間、形式的な方法に興味を持っていました。私は、私が取り組んできたいくつかのプロジェクトのいくつかの非常に具体的なサブエリアについて、形式的な方法を使用して推論しました。正式な方法でドメイン全体を指定するどころか、他のチーム メンバーに同じことを試みるよう説得することはできませんでした。

私が特に興味深いと思った 1 つの方法は、Alloyです。概念的にも表記的にも実際のプログラミング言語に非常に近いため、プロジェクト全体の基盤としてより「スケーリング」できると思います。さらに、ツールは非常に堅牢であるため、モデル検証の利点をすぐに利用できます。

皆さんのプロジェクトで Alloy を使用した実際の経験についてお聞きしたいと思います。より良いドメイン モデルの設計に役立ったと思いますか? 検証中にドメイン モデルにエラーが見つかりましたか? また利用しますか？

私はこの正式な方法の宿題の問題で立ち往生しており、何が正しくないのかわかりません。

次のように定義されている Item と ToDo の 2 つの署名があります。

指定された日付とカテゴリの項目を ToDo のリスト セットに挿入する関数を定義する必要があります。秘訣は、リスト セットがアイテムの期日順に並べられることになっていることです。ステップと日付の両方に順序があります。

私の質問は次のとおりです。ToDo.list 内のアイテムのセットを特定の日付で取得するにはどうすればよいですか? 私は機能を持っています：

そして、次のコード（およびそのバリエーション）を使用してアイテムのセットを取得しようとしました：

t.due.st が一連の日付を残すため、これは機能しません。その理由は理解できます。しかし、その時点からの他の試みは私をそこに連れて行きません。括弧を使用して、t に到達する前に「due.st」と「d」の間の結合を評価しようとしましたが、それは機能せず、角括弧を使用して順序を変更しようとしましたが、動作しません。ここで何か間違ったことをしていることは知っていますが、何が原因なのかわかりません。

関係を考えてみましょうupgrades：

upgrades私はそれが循環できないことを確認する必要があります。どうすればAlloyでそれを行うことができますか？

したがって、Alloy には次のコードがあります。

しかし、これはキューを含むインスタンスを生成しません。なぜだろうか。ノードを持つインスタンスのみが表示されます。同等の述語を試しました

しかし、出力は同じです。

何か不足していますか？

自動化されたテストケース生成の研究プロジェクトに Alloy4 を使用したいと考えています。誰でもこれで私を助けてくれますか？Alloy で生成されたインスタンスを使用して Java インスタンス オブジェクトを作成するために Alloy を使用するにはどうすればよいですか?

これは宿題で、私はそれで多くの問題を抱えています。ライブラリのモデリングにAlloyを使用しています。オブジェクトの定義は次のとおりです。

次に、すべての本が棚にあるか、常連客によって取り出されるという事実を持っている必要があります。ただし、両方の場所に配置することはできません。

私はこれを試しました...

しかし、それは機能していません...本は常に棚にあります。「すべての本について、貸し出されていない場合は棚にあります。そうでない場合は売り切れです」と言いたい。

訂正、例、およびヒントは大歓迎です。

私はALLOYにコードを持っており、レストランの予約システムを実行しようとしています。このシグニチャとそれらの間の関係があります。

私は朝食のためにそれが両方ではなく予約または無料であることができて、そして昼食と夕食で同じことを何か考えがあるという事実を置きたいですか？

Alloy を使用して代数群の構造をモデル化しようとしています。

グループは、一連の要素と特定のプロパティを持つバイナリ関係を持っているだけなので、合金に適していると思いました。

これが私が始めたものです

次の制約をcafe.alsに追加します。

• カフェから他のカフェへは車で行くことができます（直接のルートはないかもしれませんが）。
• カフェ間の散歩道は双方向です。
• すべてのカフェには、他のすべてのカフェから1つまたは2つのステップで直接アクセスできます。
• バスは、単一の非分岐ルートですべてのカフェを訪れます。（注：このためのバス関係の宣言を少し変更することをお勧めします。）

私はAlloyを使ったことがなく、教授はほとんど触れていません。私は本当に迷っています、誰かが何が起こっているのかを説明したり、問題のいずれかで私を助けてくれますか？