用佩特里网设计交通灯

工作流课程作业里的一道问题：Make some changes to the following figure, to make the two sets of traffic lights change their status in turn。（下图出自 Workflow Management: Models, Methods, and Systems 这本书。）

这是一种被称为「佩特里网」（Petri Net）的描述方法，包含 place（用圆圈表示）、token（用黑点表示）和 transition（用方形表示）等基本组件。我对于该问题的解法如下：

图中的每个 transition 都有两个输入 place 和两个输出 place，假设每个 transition 在其输入 place 都含有 token 时才能被触发，之后两个输出 place 都被 token 占用。

图中有两组交通灯，把它们分别命名为 TL1 和 TL2。假设初始状态如上图所示，此时 TL1 和 TL2 都亮红灯。开始运行后，rg1 因为两个输入 place 都被 token 占用而被触发，TL1 从红灯转至绿灯。之后，rg2 的两个输入 place 都被 token 占用，所以 TL2 也从红灯转至绿灯。然后，gy1 被触发，TL1 从绿灯转至黄灯，gy2 也因此被触发，导致 TL2 也从绿灯转至黄灯。与之前类似，此时 yr1 被触发，TL1 从黄灯转至红灯，进一步使得 yr2 被触发，TL2 也从黄灯转至红灯。此时已恢复至初始状态，完成一个周期。此过程可以不断循环。