采用 PAT工具及CSP语言,对一个问题进行自动机 建模
2015-01-15 02:52
323 查看
pat是新加坡国立开发的工具,需要的去官网下http://www.comp.nus.edu.sg/~pat/
,学了一天,是个不错的自动机验证工具,感觉还不错啊。
验证一个数是否为斐波那契数且为质数
![](http://images.cnitblog.com/blog/433976/201501/150243257451089.png)
![](http://images.cnitblog.com/blog/433976/201501/150244253087358.png)
![](http://images.cnitblog.com/blog/433976/201501/150244334334709.png)
![](http://images.cnitblog.com/blog/433976/201501/150244395261648.png)
PAT工具及CSP语言,对一个问题进行自动机建模,的确是个强大的工具。
还有一个农夫过河的问题,ppt上写的,也很不错:
状态是:
1 农夫过河
– 农夫在河边,狼和羊、羊
和菜不能同时在河边
– 农夫到对岸
• 2农夫带狼过河
– 农夫、狼在河边, 羊和菜
不能同时在河边
– 农夫、狼到对岸
• 3农夫带羊过河
– 农夫、羊在河边
– 农夫、羊到对岸
• 4农夫带菜过河
– 农夫、菜在河边,狼和羊
不能同时在河边
– 农夫、菜到对岸
• 1 农夫回来
– 农夫在对岸,狼和羊、羊和
菜不能同时在对岸
– 农夫回到河边
• 2农夫带狼回来
– 农夫、狼在对岸,羊和菜不
能同时在对岸
– 农夫、狼回到河边
• 3农夫带羊回来
– 农夫、羊在对岸
– 农夫、羊回到河边
• 4农夫带菜回来
– 农夫、菜在对岸,狼和羊不
能同时在对岸
– 农夫、菜回到河边
,学了一天,是个不错的自动机验证工具,感觉还不错啊。
验证一个数是否为斐波那契数且为质数
方法
先验证是否为斐波那契数,然后再判断质数代码
/*验证是否为 斐波那契数且是质数*/ #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);![](http://images.cnitblog.com/blog/433976/201501/150243257451089.png)
![](http://images.cnitblog.com/blog/433976/201501/150244253087358.png)
2、 是斐波那契数不是质素
#define no1goal(b==21 && f==1);![](http://images.cnitblog.com/blog/433976/201501/150244334334709.png)
3、 不是斐波那契数
#define no2goal(b==22 && f==1);//![](http://images.cnitblog.com/blog/433976/201501/150244395261648.png)
总结
验证成功。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://images.cnitblog.com/blog/433976/201501/150249309795474.png)
相关文章推荐
- 介绍Junit,一个用来在项目中进行测试和调试的工具
- 又一个语言识别工具(ANTLR)
- 解决一个问题,发布一个自己开发的小工具
- D语言环境配置的一个问题
- 一个用VC生成DLL并用于其它工具的问题
- [学术论文]从轻量级形式化方法出发的需求建模——用Radl语言对MIS系统进行规范描述的案例研究
- 发现一个小巧的建模工具Jude
- 推荐一个建模工具Visual Paradigm
- VC8实现的一个PC端查看TSK主题文件的工具,以及由其引出的VC8MFC程序脱离.net框架分发问题
- [技术讨论]业务建模的一些问题和工具选择的问题
- 一个从来不曾注意的问题,在C#语言中,对于字符串变量的赋初值问题!!
- [全程建模]与一个朋友讨论的关于书上的两个问题
- 图形编辑软件的副产品:一个基于VS2005的建模工具
- 对java中的String采用+=连接字符串需要注意的一个问题
- 我在进行J2EE开发时碰到的一个问题
- 关于UML建模工具和项目管理工具的问题
- 一个针对.net的好的建模工具 powerdesign 11
- 发现微软VS工具的一个问题,不知算不算是BUG
- 一个iBatis框架进行batch处理的问题
- 推荐一个免费的建模工具JUDE Community