5

Alloy 4 语法允许签名声明（和其他一些东西）携带private关键字。它还允许允许规范包含形式的枚举声明

enum nephews { hughie, louis, dewey }
enum ducks { donald, daisy, scrooge, nephews }

语言参考没有（据我所知）描述private关键字或enum结构的含义。

有可用的文档吗？还是它们在语法中是为未来规范保留的结构？

4

2 回答 2

3

这是我对这两个关键词的非官方理解。

enum nephews { hughie, louis, dewey }

在语义上等价于

open util/ordering[nephews] as nephewsOrd

abstract sig nephews {}

one sig hughie extends nephews {}
one sig louis extends nephews {}
one sig dewey extends nephews {}

fact {
  nephewsOrd/first = hughie
  nephewsOrd/next = hughie -> louis + louis -> dewey
}

private关键字意味着如果 sig 具有属性，则其private标签在同一模块内是私有的。这同样适用于私有字段和私有函数。

于 2012-08-16T18:57:11.943 回答
1

除了先前接受的答案之外，我想添加一些有用的见解，这些见解来自对enums 的 Alloy 一周体验，特别是与 standard 的主要区别sig。

如果你使用abstract sig + extend，你会想出一个模型，其中有许多集合对应于相同的概念。也许一个例子可以更好地澄清它。假设像

sig Car {
    dameges: set Damage
}

您可以选择使用

abstract sig Damage {}
sig MajorDamage, MinorDamage extends Damage {}

对比

enum Damage {
    MajorDamage, MinorDamage
}

在第一种情况下，我们可以提出一个与 Cars 相关联的具有不同 MinorDamage 原子（MinorDamage0，MinorDamage1，...）的模型，而在第二种情况下，您始终只有一个 MinorDamage 可供不同的 Cars 引用。

在这种情况下，使用abstract sig + extend表单可能有一定意义（因为您可以决定跟踪不同的 MinorDamage 或 MajorDamage 元素）。

另一方面，如果你想要一个currentState: set State，最好使用一个

enum State {Damaged, Parked, Driven}

映射概念，以便有准确的三个State，每个Car可以参考。这样，在 中Visualizer，您可以决定将您的模型准确地投影到其中一个状态上，它将突出显示Car与该状态关联的所有 s。当然，你不能用abstract + extend结构来做到这一点，因为投影MajorDamage0只会突出与它Car相关联的东西，Damage而不是其他东西。

所以，总而言之，这真的取决于你必须做什么。

另外，请记住，如果您有一个由 X 元素组成的枚举并执行

run some_predicate for Y

其中 Y < X，Alloy 根本不产生任何实例。所以，在我们的最后一个例子中，我们不能有一个 Y < 3。

最后一点，如果您使用 Magic Layout 按钮，枚举并不总是出现在 Visualizer 中，但正如我之前所说，您可以将模型“投影”到枚举上并在枚举的不同元素之间切换。

于 2016-11-06T07:54:37.233 回答