Practical TLA+: Planning Driven Development

© Hillel Wayne 2018

Hillel WaynePractical TLA+https://doi.org/10.1007/978-1-4842-3829-5_4

4. Constants, Models, and Imports

Hillel Wayne¹ 

(1)

Chicago, Illinois, USA

 

In the past few chapters we covered how to write complex specifications. However, our models are fairly rigid. Our knapsack spec from the last chapter had a set of hard-coded values: total capacity of the knapsack, range of values for the items, etc. In this chapter we will use the TLC configuration to simplify and generalize our model, as well as add modularity and better debugging.

Constants

What if we want to change the parameters of a specification on the fly? For example, we might want to first test our spec over a small state space to weed out the obvious errors, and then test it ...