合金：如何理解Alloy演示中的反例？

Question

出于好奇，我写了一个奇怪的Alloy演示，关于“断言”。

假设有一个“程序”，“程序”有2个“变量”，并且每个“变量”都有“数据”集中的“值”。

然后，我还设置了一个“事实”，即“品种”的所有“值”均为“ data1”。

最后，我为所有“程序”设置了一个“断言”，“程序”中“变量”的所有“值”均为“ data1”。

我认为“断言”满足“事实”，但是当我检查“断言”时，它给出了反例，对此我不明白，为什么会有反例？

代码显示如下：

enum Data{data1,data2}

sig Program{
    Var1:Variable,
    Var2:Variable
}
sig Variable{
    Value:Data
}

fact{
   all v:Variable{
       v.Value=data1
   }
}

assert test{
    all p:Program{
        all v:(Program->Variable){
            p.v.Value=data1
        }
    }
}

反例如下：

Answer 1

我对您的示例有些困惑，因为似乎未使用var1和var2字段。但是，您得到一个反例的原因可能是因为v可以为空，在这种情况下p.v.Value的值为空关系，而data1的值为单身，因此它们不相等。

Answer 2

我的问题中有两个错误，我修改了代码，现在是正确的。

enum Data{data1,data2}

sig Program{
    Var1:Variable,
    Var2:Variable
}
sig Variable{
    Value:Data
}

fact{
    all p:Program{
        //In theory, there should be "all v:(Program->Variable)", but Alloy does not support HOL.
        //all v:(Program->Variable){
            p.Var1.Value=data1
            p.Var2.Value=data1
        // }
    }
}

assert test{
    all p:Program{
         p.Var1.Value=data1
         p.Var2.Value=data2
        // And here is another mistake, Var1 and Var2 is only the subset of "all v:(Program->Variable)"
        // all v:(Program->Variable){
            // p.v.Value=data1
        // }
    }
}

check test for 10 but 1 Program