如何建立合金数据库的模型？

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

分析器告诉我模型不一致：

执行"Run for 10“Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=1 Symmetry=20 5448 vars。510个基本vars。12578条。16毫秒没有发现任何实例。谓词可能不一致。0ms。

你们能告诉我为什么吗？我只想让数据库"Data4Help“链接到一些用户，可能关系的定义是不正确的，但我不知道为什么。谢谢

Answer 1

问题是合金与String有一些问题。默认情况下，字符串签名定义一组空原子。如果要在模型中使用String，则必须使用“您自己的String”填充该集合。

请参阅How to use String in Alloy?

在您的模型中，您可以添加以下简单的事实

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