Home Articles

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

Asked
Viewed 1952 times
6

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

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

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

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

2 Answers

  • 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中,但正如我之前所说,您可以在枚举上“投影”模型并在枚举的不同元素之间切换 .

Related