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="">
> 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 a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/drcCxafy4Nk/unsubscribe.
To unsubscribe from this group and all its topics, 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.