tlaplus/tlaplus
Feature request: display which conjunct(s) of invariant were violated
オープン
#803 opened on 2023/03/22
Toolscantfixenhancementhelp wanted
Repository metrics
- Stars
- (2,153 個のスター)
- PR merge metrics
- (30d に merged 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.