Index

Tests by plug feature StringSet; CLI Option: -workers 1

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
347e4ce30c32168e44ce7f2f77cd3f25d788df3d Apalache In StringSet True Failed: TLC result is correct. Apalache does not support STRING expression (a set of all strings)
5b442ba072d614832a279cd934bf72d58bd3e78a Apalache In StringSet False Failed: TLC result is correct. Apalache does not support STRING expression (a set of all strings)
064dd30eed6c195807520cce55c2951896b522e1 Apalache NotIn StringSet True Failed: TLC result is correct. Apalache does not support STRING expression (a set of all strings)
bb44bba33b90384001583991619e8a9549d1930f Apalache NotIn StringSet False Failed: TLC result is correct. Apalache does not support STRING expression (a set of all strings)
19eab976bfc6843b55c1c83e20a62d6ab2ea0e70 TLC with reduction strategy:
  • Case Feature: For finite R replace [D -> R] with explicit function set enumeration; for infinite R replace (f \in [D -> R]) with conjunction (DOMAIN f = D /\ (\A x \in D : f[x] \in R))
FunSet StringSet True Passed
fbd1d04ed25032116100a976f7e6c69c81c82ac4 TLC with reduction strategy:
  • Case Feature: For finite R replace [D -> R] with explicit function set enumeration; for infinite R replace (f \in [D -> R]) with conjunction (DOMAIN f = D /\ (\A x \in D : f[x] \in R))
FunSet StringSet False Passed
bbb8ccacc32a8f3ac6da35221f15a260fa0e8ad2 TLC with reduction strategy:
  • Case Feature: For finite R replace [field : R] with explicit function set enumeration; for infinite R replace (f \in [field : R]) with conjunction (DOMAIN f = {'field'} /\ f['field'] \in R)
RecordSet StringSet True Passed
2d60ec7d2fd9c4bdaaf79bfce7151b695c128c80 TLC with reduction strategy:
  • Case Feature: For finite R replace [field : R] with explicit function set enumeration; for infinite R replace (f \in [field : R]) with conjunction (DOMAIN f = {'field'} /\ f['field'] \in R)
RecordSet StringSet False Passed
946adc71b46ca335f4f2296b5e2663058d378365 Apalache SeqSeq StringSet True Failed: TLC model check results are correct. Apalache does not support STRING (a set of all strings)
a181954a9ed6484934a9100b891c47b77136b55a Apalache SeqSeq StringSet False Failed: TLC model check results are correct. Apalache does not support STRING (a set of all strings)
80365cdaa2bed0d9aa9511dfd48d4b9a31534e63 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet StringSet True Passed
6a3afb40f2c51585c888ce7a17a59a625491fe38 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet StringSet False Passed