tla+ - 从对称集合中选择一项
问题描述
我有一个类似于以下的 TLA+ 规范:
CONSTANT Items
VARIABLE item
而且我想Items
是对称的,并从中选择一个元素Items
并将其存储到item
.
我一直在使用item = CHOOSE x \in Items: TRUE
,但我了解到这会破坏项目的对称性:TLC 将始终从集合中选择第一个项目。
我想以保持对称的方式选择一个项目,以允许 TLC 探索所有状态。我不在乎我们选择了哪个项目——只要它是一个,并且它来自Items
. (以后,我item
需要\in Items
.
虽然我更喜欢item
成为单个元素,但item
作为一组基数 1 也可以,所以稍后我可以检查\subseteq Items
.
建议我替换CHOOSE
为{x \in Items: TRUE}
以保持对称性并使结果为\subseteq Items
,但这不会将结果集限制为基数 1。
有没有办法让 TLA+ 从一组对称的值中给我一个项目或一组基数 1?
解决方案
自从发布问题以来,我对 TLA+/TLC 有了更多了解,这是我的答案:
要简单地从初始谓词中的对称集中选择一个元素:
item \in Items
或在一个动作中:
item' \in Items
如果您想选择一个与谓词匹配的项目,如您可以使用 CHOOSE 指定的那样,那么这是替代方法:
item \in {x \in Items: P(x)}
这将形成与谓词匹配的项目子集,然后选择其中的一个元素。
这里有一些数据显示了这种语法和 CHOOSE 之间的区别。考虑这个模块:
----------------------------- MODULE ChooseDemo -----------------------------
CONSTANT Items
VARIABLE item
TypeInvariant == item \in Items
Init == item = CHOOSE x \in Items: TRUE
Next == item' \in {x \in Items: x /= item}
=============================================================================
当Items
有三个项目:
- 不是对称集:TLC 找到 1 个初始状态和总共 7 个(3 个不同的)状态。
- 对称集:TLC 找到 1 个初始状态和总共 3 个(1 个不同的)状态。
现在考虑这个模块:
--------------------------- MODULE SetFormingDemo ---------------------------
CONSTANT Items
VARIABLE item
TypeInvariant == item \in Items
Init == item \in {x \in Items: TRUE}
Next == item' \in {x \in Items: x /= item}
=============================================================================
当Items
有三个项目:
- 不是对称集:TLC 找到 3 个(3 个不同的)初始状态和总共 9 个(3 个不同的)状态。
- 对称集:TLC 找到 3(1 个不同)初始状态和总共 5(1 个不同)状态。
因此,通过使用集合形成语法,TLC 比使用 CHOOSE 找到更多的状态。
推荐阅读
- python - 如何在熊猫中将 if/else 转换为 np.where
- python - 为什么 python 不能正确地解决这个矩阵?
- sql - 在 SQL 数据库中获取所有同名但大小写不同的数据库对象?
- xamarin - 如何更改 xamforms.control.calendar 语言?
- mdriven - 如何在移动模式下通过保存和取消隐藏闪烁的底栏?
- rest - 使用 Accept Header .Net Core 3.1 发布 - PagSeguro
- r - 如何在 ggplot 上的 r 中对活动数据拟合正弦波
- python - Jenkins 到 Linux 问题 - Python 文件执行
- python - 如何通过 Jupyter 中的 Python 命令与串行 com 端口通信?
- wordpress - Wordpress post date hook