合金分析仪4.2中未显示合金签名

我必须在大学项目的需求分析和规范文档中使用合金。我从简单的东西开始，只有签名和事实。这是我使用的签名：合金分析仪4.2中未显示合金签名

abstract sig Date{ 
    year: one Int, 
    month: one Int, 
    day: one Int 
} 

abstract sig Time{ 
    h: one Int, 
    m: one Int, 
    s: one Int 
} 

abstract sig Double{ 
    leftPart: one Int, 
    rightPart: one Int 
} 

abstract sig Bool{ 
    value: one String 
} 

sig DateBirth extends Date{} 
sig DateRide extends Date{} 
sig DateExpiry extends Date{} 


abstract sig User { 
email: one String, 
name: one String, 
surname: one String, 
gender: one Bool, 
address: one String, 
password: one String, 
dateOfBirth: one DateBirth, 
IDRide: set Ride 
} 

sig TaxiDriver extends User{ 
taxiLicense: one String, 
personalLicense: one String, 
IBAN: one String, 
positionInQueue: lone Int, 
IDTaxi: set Taxi 
} 


sig Client extends User{ 
} 


sig Zone { 
numberOfZone: one Int, 
vertexNorthWest: one Double, 
vertexNorthEast: one Double, 
vertexSouthWest: one Double, 
vertexSouthEast: one Double, 
currentQueue: set TaxiDriver 

} 


sig Taxi { 
IDTaxi: one String, 
plate: one String, 
availablePlaces: one Int, 
} 


sig Ride { 
IDRide: one String, 
origin: one String, 
destination: one String, 
dateOfRide: one DateRide, 
timeOfDeparture: one Time, 
timeOfArrival: one Time, 
price: one Double, 
numberOfPeople: one Int, 
accepted: one Bool, 
userEmail: set User 
} 


sig Credit_Card { 
number: Double, 
owner: String, 
expiryDate: DateExpiry, 
ownerEmail: one Client 
}

然后，我添加了谓词“秀”给veify的是否一致与否：

pred Show{} 
run Show for 10

上运行合金分析仪4.2这个“执行”之后是我得到的消息：

Executing "Run Show for 10" 
    Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=1 Symmetry=20 
    21067 vars. 3840 primary vars. 37164 clauses. 376ms. 
    Instance. found. Predicate is consistent. 375ms.

没问题吧？但是，当我点击“显示”时，显示器上没有显示签名“用户”（及其子签名）的实例，而所有其他人都在那里。我试图点击“下一个”数十亿次，试图看看我是否可以找到他们展示的模型，但没有。任何想法/建议？谢谢！

来源

2015-11-02 marcodeco

这可能是因为使用String。据我所知，String是合金中的一个保留字，但在这一点上并没有真正实现。尝试删除String字段或将其替换为其他字段。

在一个更为一般的说明中，Alloy不是关于建模真实数据（ints，bools和strings），而是更多地关注建模结构，即实体之间的关系。对于结构分析，通常不需要具体的数据类型。

来源

2015-11-03 06:58:40 wmeyer

实际上，字符串被实现。你只需要为那些组成生成的实例的字符串原子或字符串指定一个“池”。你可以在Q/A中找到更多关于字符串用法的地址：http://stackoverflow.com/questions/27397887/provide-alloy-with-a-pool-of-custom-strings –

构建合金模型的目的是捕捉设计或系统的本质，并探索微妙的属性。您不希望包含您在数据库模式中找到的所有细节。你的模型也有很多实现细节，比如ids（因为它们隐含在对象标识中，所以不需要），以及使用字符串而不是概念类型 - 目的地，例如，应该有一个类型作为“位置”。

所以我建议你重新开始，并首先考虑你想要这个模型回答什么样的问题。

来源

2015-11-03 14:38:08

感谢大家，删除字符串解决了这个问题。

然而，我对“合金”目的的“扭曲”观点是由于我们被要求使用它，但我们没有给出关于如何使用它的真实解释，在大多数例子中都写了所有细节。我想我必须尝试再研究一下！

来源

2015-11-04 12:03:45 marcodeco

合金分析仪4.2中未显示合金签名

回答

相关问题