問題タブ [alloy]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
alloy - 合金 - 孤立したインスタンス
私は単純な Alloy コードを書いていますが、AT MOST 1 つの A が pD に関連付けられているとどのように言うことができるか理解できません (したがって、AT MOST は 1 または 0 になります)。だから私は以下のコードを書きましたが、アサーションはDのないP1のインスタンスで反例を提示しません.私が反例を見ることができるpDのAT MOST 1つのインスタンスを持つという点で私の事実を定義する方法を教えてください. p はその D に接続されていません。
alloy - 合金 4 Int スコープ
昨年、私は合金を使用し、次の回答で実際に示唆されているように、「5 Int」などの Int ビット幅書き込みのスコープを設定できました: run command scope in Alloy
ただし、今年も Alloy 4.1.1 をダウンロードしました。
今手に入れる
変更点 ビット幅はどのように設定すればよいですか?
alloy - モジュロ演算子を合金でモデル化するにはどうすればよいですか?
モジュロ演算子を合金でモデル化する方法は?
合金を使って、4 の倍数は 2 で割り切れることを証明したい....
これが私のコードです..
これはコンパイルされません
alloy - 複数の一致があるため、この名前はあいまいです:
同じ名前の関係を持つ 2 つの署名を持つ合金モデルがあります。
これらのリレーションにアクセスしようとすると、結合がスローされ、ソルバーから次のメッセージが表示されます。
belongToポートのリレーションではなく、コンポーネントのリレーションにアクセスすることを明示的に指定する方法はありますか?
そしてmはモデルですか？
ありがとう。
alloy - モデルに 2 つのインスタンスがある場合に署名のフィールドに制限を追加する方法
私は、人々のグループを説明する次の Alloy モデルを持っています。問題を単純化します。これがサンプルコードスニップです。
これで、グループに 2 人が参加しました。次に、グループ内の人々にいくつかの制限を追加したいと思います。たとえば、グループ内の 2 人には、常に 1 人のチーム リーダーと 1 人のチーム メンバーが必要です。これを行うには、次の事実を使用します。
今、私は前進を妨げる問題に遭遇しました。私が探している望ましいモデルは、グループの国が「US」の場合、チームリーダーの役職は「US_TL」で、チームメンバーの役職は「US_TM」です。国が「UK」の場合、チームリーダーの役職は「UK_TL」、チームメンバーの役職は「UK_TM」などです。
次のようなものを追加しようとしました：
しかし、予測には明らかに何か問題があり、モデルは正しい解を生成できません。私のモデルの問題を特定するのを手伝ってくれませんか?