Как смоделировать согласованную базу данных в сплаве?

Question

Сплав новичка здесь. Я пытаюсь смоделировать медицинскую базу данных, содержащую пользователя и некоторую медицинскую информацию.

sig User{
    name: one  String,
    surname:  one String,
    socialNumber:  one String,
    address:  one String,
    age: one Int,   
    registration: one UserCredential,
    healthStatus: one HealthInformation
}{
    age>0
}
sig UserCredential{
    user: one String,
    pass: one String,
    mail:  one String
}

sig HealthInformation{}


sig Data4Help{
    users: some User,
}

pred show(d:Data4Help){
    #d.users>1
}

run show for 10

Анализатор говорит мне, что модель несовместима:

Выполнение «Запустить шоу на 10» Solver = sat4j Бит пропускная способность = 4 MaxSeq = 7 SkolemDepth = 1 Симметрия = 20 5448 вар. 510 первичных переменных. 12578 статей. 16мс. Экземпляр не найден. Предикат может быть противоречивым. 0ms.

Можете ли вы, ребята, сказать мне, почему? Все, что я хочу, - это привязка базы данных «Data4Help» к некоторым пользователям, возможно, определение отношения неверно, но я не знаю почему. Спасибо

Answer 1

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

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

В вашей модели вы можете добавить этот простой факт

fact initPoolOfString{ 
   String in "insert"+ "your"+"dummy" + "strings" + "here"
}