Re: [tlaplus] PlusCal sometimes not working in TLA+ Toolbox

[Jaak Ristioja <jaak.r...@xxxxxxxx>]

On 25.11.2015 14:50, Markus Alexander Kuppe wrote:
> what do you mean by unresponsive progress dialog? Are you talking about
> the splash screen or the one that shows up during model checking? If
> it's reproducible, can you share your spec/model.

I'm talking about the dialog that shows up during model checking. It has
a "Run in background" button. It seemed to continue running after model
checking finished and I didn't find a way to close it. I'm sorry but I
can not share my spec/model at this time.

After you last e-mail I found the toolbox unresponsive again. I let the
window manager (KDE) kill it. When I restarted the Toolbox, it had two
tabs: one for the spec and one for the model. I clicked on the model tab
and for a while the mouse cursor changed to indicate "thinking". The
model tab only shows the three regular sub-tabs: "Model Overview",
"Advanced Options" and "Model Checking Results". Now the cursor is back
to normal and the UI is unresponsive. After I minimize+restore the GUI
is not drawn. The htop process table (on the dual CPU VM) shows about
five java processes running, two of them taking nearly 100% of CPU.

Wait... during writing the previous sentence the GUI redrew itself, but
redrawing appears to happen extremely infrequently. It takes the GUI a
very long time to react to hover effects (display button shadow /
display tooltip).

Best regards,
Jaak