在书软件抽象第10页它强调合金的声明性质： 合金声明，并介绍了如何检查通过比较前后值来判断 状态的更改是否有效。 第9页是添加新电子邮件地址簿的示例。该示例显示了“添加”之后的图书状态与添加之前的图书状态的不同之处。尼斯 - 确实非常明确！ 在页135是参数化“列表”模块的示例。该示例具有“addFront”功能： fun List.addFront (e: t): List {
{ p
下面我创建了三组：名称，地址和主机。地址字段将名称映射到地址。主机字段将地址映射到主机。 sig Name {
addr: Address
}
sig Address {
host: Host
}
sig Host {}
在这里，我要求合金分析器创建一个两个关系连接的实例：addr和host。 run {one addr.host} for 1
这是所生成的
以下模型包含一个“运行”命令，该命令指示Alloy Analyzer生成关系to.address的实例，其中关系仅限于一个元组。 sig Message {
to: Name
}
sig Name {
address: Address
}
sig Address {}
run {one to.address}
但我不想约束to.address的关系。我想简单
中强加一个孤立的属性我想知道是否有办法强制签名的属性为空。我想这样，但似乎不起作用： sig C {
myattribute: lone Type
}
SIG类型{ ATT1：诠释 ATT2：.....等。 } fact {
all c: C|
(my condition)
<=>
(
no c.myattribute
海报问如何比较Alloy中的函数。在测试一个小例子（比较谓词而不是函数）来回答这个问题时，我注意到了下面的行为，这让我很困惑。 只要检查命令的边界高于3且事实'f1'处于活动状态，分析仪就不会找到反例。激活事实，分析仪按预期工作。为什么冗余事实'f1'修改分析仪的操作，以及为什么在边界高于3的情况下？ open util/ordering [V]
sig V {}
fact f1 {
我正在阅读an article that uses Alloy to model some safety and security requirements for aircraft avionics。我正在努力理解文章中显示的“事实约束”之一。 数据流入系统。数据被系统消耗。该模型声明的一组数据，一组系统，和一个consumedBy关系（数据由系统消耗的）： sig Data {
co