MSVL的约束扩展及其应用
| 摘要 | 第1-4页 |
| Abstract | 第4-7页 |
| 第一章 绪论 | 第7-13页 |
| ·研究背景 | 第7-8页 |
| ·时序逻辑与时序逻辑程序设计语言 | 第8-10页 |
| ·约束求解现状 | 第10-11页 |
| ·研究内容和组织结构 | 第11-13页 |
| 第二章 MSVL—建模、仿真和验证程序设计语言 | 第13-25页 |
| ·投影时序逻辑 | 第13-16页 |
| ·建模、仿真与验证语言 MSVL | 第16-20页 |
| ·MSVL 建模、仿真与验证工具 | 第20-24页 |
| ·本章小结 | 第24-25页 |
| 第三章 MSVL 中约束语句的语法与语义 | 第25-31页 |
| ·理论基础 | 第25页 |
| ·约束语句 | 第25-27页 |
| ·确定变量值的方式 | 第27页 |
| ·求解约束的方式 | 第27-28页 |
| ·SNF | 第28-29页 |
| ·本章小结 | 第29-31页 |
| 第四章 MSV 约束求解的具体实现 | 第31-51页 |
| ·词法和语法部分的实现 | 第31-32页 |
| ·MSVL 建模、仿真与验证工具界面修改 | 第32-33页 |
| ·SNF 到 NF 的转换 | 第33-34页 |
| ·调用 MINLP 求解器 | 第34-39页 |
| ·调用 SMT 求解器 | 第39-46页 |
| ·使用 CP 求解器 | 第46-50页 |
| ·本章小结 | 第50-51页 |
| 第五章 应用实例 | 第51-61页 |
| ·职员时间安排 | 第51-53页 |
| ·生产问题 | 第53-55页 |
| ·礼品采购 | 第55-57页 |
| ·实例分析 | 第57-59页 |
| ·本章小结 | 第59-61页 |
| 第六章 总结与展望 | 第61-63页 |
| ·总结 | 第61页 |
| ·展望 | 第61-63页 |
| 致谢 | 第63-65页 |
| 参考文献 | 第65-69页 |
