TLC Development

[Miguel Frutos]

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

[Markus Kuppe]

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

[Miguel Frutos]

Hi Markus,

Wow, that's an amazing PR.

I didn't succeed with the step by step guide, probably because I was using the latest Eclipse version. I'm not an eclipse user myself, so maybe I did something wrong. But the instructions in DEVELOPING.md [1] worked for me.

The repo is a bit overwhelming, but hopefully I can pull a thread from here.

Thanks!

Miguel

[1] https://github.com/tlaplus/tlaplus/blob/master/DEVELOPING.md

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/428549CA-87C6-4855-A49B-FE1C96F89876%40lemmster.de.

[Andrew Helwer]

If you only care about the java command-line tools and not the eclipse-based java toolbox GUI, you can confine your interest to the tlatools/org.lamport.tlatools directory. Within that directory the important entities are the src dir, which contains the tool source code, test, which contains the unit tests, and customBuild.xml, which contains Apache Ant definitions constituting the build system.

Andrew