Index


  • Introduction

  • Skipped feature combinations
  • Failed test cases
  • Tests by feature combinations
  • SYMMETRY tests
  • Tests under anomalous conditions

  • Tests by feature combinations: -workers 2
  • SYMMETRY tests: -workers 2

  • Tests by feature combinations: -workers auto
  • SYMMETRY tests: -workers auto

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
14674c082bef6f2fe6b5d5aad1e729e74dca1358 Apalache Eq NumMinus True Passed
  • Model Under Test
  • Equivalent Model
58e88970ffd2351740c3833b0b50847dd063507a Apalache Eq NumMinus False Passed
  • Model Under Test
  • Equivalent Model
5dd1d0f59bc967d91f488b8a3f68cb209093fccb Apalache Ne NumMinus True Passed
  • Model Under Test
  • Equivalent Model
fb4adf120868f0a35f614fe61e4168b1f3410b58 Apalache Ne NumMinus False Passed
  • Model Under Test
  • Equivalent Model
0f48895547aaddf330d1f0f2e8ad57880f9dd6a9 Apalache Let NumMinus True Passed
  • Model Under Test
  • Equivalent Model
016ffa323fdb78bce685fc198637e57189e01ac8 Apalache Let NumMinus False Passed
  • Model Under Test
  • Equivalent Model
9cabf640d93535a2d8ce12308948fac6c694c453 Apalache Set0 NumMinus True Passed
  • Model Under Test
  • Equivalent Model
6626ec8c649b248de16b6b6fe4c404c0c0dadcae Apalache Set0 NumMinus False Passed
  • Model Under Test
  • Equivalent Model
5e7360188f4960869519128f7a7e32e86015e841 Apalache Set1 NumMinus True Passed
  • Model Under Test
  • Equivalent Model
d70845bdf1515400ffc5eb565a67e5bb1e3ba378 Apalache Set1 NumMinus False Passed
  • Model Under Test
  • Equivalent Model
fbb2429a42e7c5dc7eb774dac9a3cf721d53c2a1 Apalache Set2 NumMinus True Passed
  • Model Under Test
  • Equivalent Model
9560d180d50fe40ec3b0c8a07296f711b147754e Apalache Set2 NumMinus False Passed
  • Model Under Test
  • Equivalent Model
91733ba01a1a93f4d247ddb3a8c79069e627f046 Apalache Fun NumMinus True Passed
  • Model Under Test
  • Equivalent Model
093310b4d1c33f7fdf8e210372558d89b9f1d826 Apalache Fun NumMinus False Passed
  • Model Under Test
  • Equivalent Model
12a4cd713f1c7df713f05bad92ec840134a615b2 Apalache In NumMinus True Passed
  • Model Under Test
  • Equivalent Model
a76d9fe04c247e53dd4c44c75e0187b92d0d5342 Apalache In NumMinus False Passed
  • Model Under Test
  • Equivalent Model
f53d9de520c115fcef40b3d1571670f4c00c8978 Apalache NotIn NumMinus True Passed
  • Model Under Test
  • Equivalent Model
a84171984250ffcd162b652761f2e4d17ef67ac8 Apalache NotIn NumMinus False Passed
  • Model Under Test
  • Equivalent Model
b98e85873adee1f90dc5f4db155db4380683a622 Apalache Record NumMinus True Passed
  • Model Under Test
  • Equivalent Model
42fd0408e639f5880c25300b20aaae903f966716 Apalache Record NumMinus False Passed
  • Model Under Test
  • Equivalent Model
0b233e8419db3e846bfd82db33ca1408739a9378 Apalache Tuple NumMinus True Passed
  • Model Under Test
  • Equivalent Model
be4be70842a44a17016c4f8c9c6fdc38c3bd5141 Apalache Tuple NumMinus False Passed
  • Model Under Test
  • Equivalent Model
a31f9bcd399333c0decb2ce898ae4fd104fc2785 Apalache FunApp NumMinus True Passed
  • Model Under Test
  • Equivalent Model
90b4cc25e9eb76d984d71b9def47ee0c853cb7e4 Apalache FunApp NumMinus False Passed
  • Model Under Test
  • Equivalent Model
eeb29330a616dbd2b2f74ebc648d38225115cfea Apalache Except1Fun NumMinus True Passed
  • Model Under Test
  • Equivalent Model
