JAVA环境下SPIN模型检测工具安装的有关问题（新手第一问，谢谢了）
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++来进行编译，我也试验了下
弱弱的问：我还站在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++来进行编译，我也试验了下