首页 文章

Alloy中'private'关键字的含义是什么？ 'enum'声明的含义是什么？

提问于
浏览 次
6

Alloy 4 grammar允许签名声明（以及其他一些东西）携带 private 关键字 . 它还允许允许规范包含表单的枚举声明

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

The language reference没有（据我所知）描述 private 关键字或 enum 构造的含义 .

有文件吗？或者它们是否在语法中作为为将来的规范保留的构造？

alloy

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 属性，则其标签在同一模块中是私有的 . 这同样适用于私有字段和私有函数 .

    回复于
  • 0

    除了之前接受的答案之外，我还想补充一些有用的见解，这些见解来自于 enum 上的Alloy的一周经验，特别是与标准 sig 的主要区别 .

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

    sig Car {
    dameges: set Damage
}

    您可以选择使用

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

    VS

    enum Damage {
    MajorDamage, MinorDamage
}

    在第一种情况下，我们可以将具有不同MinorDamage原子（MinorDamage0，MinorDamage1，...）的模型与Cars相关联，而在第二种情况下，您始终只有一个MinorDamage，不同的Cars可以参考这些 .

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

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

    enum State {Damaged, Parked, Driven}

    映射概念，以便正好有三个 State ，每个 Car 可以参考 . 通过这种方式，在 Visualizer 中，您可以决定将模型投影到其中一个状态，并突出显示与此状态关联的所有 Car . 当然，你不能用 abstract + extend 构造做到这一点，因为超过 MajorDamage0 的投射只会突出显示与 Damage 相关联的 Car 而不是其他内容 .

    所以，总之，它实际上取决于你必须做什么 .

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

    run some_predicate for Y

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

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

    回复于

相关问题