How to use String in Alloy?

Question

How to use String in Alloy?

What kind of function or operators for String are supported in Alloy?

I searched questions here and find String is a keyword in Alloy. But I cannot find any reference about how to use String in Alloy. Could you give one? If not, is possible to give a brief about String in Alloy?

Answer 1

You can actually use strings in Alloy, but only as literals to specify constant values (i.e., no string operations are supported, and Alloy does not implement a string solver). That said, the main use of strings is Alloy is to assign constant string literals to some fields for the sole purpose of making the generated instances more readable when visualized. Here is a simple example

sig Person {
  name: String,
  email: String
}
one sig P1 extends Person {} {
  name = "Joe"
  email = "[email protected]"
}
run {
  some p: Person | p.name != "Joe"
}