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 case feature Union; CLI Option: -workers 1

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
d65ba7ff36d3f795bf2d426ac66081a96a6b8a1a TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Union OneLineComment True Passed
  • Model Under Test
  • Equivalent Model
fa00e14cadb3d85e35e5689473bf3e6c7406a2ac TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Union OneLineComment False Passed
  • Model Under Test
  • Equivalent Model
54c3d1ecabe5f3b5cdce1915ef3e5e7920209d7c TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Union MultiLineComment True Passed
  • Model Under Test
  • Equivalent Model
5fe9d67cc73d1c68f93eddd6ee75948ff81b8743 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Union MultiLineComment False Passed
  • Model Under Test
  • Equivalent Model
60318e733a0f70bd5b748c7d8080d1bfc1b35cb5 Apalache Union Let True Passed
  • Model Under Test
  • Equivalent Model
69545560cbfe8547d92c5dbededed5e061110ed9 Apalache Union Let False Passed
  • Model Under Test
  • Equivalent Model
9a99955739db9b3d9d1f2d17adb2c73835719c71 Apalache Union SetEmpty True Passed
  • Model Under Test
  • Equivalent Model
0cdb81004951eaff3091ce94fb9563c6f08ac294 Apalache Union SetEmpty False Passed
  • Model Under Test
  • Equivalent Model
be1eb05fb3885333dc464afa6e64ecbf61e2b5fd Apalache Union Set0 True Passed
  • Model Under Test
  • Equivalent Model
966939c6aeadbac5b9f2bdaf59559802248ca34e Apalache Union Set0 False Passed
  • Model Under Test
  • Equivalent Model
ba8ff3e8f0e834c414509120d0c2ad0948ad67ec Apalache Union Set1 True Passed
  • Model Under Test
  • Equivalent Model
3d44db042e2902df6def69af48a26bfa3784aa10 Apalache Union Set1 False Passed
  • Model Under Test
  • Equivalent Model
67ed4b296dceedae1eab159b515325d8327d4b52 Apalache Union Set2 True Passed
  • Model Under Test
  • Equivalent Model
65ad2c4a02f201ee4ca77a535caaa6711bf88f33 Apalache Union Set2 False Passed
  • Model Under Test
  • Equivalent Model
d55943b1db35a9cd7a260aa9ec67dd56c7ffba46 Apalache Union Choose True Passed
  • Model Under Test
  • Equivalent Model
f517dea81da34292b9239a18622ba909de6579a0 Apalache Union Choose False Passed
  • Model Under Test
  • Equivalent Model
a79139f9adbab2fd4a9ab9439274fb3730d6b639 Apalache Union FunApp True Passed
  • Model Under Test
  • Equivalent Model
84044592f93191b589b9bd01fd6a67f6a2549dfa Apalache Union FunApp False Passed
  • Model Under Test
  • Equivalent Model
32fa408404e86168d3eeb84e738ba9d11e169bf1 Apalache Union Prime True Passed
  • Model Under Test
  • Equivalent Model
98f631837631216047060f49ddf24db6372a8331 Apalache Union Prime False Passed
  • Model Under Test
  • Equivalent Model
cff0df6e86732471085955460f4659c1af26f532 Apalache Union Def0 True Passed
  • Model Under Test
  • Equivalent Model
df45cd2554d32c1da51b784d6dd48606f407a454 Apalache Union Def0 False Passed
  • Model Under Test
  • Equivalent Model
c621815596eb791e3719529ee05498e5338d4cdc TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Union LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
5221ee1ee658157cf35c3688c14082eb63692982 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Union LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
abf4b27daadd74f7605fcd70a3bb041178680b0c Apalache Union Def1 True Passed
  • Model Under Test
  • Equivalent Model
a39ec1210e0186f0d819014c2cf08dc6248a26b6 Apalache Union Def1 False Passed
  • Model Under Test
  • Equivalent Model
171376d307adb169f65436927dbdaf852f6671a1 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Union LetDef1 True Passed
  • Model Under Test
  • Equivalent Model
b4e790a52ce66e9c611177b6dc8ba4577cef4a02 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Union LetDef1 False Passed
  • Model Under Test
  • Equivalent Model
