青蛙寻路问题
问题描述：
    有六只青蛙放在同一直线的七个格子里，每个青蛙占一个格子，每边放三只，格式为AAA_BBB，标志为A的青蛙只能向右跳，标志为B的青蛙只能向左跳，每次只能有一个青蛙在跳，每个青蛙每次只能跳一格或两格，并且不能跳到其它青蛙的上面，最后标志为A的青蛙和标志为B的青蛙能否互换位置，得到BBB_AAA。

建模：
    用一个数组1..7 of 1..2 表示1到7个位置，每个元素可以取0代表没有青蛙，1代表A青蛙，2代表B青蛙。
    frogA、frogB、frogC、frogD、frogE、frogF表示六只青蛙，有两个状态，是否跳到对边。

要验证的PPTL性质：
!(<>(frogA.state && frogB.state && frogC.state && frogD.state &&frogE.state&&frogF.state))
含义：并不存在某个时候，青蛙A、B、C和青蛙C、D、E互换了位置。
模型不满足该性质，说明问题存在解，反例路径即为解。