由于QWebEngine只支持VS编译，在程序发布时各种VC运行时真的让人很崩溃，感谢初雨开源的VC_LTL让我们从VC运行时解脱出来。记录一下编译过程。 1.编译环境： Windows10x64+VS2019社区版+Python2.7+Perl5.28.1+Ruby2.6.3+LLVM6.0; Qt5.12.8+ICU4C66+OpenSSl1.1.1d+VC-LTL4.1.0.2 2.编译脚本

这里记录一下学习LTL2BA和SPIN实现LTL satisfiability checking 1. LTL satisfiability checking关注这样一类问题：对于一个系统，给定一个由线性时序逻辑（LTL）描述的性质，判断系统是否具有该性质，解决该问题的理论方法之一简单理解是将LTL性质转换为等价的Buchi自动机，再列举系统所有的运行轨迹，检验这些运行轨迹能否使得Buchi自动

系统结构 smv_parser,对smv_parser的结果进行分析 突发性wet，比如水泼了 -> State: 33.7 <-homePresentState = presentruninfan12.timer = 1runinfan27.timer = 2runinfan61.timer = 3runinalarm.timer = 3-> State: 33.8 <-homewate