03683e438f54e5da32328fdf0bdce41951f58dcd Apalache Except1Fun NumMinus False Passed
  • Model Under Test
  • Equivalent Model
c51e2c72870ed27e0cf19768c32bb9cf3ff2a434 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt NumMinus True Passed
  • Model Under Test
  • Equivalent Model
9839dd355a822915590eba1584f36a6471142e59 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt NumMinus False Passed
  • Model Under Test
  • Equivalent Model
a24724c83bfa85a3a7d1845cc26237c352e592c4 Apalache Except1Rec NumMinus True Passed
  • Model Under Test
  • Equivalent Model
729fc29d4cb467c6cdeba40177d02330ceb629fb Apalache Except1Rec NumMinus False Passed
  • Model Under Test
  • Equivalent Model
577b94c287e464a01111a680d04b33d29a8a7078 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumMinus True Passed
  • Model Under Test
  • Equivalent Model
ff1ac7f0568b4f90c73c268e8bf34a1c9e17ad3e TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumMinus False Passed
  • Model Under Test
  • Equivalent Model
a346609af44e95d044e6cf3c4a57195218f07dcb Apalache Except2Fun NumMinus True Passed
  • Model Under Test
  • Equivalent Model
0ddbbba13e9bfc69a8b582222d46057df6df4608 Apalache Except2Fun NumMinus False Passed
  • Model Under Test
  • Equivalent Model
2a05258c1ede9cb6b51ac36d6dcc68e52fd9f7ba Apalache Prime NumMinus True Passed
  • Model Under Test
  • Equivalent Model
fa5ae43a057c017e5c6a2780639780fc21a36f74 Apalache Prime NumMinus False Passed
  • Model Under Test
  • Equivalent Model
41eaad9147596315fd5db51ba77d0bb735ba20ad Apalache NumUnaryMinus NumMinus True Passed
  • Model Under Test
  • Equivalent Model
597177f7bc1989feb3f6fe86af53fefd48ee1be6 Apalache NumUnaryMinus NumMinus False Passed
  • Model Under Test
  • Equivalent Model
946fa57c64e88bbc74d1631d35b5068b8dc69f04 Apalache NumPlus NumMinus True Passed
  • Model Under Test
  • Equivalent Model
8d1f8809f9ea9fbe74c9c90e103c5e72a9994e72 Apalache NumPlus NumMinus False Passed
  • Model Under Test
  • Equivalent Model
455ab83e76acdaa242d9f3f34b2365cdb6693d07 Apalache NumMinus NumMinus True Passed
  • Model Under Test
  • Equivalent Model
ff4afdf1f35fbbb1b904765aeafeef943e1db27b Apalache NumMinus NumMinus False Passed
  • Model Under Test
  • Equivalent Model
23ff9d7e2ef088372c5431c643dd1727e6659aee Apalache NumMul NumMinus True Passed
  • Model Under Test
  • Equivalent Model
389e65dfba868f00e51fa3ae26334b77a7ffd33e Apalache NumMul NumMinus False Passed
  • Model Under Test
  • Equivalent Model
1bd59be9744def68a5e7fc853b20a70c6ee273e3 Apalache NumDiv NumMinus True Passed
  • Model Under Test
  • Equivalent Model
aee3ce09fa97d6dd41a3cedec71f57f30233dc6a Apalache NumDiv NumMinus False Passed
  • Model Under Test
  • Equivalent Model
bb81417638c3742d7d624b045e734ead2d8fdf66 Apalache NumMod NumMinus True Passed
  • Model Under Test
  • Equivalent Model
41212285b57240391d51f09c3a9e38c6971e7a0d Apalache NumMod NumMinus False Passed
  • Model Under Test
  • Equivalent Model
e2a4a78b19c4b1b8c829854eb63e4cf6284952bc Apalache NumPow NumMinus True Passed
  • Model Under Test
  • Equivalent Model
cd5b2e23b40c26f57d27823a50a634fead20f560 Apalache NumPow NumMinus False Passed
  • Model Under Test
  • Equivalent Model
8d0c929c5261f31432ebb7e0f5358a5bd4c326a5 Apalache NumGt NumMinus True Passed
  • Model Under Test
  • Equivalent Model
cf1de4a29dc02a074da0679212c652b0659af2eb Apalache NumGt NumMinus False Passed
  • Model Under Test
  • Equivalent Model
