Alloy 中的赋值和枚举的使用

Question

如何在Alloy中分配变量？

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 更大的值时检查变量的反例。但我不确定如何在 Alloy 中分配变量。我唯一想到的就是跟随，但它不起作用-

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

但是，我相信它只会检查 4 和 return 是否相等。它与任务无关。所以我的问题是 a.variable_2>b.variable_2

时我应该如何产生反例

以及如何在 alloy 中使用 Int 枚举？喜欢- Enum MetricValue {1,2,3,4,5} 分配 a.variable 1.

编辑我仍然无法找到反例，即使当我切换 ca 和 cb 的 variable_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)  
}

请注意，在 Alloy 中，+ 是 UNION 运算符。它不会像您预期的那样求和或连接。

编辑它不起作用有两个原因：

您写道：variable_2 = Int 而不是 variable_2: Int。通过这样做，没有有效的实例包含由 CA 或 CB 类型化的原子，因为例如ClassA.variable2 被限制为所有整数的集合，CA.variable2 被限制为 1
没有定义字符串原子。这是 Alloy 的奇怪部分之一。如果你想在你的模型中使用字符串，你需要在某处指定字符串文字，例如事实上。

这是您的模型，已更正：

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")}

如果您还有问题，请创建一个新问题。

-

Alloy 中的赋值和枚举的使用

Value assignment in Alloy and use of Enum

enums

alloy

first-order-logic

declarative-programming