CN: Check countermodels

[cassiatorczon]

When the solver returns a countermodel, checks resources not given to the solver to see if their outputs in the countermodel could actually have come from those resources. (Undecidable in general, so this can return "unknown".)

[dc-mak]

Looking good - couple of things, but happy to ship and address in a follow-up as well if pragmatic.

[dc-mak]

Whoever squashes and merges this in, please make sure the commit message contains the top comment on this PR.

[cp526]

It looks like it's now just the formatting that's failing. When that's fixed, and if you're happy, we can go ahead and merge. Probably we'll have to do the squash-and-merge option.

[cassiatorczon]

Sorry, I should have left a comment - I was just debugging, one of the last set of changes seems to have introduced a bug. (The bug just seems to cause checkPred to miss some predicates it previously correctly identified as invalid. It doesn't show any erroneous information.)

[cp526]

Sorry, I should have left a comment - I was just debugging, one of the last set of changes seems to have introduced a bug. (The bug just seems to cause checkPred to miss some predicates it previously correctly identified as invalid. It doesn't show any erroneous information.)

Ah, sorry, I had assumed this was finished. In that case, best to make a small new PR with a fix (rather than reverting committed changes, I think).

[dc-mak]

Whoever squashes and merges this in, please make sure the commit message contains the top comment on this PR.

I would very much like to improve our commit standards and cooperation on this would be much appreciated. If you have not reviewed this in a while, please take a moment to remind yourself of this. If you disagree, please open a separate issue and explain what and why.
https://github.com/rems-project/cerberus/blob/master/backend/cn/CONTRIBUTING.md#git-guidelines

I have struggled with the uninformative messages and non-atomic commits often enough in this repo to have wasted a lot time and effort. On the other hand, when the commits are small and the messages accurate, though this meant a little bit of extra work for the original author, this helped tremendously with understanding, debugging, maintaining, updating, refactoring, catching regressions, and adding new features.

Having tests and reasonable commits, including on development branches helps avoid regressions and bugs.