d7b9392b2402129c95a426fb7eb31543ce6942eb Apalache NumGe NumMinus True Passed
  • Model Under Test
  • Equivalent Model
a9c79f36c79adb859f0dce89e93c0b4b9cda2670 Apalache NumGe NumMinus False Passed
  • Model Under Test
  • Equivalent Model
e0cc7b8b29d5ef2063d18f0475ec0d59cf72ceeb Apalache NumLt NumMinus True Passed
  • Model Under Test
  • Equivalent Model
e207d2b38fc7a27359e1a4771b5c0faf783477a8 Apalache NumLt NumMinus False Passed
  • Model Under Test
  • Equivalent Model
b1864f1e501fda1a19fc7c92204a77e95bef7f11 Apalache NumLe NumMinus True Passed
  • Model Under Test
  • Equivalent Model
7eda53a03a9e91d3fd6f6e5866d89618689b7dd8 Apalache NumLe NumMinus False Passed
  • Model Under Test
  • Equivalent Model
bea94f2df2397481de05c545d9eb39592c50c511 Apalache DefFun NumMinus True Passed
  • Model Under Test
  • Equivalent Model
e96b6108fca0285e60af28f20e0b9eca55505bf9 Apalache DefFun NumMinus False Passed
  • Model Under Test
  • Equivalent Model
c2134b41f732b05bf207308a50afb9d829479d68 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumMinus True Passed
  • Model Under Test
  • Equivalent Model
3ad0630a5ea9e8ccfb8b291bb2324bd89c88cd71 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumMinus False Passed
  • Model Under Test
  • Equivalent Model
6f48ee4f696647e7b28dec30e2d0aa0bb40e9685 Apalache DefFunRecursive NumMinus True Passed
  • Model Under Test
  • Equivalent Model
8d609f3e119096a2282f858826ed0ac53d5fb280 Apalache DefFunRecursive NumMinus False Passed
  • Model Under Test
  • Equivalent Model
a5e3c57a444e4199672402a2ab4c3a2f6b9778da TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumMinus True Passed
  • Model Under Test
  • Equivalent Model
4e5e3622796858d08f71e2281b411e06ca7c256a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumMinus False Passed
  • Model Under Test
  • Equivalent Model
a83e24d3a4fa635ab6f8c7699225fab32c6bbe8b Apalache Def0 NumMinus True Passed
  • Model Under Test
  • Equivalent Model
e184cd7717e30451a2590a6456f0a3afad4bc50a Apalache Def0 NumMinus False Passed
  • Model Under Test
  • Equivalent Model
3eeccf496c7c621fc80b4880caa10de36caa4ecf TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumMinus True Passed
  • Model Under Test
  • Equivalent Model
f67147a0883e31be1bf1dc99274c83a2c6744caa TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumMinus False Passed
  • Model Under Test
  • Equivalent Model
afb20ee727ea482b96ae6bd0b7b4a032d882eb25 Apalache Def1 NumMinus True Passed
  • Model Under Test
  • Equivalent Model
c059369daaa32b840ae754c1904a39691edba538 Apalache Def1 NumMinus False Passed
  • Model Under Test
  • Equivalent Model
6b3ff0bdaa5e78f28031505a4f8a6ef5168b5201 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumMinus True Passed
  • Model Under Test
  • Equivalent Model
90ffed440230a9e59f4d5c9f073b1216c4694c5c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumMinus False Passed
  • Model Under Test
  • Equivalent Model
509f8dea8877904c6adefa3c5e04c1d6fce04d3a Apalache Def2 NumMinus True Passed
  • Model Under Test
  • Equivalent Model
b2fab82c17df80d442ef6e2b09ce7f86f227ed50 Apalache Def2 NumMinus False Passed
  • Model Under Test
  • Equivalent Model
98446430fe34208dbf57e773d77dbc7e33d1e4cd TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumMinus True Passed
  • Model Under Test
  • Equivalent Model
8d55abe31ce6b017f1ff44c389ef34b6ba8e7fd8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumMinus False Passed
  • Model Under Test
  • Equivalent Model
4c639d9e9d6fc0d811ab6f60755cf3a36946eb93 Apalache Def1Recursive NumMinus True Passed
  • Model Under Test
  • Equivalent Model
