CODEWITHSUNDEEP
distributed-systemtla+formalize
Oliver Young
Oliver Young

Reputation: 585

Questions about constant operator in TLA+

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?

Upvotes: 1

Views: 98

Answers (1)

Hovercouch
Hovercouch

Reputation: 2314

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?"

Upvotes: 2

Related Questions