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

Useless wrapper in verify/error? #96

Closed Alex-Fischman closed 1 year ago

Alex-Fischman commented 1 year ago

In verify/error.rs, there's a struct called SolveError that just wraps a Vec without providing or removing any functionality. Can this wrapper be removed?

tchajed commented 1 year ago

I don't want to remove it since I'd prefer to have errors always be structs; it provides a place to add documentation at the very least, and makes it easier to add more structured data later if needed. The cost of having a little extra work on wrapping/field access is worth it if a refactoring is needed.