Windows环境下如何为Alloy配置electrod/nuXmv求解器？

前置检查 #

• 新开CMD窗口执行nuXmv -v，能正常返回版本号才算PATH配置生效。如果提示找不到命令，先重启电脑让系统环境变量全局加载，再重新校验，很多人加完PATH不重启导致Alloy读不到路径，做无用功。
• 确保你用的Alloy是6.1及以上版本，老版本没有内置Electrod后端，不支持SMV类求解器接入，不用浪费时间尝试。

配置步骤 #

• 启动Alloy，点开顶部菜单栏Options -> Solvers。如果列表里已经有nuXmv选项但是显示灰色不可选，是默认路径匹配不上本地安装位置，直接手动添加新条目即可。
• 点击窗口内的Add按钮，按以下要求填写配置项：
  • 名称栏：填写辨识度高的自定义名称即可，比如本地nuXmv，后续会显示在求解器选择菜单中
  • 求解器类型：下拉选择Electrod (SMV)，不要选成SAT类求解器，类型不匹配会导致调用失败
  • 可执行文件路径：如果已经确认PATH配置生效，直接填nuXmv即可；如果怕系统识别不准，就点旁边的浏览按钮，手动选中nuXmv安装目录下的nuXmv.exe文件
  • 其余启动参数保持默认即可，内置的传参规则已经适配nuXmv的调用要求，不需要手动修改
• 填完所有项后点OK保存配置，回到求解器列表选中刚添加的nuXmv条目，你可以点Set as Default设为默认求解器，也可以在运行具体模型时临时选择。

有效性验证 #

新建一个带时态算子（比如always、eventually）的Alloy模型点击执行，查看执行日志：如果出现nuXmv的进程启动日志，没有报"无法启动求解器"、"找不到可执行文件"类错误，最后能正常返回实例/反例，就说明配置成功。

常见踩坑说明 #

• 加完系统PATH一定要重启Alloy：Alloy基于Java开发，启动时就会加载当时的系统环境变量，不重启无法读取你后续新增的PATH条目
• nuXmv的安装路径不要包含中文、特殊字符或者空格，否则调用时会因为路径转义问题启动失败
• 如果调用时提示nuXmv语法错误，请更换为2.0.0及以上版本的稳定版nuXmv，过旧版本不兼容Electrod生成的SMV文件格式

内容的提问来源于stack exchange，提问作者Juan Benavides