的？”），而Datalog则编码了所有可达到的数据包。对于STM，我们同时提供了查询类型的结果。所有的STM实验是在最小TTL下运行的；例如，Stanford的TTL中的可达性为3，回路检测是4，更高的TTLs很明显的增加了运行时间。我们不对“基准云”提供STM运行时间，因为AIISAT算法不支持不确定性。我们不能在基准云上运行Hassel C，因为HasselC已经硬连接了假设，就像路由端口数量接着详细的命名策略。
NoD在编码所有的解决方案上都要比model checker或者SAT solvers处理一个解决方案要更快。Model checkers 的表现似乎是随着路径长度的增加而指数递减的。甚至AIISAT算法要比Datalog慢大约200倍。对于Stanford测试，HasselC只用了0.9秒钟，要比Datalog更快。对于增量分析，Netplumber和veriFlow也要比Datalog要快。然而，这些已有的工具中，没有一个有能力去更高层次上建模并且建模动态网络就像NoD那样。此外，NoD的速度也是在可以接受范围中。
参考文献：
[1] Colin Scott et al.,Troubleshooting Blackbox SDN Control Software with Minimal Causal Sequences, in SIGCOMM 2014
[2] Thomas Ball et al., VeriCon: Towards Verifying Controller Programs in Softwre-Defined Networks, in PLDI 2014
[3] Nuno P. Lopes et al., Checking Beliefs in Dynamic Networks, in NSDI 2015 [4] https://www.opennetworking.org/sdn-resources/sdn-definition [5] http://eastzone.github.com/atpg/docs/NetDebugSurvey.pdf
[6] Richard Skowyra et al., A verification Platform for SDN-Enabled Applications [7] Fogel Ari et al., A General Approach to Network Configuration Analysis, in USENIX NSDI 2015
[8] http://blog.csdn.net/freezgw1985/article/details/16873677 [9] http://network.51cto.com/network/content2013/SDNkepu/ [10]