search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
621 stars 140 forks source link

Fixed temporal_deep tests #1180

Closed binghe closed 8 months ago

binghe commented 8 months ago

Hi,

HOL built by Moscow ML is still working, including the HolBdd examples and temporal_deep examples with a SMV checker. When HOL4_SMV_EXECUTABLE is set to NuSMV, nuXmv or NuRV (all from FBK), the self tests in examples/temporal_deep/src/model_check/selftest.sml also still work but there are two unmatched parentheses by last commit (in 2018).

Chun

binghe commented 8 months ago

In #1179, the latest updates to Docker image binghelisp/hol-dev:latest now contains an installation of NuRV [1], which is compatible with the original SMV checker. When pulling this image and building HOL with Moscow ML, all tests under examples/temporal_deep/src/model_check will work, with help of the SMV checker on LTL formulas.

[1] https://es-static.fbk.eu/tools/nurv/

mn200 commented 8 months ago

Thanks for this!