e2a7c6daefb3c40ede5a509db720f4b44adb45db Apalache Def1Recursive NumMinus False Passed
  • Model Under Test
  • Equivalent Model
c7611e99006ef9ebf54b41f79fc704064c37604b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumMinus True Passed
  • Model Under Test
  • Equivalent Model
475b719db7997604076be7578c6eb37b2f886e4e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumMinus False Passed
  • Model Under Test
  • Equivalent Model
8aa84de537691605a2a2b25ff486224e8e17196f Apalache Extends NumMinus True Passed
  • Model Under Test
  • Equivalent Model
9b01fc8958fb82c30b186ba07b5004ff8203c15e Apalache Extends NumMinus False Passed
  • Model Under Test
  • Equivalent Model
6a8825f190c8cc3986be579535ec6ed034e7f5ee Apalache ExtendsInDifferentFolder NumMinus True Passed
  • Model Under Test
  • Equivalent Model
78b74e8ef507e8bde8c9942ad08c0844ee2abf42 Apalache ExtendsInDifferentFolder NumMinus False Passed
  • Model Under Test
  • Equivalent Model
d8ec211cb6d6a813bf967a42473f03c3c1cff96e Apalache Variable NumMinus True Passed
  • Model Under Test
  • Equivalent Model
82b14e2052519aa69d829c6dfa8cc69db8e85eed Apalache Variable NumMinus False Passed
  • Model Under Test
  • Equivalent Model
6e5fc3bb0aaead8a212594827ee45e67fe3b1203 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude NumMinus True Passed
  • Model Under Test
  • Equivalent Model
6a7ca2256e10bf4f98366b7263c296a5428f0194 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude NumMinus False Passed
  • Model Under Test
  • Equivalent Model
eda2a051dba74030f9b56b1a96136518c1f48383 Apalache Constant NumMinus True Passed
  • Model Under Test
  • Equivalent Model
fe64f6f819ece95d9fe3566a06bbd250f4bc28dc Apalache Constant NumMinus False Passed
  • Model Under Test
  • Equivalent Model
9a891b5e67c5a3177768f95687f97ac818b078cf Apalache ConstantRank1 NumMinus True Passed
  • Model Under Test
  • Equivalent Model
df1ef18a0401394424bd685240227dd72950743d Apalache ConstantRank1 NumMinus False Passed
  • Model Under Test
  • Equivalent Model
142d1d45d1abb17c2a813773fbf5d9a7d249bad3 Apalache Instance NumMinus True Passed
  • Model Under Test
  • Equivalent Model
f7f136c8c6ed7fca1a7e2ae75e8de7eea65731f8 Apalache Instance NumMinus False Passed
  • Model Under Test
  • Equivalent Model
2d820ca0d9583aecd0a1acc6982abae5457fc41f Apalache InstanceWith NumMinus True Passed
  • Model Under Test
  • Equivalent Model
ad2af1edb4a8ecc55c67a011c38ed4668fc3ef2e Apalache InstanceWith NumMinus False Passed
  • Model Under Test
  • Equivalent Model
31213eae3b9cf44df022d469b81ad803bbf9aeb6 Apalache InstanceNamed NumMinus True Passed
  • Model Under Test
  • Equivalent Model
27b46436afe281a9c43c5f459c9fdd93c4b52e42 Apalache InstanceNamed NumMinus False Passed
  • Model Under Test
  • Equivalent Model
4c25e55eed52c0f5632b2e1d99662c14bf720b28 Apalache InstanceNamedWith NumMinus True Passed
  • Model Under Test
  • Equivalent Model
7637a52ebe5f74ad3f70f8797698f22f798fd265 Apalache InstanceNamedWith NumMinus False Passed
  • Model Under Test
  • Equivalent Model
21b13e4cc8b6a5d9289fdcfc807794b461cc8b84 Apalache InstanceInFolder NumMinus True Passed
  • Model Under Test
  • Equivalent Model
2dd88af4c7781e539db5e221d4df52ac78df2156 Apalache InstanceInFolder NumMinus False Passed
  • Model Under Test
  • Equivalent Model
5e6c8ac64b2bcf55bceb6ebe5f8db204e4eb70a0 Apalache InstanceWithInFolder NumMinus True Passed
  • Model Under Test
  • Equivalent Model
fae894160ee7982851af4e21286d473cd41d26ab Apalache InstanceWithInFolder NumMinus False Passed
  • Model Under Test
  • Equivalent Model
