Index

Failed test cases with explanation

This page is an index of all failed test cases. Every failed test case must have an associated explanation. There must be no failed tests without explanation

Test Cases

Id Type Case Feature Plug Feature Check Deadlock Test Failure Explanation Test Models
ab78aa39fe9beb288acc2b0858d326c89c384394 Apalache AndProp BoolFalse True TLC reports an error if it sees trivially false property. Whereas Apalache returns violation
5f286ab4bd180ba58d337bae341c7399907d0125 Apalache AndProp BoolFalse False TLC reports an error if it sees trivially false property. Whereas Apalache returns violation
347e4ce30c32168e44ce7f2f77cd3f25d788df3d Apalache In StringSet True TLC result is correct. Apalache does not support STRING expression (a set of all strings)
5b442ba072d614832a279cd934bf72d58bd3e78a Apalache In StringSet False TLC result is correct. Apalache does not support STRING expression (a set of all strings)
064dd30eed6c195807520cce55c2951896b522e1 Apalache NotIn StringSet True TLC result is correct. Apalache does not support STRING expression (a set of all strings)
bb44bba33b90384001583991619e8a9549d1930f Apalache NotIn StringSet False TLC result is correct. Apalache does not support STRING expression (a set of all strings)
85de1265e6ddc5777839a5372c6cb145958cec88 Apalache Choose BoolFalse True CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
e9af4b5dda8a82ec1c6e9d135089645fb4fded7d Apalache Choose BoolFalse False CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
cc558a2e9f56efa6d0c6a991647611410173c8f4 Apalache Choose And True CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
c530df788f11eab722295a74084444a71942868f Apalache Choose And False CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
6f4b6450456ea77d11909cabd20cdee0a7323965 Apalache Choose Not True CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
f2f82f385106fcf3529bcb41555fcf0e475d4ab8 Apalache Choose Not False CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
34ae665676973327b27a581ad0eaa89dab85247a Apalache Choose Ne True CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
fef49c794ebed4050d2c975d336b40177678bffb Apalache Choose Ne False CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
910abb8211bdd4e49b0b5c78224ad41d8b78fad1 Apalache Choose NotIn True CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
f33b2188a4f969e97c7a0e8e996f37d9c8b02e04 Apalache Choose NotIn False CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
b9f3d8e711282828d92e27c533085dae5d539420 Apalache Choose Prime True CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
b97daa0d0f86ec9dcc7a7729ac2289f9802425f7 Apalache Choose Prime False CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
55f95aef57f44226000613b2eae7fb71e80ed346 Apalache Choose NumLt True CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
05c14cc9b8e2d432a5d3b33fe26833d1bbcaa14c Apalache Choose NumLt False CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
4493f66012b2bb44826f65d0defa60c9ca91e152 Apalache Choose NumLe True CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
fd1f4c2fa95da9521dd80b2b24cfbce6a63fbc68 Apalache Choose NumLe False CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
efcbb86d8e825035422ef00dabb32e954a932280 Apalache Choose SubsetEq True CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
c2e7701c74244b41eb1004ddb9a7e058a47a0c1a Apalache Choose SubsetEq False CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
6c65754b60c324fac1386bc062d7a257290df344 Apalache Choose Equivalence True CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
9580c4c94498621cae1061cf1b62dbd20530e314 Apalache Choose Equivalence False CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
65cf83d03843a162e4db3125fda5c3129da22212 Apalache Choose BagBagIn True CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
8a3d42c2decdc31f60dacb204bb371dd57296414 Apalache Choose BagBagIn False CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
60c7365b4ab7bd2051d5d3a1e2bdd53e417a28d4 Apalache Choose BagSubsetEqBag True CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
79f8bff2282b53f2375f9055f6f0d44e921b2f5d Apalache Choose BagSubsetEqBag False CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
c13904bb75faf80f894aea118a68219ddc797f11 Apalache ChooseInDef InDef2 True Apalache does not support tuple syntax in CHOOSE, e.g. CHOOSE <> \in S
f3e19c279e6d80a435e9c02808f6e1a4c5568a27 Apalache ChooseInDef InDef2 False Apalache does not support tuple syntax in CHOOSE, e.g. CHOOSE <> \in S
cdf78ceed0b53146c6672f9140c27fd4bb68da5b Apalache FunApp TupleEmpty True TLC reports an error if there is an attempt to apply a function with value not from its domain. Apalache is unable to detect such situation and returns arbitrary value.
a4604139020fc219015253d4a621cfdf1a4c7cef Apalache FunApp TupleEmpty False TLC reports an error if there is an attempt to apply a function with value not from its domain. Apalache is unable to detect such situation and returns arbitrary value.
b180a5b4624bd8aea0a581e8da5e3aacda085a61 Apalache FunApp SeqTail True SeqTail produces empty sequence and TLC reports an error if there is an attempt to apply a function with value not from its domain. Apalache is unable to detect such situation and returns arbitrary value.
b340fe3b08248a58461c6d0e26d654c6462d3059 Apalache FunApp SeqTail False SeqTail produces empty sequence and TLC reports an error if there is an attempt to apply a function with value not from its domain. Apalache is unable to detect such situation and returns arbitrary value.
1b80418d75c0f0644d7909116df20d2ce863a964 Apalache Except0 TupleEmpty True CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
ea53af8dd5d5e1b94168ffe2b33a00e5becc32a0 Apalache Except0 TupleEmpty False CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
aa5392bc0869e89bde5088be9e82ae04069e3c73 Apalache Except0 DefFunRecursive True TLC result is correct. The reason they are different is CHOOSE operator, which is allowed to return different values for TLC and Apalache if applied to a set with more than one element. Moreover, in this case, Apalache produces result, which violates TLA+ CHOOSE semantics
fd438e654d87e6c621db9cc8ef25d6b1e6c7a8d1 Apalache Except0 DefFunRecursive False TLC result is correct. The reason they are different is CHOOSE operator, which is allowed to return different values for TLC and Apalache if applied to a set with more than one element. Moreover, in this case, Apalache produces result, which violates TLA+ CHOOSE semantics
1388c118def13e467811caae1e2c5aa49f9d1e13 Apalache Except0 SeqConcat True Both results are correct. The reason they are different is CHOOSE operator, which is allowed to return different values for TLC and Apalache if applied to a set with more than one element. In this case, SeqConcat function from Sequences standard module is used to add one more element into non empty sequence
9d9e6f88b9f6d5ce7ea072d881d513f0f97ccb57 Apalache Except0 SeqConcat False Both results are correct. The reason they are different is CHOOSE operator, which is allowed to return different values for TLC and Apalache if applied to a set with more than one element. In this case, SeqConcat function from Sequences standard module is used to add one more element into non empty sequence
e12db5064497d0de3d9b20ce5bd6ff71169cd11b Apalache Except0 SeqTail True Except0 uses CHOOSE to select an argument. CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
8a70e1ffbdd262912cbcd8e82292579147ec57a7 Apalache Except0 SeqTail False Except0 uses CHOOSE to select an argument. CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
cdb1ba69f63bc435b34e165b27031eac3bbd21eb Apalache Except0 SeqAppend True Both results are correct. The reason they are different is CHOOSE operator, which is allowed to return different values for TLC and Apalache if applied to a set with more than one element. In this case, Append function from Sequences standard module is used to add one more element into non empty sequence
6b0fa28307d11363d42c7c9bcc0c47f188897158 Apalache Except0 SeqAppend False Both results are correct. The reason they are different is CHOOSE operator, which is allowed to return different values for TLC and Apalache if applied to a set with more than one element. In this case, Append function from Sequences standard module is used to add one more element into non empty sequence
4142febf3f1f73ebb34b120aa12dc0bb2de8b6fd Apalache NumPlus NumMaxInt True TLC internally represents integers as 32 bit numbers and reports an error if the value is overflowed. Apalache is unable to detect overflows
1745d72d9d851029e3331ff2327ed2ce209afee8 Apalache NumPlus NumMaxInt False TLC internally represents integers as 32 bit numbers and reports an error if the value is overflowed. Apalache is unable to detect overflows
ebfc33eff1b8ad16fe92ed6a179ac451d0dac89e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Boxed True TLC expects temporal properties to be specified directly without using operators or LET expression. Otherwise it reports an error
a1dc6ecff969a30f8b2a4fd310b4f54b0b3ff77a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Boxed False TLC expects temporal properties to be specified directly without using operators or LET expression. Otherwise it reports an error
b2764bdde952b581ea57a9b4cc3c9d15e04cefa9 Apalache Def1 Boxed True There is a known TLC bug (https://github.com/tlaplus/tlaplus/issues/720), which causes TLC to report an error, when a parameterized operator is used to specify a property
41b3104fca3384e9525d42ba801375965de689db Apalache Def1 Boxed False There is a known TLC bug (https://github.com/tlaplus/tlaplus/issues/720), which causes TLC to report an error, when a parameterized operator is used to specify a property
147e8a4cffe636b65800f847b08f93ff7768dd49 Apalache Def2 Boxed True There is a known TLC bug (https://github.com/tlaplus/tlaplus/issues/720), which causes TLC to report an error, when a parameterized operator is used to specify a property
1374059dc9765e9c8f151f32751f7a17f4a2d57b Apalache Def2 Boxed False There is a known TLC bug (https://github.com/tlaplus/tlaplus/issues/720), which causes TLC to report an error, when a parameterized operator is used to specify a property
700686892478b230bbe283a468506893a0efaf04 Apalache Def1Recursive Boxed True There is a known TLC bug (https://github.com/tlaplus/tlaplus/issues/720), which causes TLC to report an error, when a parameterized operator is used to specify a property
f804f1d679b5f3101dd683d0c661e28532e4e8b2 Apalache Def1Recursive Boxed False There is a known TLC bug (https://github.com/tlaplus/tlaplus/issues/720), which causes TLC to report an error, when a parameterized operator is used to specify a property
2f0bb8c183b4afc95546b875ffc45beb24e13230 Apalache ConstantRank1 ConstantRank1 True TLC doesn't allow to use constant as a replacement value for another constant in CFG, even though the former constant is fully defined at this point
fddb90daec356c4b98a52883ae4cff1fb9b6875e Apalache ConstantRank1 ConstantRank1 False TLC doesn't allow to use constant as a replacement value for another constant in CFG, even though the former constant is fully defined at this point
3f3001acd9119182626f3574409308511d49d62e Apalache Enabled Prime True TLC model check results are correct. Apalache does not support ENABLED operator and if used with prime operator it is irreducible to equivalent ENABLED-free form
c7f97baecf90cb807d26ee99123473a6f8b317f7 Apalache Enabled Prime False TLC model check results are correct. Apalache does not support ENABLED operator and if used with prime operator it is irreducible to equivalent ENABLED-free form
b25a22e9df9367b51dc51b5adb0e198e943d03b5 Apalache Lambda Boxed True TLC does not support boxed operator in LAMBDA expressions and reports an error
4435a5467f708d6ab63fc8edd9966dbc27a3e96e Apalache Lambda Boxed False TLC does not support boxed operator in LAMBDA expressions and reports an error
a110750136d046336d0a5077f28cefa7d7a38605 Apalache Unchanged Variable True TLC model check results are correct. Specification uses UNCHANGED twice in the same action and Apalache complains about spurious manual assignment, because it is unable to detect that the second usage is just no-op
d621f2ef4ad3be8f4e084ccd91d1730804f2a9c8 Apalache Unchanged Variable False TLC model check results are correct. Specification uses UNCHANGED twice in the same action and Apalache complains about spurious manual assignment, because it is unable to detect that the second usage is just no-op
e7d5262aa94a255dfbd4ba5e2f1e9a54c97c7e4f Apalache SeqSeq NatSet True TLC model check results are correct. Apalache is unable to check the model, SeqSeq replacement does not work with infinite sets (Nat)
2588a3aac4ad1d167993af497aa0ceab3769e752 Apalache SeqSeq NatSet False TLC model check results are correct. Apalache is unable to check the model, SeqSeq replacement does not work with infinite sets (Nat)
c17231d50527c3e5fdfc42fbb77a8cb24db6f25b Apalache SeqSeq IntSet True TLC model check results are correct. Apalache is unable to check the model, SeqSeq replacement does not work with infinite sets (Int)
072786e1f8f0bf2d59e8b8468ac417a79ea7f6dc Apalache SeqSeq IntSet False TLC model check results are correct. Apalache is unable to check the model, SeqSeq replacement does not work with infinite sets (Int)
946adc71b46ca335f4f2296b5e2663058d378365 Apalache SeqSeq StringSet True TLC model check results are correct. Apalache does not support STRING (a set of all strings)
a181954a9ed6484934a9100b891c47b77136b55a Apalache SeqSeq StringSet False TLC model check results are correct. Apalache does not support STRING (a set of all strings)
241439717be0ec493be023b444bdb8c4262c80ed Apalache SeqSubSeq TupleEmpty True TLC requires the second argument of SeqSubSeq to be in domain of the sequence and returns an error otherwise. Apalache always returns some sequence
40db46ac9db7ea5895d1f9d252f78ddbeed1317f Apalache SeqSubSeq TupleEmpty False TLC requires the second argument of SeqSubSeq to be in domain of the sequence and returns an error otherwise. Apalache always returns some sequence
e482c5a76e7f757e9d4a414b2d9e947d4f9f9d5a Apalache SeqSubSeq NumZero True TLC requires the second argument of SeqSubSeq to be in domain of the sequence and returns an error otherwise. Apalache always returns some sequence
82060af70766c1abbf3b87848db5bee5b514b36c Apalache SeqSubSeq NumZero False TLC requires the second argument of SeqSubSeq to be in domain of the sequence and returns an error otherwise. Apalache always returns some sequence
50780b1b4f662f20b8e04a43041b58e8c99cb876 Apalache SeqSubSeq NumUnaryMinus True TLC requires the second argument of SeqSubSeq to be in domain of the sequence and returns an error otherwise. Apalache always returns some sequence
bf75ac824a18bbf6c47d7f496587d59835eca063 Apalache SeqSubSeq NumUnaryMinus False TLC requires the second argument of SeqSubSeq to be in domain of the sequence and returns an error otherwise. Apalache always returns some sequence
3ec1b130d755a4171f0ea760edbdb6c70a983152 Apalache SeqSubSeq NumMod True TLC requires the second argument of SeqSubSeq to be in domain of the sequence and returns an error otherwise. Apalache always returns some sequence
40bd407efeb40fb2903926bdab5cf529bacfed8a Apalache SeqSubSeq NumMod False TLC requires the second argument of SeqSubSeq to be in domain of the sequence and returns an error otherwise. Apalache always returns some sequence
186a484931432d9055cc55ea9908f4b619eb4e68 Apalache SeqSubSeq BagCopiesIn True TLC requires the second argument of SeqSubSeq to be in domain of the sequence, which doesn't include zero, and returns an error otherwise. BagCopiesIn returns zero, because there no such value in the bag, therefore TLC reports error. Apalache always returns some sequence and doesn't crash in such situations
1e51fed60a710cf8752f73c807de2510e96a90fe Apalache SeqSubSeq BagCopiesIn False TLC requires the second argument of SeqSubSeq to be in domain of the sequence, which doesn't include zero, and returns an error otherwise. BagCopiesIn returns zero, because there no such value in the bag, therefore TLC reports error. Apalache always returns some sequence and doesn't crash in such situations
093b5c2b34aba6e26c00c1c26704f40caadb0ddd Apalache SeqSubSeq SeqTail True TLC requires the second argument of SeqSubSeq to be in domain of the sequence and returns an error otherwise. Apalache always returns some sequence
899e9ddba7041cce422b9427fc6de31ff23e1c06 Apalache SeqSubSeq SeqTail False TLC requires the second argument of SeqSubSeq to be in domain of the sequence and returns an error otherwise. Apalache always returns some sequence
4cf1156e005f4d434d61c44c22b5fa2461c7235e Apalache SeqHead TupleEmpty True Head of empty sequence results in error in TLC. Apalache is unable to detect such an error and instead returns arbitrary value
13b8a5df936f0a06bfc14d43a657bcbec061b694 Apalache SeqHead TupleEmpty False Head of empty sequence results in error in TLC. Apalache is unable to detect such an error and instead returns arbitrary value
40a2cd5141b4338d90ceb2a6ef7eb7dc3bf39f4b Apalache SeqHead SeqTail True Head of empty sequence results in error in TLC. Apalache is unable to detect such an error and instead returns arbitrary value
b40b7b84fd06cc86dbc07d7161924a9dc068e129 Apalache SeqHead SeqTail False Head of empty sequence results in error in TLC. Apalache is unable to detect such an error and instead returns arbitrary value
cd16e1f8c4d71514b565193260eedc22a3183858 Apalache SeqTail TupleEmpty True Tail of empty sequence results in error in TLC. Apalache is unable to detect such an error and instead returns arbitrary value
fc8253e6317e8891a7069c098f558350613a8404 Apalache SeqTail TupleEmpty False Tail of empty sequence results in error in TLC. Apalache is unable to detect such an error and instead returns arbitrary value
a025967b62b9b305dac3dc23e62d7dc08fce8dac Apalache SeqTail SeqTail True Tail of empty sequence results in error in TLC. Apalache is unable to detect such an error and instead returns arbitrary value
1fd80d772f693595c15cddcefe33d780e62ce1d5 Apalache SeqTail SeqTail False Tail of empty sequence results in error in TLC. Apalache is unable to detect such an error and instead returns arbitrary value