首页 > 代码库 > 采用 PAT工具及CSP语言，对一个问题进行自动机 建模
采用 PAT工具及CSP语言，对一个问题进行自动机 建模
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;
验证过程和结果
1、是斐波那契数且是质数
#define goal (b==13 && f==1);
2、 是斐波那契数不是质素
#define no1goal(b==21 && f==1);
3、 不是斐波那契数
#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
采用 PAT工具及CSP语言，对一个问题进行自动机 建模
声明：以上内容来自用户投稿及互联网公开渠道收集整理发布，本网站不拥有所有权，未作人工编辑处理，也不承担相关法律责任，若内容有误或涉及侵权可进行投诉： 投诉/举报 工作人员会在5个工作日内联系你，一经查实，本站将立刻删除涉嫌侵权内容。