首页 文章

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

提问于
浏览 次
0

我必须在大学项目的需求分析和规范文档中使用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.

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

modeling specifications requirements analyzer alloy

3 回答

  • 1

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

    更一般地说，Alloy不是关于建模实际数据（整数，粗体和字符串），而是关于建模 structure ，即实体之间的关系 . 对于结构分析，通常不需要具体的数据类型 .

    回复于
  • 0

    构建Alloy模型的目的是捕获设计或系统的本质并探索细微属性 . 您不希望包含在数据库模式中找到的所有详细信息 . 你的模型也有很多实现细节，例如id（由于它们隐含在对象标识中而不需要），并且使用字符串而不是概念类型 - 目的地，例如，应该具有这样的类型作为“位置” .

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

    回复于
  • 1

    感谢大家，_1293939解决了这个问题 .

    然而，我对Alloy的目的的“扭曲”观点是由于我们被要求使用它而我们没有得到如何使用它的真实解释，在大多数例子中所有细节都是写的 . 我想我将不得不尝试更多地研究它！

    回复于

相关问题