search

Apress / practical-tla-plus

Source Code for 'Practical TLA+' by Hillel Wayne
Other
287 stars 67 forks source link

Fix typo of constant in knapsack.tla. #14

Open isislovecruft opened 3 years ago

isislovecruft commented 3 years ago

The CAPACITY constant should be upper-cased.

isislovecruft commented 3 years ago

Also thanks for the great book! It's been quite a helpful learning resource.

hwayne commented 3 years ago

Interesting; I looked through the book and I don't think I use CAPACITY anywhere, just Capacity. Would you mind sharing the code you have that's causing the problem?

isislovecruft commented 3 years ago

The first instance of the variable is described as a constant, i.e.:

EXTENDS TLC, Integers, Sequences

PT == INSTANCE PT

CAPACITY == 7

Items == {"a", "b", "c"}

Before (I think?) you later move on in the next chapter (?? sorry don't have the book in front of me at the moment) to explain placing constants such as these directly into the model checker.