如何在合金中分配变量?
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
您可以通过事实将字段限制为单个值。在您的情况下,签名事实很方便。
看起来像这样:
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")}
如果您仍然有疑问,请创建一个新的。
-