TeamAmalgam / kodkod

Kodkod relational model finder
Other
3 stars 0 forks source link

Gracefully terminate if no solutions exist #9

Open mhyee opened 11 years ago

mhyee commented 11 years ago

"In the multi-objective optimizer there are multiple threads, at least two. One does computation and another displays results to the user. These threads communicate with each other through a queue. The computation thread puts things on the queue and the display thread pops them off. When there are no more answers to be found the computation thread puts a poison pill on the queue: that's how the display thread knows that the computation is over."

However, it seems (not 100% sure) that if there are no solutions, the poison pill gets in and the display thread crashes, instead of terminating gracefully.

mhyee commented 10 years ago

I feel that our refactor should have taken care of this. However, we haven't actually verified this.

Quickly edit a model so it has no solutions and run it through. If Moolloy gracefully terminates, close this issue. Otherwise, update this issue.

mhyee commented 10 years ago

We have not actually fixed this. The error is something different now.

I tried this with queens_3_metrics_2, which has no solutions (since it's a 3x3 board), and got the following error:

Exception in thread "main" Fatal error:
Unknown exception occurred: java.util.NoSuchElementException
    at edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod.execute_command(Unknown Source)
    at edu.mit.csail.sdg.alloy4whole.multiobjective.RanMultiobjectiveModel.main(Unknown Source)
Caused by: java.util.NoSuchElementException
    at kodkod.multiobjective.concurrency.BlockingSolutionIterator.next(BlockingSolutionIterator.java:68)
    at kodkod.multiobjective.concurrency.BlockingSolutionIterator.next(BlockingSolutionIterator.java:11)
    at edu.mit.csail.sdg.alloy4compiler.translator.A4Solution$Peeker.next(Unknown Source)
    at edu.mit.csail.sdg.alloy4compiler.translator.A4Solution.solve(Unknown Source)
    ... 2 more