《表1 实验用例参数：线性时序逻辑公式的可监控性量化算法》

  提示：宽带有限、当前游客访问压缩模式

本系列图表出处文件名：随高清版一同展现

《线性时序逻辑公式的可监控性量化算法》

1. 获取 高清版本忘记账户？点击这里登录

1. 下载图表忘记账户？点击这里登录

根据MPMC算法，我们设计并实现了原型系统工具monic.monic是在Linux环境下基于Spot[14]，并使用C++语言和shell脚本语言共同进行开发的，可通过命令行的方式运行．考虑到算法的性能会受到公式规模大小的影响，因此，我们利用Spot工具进行随机用例公式集合的生成．Spot工具可以通过设置LTL公式的原子命题个数及语法树大小（公式长度）来随机生成不同的公式，每个用例集合为一百个LTL公式，用例公式的参数设计如表1所示，表中的ap＿nums表示原子命题个数，length表示公式的长度．本次实验的机器配置为8G内存，双核CPU，实验使用Ubuntu16.04的64位Linux操作系统，gcc 5.4.0编译器．