如何在 alloy 中建模一致的数据库？

Question

Alloy 这里是新手。我正在尝试为包含用户和一些医疗信息的医疗数据库建模。

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 show for 10" Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=1 Symmetry=20 5448 个变量。 510个初级变量。 12578 个条款。 16 毫秒。没有找到实例。谓词可能不一致。 0 毫秒。

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

Answer 1

问题是 Alloy 在使用字符串时遇到了一些问题。默认情况下，String 签名定义了一个空的原子集。如果您想在模型中使用字符串，则必须使用 "your own Strings" 填充该集合。

见How to use String in Alloy?

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

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

如何在 alloy 中建模一致的数据库？

How to model a consitent database in alloy?

modeling

alloy