What temporal formula to use for knapsack problem?

Question

In "Practical TLA+" by Hillel Wayne, Chapter 3 goes over an implementation of the Knapsack Problem in PlusCal.

Although I understand the implementation, I don't understand how to run it. He mentions:

Since we’re adding a PlusCal spec, remember to remove “evaluate constant expression” and set “What is the behavior spec?” to “Temporal formula.” When you run this, you should get something like what is shown in Figure 3-3.

What's the "Temporal Formula"? Where is it in the Model menu? Alternatively, how would I run this using the VSCode TLA+ plugin? I feel like I missed some details I need to actually run/verify this specification.

Answer 1

TLA+ specifications can specify different things, not only iterative algorithms. The knapsack.tla that you have linked specifies the problem and the definition of an optimal solution without describing a good way to really find it with a computer.

ValidKnapsacks(itemset) ==
  {sack \in [Items -> 0..4]: KnapsackSize(sack, itemset) <= Capacity}

[Items -> 0..4] is the set of all possible mappings from Item to the sizes 0..4. The optimal solution is in the subset that fits in a knapsack of size Capacity, hence the expression KnapsackSize(sack, itemset) <= Capacity.

Another TLA+ definition defines which one of the knapsacks is the best of them all in an impressively high-level way:

BestKnapsack(itemset) ==
  LET all == ValidKnapsacks(itemset)
  IN CHOOSE best \in all:
    \A worse \in all \ {best}:
      KnapsackValue(best, itemset) > KnapsackValue(worse, itemset)

It basically says: among all of the valid knapsacks, the best knapsack is the one that is better (higher KnapsackValue) than all others.

What you are looking for is an specification of an iterative algorithm that matches this solution specification. The specification of the algorithm will have Init and Next formulas and then you can check that it eventually terminates — usually called Termination — and the state variable storing the knapsack would then contain the BestKnapsack.

But you can "run" these definitions by typing an expression in the "Evaluate Constant Expression" box.

The author also wrote two refined definitions of BestKnapsack — BestKnapsackOne and BestKnapsackTwo. They are still functional and we call them refined because they are getting closer to something implementable in an iterative algorithm.

You can evaluate them just like done above for BestKnapsack(HardcodedItemSet). They are correct refinements if they match the output of BestKnapsack for all possible inputs. Since this is model checking, "all possible inputs" is qualified with "up to a certain size" and we assume (or prove) that the solution extends to any size.

Answer 2

It's under "model overview > what is the behavior spec".