CTL 模型检查器（ctlmc）基于 JavaBDD 库实现，使用了 BDD 技术

CTL模型检查 ，使用 （ 库）实现。 用法 Usage: program (CTL specification) (path to model file) e.g.: program 'AG(Not(And("c1"="T", "c2"="T")))' "model.fsm" 参数： CTL 规范（例如Imply(AG("t1"="T"), AF("c1"="T")) ）； 模型文件的路径，采用具有以下限制： 所有国家都必须通过其原子命题的价值得到明确的识别。 快速开始 安装和 使用make test运行make test 用make package准备 jar make package 使用java -jar /path/to/ctl-model-checking.jar 'AG(Not(And("c1"="T", "c2"="T")))' ./src/test/resou