问题标签 [transition-systems]

我正在制作一个可以在过渡系统上执行一些操作并且还需要可视化它们的工具。

虽然没有太多关于 ruby​​-gem 的文档（这是我能得到的最好的：http ://www.omninerd.com/articles/Automating_Data_Visualization_with_Ruby_and_Graphviz ），但我设法从我的转换系统制作了一个图表。（随意使用它，周围没有太多示例代码。也欢迎评论/提问）

只有一件事我不能做：在开始状态下“无中生有”地画一个箭头。建议任何人？

我使用 Z3 的 PDR 引擎来证明转换系统中的不变量。当转换系统包含一个计数器循环时，必须通过该循环才能达到特定状态，则性能很慢。

在下面的源代码中，您会看到一个包含 3 个状态和 3 个转换的转换系统示例，该转换系统使用Z3 Fixedpoint Homepage上的转换系统 Python 类实现。在最后一行中，查询从状态 L0 开始到达状态 L2。因此转换 t2 必须经过 y 次。

如果我初始化 y==10，则答案计算得很快。但是初始化 y==1000 时性能很慢。

是否有可能以 Z3 获得更好性能的其他方式计算从 L0 到 L2 的路径？

我是新手。我想检查转换系统是否满足给定的 LTL 属性。但我不知道如何在 promela 中建模过渡系统。例如下图所示的转移系统有两种状态，初始状态为s0。如何检查LTL属性：<>q是否满足。有人知道如何在 promela 中描述这个问题吗？对了，spin中LTL的next算子怎么用？

我是 promela 的新手。我有一个用 promela 编写的程序：

有人知道如何为这个程序绘制过渡系统吗？

我想对 HTTP 交互进行建模，即一系列 HTTPRequest/HTTPResponse，并且我试图将其建模为转换系统。我使用以下方法在类 State 上定义了一个排序：

其中状态只是一组消息：

每对 (HTTPRequest->HTTPResponse) 和 (HTTPResponse->HTTPRequest) 在我的转换系统中都表示为一条规则。这些规则在 Alloy 中表示为谓词，可以让一个状态从一种状态移动到另一种状态。

例如，这是在收到特定 HTTPRequest 后生成 HTTPResponse 的规则：

不幸的是，创建的模型似乎太复杂了：我们有十几个规则（比上面的更复杂，但遵循相同的模式）并且执行速度非常慢。

编辑：特别是，CNF 生成非常慢，而求解需要相当长的时间。

您对如何模拟类似的过渡系统有什么建议吗？

非常感谢！

目前我正在尝试将系统原型转换为过渡系统模型。我有一些 LTL 属性，我想使用模型检查工具 NuSMV 验证这些属性。我只是介绍如何通过定义原子属性和其他数学方面来开始建模。

模型的图示

我正在开发一个不是依赖解析器的解析器，但它仍然是一个基于转换的系统。我没有像 arc-transition 那样使用 SHIFT、REDUCE-LEFT 和 REDUCE-RIGHT 3 个动作，而是为我的解析器提出了自己的动作。正如我通过 Andor 等人的论文所理解的那样。(2016)，只要系统遵循论文中定义的一些规则，我就可以在任何基于转换的系统上训练 SyntaxNet。但我不知道我应该从哪里开始。我查看了代码，但似乎它们主要用于训练依赖解析器（具有 3 个动作 SHIFT、REDUCE-LEFT 和 REDUCE-RIGHT）。如果您能突出显示代码中可以帮助我实现目标的某些部分，我将不胜感激。

另外，我不太明白 SyntaxNet 如何将 ConNLL 数据格式转换为黄金训练数据，你能告诉我哪个源文件负责这个任务吗？

非常感谢您提前

我正在努力从交错程序图的转换系统中定义原子命题。

初始状态包含内容

从经典基本自动售货机的过去示例中，包含的状态soda使 AP ={paid} 这是直截了当的。

但是我不确定如何为包含位置和变量的状态定义 AP

我在让随机数生成器工作时遇到问题，我不知道为什么。我必须在学校的实验室中执行此操作，并且该程序应该通过随机选择下一个状态来打印非确定性转换系统的轨迹。谁能告诉我这有什么问题？