摆渡者难题
问题描述：
     一个船夫、山羊、卷心菜和狼都在河的一边。船夫至多可搭载一位乘客过河。如果船夫离开，山羊会吃掉卷心菜，狼也会吃掉山羊。船夫能否将它们（包括狼、山羊、卷心菜）安全送到河对岸？
建模：
    船夫（ferryman）、山羊（goat）、卷心菜（cabbage）和狼（wolf）都有两个状态，一个在河此岸、一个在河彼岸，用布尔变量表示；
    船夫可以携带山羊、卷心菜、狼或者什么都不带，用一个枚举类型的变量表示carry：{goat，cabbage，wolf，0}；

要验证的PPTL性质：
!(([](((goat=cabbage)||(goat=wolf))->(goat=ferryman)))->(<>(cabbage &&goat && wolf && ferryman)))
含义：不存在，总是满足如果羊和卷心菜在一边或者羊和狼在一边，那么羊和船夫一定在一边的情况下，存在某个状态，卷心菜、羊、狼和船夫都到了河的对岸 的情况。
模型不满足该性质，说明问题存在解，反例路径即为该解。