# [tlaplus] Re: Error launching TLAPS on SimpleMath.tla and Bug Tracker Link broken

Hi,

I think I found the problem:, line 76 of SimpleMath.tla contains a comment that TLAPS does not seem to like
(*{a, b} \in {{a, b}, c, {d, e}}*)

Greetings,
Michael

> On 19 Nov 2020, at 13:33, Michael Leuschel <michael.leuschel@xxxxxxxxx> wrote:
>
> Hi,
>
> I just downloaded and installed TLAPS 1.4.5 on macOS Mojave using the latest TLA+ Toolbox 1.7.0.
> I wanted to try out TLAPS on some simple maths theorems and chose SimpleMath.tla (that comes with TLC, I think).
> However, there was the error message below.
> When clicking on the Link to submit the bug report and then clicking on “Bug tracker for TLAPS/tlapm" I get an error “requested URL was not found”.
> Hence my message to this group, maybe somebody knows what is happening.
>
> I was able to start TLAPS for the DieHard.tla example (but it has not theorems).
>
> Greetings,
> Michael
>
> <Screenshot 2020-11-19 at 13.23.59.png>
>
> <Screenshot 2020-11-19 at 13.31.39.png>

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.