Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Explaining causality errors by incremental solving #4

Open
ptal opened this issue Jul 19, 2018 · 2 comments
Open

Explaining causality errors by incremental solving #4

ptal opened this issue Jul 19, 2018 · 2 comments

Comments

@ptal
Copy link
Owner

ptal commented Jul 19, 2018

The compiler just reports that a causality analysis occurred without giving information on the variables that generate this error.
This is a well-known weakness of constraint programming: it is hard to debug (or in this case explain) unsatisfiable instances.
There exists however a bunch of techniques, references and techniques can be found in Chapter 6 of "Making the Most of Structure in Constraint Models", Kevin Leo, 2018.
We could also take advantage of the iterative structure of our problem by testing the satisfiability each time we add a constraint into the model.

@ptal
Copy link
Owner Author

ptal commented Jul 19, 2018

There is another problem with the current technique: models generated share a part of their constraints.
This is for example the case for P ; when C then Q else R, a model is generated for P,C,Q and for P,!C,R and thus have P in common.
Hence, if a constraint in P is invalid, it generates two errors.
For now, to avoid this problem, we stop the causality analysis after the first error.

@ptal ptal changed the title Explaining causality errors Explaining causality errors by incremental solving Jul 23, 2018
@ptal
Copy link
Owner Author

ptal commented Aug 4, 2018

We already perform a postfix addition of the constraints into the CSP model. Therefore, if we solve the sub-problems, we will first test the smallest block of code first, and if they are satisfiable, we test their combinations.
In addition, if we attach the partially solved CSP to each process, we also solve #5.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant