search

flyvy-verifier / flyvy

An experimental framework for temporal verification based on first-order linear-time temporal logic. Our goal is to express transition systems in first-order logic and verify temporal correctness properties, including safety and liveness.
BSD 2-Clause "Simplified" License
14 stars 1 forks source link

Missing documentation for inference and temporal-verifier crates #95

Open Alex-Fischman opened 1 year ago

Alex-Fischman commented 1 year ago

See commit 5cce4ab85e9135c7916f394f8cf55a962f1636a6, which was added so that we could get the multiple crates branch merged as quickly as possible and unblock everyone. However, we do want documentation for all our files.

To resolve this issue, uncomment the lines in that commit, and fix all resulting warnings.

It would be great if the original authors of the files in the inference crate could add documentation for them, so that the docs are as accurate as possible.

tchajed commented 1 year ago

@edenfrenkel this isn't urgent but the remaining documentation work is almost all (maybe entirely) in your inference code. When you get a chance it would be great to expand the documentation - even partial progress on any public APIs would be useful.