9ffbb855b191e10d083a4b51a3d3e4134cfaf750 Apalache Union Def2 True Passed
  • Model Under Test
  • Equivalent Model
9a068fca2d2a5e47cde60ac165f2a1df6162497c Apalache Union Def2 False Passed
  • Model Under Test
  • Equivalent Model
e1cda3bd33c36765651f11388ae43384ab4a0e2c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Union LetDef2 True Passed
  • Model Under Test
  • Equivalent Model
ee1eac4d46ad07a84ae839ea9999375ccf9d827a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Union LetDef2 False Passed
  • Model Under Test
  • Equivalent Model
25cc55a13f088109e706bdf08e37f0210e45d67d Apalache Union Def1Recursive True Passed
  • Model Under Test
  • Equivalent Model
9a853201d4ab3ad6c6e07b3d563a9bf16950a4ac Apalache Union Def1Recursive False Passed
  • Model Under Test
  • Equivalent Model
9e625a5e04ffc2cdebd761cca62724d132bf4724 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Union LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
3f1713b14e9e981b1f4b7c9f5bd03746f4e7bc3b TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Union LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
e2a0ad1f42e44a159617ecfbb2b1355d78cd33b3 Apalache Union Extends True Passed
  • Model Under Test
  • Equivalent Model
310d37d4b80221fe2480d2caa68ef543cfa7e281 Apalache Union Extends False Passed
  • Model Under Test
  • Equivalent Model
0c79bac8f6f350c9f5d5c210110524a876b726ef Apalache Union ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
3a22d22c44f5bcef89262df00035bfe6f1fb08e1 Apalache Union ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
b87bcf52564383fc41b1f3afd19e2bf4ee33748a Apalache Union Variable True Passed
  • Model Under Test
  • Equivalent Model
9fd1c1d48592f0ab145929a2661fd1b5874d2b16 Apalache Union Variable False Passed
  • Model Under Test
  • Equivalent Model
456aaadc7a4d938331d745f912282a76b0ce72da Apalache Union Constant True Passed
  • Model Under Test
  • Equivalent Model
1d91330ba83e16739c671118260c20c791256e0c Apalache Union Constant False Passed
  • Model Under Test
  • Equivalent Model
88df97e16507577a30f057ee6f21f03648c2de91 Apalache Union ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
5ceb6ff9110f6c62fbace991d63fdcb2c528c1a1 Apalache Union ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
64bff6315c47c00b73ed22774dec5958660019b6 Apalache Union Instance True Passed
  • Model Under Test
  • Equivalent Model
84a75c71139536ce202d818112b8af98cf1aa7c1 Apalache Union Instance False Passed
  • Model Under Test
  • Equivalent Model
9cbe4faf5da1e26b262f264c50d5d326f35c58ff Apalache Union InstanceWith True Passed
  • Model Under Test
  • Equivalent Model
6b58fcffbef71ad9ea14ce911a5e7722c38a1ddf Apalache Union InstanceWith False Passed
  • Model Under Test
  • Equivalent Model
981facb2408cbf5780fd429c19803790b6354300 Apalache Union InstanceNamed True Passed
  • Model Under Test
  • Equivalent Model
93a413624bf26c465482344187be5374d6425fb1 Apalache Union InstanceNamed False Passed
  • Model Under Test
  • Equivalent Model
af7d7eba1a86ac885d9427ff57b1d38378b44b7e Apalache Union InstanceNamedWith True Passed
  • Model Under Test
  • Equivalent Model
660d8e5f25b6fa14b426c4fd6529aa29dbc01960 Apalache Union InstanceNamedWith False Passed
  • Model Under Test
  • Equivalent Model
d6468f6e19b0fca19210fde24a7d5f596d71182b Apalache Union InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
f6950808272ede0b297be85984d45c5d4dfd6aaf Apalache Union InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
54871aa4f89e16c1d5a4728db95e150e25fc8365 Apalache Union InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
3e8098909d4ae53935fa1b2fe3cf18a780e9739d Apalache Union InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
bfbfe17f6e690354e0aa25ea90cf0889f46a95df Apalache Union InstanceNamedInFolder True Passed
  • Model Under Test
  • Equivalent Model
