[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Declared variables found undefined during evaluation

From: Leslie Lamport <tlapl...@xxxxxxxxx>
Date: Thu, 23 Aug 2018 13:45:12 -0700 (PDT)
References: <AE18347A-18CA-4563-8A57-92099BAE2FC4@gmail.com> <49DE311F-116D-46BD-800E-001A79938891@gmail.com>

Just to clarify Stephan's response: The spec you wrote is, I believe, legal TLA+ and means what you expect it to mean. However, TLC will handle the liveness property only if P is a constant.

Follow-Ups:
- Re: [tlaplus] Declared variables found undefined during evaluation
  - From: Zixian Cai

References:
- Declared variables found undefined during evaluation
  - From: Zixian Cai
- Re: [tlaplus] Declared variables found undefined during evaluation
  - From: Stephan Merz

Prev by Date: Re: [tlaplus] How can I verify spec satisfies the properties for infinite states?
Next by Date: Re: [tlaplus] Declared variables found undefined during evaluation
Previous by thread: Re: [tlaplus] Declared variables found undefined during evaluation
Next by thread: Re: [tlaplus] Declared variables found undefined during evaluation
Index(es):
- Date
- Thread