Re: [tlaplus] TLC Development

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

Hi Miguel,

Thank you for volunteering.  We need more people to help with the TLA+ Tools. The tools, including TLC, comprise many different components.  We have a setup guide for an Eclipse-based development environment [1], but we are also in the process of overhauling our build system and improving the contributor experience.

Right now, perhaps, the best way to get started might be to review a recent pull request [2].  This PR introduces subtle changes to the behavior of a core filesystem abstraction in TLC, triggered by an API change in Java.  The PR is an excellent starting point because the Java changes are confined to a single, almost dependency-free class. More importantly, Calvin wrote a TLA+ spec modeling the behavior change.  This could be reviewed even if you are not familiar with or have a distaste for Java.

If you are interested in contributing to the TLA+ Tools long term, consider joining our monthly community meetings [3].

Thanks,
Markus

[1] https://github.com/tlaplus/tlaplus/tree/master/general/ide
[2] https://github.com/tlaplus/tlaplus/pull/907
[3] https://calendar.google.com/calendar/embed?src=cb3f93f188c92378a8fec42b25365ab2a64665d770a8265c1fcec00e03823c6c%40group.calendar.google.com&ctz=America%2FLos_Angeles


> On May 8, 2024, at 1:36 AM, Miguel Frutos <m.frutos@xxxxxxxxx> wrote:
> 
> Hello,
> 
> I was trying to have a look at the source code of TLC to understand a bit more about the inner part of the model checking, but found it a bit overwhelming.
> 
> Is there any guide with how to configure the development environment, and how the code is structured?
> 
> Thanks

-- 
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/428549CA-87C6-4855-A49B-FE1C96F89876%40lemmster.de.