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

Prime missing from mutable axioms in SAT checker #158

Open edenfrenkel opened 11 months ago

edenfrenkel commented 11 months ago

Shouldn't there be a prime added to the mutable axioms in the line below? I think that the idea was to add all axioms to the initial states, and then only the mutable ones to post-states of a transition.

https://github.com/vmware-research/temporal-verifier/blob/343eb699ccbec27620c4002089554ffeeb97efd8/bounded/src/sat.rs#L42

edenfrenkel commented 11 months ago

This also appears to be the case in bdd.rs and smt.rs:

https://github.com/vmware-research/temporal-verifier/blob/343eb699ccbec27620c4002089554ffeeb97efd8/bounded/src/bdd.rs#L66

https://github.com/vmware-research/temporal-verifier/blob/343eb699ccbec27620c4002089554ffeeb97efd8/bounded/src/smt.rs#L29

Alex-Fischman commented 11 months ago

Seems like a bug. Is there a simple test we could add to check that it's wrong?

odedp commented 11 months ago

I'm not even sure we mean to support mutable axioms, but the idea would be something like:

mutable p: bool
mutable q: bool

assume always q <-> p # mutable axiom
assume p # init
assume always p' <-> (p & q) # tr
assert always p # safety