Сплав: используйте для String

String в Alloy очень похож на любой другой знак. Единственное отличие состоит в том, что вы можете назначать строковые литералы полям типа String, например,

some p: Password | p.password = "secret"

Строковые функции в Alloy не поддерживаются. Решение ограничений, таких как

some p: Password | len[p.password] > 5

потребуется специализированный решатель строк, которым Alloy не является.

Если вас интересует только длина пароля, вы можете сделать что-то вроде

sig Char {}
sig Password { 
   password: seq Char 
} { 
   #password > 5
}

Если вам нужно решить более сложные ограничения строк (включая регулярные выражения), вам следует обратиться к специализированным программам решения строк, например, Хампи.