问题标签 [tlc]

我试过了

但 TLC 给了我一个语法错误：

错误：TLC 在第 1 行的配置文件中发现错误。它需要 = 或 <-，但没有找到。

我也尝试将Sequences模块包含在配置文件中，但无济于事。

那么......我必须做些什么来分配一个序列？

几天来，在各种情况下，我一直在 TLA+ 工具箱中遇到以下错误：

以下是我想出的最简单的模块，它将重现该问题。我已经看到一些提到被覆盖的值，但是我看不出我是如何在规范中做一些事情来导致这个问题的。

有没有人看到错误，或者可以解释我错过了什么？

将 TypeOK 设置为不变量时，出现完整错误

我是新TLA+用户。我读到该TLA工具箱允许我们在模型检查完成后可视化状态图。

为此，我需要安装 dot 。但我不知道如何启动可视化。我可以使用 GUI 购买还是需要使用专用命令行？

谢谢

我有一个 TLA+ 模块，总结起来是这样的：

当我尝试使用 TLC 对此进行模型检查时，我收到以下错误：

TLC 引发了意外的异常。这可能是由规格或模型中的错误引起的。请参阅用户输出或 TLC 控制台以获取有关发生情况的线索。异常是 java.lang.RuntimeException：TLC 无法处理规范的这种结合：第 X 行，Y 行到 Z 行，模块组的 T 行

...指向Next.

我相信我Next的写得很好，因为这是一个与Next我的非常相似的示例模型：https ://github.com/tlaplus/Examples/blob/master/specifications/aba-asyn-byz/aba_asyn_byz.tla#L110

此外，Leslie Lamport指定系统的第 14.2.2 节说：

只有当表达式等于有限集[...]时，TLC 才能评估集值表达式。只有当 TLC 可以枚举集合S时，TLC 才会评估以下形式的表达式：

并提供“ S中存在x使得p ”的例子。

我该如何解决这个错误？

我有以下规格：

（我将这个规范简化到它没有做任何有用的事情的地步。）

当我尝试通过 TLC 运行它时，我收到以下错误：

在评估中，标识符成员要么未定义，要么不是运算符。

错误指向该Init行。

当我将Init行更改为：

它验证得很好。

我想要前一个功能，因为我的意思是members成为一个人的集合，而不是一个人。

根据Leslie Lamport's Specifying Systems的第 16.1.6 节，“TLA+ 在集合上提供了以下运算符：”并列出了\in和\subseteq。

为什么 TLA+ 不让我使用\subseteq？

tlc 可以保存为文本文件并具有可追溯性。

是否可以在状态流设计中使用 tlc？或者有什么其他建议可以在 sateflow 项目中保留 tracebilty 功能？

在我的 Internet 安全课程中，我得到了一个项目，我最终将通过创建证书来利用网站上的“记住我的密码”，手动将其放入我的“客户端”浏览器中以获得信任，然后能够当客户端连接到网站的服务器时，嗅探所有会话 ID。完成此操作后，我将使用会话 ID 发布到个人资料提要（例如 Twitter），但这部分将在课程后面进行。但是，我不知道我首先要如何使用证书？如果它是一个真正的网站，我想我会制作该网站的副本或网络钓鱼版本，但这不是我的教授想要的。他说要创建证书，将其上传到我用来登录推特的任何浏览器中，不知何故我' 将能够嗅探加密流量并使用 PCAP 库查看会话 ID。他想要的只是让我在报告中记录ID..

我正在考虑使用类似于 DHCP 流氓服务器的东西，但我认为我不会使用我自己制作的证书。

我已经开始使用 pyCharm 设置我的 GUI，但是我在编译时遇到了一些错误，因为添加了一个菜单栏。

我已经删除了与菜单栏相关的所有代码，它可以工作，但它没有帮助，因为我想添加一个菜单栏。

我在cc65上进行版本升级，遇到了linuxdoc-tools的问题。由于我无法修复linuxdoc-tools并且有一个简单的解决方法，我决定添加一个 if 语句来通知用户以及解决方法：

粗鲁，但我能做的最好，因为我既不是perl5也不是linuxdoc-tools维护者，我不想在版本升级上花费太多时间。

但是，MacPorts 不理解exit 1并且ui_error不会自行停止执行。

我如何停止执行，以免浪费用户时间在构建上，否则最终会失败。

我有以下队列规范：

当我使用以下常量值运行 TLC 时：

还有这些限制：

它报告这些错误：

但是规范允许 中的值(0 .. L)，那么为什么 TLC 报告q=1, q=2, q=3,q=4作为无效状态？

错误跟踪输出如下：

一个人应该如何识别那些被认为是错误的和那些不是来自这个跟踪的？界面不显示红灯q=0。