Alloy newbie here. I'm trying to model a medical database containing user and some medical information.
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
The analyzer tell me the model is inconsistent:
Executing "Run show for 10" Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=1 Symmetry=20 5448 vars. 510 primary vars. 12578 clauses. 16ms. No instance found. Predicate may be inconsistent. 0ms.
Can you guys tell me why? All I want is having the database "Data4Help" linked to some users, probably the definition of the relation is incorrect but I don't know why. Thank you