论文部分内容阅读
约束出现在很多实际应用之中，例如调度问题、迷宫以及组合优化问题等，MSVL是一种时序逻辑程序设计语言，能够对计算机系统进行建模、仿真与验证。但是，目前MSVL并不能被很方便的用于求解实际生活中的约束问题。本文通过三种方式实现了在MSV建模、仿真与验证工具集中加入求解约束的功能，使其有更广泛的适用性。首先，介绍了投影时序逻辑PTL和MSVL的基本语法和语义，以及MSV工具集的实现原理和基本功能；接着，引入了约束语句的语法；然后，基于上述理论基础，在MSV工具中增加了与约束语句相关的词法和语法，并且通过三种不同的方式(分别为调用MINLP、SMT以及CP求解器)实现了约束求解功能；最后，通过三个实例验证了实现方法的正确性，并且对比了上述三种实现方式，分析结果表明，MINLP和CP方法在求解最优化问题时较SMT方法更优。