tlaplus/tlaplus
Feature request: display which conjunct(s) of invariant were violated
開放
#803 建立於 2023年3月22日
Toolscantfixenhancementhelp wanted
倉庫指標
- 星標
- (2,153 顆星)
- PR 合併指標
- (30 天內沒有已合併 PR)
描述
Often I'll have an invariant consisting of a set of conjuncts like:
TypeInvariant ==
/\ x \in Nat
/\ y \in Int
If this invariant is violated, TLC will print out that TypeInvariant was violated but won't say which conjunct. If an invariant consists of a simple non-nested list of conjuncts, it would be a nice feature for TLC to print out which conjunct was violated.