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:
- 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:
- Define a tuple of variables in the TLA+ spec; these are the variables you'll use in your view
- Use the VIEW keyword in the MC.cfg file of your model to expose the view above
- Add the view in the TLC advanced options
- Add the -view flag to the TLC command line flags
- 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?
Andrew