問題タブ [alloy]

Alloy API を使用すると、その特定の Alloy モジュールを操作するために必要なすべてのものを含む CompModule を Alloy ファイルから取得できます。

これは、 CompUtil.parseEverything_fromFile(...) を使用して簡単に実現できます。

私の質問は次のとおりです。CompModule から合金言語に移行する方法はありますか? または、署名のリストと事実から合金モデルに移動します。（力ずくでできると思いますが、ユーティリティが存在するかどうかを知りたいです。）

ご協力ありがとうございました ！

乾杯

Event-Condition-Action ルールを Alloy に変換する方法 ( http://alloy.mit.edu/alloy/ )

Linked ListからElementを削除してStackにプッシュしたいのですが、こんなコードを書いてみました。要素をスタックにプッシュするコードを書いていましたが、エラーが発生しています。そのコードはコメントにあります。

//双方向リンクリスト

//スタック

要素をスタックに挿入するために、このコード(コメント内)を試しました。しかし、これによりインスタンスが見つかりませんというエラーが発生します。

値を表すコインのリストを作成しようとしています.9 rsにシーケンス 5->2->2 が含まれるとします。8rs は 5rs->2rs->1rs になります。7rs は 5->2 になります。硬貨は 10Rs、5rs、2rs、1rs のいずれかです。このコードでは、tenr は値が 10 のコインのリストを意味し、tenrs は 10 rs のコインを意味します。どうすればそのようなリストを作成できますか? 私は試してきましたが、すべて無駄です。また、実行して表示をクリックすると、単一のコイン ノードに割り当てられた複数のコインが表示されます。どんな助けでも大歓迎です。実際に自販機で使ってみました。私はあなたのコードをチェックし、現在それを実装しようとしています。自動販売機用のコードも提供しています。

自動販売機

正常に動作する自動販売機を作成しました。取引が完了したら、商品の数量から 1 を引きたいです。理解のためにコードにコメントを付けました。Pred Chocolate のコメントの一部は無視してください。どういうわけか私は減算しようとしていますが、それはうまくいきません。何が問題なのかわかりません。どんな助けでも大歓迎です。

私は、次のような問題文を経験しました: 外科医は 3 人の患者を手術しなければなりませんが、手袋は 2 組しか持っていません。交差汚染があってはなりません。外科医はどの患者の血液とも接触してはならず、患者は別の患者の血液と接触してはなりません。外科医が作業するには両手が必要です。彼女はどうやってそれをしますか？この問題を Alloy で表現し、アナライザーを使用して解決策を見つけます。

私はすでにいくつかの署名を宣言しましたが、require の事実と述語の宣言に固執しました。誰でも私を助けることができますか？私のコードは次のとおりです。

\ よろしくお願いします

Alloy 4 の述語と関数の違いを理解するのに苦労しています。Software Abstractions のセクション 4.5.2 を読みましたが、まだ明確ではありません。誰かが私を理解するのを手伝ってもらえますか?