Как использовать String в Alloy?

Question

Как использовать String в Alloy?

Какие функции или операторы для String поддерживаются в Alloy?

Я искал вопросы здесь и нашел, что String - это ключевое слово в Alloy. Но я не могу найти ссылку на то, как использовать String в Alloy. Не могли бы вы дать один? Если нет, можно ли дать краткое описание String in Alloy?

Answer 1

На самом деле вы можете использовать строки в Alloy, но только как литералы для указания постоянных значений (т. Е. Строковые операции не поддерживаются, и Alloy не реализует решатель строк). Тем не менее, основное использование строк в Alloy - это присвоение константных строковых литералов некоторым полям с единственной целью сделать сгенерированные экземпляры более читаемыми при визуализации. Вот простой пример

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