标签：
pat是新加坡国立开发的工具，需要的去官网下http://www.comp.nus.edu.sg/~pat/
，学了一天，是个不错的自动机验证工具，感觉还不错啊。
验证一个数是否为斐波那契数且为质数
先验证是否为斐波那契数，然后再判断质数
/*验证是否为 斐波那契数且是质数*/ #define goal (b==13 && f==1); //是斐波那契数且是质数 #define no1goal(b==21 && f==1);// 是斐波那契数不是质素 #define no2goal(b==22 && f==1);// 不是斐波那契数 var a = 0; var b = 1; var t = 0; var s = 2; var f = 0; FBNQ() = [ b>0 ] fbnq1{t=b;b=a+b;a=t;}->FBNQ() [][b>1] fbnq2{s = 2;}->ZHISHU(); ZHISHU() = if( s*s <= b && b%s==0 ) { zhishu1{f=0;}->FBNQ() } else if(s*s <= b) { zhishu2{s=s+1;}->ZHISHU() } else { zhishu3{f=1;}->ZHISHU() }; #assert FBNQ() reaches goal; #assert FBNQ() reaches no1goal; #assert FBNQ() reaches no2goal;
#define goal (b==13 && f==1);
#define no1goal(b==21 && f==1);
#define no2goal(b==22 && f==1);//
验证成功。
PAT工具及CSP语言，对一个问题进行自动机建模，的确是个强大的工具。
还有一个农夫过河的问题，ppt上写的，也很不错：
状态是：
1 农夫过河
– 农夫在河边，狼和羊、羊
和菜不能同时在河边
– 农夫到对岸
• 2农夫带狼过河
– 农夫、狼在河边， 羊和菜
不能同时在河边
– 农夫、狼到对岸
• 3农夫带羊过河
– 农夫、羊在河边
– 农夫、羊到对岸
• 4农夫带菜过河
– 农夫、菜在河边，狼和羊
不能同时在河边
– 农夫、菜到对岸
• 1 农夫回来
– 农夫在对岸，狼和羊、羊和
菜不能同时在对岸
– 农夫回到河边
• 2农夫带狼回来
– 农夫、狼在对岸，羊和菜不
能同时在对岸
– 农夫、狼回到河边
• 3农夫带羊回来
– 农夫、羊在对岸
– 农夫、羊回到河边
• 4农夫带菜回来
– 农夫、菜在对岸，狼和羊不
能同时在对岸
– 农夫、菜回到河边
• /*0表示在河边， 1表示在对岸*/
• var farmer=0;
• var wolf=0;
• var goat=0;
• var carbage=0;
• Cross() =[ farmer==0 && ((! (wolf==0 && goat==0) ) && (! (goat==0 &&
carbage==0))) ] farmer_cross{farmer=1;}->Return()
• [] [ farmer==0 && wolf==0 && (! (goat==0 && carbage ==0)) ]
farmer_wolf_cross{farmer=1;wolf=1;}->Return()
• [] [ farmer==0 && goat==0] farmer_goat_cross{farmer=1;goat=1;}->Return()
• [] [ farmer==0 && carbage==0 && (! (wolf==0 && goat==0)) ]
farmer_carbage_cross{farmer=1;carbage=1;}->Return();
• Return() =[ farmer==1 && ((! (wolf==1 && goat==1)) && (! (goat==1 &&
carbage==1))) ] farmer_return{farmer=0;}->Cross()
• [] [ farmer==1 && wolf==1 && (! (goat==1 && carbage ==1)) ]
farmer_wolf_return{farmer=0;wolf=0;}->Cross()
• [] [ farmer==1 && goat==1] farmer_goat_return{farmer=0;goat=0;}->Cross()
• [] [ farmer==1 && carbage==1 && (! (wolf==1 && g
标签：
原文地址：http://www.cnblogs.com/juandx/p/4225373.html
