问题标签 [pi-calculus]

在 Milner 的 Pi 演算中，当多个进程从同一个通道读取时，评估语义是什么？

规则说

!x(a). P | ?x(b) Q ~> P | Q[a/b]

但是像这样的情况呢

!x(a). P | ?x(b) Q | ?x(c) R

?

我想在 JAVA 中实现 `pi-calculus。对于并发，我使用Deuce STM library。更改 JAVA 语法会很困难，因此我计划使用带注释的变量和通用函数/类。

例如。

所以一个通道将是这个类的一个实例。

我对如何对流程进行建模以允许它们通过这些渠道进行交互感到困惑。

有什么帮助/建议吗？

谢谢你。

我已经为pi calculus编写了一个JAVA库，它利用Deuce STM来管理并发进程。 我进一步希望证明我的库的类型安全。 Deuce STM 库类型安全吗？如果是，将不胜感激一些相同的链接。

我的 occam-pi 应用程序有一个长时间运行的生产者进程，定义如下：

它在通道上发送一个c从 增加start的值step。此处提供了完整示例。

这很好用，我被引导相信无限循环在 CSP中是惯用的。当我的消费算法完成时，问题就出现了。在此示例中，一旦消费者完成，就会发生死锁。

这里描述的TAGGED.INT协议试图解决关闭进程网络的问题，但是，根据我目前的理解，没有简单的方法可以终止主要工作是在通道上发送的生产者。感觉停止生产者的唯一方法是使用某种控制通道并黑洞输出：

此处提供了完整的工作示例。这样做的问题是代码更加不可读-我知道是主观的，但对软件工程很重要-与原始意图相比，原始意图令人费解。这似乎与奥卡姆剃刀原理相矛盾！

使用JCSP、C++CSP2和python-csp可以显式毒化通道以关闭进程网络。出于某种原因，争吵 occam 这样做会污染关闭逻辑的代码，并且看起来不合逻辑。

所以问题是，是否有一种方法可以在不使用示例中的显式通道的情况下终止生产者control进程？

编辑：

此邮件列表存档（ Poison ）中可能包含有关此主题的更多信息，这已经很老了（> 10 年）。所以问题仍然存在，从那时起有什么变化吗，或者这是在 occam-pi 中实现“进程终止”的最佳方式？

我对 Milner 的 Pi 微积分有点着迷，虽然我可以在白板上画出小图，但我很好奇是否有任何好的（或坏的）建模系统可以用来检查你的逻辑，以类似于 TLA+ 之类的方式。

如果这样的系统不存在或由于 没有必要reason x，我希望尽可能解释原因。