[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Advanced TLC: views and module overrides

Markus mentioned module overrides in his recent TLC talk, and views came up in an issue on GitHub. Both of these topics are mentioned in the Specifying Systems TLC chapter, but not in enough detail to get them to work. They are of great interest to me in a spec I am currently writing. I have the following questions:
  1. Given a spec with some set of variables, what steps are required to get TLC to run using a view on a subset of those variables? As far as I can tell, we have to do something like the following:
  2. Given a TLA+ module defining some operators, how do I implement those operators in Java and get TLC to use the Java implementation while model-checking?