You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
With AG queries, they are always "true" until you find a counter-example, then they are "false", but with a solution. Right now, we are doing the opposite.
In other words: AG queries (safety queries) should be disproven by finding a trace, not proven.
Solutions should be refactored to have:
structquery_answer_t {
query_t q;
std::optional<state_it_t> witnessing_state; // backtraceable - if optional is empty, no trace is availble (yet)bool witnessing_state_is_proof_of_unsat; // when true, then the query is _not_ satisfied
}
or something like that.
See forward_reachability_searcher.cpp:84
The text was updated successfully, but these errors were encountered:
With AG queries, they are always "true" until you find a counter-example, then they are "false", but with a solution. Right now, we are doing the opposite.
In other words: AG queries (safety queries) should be disproven by finding a trace, not proven.
Solutions should be refactored to have:
or something like that.
See forward_reachability_searcher.cpp:84
The text was updated successfully, but these errors were encountered: