search

bmoth-mc / bmoth

Model Checker for (a subset of) classical B based on Z3
MIT License
9 stars 1 forks source link

UI: Button to stop model check #75

Closed Mareikes closed 7 years ago

Mareikes commented 7 years ago

if we got an infinite model where our model checker can't find any violations we should be able to halt the check manually

x-moe-x commented 7 years ago

Is it necessary to make doModelCheck(...) interuptable?

wysiib commented 7 years ago

maybe we should make it run in a thread, and put a progress bar in front?

x-moe-x commented 7 years ago

But how to know about the progress?

Lunnaris01 commented 7 years ago

I think some icon showing the process is running would be a good Idea.

wysiib commented 7 years ago

we can't tell about the progress as we do not know how many states will be found eventually. Maybe just some process bar showing that something is happening? Even better, we could have a dialog showing the current size of the queue and the number of states analysed so far.

Lunnaris01 commented 7 years ago

Could it be a good idea to change the modelchecker into an interruptable Thread?

x-moe-x commented 7 years ago

I will implement a method to stop the current checking session, so the executing thread can stop checking on being interrupted.

x-moe-x commented 7 years ago

Model checking can be aborted via ModelChecker::abort() now.