交通信号灯控制模型
    交通灯控制系统（TLCS）常见于我们的日常生活中。大家都知道，绿色灯主干道的持续时间应该比红色的灯光在高峰时间更长。现在，一个简单的规则作出描述。我们假设有在系统中两个模式。模式1代表了下班时间和模式0代表其他时间。如果当前时间是在7点和9点17点和19点之间，或系统处于模式1。
该系统可以根据时间点从模式0转换到模式1和模式1转换到模式0。
在TLCS的过程可以表示如下：
（1）系统开始于0时;
（2）系统的模式设置为0，东西方向绿灯亮和南北方向红灯亮。这种状态持续25秒;
（3）东西方向黄灯闪烁和南北方向红灯亮。这种状态持续5秒;
（4）东西方向红灯亮和南北方向绿灯亮。这种状态持续25秒;
（5）东西方向红灯亮和南北方向黄灯闪烁。这种状态持续5秒。根据当前时间，所述模式被设置为下一个状态。如果当前时间是在7点和9点17点和19点之间或之后，下一步是（6），否则下一步骤是（2）;
（6）系统的模式设置为1，东西方向绿灯亮和南北方向红灯亮。这种状态持续30秒;
（7）东西方向黄灯闪烁和南北方向红灯亮。这种状态持续5秒;
（8）东西方向红灯亮和南北方向绿灯亮。这种状态持续20秒;
（9）东西方向红灯亮和南北方向黄灯闪烁。这种状态持续5秒。根据当前时间，所述模式被设置为下一个状态。如果当前时间是在7点和9点或者17点和19点之间或之后，下一步是（6），否则下一步骤是（2）。
这里我们使用EW_G，EW_Y，EW_R，SN_G，SN_Y和SN_R分别代表东西方向绿灯的，东西方向黄灯，东西方向红灯，南北方向绿灯，南北方向黄灯和南北方向红灯。

要验证的PPTL性质：
1.[](!(SN_G&&EW_G))
含义：永远不会出现南北方向的绿灯和东西方向的绿灯同时亮的情况。
模型满足该性质。

2.()( ((EW_G&&SN_R)&&()()()()(EW_G&&SN_R))*)
含义：每隔四个状态，都会满足东西方向绿灯亮而且南北方向红灯亮的状态。
模型满足该性质。