e19241be0e9c38794fa319f037c53f5065dcf6af Apalache InstanceNamedInFolder NumMinus True Passed
  • Model Under Test
  • Equivalent Model
659ee2f2efb589fe215f2564732cc88ffaada9b1 Apalache InstanceNamedInFolder NumMinus False Passed
  • Model Under Test
  • Equivalent Model
d2163c5d12e9c50727546c47a9d0aad5e8876f62 Apalache InstanceNamedWithInFolder NumMinus True Passed
  • Model Under Test
  • Equivalent Model
bd2bb5f47b64472aabbaa3b2cb462784ff8c1ed9 Apalache InstanceNamedWithInFolder NumMinus False Passed
  • Model Under Test
  • Equivalent Model
083298025451bcd0e04800f65757f1d9844dc397 Apalache Lambda NumMinus True Passed
  • Model Under Test
  • Equivalent Model
5f2cb5a0acff8f9f425b02fd3aaa84df0e0917a2 Apalache Lambda NumMinus False Passed
  • Model Under Test
  • Equivalent Model
6d61d8c6856c421af459afc4bdfa3eca2f6ab53d Apalache IfThen NumMinus True Passed
  • Model Under Test
  • Equivalent Model
68033ef4dc1c444269896118e98822dd2b695b0f Apalache IfThen NumMinus False Passed
  • Model Under Test
  • Equivalent Model
37d27cce609a1df49099ebb4ad86dadc223ab49d Apalache IfElse NumMinus True Passed
  • Model Under Test
  • Equivalent Model
94609f1b020d2a7f2943844f2dce2f87721a8231 Apalache IfElse NumMinus False Passed
  • Model Under Test
  • Equivalent Model
74ee154898d690b63ecbc92d31d5d7cd4ed144a0 Apalache Unchanged NumMinus True Passed
  • Model Under Test
  • Equivalent Model
9a56759a1619c7e1c001d7a8bbb66535583cec78 Apalache Unchanged NumMinus False Passed
  • Model Under Test
  • Equivalent Model
30760c62c4c515dac8cb3b45cf0ece18a2d02e2e Apalache SeqSubSeq NumMinus True Passed
  • Model Under Test
  • Equivalent Model
3352bc8719aede252b6668197d144e9ae8643ec1 Apalache SeqSubSeq NumMinus False Passed
  • Model Under Test
  • Equivalent Model
cb1724e1f84a64c7aa81e560946c27390afc8174 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange NumMinus True Passed
  • Model Under Test
  • Equivalent Model
ebbc2a299fd7bd38c1bce04fd8225a5ba7da397a TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange NumMinus False Passed
  • Model Under Test
  • Equivalent Model
1154ddfdc2a5ea86f5db13305d7b74b2feff977f TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumMinus True Passed
  • Model Under Test
  • Equivalent Model
84b0366f09b40cd2582c3a1b51027fd7f1c9673e TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumMinus False Passed
  • Model Under Test
  • Equivalent Model
fa19944bed9315e0e0153734bf2a209e3b9d5b17 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumMinus True Passed
  • Model Under Test
  • Equivalent Model
1603baa382256471ce6af3e3be52aea70e39abf3 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumMinus False Passed
  • Model Under Test
  • Equivalent Model
325802c817bb12df3ac166de899acb550141d912 Apalache BagBagIn NumMinus True Passed
  • Model Under Test
  • Equivalent Model
9d813d5856b6beb10a1a2efcb284c56a4f1a3d70 Apalache BagBagIn NumMinus False Passed
  • Model Under Test
  • Equivalent Model
0b203c7ec97ff6af07f1fc15cb70274042d45f6b Apalache BagCopiesIn NumMinus True Passed
  • Model Under Test
  • Equivalent Model
a718a0ad1ed1efd1ee16049a7c394ab822104f31 Apalache BagCopiesIn NumMinus False Passed
  • Model Under Test
  • Equivalent Model
5b7f3451c9dd78d1f60e706639458c83d4af1e71 Apalache SeqAppend NumMinus True Passed
  • Model Under Test
  • Equivalent Model
2ef3ecc06e9f4092be5bd238d658cf3991e5b65b Apalache SeqAppend NumMinus False Passed
  • Model Under Test
  • Equivalent Model