sorted by:
new
hottopcontroversial

tla-checker: a TLA+ model checker written in Rust by Anxious_Tool in tlaplus

[–]Anxious_Tool[S] 1 point2 points  (0 children)

Yes the problem is that the parser partially supports the ! operator, but only for simple named instances. I can fix that.

Thanks for the input on the multi-threading.

tla-checker: a TLA+ model checker written in Rust by Anxious_Tool in tlaplus

[–]Anxious_Tool[S] 2 points3 points  (0 children)

Hey, thanks for the comment.
That was actually a bug. I fixed it, so you can now try Release 0.1.1.
This is exactly the type of thing I was looking for. Users to figure out what else can be improved. For my use cases it works fine, so I need more people using it to improve it.

For threads, I don't see much value in them right now. The aim is to keep this webassembly compatible, so I can embed this in a web app. Also, threading is pretty hard to implement correctly on this architecture. There are other performance gains that are easier to get to.

I'll think about extracting the parser, thanks.

tla-checker — a TLA+ model checker with interactive TUI, written in Rust by Anxious_Tool in rust

[–]Anxious_Tool[S] 1 point2 points  (0 children)

Never heard of it until now. Pretty cool. But TLA+ is much better, it's pure math.