MyException - 我的异常网
当前位置:我的异常网» J2SE » JAVA环境下SPIN模型检测工具安装的有关问题(新手第

JAVA环境下SPIN模型检测工具安装的有关问题(新手第一问,谢谢了)

www.MyException.Cn  网友分享于:2013-02-21  浏览:124次
JAVA环境下SPIN模型检测工具安装的问题(新手第一问,多谢了)
弱弱的问:我还站在JAVA的大门外,但要用到模型检测工具SPIN,安装使用一直出现问题,经过一番请教搜索,没有得到实质性的解决,现将我遇到的问题描述如下:
(一)下载http://202.194.89.125/Soft/UploadSoft/jdk-1_5_0_04-windows-i586-p.exe 后一直默认安装,没有做任何修改,安装后修改环境变量按如下说明:(设置环境变量:1.右击“我的电脑”,点击“属性”:选择“高级”选项卡,点击“环境变量”
  2.在“系统变量”中,新建系统变量名JAVA_HOME 变量值C:\Program Files\Java\jdk1.5.0_04
  新建系统变量名Path,变量值%JAVA_HOME%\bin;%JAVA_HOME%\jre\bin 
  新建系统变量名CLASSPATH,变量值.;%JAVA_HOME%\lib;%JAVA_HOME%\lib\tools.jar 
(二)SPIN有如下安装说明:
  1、 WIN32环境下SPIN的安装和使用 
  从[http://spinroot.com/spin/Src/index.html]下载最新的pc_spin*.zip文件(或
  pc_spin412.zip:),解压pc_spin*.zip然后将spin*.exe拷贝到例如D:\SPIN下,进入控制台,转到D:\SPIN目
  录下就可以用spin的当前版本对模型进行检测了,在VC6.0环境下,编译SPIN产生的pan.c文件,得到pan.exe
  可以用spin*.exe在Windows控制台环境下对模型进行相应的检测和错误迹观察了。 
  2、 Java环境下SPIN的安装和使用 
  上述smv.exe只有控制台界面,以色列的Mordechai (Moti) Ben-Ari使用Java作出了图形界面jSPIN,可如下安装
  使用: 在Windows2000/NT/XP下 - 使用VC++6.0编译器:先安装并运行成功:VC++6.0、JDK1.5.0
  将jspin1-1-5.zip解压,得目录\jspin1-1-5,可将此目录放于例如:d:\jspin1-1-5
  将SPIN4.1.2(Win32版): pc_spin412.zip解压到后将spin412.exe取出放入d:\jspin1-1-5;
  打开d:\jspin1-1-5的config文件,做如下改变:
  设置示例文件所在目录 SOURCE_DIRECTORY=d\:\\jspin1-1-5\\examples
  设置spin412.exe所在目录 SPIN= d\:\\jspin1-1-5\\spin412.exe
  设置VC++6编译命令 C_COMPILER=cl -w -nologo pan.c
  (估计这是我的一大门槛之一,安装时我选择的路径同样是默认,装好后桌面有jSpin快捷方式,没有进行任何更改时
  同样可以运行,记事本打开C:\jspin\config.cfg,修改如下,其他没有做任何改变
  SOURCE_DIRECTORY=c\:\\jspin\\jspin-examples
  SPIN=c\:\\jspin\\spin.exe
  C_COMPILER_OPTIONS=cl -w -nologo pan.c这一句存在问题可能性较大
  保存退出
(三)双击桌面图标jSpin运行
  有如下正确协议,复制如下代码到左侧窗口,FILE->SAVE->SEM.PML->保存
  byte sem = 1;
  byte critical = 0;
  #define sss (sem>0)
  #define mutex (critical <= 1)
  active proctype P1 () {
do :: 
atomic { sem > 0; sem--; }
critical++;
critical--;
sem++;
od
  }
  active proctype P2 () {
do :: 
atomic { sem > 0; sem--; }
critical++;
critical--;
sem++;
od
  }
 点击Verify按钮出现如下错误
c:\jspin\spin.exe -a SEM.PML ... IO exception
java.io.IOException: CreateProcess: c:\jspin\spin.exe -a SEM.PML error=2done!
c:\mingw\bin\gcc.exe -DSAFETY cl -w -nologo pan.c ... IO exception
java.io.IOException: CreateProcess: c:\mingw\bin\gcc.exe -DSAFETY cl -w -nologo pan.c error=3done!
c:\jspin\jspin-examples\pan -m2000 -X ... IO exception
java.io.IOException: CreateProcess: c:\jspin\jspin-examples\pan -m2000 -X error=2done!

真诚期待高手解决问题,不胜感激~!!!!!!!
所用文件地址如下:
JDKhttp://202.194.89.125/Soft/UploadSoft/jdk-1_5_0_04-windows-i586-p.exe
pc_spin517.ziphttp://spinroot.com/spin/Src/pc_spin517.zip
jspin-4-6.exehttp://stwww.weizmann.ac.il/g-cs/benari/jspin/jspin-4-6.exe
文中的安装说明来自[url=http://210.40.7.188/E'ojc/MXJC/SPIN/000/001.asp][/url]
再次感谢了!!!!!!!!


------解决方案--------------------

------解决方案--------------------
你的问题我又研究了下

如果你只是想运行jspin
那只要安装JDK 、 jspin-4-6.exe 、 mingw.exe 这三项就可以了
按默认的设置安装就行了 jspin已经自带spin.exe了
安装后不用进行修改可以直接使用 
这样安装是通过windows下的gcc来编译的 安装mingw.exe 就是安装这个东西
jspin默认就是用gcc编译的

要是VC++来进行编译,我也试验了下

文章评论

程序员必看的十大电影
程序员必看的十大电影
编程语言是女人
编程语言是女人
Web开发人员为什么越来越懒了?
Web开发人员为什么越来越懒了?
科技史上最臭名昭著的13大罪犯
科技史上最臭名昭著的13大罪犯
老美怎么看待阿里赴美上市
老美怎么看待阿里赴美上市
要嫁就嫁程序猿—钱多话少死的早
要嫁就嫁程序猿—钱多话少死的早
60个开发者不容错过的免费资源库
60个开发者不容错过的免费资源库
我的丈夫是个程序员
我的丈夫是个程序员
程序员应该关注的一些事儿
程序员应该关注的一些事儿
如何区分一个程序员是“老手“还是“新手“?
如何区分一个程序员是“老手“还是“新手“?
10个帮程序员减压放松的网站
10个帮程序员减压放松的网站
每天工作4小时的程序员
每天工作4小时的程序员
Java程序员必看电影
Java程序员必看电影
程序员的一天:一寸光阴一寸金
程序员的一天:一寸光阴一寸金
总结2014中国互联网十大段子
总结2014中国互联网十大段子
 程序员的样子
程序员的样子
程序员眼里IE浏览器是什么样的
程序员眼里IE浏览器是什么样的
老程序员的下场
老程序员的下场
程序员的鄙视链
程序员的鄙视链
10个调试和排错的小建议
10个调试和排错的小建议
“懒”出效率是程序员的美德
“懒”出效率是程序员的美德
一个程序员的时间管理
一个程序员的时间管理
亲爱的项目经理,我恨你
亲爱的项目经理,我恨你
做程序猿的老婆应该注意的一些事情
做程序猿的老婆应该注意的一些事情
写给自己也写给你 自己到底该何去何从
写给自己也写给你 自己到底该何去何从
漫画:程序员的工作
漫画:程序员的工作
5款最佳正则表达式编辑调试器
5款最佳正则表达式编辑调试器
什么才是优秀的用户界面设计
什么才是优秀的用户界面设计
聊聊HTTPS和SSL/TLS协议
聊聊HTTPS和SSL/TLS协议
我跳槽是因为他们的显示器更大
我跳槽是因为他们的显示器更大
初级 vs 高级开发者 哪个性价比更高?
初级 vs 高级开发者 哪个性价比更高?
“肮脏的”IT工作排行榜
“肮脏的”IT工作排行榜
代码女神横空出世
代码女神横空出世
不懂技术不要对懂技术的人说这很容易实现
不懂技术不要对懂技术的人说这很容易实现
程序员都该阅读的书
程序员都该阅读的书
十大编程算法助程序员走上高手之路
十大编程算法助程序员走上高手之路
程序员和编码员之间的区别
程序员和编码员之间的区别
那些争议最大的编程观点
那些争议最大的编程观点
鲜为人知的编程真相
鲜为人知的编程真相
程序员周末都喜欢做什么?
程序员周末都喜欢做什么?
Web开发者需具备的8个好习惯
Web开发者需具备的8个好习惯
如何成为一名黑客
如何成为一名黑客
团队中“技术大拿”并非越多越好
团队中“技术大拿”并非越多越好
看13位CEO、创始人和高管如何提高工作效率
看13位CEO、创始人和高管如何提高工作效率
为啥Android手机总会越用越慢?
为啥Android手机总会越用越慢?
软件开发程序错误异常ExceptionCopyright © 2009-2015 MyException 版权所有