如何在合金中使用字符串？

Question

如何在合金中使用字符串？

在合金中支持字符串的哪种函数或运算符？

我在这里搜索问题，发现字符串是合金中的一个关键字。但我找不到任何关于如何在合金中使用字符串的参考资料。你能给我一个吗？如果不是，可以简单介绍一下合金中的弦吗？

Answer 1

实际上，您可以在合金中使用字符串，但只能将其用作指定常量值的文字(即，不支持字符串操作，并且合金不实现字符串解算器)。也就是说，字符串的主要用途是将常量字符串字面值分配给某些字段，唯一的目的是使生成的实例在可视化时更具可读性。下面是一个简单的例子

sig Person {
  name: String,
  email: String
}
one sig P1 extends Person {} {
  name = "Joe"
  email = "joe@email.com"
}
run {
  some p: Person | p.name != "Joe"
}