TeamAmalgam / kodkod

Kodkod relational model finder
Other
3 stars 0 forks source link

Prioritize magnifier tasks in OGIA #42

Open mhyee opened 10 years ago

mhyee commented 10 years ago

Currently, magnifier tasks are only run when all Pareto points have been found.

One of the nice properties of the GIA is that it outputs (Pareto optimal) solutions as they are found. So you can cancel the program and still have some solutions. We don't really get this with the way OGIA currently works.

So we should make it so that a thread searches for a new Pareto point if there are no magnifier tasks to run.

Edit: We might want to be smarter about this. Having all threads on magnifier means we make no progress on finding a new Pareto point. So we might want one thread to always be finding new Pareto points.