alloy - Alloy で状態を実行中に間違った sig オブジェクトが参照される

Question

私は合金が初めてです。Alloy を使用してシステムを形式化しようとしています。ここでは、イベントに基づいて特定の操作を実行したいと考えています。このために、enum Event を使用して追跡したいイベントのリストがあります。そしてAlloyのオーダリング機能を使って全ての状態を調べています。それぞれの状態で、混合オブジェクトを取得して操作を実行しています。

私が現在直面している問題は - 私のシステムには、ClassA と ClassB の 2 つの sig オブジェクトがあります。合金コードを実行した後、フロー図を生成しています。残念ながら、ClassB が Mixture オブジェクトの ClassA を参照していることに気付きました。図を添付します

ここにも完全なコードを添付しています。問題のデバッグを手伝ってくれる人はいますか? さまざまな述語とロジックを課そうとしましたが、どれも機能しませんでした。

open util/ordering[State]


abstract sig Base{
 name: String,
 value : Int
}{
value >= 0
}

sig ClassA extends Base{

}{

name = "Class A"
}

sig ClassB extends Base{


}{
name = "Class B"
}

enum Event {EVENT1, EVENT2}


sig State{

mixture: Mixture
}

sig Mixture{
classA: Base,
classB: Base
} {
    classA != classB
}


fact {
    all s: State, s': s.next{
        s.mixture ! in  s'.*next.mixture
        operation [s.mixture]       

    }
}


pred operation [mixture: Mixture]{
    all ev: Event| ev = EVENT1 => {
        mixture.classA.name = "Class A" => {
                mixture.classA.value = 1    
        }
    }

}

run random {} for 3