alloy - 在 Alloy 中执行状态时引用了错误的 sig 对象

Question

我是合金新手。我正在尝试使用合金来形式化一个系统。在这里，我想根据事件执行某些操作。为此，我有一个要使用枚举事件跟踪的事件列表。我正在使用合金的订购功能浏览所有状态。在每种状态下，我都采用混合对象并运行操作。

我目前面临的问题是 - 在我的系统中，我有两个 sig 对象 - ClassA 和 ClassB。执行合金代码后，我正在生成流程图。不幸的是，我注意到我的 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

Answer 1

你有

sig Mixture{
classA: Base,
classB: Base
}

在您的图表中，关系被命名为classA和classB。由于 each 可以指向任意Base的 ，因此没有什么可以停止classA指向一个ClassB实例。你可能想要类似的东西

sig Mixture {
    , classA: ClassA
    , classB: ClassB
}