search

ptal / bonsai

Programming language based on the synchronous and constraint paradigms
Apache License 2.0
15 stars 0 forks source link

Explaining causality errors by incremental solving #4

Open ptal opened 6 years ago

ptal commented 6 years ago

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 commented 6 years ago

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 commented 6 years ago

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.