问题标签 [spin]

考虑以下Promela两个操纵共享变量的进程的模型N：

当两个过程都结束时，我如何使用LTL formula来找出变量可以具有的最小值？N

请我是 tihs 领域的大佬，如何将用 systemC 代码编写的经典示例 FIFO 转换为具有 LTL 属性的 PROMELA 语言满足以下三个属性：

互斥：生产者和消费者进程从不同时访问共享缓冲区。

非饥饿：消费者经常无限地访问缓冲区。（您可以假设生产者永远不会用完要提供的数据，而消费者永远不会停止尝试读取新数据。）

生产者-消费者：生产者永远不会覆盖数据缓冲区，除非消费者已经读取了当前数据消费者永远不会读取数据缓冲区，除非它包含新数据。生产者-消费者的常用算法使用单个标志位。标志位在数据准备好读取时由生产者设置，一旦读取数据由消费者取消设置。为了这个赋值，我们只需要建模数据缓冲区是否已经被读取，而不是建模数据的内容。我们将为此使用一个位。

您的任务是在 Promela 中对该算法进行建模，然后验证有关它的上述属性。记住 (1) 和 (3) 是安全属性，但 (2) 是活性属性，​​这将有所帮助。您可以在适当的情况下同时使用 LTL 和内联断言。

这是我第一次尝试解决这个问题：

我创建了两个基本流程，生产者和消费者。

生产者通过通道fwrite绑定到另一个名为write的进程，而消费者通过通道fread绑定到另一个名为read的进程。这里，read和write包含读写指针。

消费者是不完整的，我只是勾勒出我的想法。我希望在通道或FIFO表的总写入之后发生读取，并且生产者可以写入N个信息而不满足FIFO的大小。

这个系统（只是一个例子）应该模拟一个读取器/写入器队列，其中读取器请求一定的帧跨度[rq_begin,rq_end]，然后写入器应该至少使这个跨度可用。[av_begin,av_end]是可用帧的跨度。

这 4 个值是绝对帧索引，rq_begin当阅读器读取下一个帧跨度时会无限增加。

系统无法直接验证，因为这些值是无范围的（生成无限多的状态）。Promela/Spin（或类似软件）是否支持验证这样的系统，并自动对其进行转换以使其成为有限的？

例如，如果所有 4 个值都增加了相同的数量，情况仍然相同。或者可以将其重新表述为一个模型，该模型具有用于这些值差异的变量，例如av_end - rq_end。

我正在使用 Promela/Spin 来验证一个更复杂的排队系统，它使用像这样的绝对帧索引。

我尝试通过旋转来解决有关农夫、狼、山羊和卷心菜的任务。

所以，我找到了以下 promela 描述：

我在那里添加了一个 LTL 公式： ltl ltl_0 { <> fin && [] ( wg && gc ) } 来验证，狼不会吃山羊，山羊不会吃卷心菜。我想举一个例子，农民如何能够无损地运输他的所有需求（wgc）。

当我运行验证时，我得到以下结果：状态向量 20 字节，深度达到 59，错误：1 64 个状态，存储 23 个状态，匹配 87 个转换（= 存储+匹配）0 个原子步骤哈希冲突：0（已解决）

这意味着该程序为我生成了一个示例。但我无法解释它。*.pml.trial 文件内容为：在此处输入图片描述

请帮我解释一下。

我有以下程序使用PROMELA中的进程对FIFO进行建模：

我想在程序中添加wr_ptr和以指示执行更新rd_ptr时相对于 FIFO 深度的写入和读取指针：PUSH

以及类似的POP更新机会

你能帮我把这个添加到这个程序中吗？

还是我应该将其设为 ltl 属性并使用它来检查它？

来自评论：我想验证这个属性，例如如果fifo已满，不应该有写请求，这是正确的语法吗？full表示fifo已满，wr_idx是写指针，我不知道如何在属性 ltl fifo_no_write_when_full {[] (full -> !wr_idx)} 中访问 fifo 进程的完整、空、wr_idx、rd_idx、深度

