您是否创建了使用封装的Alloy模型?如果是的话,你介意分享你的模型,以便我(和其他人)可以从中学习吗?

我正在写一篇论文来解释什么是封装,它的好处,以及如何在Alloy中进行封装 . 以下是我目前所写的内容 . 你看到它有什么错误吗?我提供的示例是否有用?您的任何建议将不胜感激 .

合金中的封装

怎么做合金封装?

util / ordering模块使用封装:你用一个set调用模块,然后突然在set上有所有这些函数:first,last,next,prev等 . 你可以屏蔽排序模块如何实现这些功能 . 这是封装 .

在创建Alloy模型时使用封装 . 封装的好处是您可以重新设计封装模块,而不会影响模型的其他部分 .

以下是如何实现封装:

  • 创建一个模块 .

  • 要么用户通过模块参数传入集合,要么在模块中创建集合 .

  • 使用 private 关键字创建内部表示 .

  • 在集合上创建操作( predfun ) .

  • 然后,用户通过模块提供的操作对集合进行操作 .

说明Alloy中封装的示例

为交通灯的颜色创建一个模块 . 颜色组(红色,黄色,绿色)在模块中定义并且是公共的 . 颜色改变的顺序(例如,红光序列到黄光,其序列为绿光,其序列为红光)是私人的 . 该模块提供了一个 fun 用户调用以获取下一个颜色 .

这是模块

module traffic_light_color

private one sig Color_Sequence {
    Next: Color -> Color
} {
    Next = red -> yellow + yellow -> green + green -> red
}

fun next : Color -> Color { Color_Sequence.Next }

abstract sig Color {}
one sig red extends Color {}
one sig yellow extends Color {}
one sig green extends Color {}

以下是模块的示例用法

open traffic_light_color
open util/ordering[Time]

sig Time {}

sig Traffic_Light {
    color: Color one -> Time
} {
    all t: Time - first | color.t = traffic_light_color/next[color.(t.prev)]
}

run {}