Alloy 个签名未在 Alloy Analyzer 4.2 中显示

Question

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

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 运行 "Execute" 之后，这是我收到的消息：

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.

没问题吧？但是，当我单击 "Show" 时，显示屏上没有显示签名 "User"（及其子签名）的实例，而所有其他签名都在那里。我尝试点击 "Next" 无数次，想看看是否可以找到展示它们的模型，但没有。有 idea/suggestion 吗？谢谢！

Answer 1

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

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

Answer 2

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

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

Answer 3

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

然而，我对 Alloy 目的的 "distorted" 看法是因为我们被要求使用它，但没有得到关于如何使用它的真正解释，在大多数示例中，所有细节都已写入。我想我将不得不尝试更多地研究它！

Alloy 个签名未在 Alloy Analyzer 4.2 中显示

Alloy signatures not shown in Alloy Analyzer 4.2

modeling

requirements

specifications

analyzer

alloy