这是我在 Stack Exchange 上的第一个问题，所以如果有任何违反准则的内容，请告诉我。

我有一个用 Promela 为大学操作系统和并发系统课程编写的程序。有两个进程正在运行，它们增加了一个变量 n。我们的任务是编写流程，然后使用 Spin 中的验证工具来证明 n 可以取值 4。我已经阅读了所有命令行参数并搞砸了，但没有任何结果对我来说，“插入这个修饰符后跟一个变量名来检查所有可能的值”。

请注意，这种类型的代码内置了竞争条件。例如，在决定消息接收操作将不可执行之前，该进程应该等待多长时间？可以通过使用消息轮询操作来避免该问题，例如，如下所示：

以上引用来自http://spinroot.com/spin/Man/else.html

我无法理解这种论点。只是 Spin 可以决定q?a：如果q是空的，那么它是可执行的。否则，它正在阻塞。

给定的参数引发了竞争条件。

但是，我可以提出同样的论点：

从 Spin 的角度来看，这没问题。但是，我在问，例如，在决定 的值x不会被其他进程增加之前，该进程应该等待多长时间？

在这里，http ://spinroot.com/spin/Man/Manual.html ，写着：

在 Promela 中，还有另一种避免测试和设置问题的方法：原子序列。通过在花括号中加上关键字 atomic 前缀语句序列，用户可以指示该序列将作为一个不可分割的单元执行，与任何其他进程不交错。如果除第一条语句之外的任何语句在原子序列中阻塞，则会导致运行时错误。这就是我们如何使用原子序列来保护对前面示例中的全局变量状态的并发访问。

在这里，http ://spinroot.com/spin/Man/atomic.html写着：

如果原子序列中的任何语句阻塞，则原子性丢失 如果原子序列中的任何语句阻塞，则原子性丢失，然后允许其他进程开始执行语句。当被阻塞的语句再次变为可执行时，原子序列的执行可以随时恢复，但不一定立即恢复。在进程可以恢复序列剩余部分的原子执行之前，该进程必须首先与系统中的所有其他活动进程竞争以重新获得控制权，也就是说，它必须首先被调度执行。

那么，什么是真实的？从第一个引用我们可以了解到它不允许在 atomic 中阻塞（不是第一个语句）

从第二个引文中，我们了解到可以在 atomic 中阻塞。你只是失去了原子性，就是这样。

I am working on a promela model that it fairly simple. Using two different modules, it acts as a crosswalk/Traffic light. The first module is the traffic light that outputs the current signal (green, red, yellow, pending). This module also receives as an input a signal called "pedestrian" which acts as an indicator that there are pedestrians wanting to cross. The second module acts as the crosswalk. It receives output signals from the traffic light module (green, yellow, green). It outputs the pedestrian signal to the traffic light module. This module simply defines whether the pedestrian(s) is crossing, waiting or not present. My issue is that upon running the model in Spin, it times out once the crosswalk begins toe execute its first few statements. I have attached the image of the trace I receive from the command line. I am completely new to Spin and Promela and so I am not entirely sure how to use the information form the trace to find my issue in the code. Any help is greatly appreciated.

Here is the code for the complete model:

我正在研究一个相当简单的 promela 模型。使用两个不同的模块，它充当人行横道/交通灯。第一个模块是输出当前信号（绿色、红色、黄色、待定）的交通灯。该模块还接收一个称为“行人”的信号作为输入，该信号用作指示有行人想要穿过的信号。第二个模块充当人行横道。它接收来自交通灯模块的输出信号（绿色、黄色、绿色）。它将行人信号输出到交通灯模块。该模块仅定义行人是否正在过马路、等待或不存在。我的问题是，一旦计数值达到 60，就会发生超时。我相信声明“SigG_out！1”会导致错误，但我不知道为什么。我附上了从命令行收到的跟踪图像。我对 Spin 和 Promela 完全陌生，所以我不确定如何使用跟踪中的信息在代码中找到我的问题。任何帮助是极大的赞赏。

这是完整模型的代码：