1

我正在尝试在 Scala 中为“CSP”实现解析器和语义。我已经实现了 parser ，现在我正忙于研究语言的语义部分。我对并发系统和非确定性选择的世界完全陌生。所以这是我的问题：

我想按照此处的说明实现“非确定性选择”和“接口并行” 。

我现在可以理解该过程，但在涉及非确定性时我无法直截了当。我需要一个好的数据类型来在 Scala 中实现这一点，我正在考虑将所有进程放在一个列表中，然后随机化该列表，然后从修改后的列表中选择一个元素。但这对我来说听起来不是那么不确定。

有没有人在这个问题上经历过并且知道一个好的算法？

4

2 回答 2

1

我对 CSP 的非常有限的理解是 CSP 运算符对应于以下 Haskell 类型：

-- Prefixing corresponds to functions
x :: A
P :: B
x -> P :: A -> C

-- Choice corresponds to product
P :: A
Q :: B
P □ Q :: (A, B)

-- Non-determinism corresponds to sum
-- I don't know how to make the non-determinism symbol, so I use (△)
P :: A
Q :: B
(P △ B) :: Either A B

然后，您可以使用代数同构来减少 CSP 表达式。使用维基百科示例：

(coin -> STOP) □ (card -> STOP)

-- translates to the following Haskell type:
(coin -> Stop, card Stop)

-- which is algebraically isomorphic to:
(Either coin card -> Stop)

-- translates in reverse back to CSP:
coin □ card -> STOP

另外，我认为维基百科的一个例子是错误的（或者我错了）。我相信这个表达式应该简化为：

(a -> a -> STOP) □ (a -> b -> STOP)

-- translates to the following Haskell type:
(a -> a -> STOP, a -> b -> STOP)

-- which is algebraically isomorphic to:
a -> Either a b -> STOP

-- translates in reverse back to CSP:
a -> (a △ b) -> STOP

不过，我还没有弄清楚接口并行的等价物。它似乎不符合一个优雅的概念。

于 2013-06-20T00:19:16.227 回答
1

这是一个高级话题。解析方面很容易。编写正确的并发原语非常困难，几乎可以肯定需要使用 FDR 等工具进行形式验证。

如果您只对编写表达式解析器部分而不是并发原语感兴趣，您可能更愿意在JCSP的基础上进行构建，它已经在 J​​ava API 中提供了这些原语。这个（UKC）的作者使用形式验证来验证它的组件，特别是通道和替代（选择）部分。

于 2013-06-21T09:04:25.330 回答