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

[Michael Leuschel <michael.leuschel@xxxxxxxxx>]

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.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/F828AFD2-EAD5-460B-9B57-08762EB87D92%40gmail.com.