合金中的价值分配和枚举的使用

Question

如何在合金中分配变量？

Sig ClassA{
    variable_1: String,
    variable_2: Int
}
Sig ClassB{
    variable_1: String,
    variable_2: Int
}
pred isLess[a:ClassA,b:ClassB]{
    a.variable_2 < b.variable_2
}
assert integrityTest{
    all a:ClassA,b:ClassB| isLess[a,b]
}

现在，当我在a.variable_2中分配一些更大的值时，我想检查变量的反例，而不是b.variable_2。但是我不确定如何在合金中分配变量。我想出的唯一一件事就是关注，但它不起作用 -

pred assignValue[a:ClassA]{
    a.variable_2 = Int[4]  
}

但是，我相信它只会以4的比例检查平等，然后返回为false。它与作业无关。所以我的问题是当a.variable_2>b.variable_2

时我应该如何产生反例

我如何在合金中使用int枚举？类似-Enum MetricValue {1,2,3,4,5}分配A.Variable1。

编辑 即使我可以手动检查CA和CB的变量_2值时，我仍然很难找到反例。

。 。

 sig ClassA{ 
    variable_1: String, 
    variable_2 = Int 
 } 
 sig CA extends ClassA{}{ 
    variable_2 = 1 
 } 
 sig ClassB{ 
    variable_1: String,
    variable_2 = Int 
 } 
 sig CB extends ClassB{}{ 
    variable_2 = 4 
 }
 pred checkAllConstraint [ca: ClassA, cb: ClassB] { 
    ca.variable_2 > cb.variable_2 } 
  assert checkAll{ 
    all ca: ClassA, cb: ClassB | checkAllConstraint[ca,cb] 
  } 
  check checkAll for 15

Answer 1

您可以通过事实将字段限制为单个值。在您的情况下，签名事实很方便。

看起来像这样：

sig ClassA{
  variable_1: String,
  variable_2: Int
}{
    variable_1="hello world"
    variable_2=4
}

要将字段绑定到一个集合中的一个值，您可以使用" in"关键字而不是" ="，如下所示：

sig ClassA{
variable_1: String,
variable_2: Int
}{
    variable_1 in ("hello" + "world")
    variable_2 in (1+2+3+4)  
}

请注意，合金 是工会运营商。它不会像您期望的那样概括或加入。

编辑它是由于两个原因而行不通的：

• 您写道：variable_2 = Int而不是variable_2: Int。通过这样做，没有有效的实例包含CA或CB键入的原子，因为例如ClassA.variable2被限制为所有整数的集合，CA.variable2被限制为1
• 未定义字符串原子。那是合金的怪异部分之一。如果您想在模型中使用字符串，则需要在指定的某个地方将字符串英语列出来，例如实际上。

这是您的模型，已更正：

sig ClassA{ 
    variable_1: String, 
    variable_2 : Int 
 } 
 sig CA extends ClassA{}{ 
    variable_2 = 1 
 } 
 sig ClassB{ 
    variable_1: String,
    variable_2 : Int 
 } 
 sig CB extends ClassB{}{ 
    variable_2 = 4 
 }
 pred checkAllConstraint [ca: ClassA, cb: ClassB] { 
    ca.variable_2 > cb.variable_2 } 
  assert checkAll{ 
    all ca: ClassA, cb: ClassB | checkAllConstraint[ca,cb] 
  } 
  check checkAll for 15
fact { String in ("test"+"test2"+"test3"+"test4")}

如果您仍然有疑问，请创建一个新的。

-