[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

On 25.11.2015 14:09, Jaak Ristioja wrote:
> 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).

Hi Jaak,

the newest nightly build [1] does not show this problem anymore.


[1] http://tla.msr-inria.inria.fr/tlatoolbox/ci/products/