1、Petri Nets基本概念
用Petri Nets表示红绿灯的状态
- 图中的正方形Transition代表的是从一个状态转换到另一个状态的关系。
- 一个Petri Net在设定好之后就是静止不变的，但是在上图中的那个红色实心圈Token是一个可以移动的点，它表示当前的状态，可以沿着Petri Net规定的路径进行移动
- 在一个Petri Net中，当前的状态被叫做Marking
-
reachable marking和unreachable marking:这是只有一个Token的情况
拥有两个Token的情况 - 关于Transition的两个状态区分：Enabled和Fire——
Enabled状态和Fire操作示意
上图中的正方形Transition有两个输入，只有同时又两个Token位于输入位置，这个正方形Transition才可以生效，即进入Eabled状态。
同时，进入Enabled状态之后，正方形Transition可以通过Fire操作来消费（Consume）一个Token，然后产生（Produce）一个Token并将其放置在输出Place上
特殊情况说明：
Petri Net上有可以同时输入输出的Place（初始状态）
此处p3 Place也必须要有Token存在，Transition才能生效
Petri Net上有可以同时输入输出的Place（结束状态）
2、State Explosion
有6个Token
因为这里每个Transition初始状态有6个Token且Fire操作的顺序并不 固定，所以最终会有超过100000个最终的State
3、安全的同步问题
红绿灯同步问题
两个同时运行的线程，我们希望它们能异步运行，始终保证一个红灯一个绿灯的情况
我们添加一个Place节点：
安全的红绿灯配置
注意这里没有出现红灯的显示，这里同样还有一个问题，就是如何保证r1装置和r2装置轮流进入绿灯状态，所以上述是non-deterministic的，所以我们对这个进行改进：
改进后的安全的红绿灯配置
4、 Reachability Graph
Reachability Graph示意图
上图中右图就是根据左边的Petri Net写出的 Reachability Graph
更加复杂的情况
注意这里从初始状态开始，t2的执行顺序是两个p1和一个p3同时进入t2，然后被转换成了一个p4！！！！
