java环境下运行模型检测工具Spin遇到的问题（新手求教）

安装了JDK 1.6，Jspin4-6和mingw-get-inst-20120426.exe之后。检查了一遍都能正常运行。
但是在运行JSPIN时在左匡中输入用promela描述的协议（如下），
按照FILE->SAVE->SEM.PML->保存 步骤运行，结果运行出现这样的错误：
Saved sem.pml
bin\spin.exe -a sem.pml ... done!
c:\mingw\bin\gcc.exe  -DSAFETY  -o pan pan.c ... done!
D:\jspin\jspin-examples\pan  -m2000 -X ... IO exception
java.io.IOException: Cannot run program "D:\jspin\jspin-examples\pan" (in directory "D:\jspin\jspin-examples"): CreateProcess error=2, ϵͳÕҲ»µ½ָ¶done!
具体协议为：
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
  }