Questions about constant operator in TLA+

Question

I am reading book "Specifying Systems" recently. In Chapter 5, Leslie define constant operator Send(,,,).

I am confused about how to assign value (True/False) to this constant expression? Do we need to assign True/False to every (p, v, m, m') in the TLC model checker?

Answer 1

You can assign to Send in two ways:

1. If you instantiate it in another module, you can pass in the operator you want with WITH: Instance Foo WITH Send <- Op \*...
2. You can assign an operator in TLC, under "What is the model?"