如何在合金中建模一致的数据库？答案

【问题标题】：How to model a consitent database in alloy?如何在合金中建模一致的数据库？
【发布时间】：2018-11-10 16:56:40
【问题描述】：

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

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”链接到一些用户，可能关系的定义不正确，但我不知道为什么。谢谢

【问题讨论】：

标签： modeling alloy

【解决方案1】：

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

见How to use String in Alloy?

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

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

【讨论】：