如何建立合金的常态数据库? [英] How to model a consitent database in alloy?

问题描述

合金新手在这里.我正在尝试建立一个包含用户和一些医疗信息的医疗数据库.

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:

执行"10人跑步表演" 解算器= sat4j位宽= 4 MaxSeq = 7 SkolemDepth = 1对称= 20 5448个变量. 510个主要变量. 12578条. 16毫秒 找不到实例.谓词可能不一致. 0毫秒.

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.

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

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

推荐答案

问题是Alloy与弦乐有关.默认情况下，字符串签名定义了一组空原子.如果要在模型中使用字符串，则必须使用您自己的字符串"填充该集合.

The problem is that Alloy has some troubles with Strings. By default, the String signature defines an empty set of atoms. If you want to use Strings in your model, you will have to populate that set with "your own Strings".

请参见如何在Alloy中使用弦乐?

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

In your model, you could add this simple fact

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

这篇关于如何建立合金的常态数据库?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！