Introduce monitor state when creating a property #104
Conversation
|
Ran some tests. There are no discrepancies so I think it looks good. Interpolant-based model checking is solving less than this baseline, but I'm pretty sure that's not related to this (there was another change to interpolant based model checking since that baseline run).
|
engines/mbic3.cpp
Outdated
| assert(ts_.only_curr(bad_)); | ||
| assert(ts_.only_curr(ts_.init())); | ||
|
|
There was a problem hiding this comment.
A minor thing: I think that these assertions are redundant here since assert(ts_.only_curr(bad_)); is checked already in super::initialize();
Also, assert(ts_.only_curr(ts_.init())) is redundant because we check that in the TS class in the respective functions used to construct init_, but we can keep these assertions here for documentation.
There was a problem hiding this comment.
That's a very good point! I don't feel strongly either way. What do you think -- should we leave it there for documentation or remove it?
There was a problem hiding this comment.
Then I suggest to remove them, just for consistency with the other engine classes that are derived from Prover, and which do not have these assertions.
| ts_.make_sort(BOOL)); | ||
| break; | ||
| } | ||
| catch (SmtException & e) { |
There was a problem hiding this comment.
I am not very familiar with the smt-switch code: is it guaranteed that an SmtException will always be thrown when ts_.make_statevar(...) fails, regardless of the cause of failure? (to avoid getting stuck in the infinite loop)
There was a problem hiding this comment.
Good question -- an SmtException is the parent class for all exceptions thrown by smt-switch, but it is possible that some other type of exception is thrown in the underlying solver and is not caught correctly by smt-switch. In that case, I believe we still wouldn't be stuck in the infinite loop because we'd get an uncaught exception.
|
Thanks for the review! Responded to the comments directly and I'm happy to make changes based on how that discussion goes. |
Co-authored-by: Ahmed Irfan <[email protected]>
| @@ -148,8 +149,7 @@ void Prover::print_coi_info() | |||
| cout << " " << statevar << "\n"; | |||
|
|
|||
| cout << "constraints: \n"; | |||
| for (auto constr : ts_.constraints()) | |||
| cout << " " << constr << "\n"; | |||
| for (auto constr : ts_.constraints()) cout << " " << constr << "\n"; | |||
There was a problem hiding this comment.
is this formatted by git-clang-format?
There was a problem hiding this comment.
Yeah it must have been because I didn't intend to change that code otherwise, except for removing a trailing space.
Automatically introduces a monitor state value (and logs a warning for verbosity >= 1) if the property has inputs or next states in it. This was previously done only for the BTOR2 frontend, but now happens internally in a
Propertyobject. This extends the counterexample trace by one step, but allows us to use any state invariant checking technique (not just unrolling based ones).One disadvantage of this PR is that it modifies the transition system in place. Thus, if we're checking many properties on the same transition system, we could end up with too many monitor state variables. I've opened an issue for that which we can address later.
@leonardt