Alloy Analyzer 4.2 中未显示合金特征

Question

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

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
}

然后，我添加了谓词“show”来验证它是否一致：

pred Show{}
run Show for 10

在 Alloy Analyzer 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.

没问题吧？但是，当我单击“显示”时，显示屏上没有显示签名“用户”（及其子签名）的实例，而所有其他签名都在那里。我试图点击“下一步”无数次，试图查看是否可以找到显示它们的模型，但没有。 有什么想法/建议吗？谢谢！

Answer 1

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

但是，我对 Alloy 用途的“扭曲”看法是因为我们被要求使用它，但我们没有得到关于如何使用它的真正解释，在大多数示例中，所有细节都被写入。我想我得再努力研究一下！

Answer 2

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

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

Answer 3

可能是因为使用了String。据我所知，String 是 Alloy 中的保留字，但目前还没有真正实现。尝试删除 String 字段或将其替换为其他内容。

更笼统地说，Alloy 与其说是对真实数据（整数、布尔值和字符串）进行建模，不如说是对结构 建模，即实体之间的关系。对于结构分析，通常不需要具体的数据类型。