-
- Downloads
Reduce (SUBSET A \subseteq SUBSET B) to (A \subseteq B) to avoid its
inherent exponential blowup. [Feature][TLC]
Showing
- tlatools/src/tlc2/tool/Tool.java 1 addition, 6 deletionstlatools/src/tlc2/tool/Tool.java
- tlatools/src/tlc2/value/Enumerable.java 1 addition, 0 deletionstlatools/src/tlc2/value/Enumerable.java
- tlatools/src/tlc2/value/EnumerableValue.java 40 additions, 0 deletionstlatools/src/tlc2/value/EnumerableValue.java
- tlatools/src/tlc2/value/IntervalValue.java 11 additions, 1 deletiontlatools/src/tlc2/value/IntervalValue.java
- tlatools/src/tlc2/value/SetCapValue.java 1 addition, 1 deletiontlatools/src/tlc2/value/SetCapValue.java
- tlatools/src/tlc2/value/SetCupValue.java 1 addition, 1 deletiontlatools/src/tlc2/value/SetCupValue.java
- tlatools/src/tlc2/value/SetDiffValue.java 1 addition, 1 deletiontlatools/src/tlc2/value/SetDiffValue.java
- tlatools/src/tlc2/value/SetEnumValue.java 1 addition, 1 deletiontlatools/src/tlc2/value/SetEnumValue.java
- tlatools/src/tlc2/value/SetOfFcnsValue.java 1 addition, 1 deletiontlatools/src/tlc2/value/SetOfFcnsValue.java
- tlatools/src/tlc2/value/SetOfRcdsValue.java 1 addition, 1 deletiontlatools/src/tlc2/value/SetOfRcdsValue.java
- tlatools/src/tlc2/value/SetOfTuplesValue.java 1 addition, 1 deletiontlatools/src/tlc2/value/SetOfTuplesValue.java
- tlatools/src/tlc2/value/SetPredValue.java 1 addition, 1 deletiontlatools/src/tlc2/value/SetPredValue.java
- tlatools/src/tlc2/value/SubsetValue.java 11 additions, 1 deletiontlatools/src/tlc2/value/SubsetValue.java
- tlatools/src/tlc2/value/UnionValue.java 1 addition, 1 deletiontlatools/src/tlc2/value/UnionValue.java
- tlatools/test-model/EmptySubsetEq.cfg 4 additions, 0 deletionstlatools/test-model/EmptySubsetEq.cfg
- tlatools/test-model/EmptySubsetEq.tla 13 additions, 0 deletionstlatools/test-model/EmptySubsetEq.tla
- tlatools/test-model/SubsetEq.cfg 4 additions, 0 deletionstlatools/test-model/SubsetEq.cfg
- tlatools/test-model/SubsetEq.tla 22 additions, 0 deletionstlatools/test-model/SubsetEq.tla
- tlatools/test/tlc2/tool/EmptySubsetEqTest.java 65 additions, 0 deletionstlatools/test/tlc2/tool/EmptySubsetEqTest.java
- tlatools/test/tlc2/tool/SubsetEqTest.java 55 additions, 0 deletionstlatools/test/tlc2/tool/SubsetEqTest.java
Loading
Please register or sign in to comment