PlusCal sometimes not working in TLA+ Toolbox

[Jaak Ristioja]

Hello!

Sometimes when I run the PlusCal translator in the Toolbox, a progress
information window quickly flashes, and I'm back to the editor with
nothing inbetween the \* BEGIN/END TRANSLATION lines. No error is displayed.

This seems to be specific to some .tla files and not others. Is my
800-line PlusCal source too long?

How do I debug this?

Best regards,
Jaak

[Markus Alexander Kuppe]

Hi Jaak,

is there anything related in the .log file in the workspace/.metadata/
directory?

I'm not aware of a spec length restriction.

Cheers
Markus

[Jaak Ristioja]

On 24.11.2015 18:36, Markus Alexander Kuppe wrote:
> On 24.11.2015 17:11, Jaak Ristioja wrote:
>> Sometimes when I run the PlusCal translator in the Toolbox, a progress
>> information window quickly flashes, and I'm back to the editor with
>> nothing inbetween the \* BEGIN/END TRANSLATION lines. No error is displayed.
>>
>> This seems to be specific to some .tla files and not others. Is my
>> 800-line PlusCal source too long?
>>
>> How do I debug this?
>
> Hi Jaak,
>
> is there anything related in the .log file in the workspace/.metadata/
> directory?

Ok, so that's where the log file is. Looks like a
java.lang.ArrayIndexOutOfBoundsException at
pcal.PcalFixIDs.FixMultiprocess(PcalFixIDs.java:194).

Attached the log file.

Best regards,
Jaak

[Markus Alexander Kuppe]

On 24.11.2015 17:48, Jaak Ristioja wrote:
> Ok, so that's where the log file is. Looks like a
> java.lang.ArrayIndexOutOfBoundsException at
> pcal.PcalFixIDs.FixMultiprocess(PcalFixIDs.java:194).
>
> Attached the log file.

Hi Jaak,

can you give the current nightly build [1] a try? It seems your problem
has already been fixed [2].

Thanks
Markus

[1] http://tla.msr-inria.inria.fr/tlatoolbox/ci/products/
[2]
http://tlaplus.codeplex.com/SourceControl/changeset/66731c044a0f7e35e5b3674a2a3ef4623f853008

[Jaak Ristioja]

Indeed! The nightly I tried does not have this problem. Thanks!

However it seems to have problems with the progress dialog not closing
properly. After some clicking around the GUI became totally
unresponsive, not even repainting itself after minimize+restore.

Are there any plans for the next TLA Toolbox (bugfix) release?

Thanks,
Jaak

[Markus Alexander Kuppe]

On 25.11.2015 13:34, Jaak Ristioja wrote:
> However it seems to have problems with the progress dialog not closing
> properly. After some clicking around the GUI became totally
> unresponsive, not even repainting itself after minimize+restore.
>
> Are there any plans for the next TLA Toolbox (bugfix) release?

Hi Jaak,

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.

There are plans for a new TLA+ Toolbox release, but it's too early to
communicate any dates.

Thanks
Markus

[Jaak Ristioja]

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

[Markus Alexander Kuppe]

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.

Cheers
Markus

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

[Jaak Ristioja]

On 26.11.2015 18:13, Markus Alexander Kuppe wrote:
> the newest nightly build [1] does not show this problem anymore.

I did some quick tests and I can confirm that the nightly dated
26-Nov-2015 16:29 does not have this problem. Thanks! :)

Jaak