问题描述：        
    某合唱团的4名成员A,B,C,D赶往演出现场，他们途中要经过一座小桥。当他们赶到桥头时，天已经黑了，周围没有灯，他们只有一只手电筒。桥很窄一次最多只许2人一起过桥，过桥人手里必须有手电筒。4个人的步行速度都不同，若2人同行，则以较慢者的速度为准。A需花1分钟过桥，B过桥需要2分钟，C需花5分钟，D需花10分钟过桥。请问：他们能在17分钟过桥吗？
建模：
     4个人personA，personB，personC，personD用布尔变量表示是否已经过桥。
     Time为枚举变量为过桥花费的不同时间{1,2,5,10,0}
     Total总时间，设置为17。

要验证的PPTL性质：
!(<>(personA && personB && personC && personD && total>0))
不存在，在17分钟，未来某个状态A、B、C、D四人都过桥 的情况。
模型不满足该性质，说明问题有解。