6759005afde8761ea05bee23d6b341039c9c6176 Apalache Union InstanceNamedInFolder False Passed
  • Model Under Test
  • Equivalent Model
2be354829895a975a3c3d09d231ee4ab15c86743 Apalache Union InstanceNamedWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
dd6c8a1bcc96913650dc1e0c047636fb24d2f437 Apalache Union InstanceNamedWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
1389dc181046bb3ffd69ddeca64f8b7cafb5bfd0 Apalache Union SetDiff True Passed
  • Model Under Test
  • Equivalent Model
e00686b82d68b37c83319fa6b5c0548ea246fbfc Apalache Union SetDiff False Passed
  • Model Under Test
  • Equivalent Model
3ea03eaa5261993eac583f46d73d2813a969f4d9 Apalache Union SetUnion True Passed
  • Model Under Test
  • Equivalent Model
607545577658e9a2aad0ded26b5fc9c31a28b1db Apalache Union SetUnion False Passed
  • Model Under Test
  • Equivalent Model
87e88c49c49516b04ac1c73f608e74bec2bcc122 Apalache Union SetIntersect True Passed
  • Model Under Test
  • Equivalent Model
b0c46acd654a744170b3b80c27a2b1303bf009a0 Apalache Union SetIntersect False Passed
  • Model Under Test
  • Equivalent Model
4244e583825f7651d25576e9ed665c215896abbf Apalache Union IfCond True Passed
  • Model Under Test
  • Equivalent Model
4c92879bf750b4de2886626f2ed93cd96ae6bebe Apalache Union IfCond False Passed
  • Model Under Test
  • Equivalent Model
ae5a4856361897f137f65a0cde0e563d47f01d06 Apalache Union IfThen True Passed
  • Model Under Test
  • Equivalent Model
db645a18564ae7c1dd89c12b25bc80f85a5ee353 Apalache Union IfThen False Passed
  • Model Under Test
  • Equivalent Model
a3b8ac239013b35f6a895dbbf29d2f63179f39a0 Apalache Union IfElse True Passed
  • Model Under Test
  • Equivalent Model
7447037a14e5d148ec09d8bdc4688278098bb47f Apalache Union IfElse False Passed
  • Model Under Test
  • Equivalent Model
7064790e221a088bad0fc8e3c7d572415d77f501 Apalache Union Subset True Passed
  • Model Under Test
  • Equivalent Model
565f6ac6d5f13d6229a323f22f84286ce2b04965 Apalache Union Subset False Passed
  • Model Under Test
  • Equivalent Model
cd96adcc1acb43463a75813b11f9a5dad8020e18 Apalache Union Domain True Passed
  • Model Under Test
  • Equivalent Model
1ebe17190d44f404566cea43d71daaf91f7f0ecc Apalache Union Domain False Passed
  • Model Under Test
  • Equivalent Model
cc0264191644f9ec2440dd33482ba53601533310 Apalache Union Union True Passed
  • Model Under Test
  • Equivalent Model
1d86c5429bbd89b646e0d2188a48d6ae353ef226 Apalache Union Union False Passed
  • Model Under Test
  • Equivalent Model
0be6ec10ec195891d753bc55d8e0fa974c195ff5 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Union TlcEval True Passed
  • Model Under Test
  • Equivalent Model
6dd9c443dbc1381a83ec7da5ce83076d55d9f7dc TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Union TlcEval False Passed
  • Model Under Test
  • Equivalent Model
b432a5fe2d123f27b81230d5cee1b5e2c164d38a Apalache Union BagBagToSet True Passed
  • Model Under Test
  • Equivalent Model
44a0d13cce3b5de230c93e7d9fb51cbcc514f8bb Apalache Union BagBagToSet False Passed
  • Model Under Test
  • Equivalent Model
ad8ef50f1d0b45346be31303bf0c3150888403b2 Apalache Union SeqHead True Passed
  • Model Under Test
  • Equivalent Model
355b0051ba396cf3a6913e852ff29b1816021b7e Apalache Union SeqHead False Passed
  • Model Under Test
  • Equivalent Model