文件名称：zustre:用于Lustre程序的模型检查器和承担保证合同生成器
文件大小：49KB
文件格式：ZIP
更新时间：2024-06-04 03:43:09
checker model lustre Python
祖斯特 Zustre是用于Lustre程序的基于SMT的模块化PDR样式验证引擎。 它也是生成模式感知的假定担保样式正式合同的引擎。 ## License ## Zustre是在经过修改的BSD许可证下分发的。 有关详细信息，请参见。 演示版 依存关系 （可选） Python v。2.7。 （或以上） 汇编 单独构建 cd zustre ; mkdir build ; cd build cmake -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX=run -DLUSTREC_ROOT=LUSTREC_DIR ../ ，其中LUSTREC_DIR是包含的目录。 请注意，您需要事先单独编译LustreC。 cmake --build . 建立祖斯特雷 cmake --build . --target install cmake --
【文件预览】：
zustre-master
----src()
--------reg_test.py(4KB)
--------pick_inv.py(2KB)
--------zustre.py(11KB)
--------z3_utils.py(10KB)
--------utils.py(2KB)
--------Matlab.py(4KB)
--------CexSF.py(6KB)
--------__init__.py(7KB)
--------CMakeLists.txt(1KB)
--------__main__.py(3KB)
--------cocoprinter.py(30KB)
--------CoCoSpec.py(19KB)
--------zustrepy(5KB)
--------sfunction.py(2KB)
--------Cex.py(6KB)
--------LogManager.py(3KB)
--------stats.py(7KB)
----CMakeLists.txt(5KB)
----.travis.yml(1KB)
----LICENSE(2KB)
----cmake()
--------FindLUSTREC.cmake(542B)
--------FindZ3.cmake(922B)
--------TargetArch.cmake(6KB)
--------FindGmp.cmake(620B)
----README.md(3KB)
----tests()
--------automata_counter.lus(919B)
--------const_example.lus(559B)
--------two_counters.lus(481B)
--------cocosepc()
--------traffic.lus(528B)
--------sim2lus_test_1.lus(906B)
--------speed2.lus(1KB)
--------cex_test.lus(480B)
--------automata1.lus(385B)