Index

Tests by case feature Subset; CLI Option: -workers 1

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
de88e09ffc201677667e6aa3d7b1be220668c67f TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Subset OneLineComment True Passed
c08034a46c0e2c01cdbe64164dc8aad9c8ca5419 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Subset OneLineComment False Passed
25a9d6264bea695274f85f9070bdf1304ae9a92f TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Subset MultiLineComment True Passed
7a6e66d8c2f83b5e99305d19b98d707254b7aca8 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Subset MultiLineComment False Passed
86791ea5b266eb262c678a3a0569b698cbab3347 Apalache Subset BoolSet True Passed
cbc6d6c241f77bd9d790769295434148bbe68c12 Apalache Subset BoolSet False Passed
167dc31d64d9a8550b33ef3b7a819426f911fdab Apalache Subset Let True Passed
597a84f873b795ecf4fada528d03a668f1080ba8 Apalache Subset Let False Passed
834f594fe9bdabcab1a8c5dc1de5f98e2ee3c652 Apalache Subset SetEmpty True Passed
58e981aef4ee1e0bd0b4040033d8f0a0fdbef1fc Apalache Subset SetEmpty False Passed
c733a3960b2a7027cbc1379a6bdc558c0e810e4f Apalache Subset Set0 True Passed
f45826c075a56deb8b9ac414eb59b6080dc260ba Apalache Subset Set0 False Passed
a45584d40038a069aa432f45b9244401b7870c3a Apalache Subset Set1 True Passed
f5b10c79d2220f6616b8a952a3e854effa650913 Apalache Subset Set1 False Passed
1f3e714ee9a86aa4fb163837cab9b13d28a14e20 Apalache Subset Set2 True Passed
68a137c89c133547d3cb0dde5ba712b7d34843b1 Apalache Subset Set2 False Passed
cdc3c62ef9375481dca5087bdced877a911b57cb Apalache Subset Choose True Passed
0912c8e640bcd61275c30ef65c60519c509dee2a Apalache Subset Choose False Passed
d0936637cbcefebd5ebeb809d18e89ede242e431 Apalache Subset FunApp True Passed
a2de11ccda1c91256262683343a34602e349dd63 Apalache Subset FunApp False Passed
9645120f8debcf0d1c656e5b7cb6fdeb2cc60397 Apalache Subset Prime True Passed
20d661e75d4405a4961c30b08ee825b43582a3ee Apalache Subset Prime False Passed
e86e0a7d750429c8c82d58395f71a570a9fa2932 Apalache Subset Def0 True Passed
629f77f71674b9cea5a6fe5a538564a0649df8c8 Apalache Subset Def0 False Passed
2e769c061a72501e203b6d534278e775bc10ca52 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Subset LetDef0 True Passed
b06810b75c7d8df84568df2cb78458cf70c4e9fa TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Subset LetDef0 False Passed
861407c23f36f47168f7a192300818c110fa17f5 Apalache Subset Def1 True Passed
1a72cb144ef3de4bdae7a0874aaa996401c4fc4f Apalache Subset Def1 False Passed
0cf167e66d8be8704ecf077272d3184887bac661 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Subset LetDef1 True Passed
e6924791e52a6b323c95e9bd4d5f612d02032dc3 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Subset LetDef1 False Passed
6376a0ef7c275da79ac517a84905647c8ef38b82 Apalache Subset Def2 True Passed
2ccfccc029853ebebc1c8a7451177ea406176059 Apalache Subset Def2 False Passed
789d9e542b350a9aa8eb69ae98e9d2a8fdfb2bbc TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Subset LetDef2 True Passed
0490453d840a7c1570a088ade921f81b0556c5b9 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Subset LetDef2 False Passed
77d55aac26af8ede48ac41d2d57e4a61258676df Apalache Subset Def1Recursive True Passed
449884b06824c68bf2da258a7a11e1063a238d57 Apalache Subset Def1Recursive False Passed
2e605745078af1149330ea87d6ddc905328f1ca9 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Subset LetDef1Recursive True Passed
7f2cbd802c5620dba213338166aec87531d6bdeb TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Subset LetDef1Recursive False Passed
0fd6ebbc31be4bd5ba3d55e7cc49558e033e2e27 Apalache Subset Extends True Passed
7987ab43351df8ed2c58b4aeb0a7e27ffbd73444 Apalache Subset Extends False Passed
9e0b13a25727b17cffe645b3d016f809d460c82c Apalache Subset ExtendsInDifferentFolder True Passed
08dda511771232186eaa23b09a687d17bc212888 Apalache Subset ExtendsInDifferentFolder False Passed
9d38a256aeb670189981d8914600655239651276 Apalache Subset Variable True Passed
892d79707f31b71f4013dde9799a9293ea3bdd0b Apalache Subset Variable False Passed
c5246ab4bb8616da31e0efd80402b74b7a1104d7 Apalache Subset Constant True Passed
1a5d1dc7f94856fa7f0c3f90b3ad4320b6c80811 Apalache Subset Constant False Passed
9030748409e14cbeecfe73a5eca9fee67f479c83 Apalache Subset ConstantRank1 True Passed
5d8386d32a502b456256faa280912f49fa4d644c Apalache Subset ConstantRank1 False Passed
09ea4063ec9c96d4a6625e8f4cf4024c6787bfa7 Apalache Subset Instance True Passed
56834f672aa888e4c060235a4215fd03dd2628a2 Apalache Subset Instance False Passed
ea75818ca32a0cb047da2db70d0547dacb7dde20 Apalache Subset InstanceWith True Passed
d6a3483e0bfd52bf52a10c278a010b2ea15558fb Apalache Subset InstanceWith False Passed
ab945c58e4ef7741cb270bc45c48c72edb6d6a05 Apalache Subset InstanceNamed True Passed
0add343e39d80bf7078cd6bff55b7c415c33f9da Apalache Subset InstanceNamed False Passed
d92a93b17484960bf9f05df55d3ca20b107c9224 Apalache Subset InstanceNamedWith True Passed
17913933a22d345fab2e713d9f1cae987afb36d8 Apalache Subset InstanceNamedWith False Passed
18e022c464d5d75d1363c65943afaf06aa4fbbe3 Apalache Subset InstanceInFolder True Passed
e9a4fef40af8c6b67b3d1b99b1b8e1e9c253dc36 Apalache Subset InstanceInFolder False Passed
196802741f3598efc4c5d9e39a65b971ab87d4e9 Apalache Subset InstanceWithInFolder True Passed
4270016eb7a753d8996380d9d129386ef84185ba Apalache Subset InstanceWithInFolder False Passed
d0d0b88049ba9583c17a2662b2a54c6b67f192cf Apalache Subset InstanceNamedInFolder True Passed
7895dded7fc2fadf5823a2a60356ca8455fba9cd Apalache Subset InstanceNamedInFolder False Passed
dc81f92751a76e5b539bf667cdcee7a9f60361db Apalache Subset InstanceNamedWithInFolder True Passed
5f6ec5e0af09cfadc7cab054c42f517bd5282de8 Apalache Subset InstanceNamedWithInFolder False Passed
5c2450777a041aef3d0f9a452da232c83f4a333b Apalache Subset Cross2 True Passed
d6d92c7c69b5ecf01beca5edfa4c8988e7b77db6 Apalache Subset Cross2 False Passed
c62290d7d7e6e41fd4d5d18033ecce593a911dfe Apalache Subset Cross3 True Passed
1995c37b6f451db2a035d5c18ea0deddeee1c361 Apalache Subset Cross3 False Passed
331b847ff4108627dc01fe072d2ed2355af65372 TLC with reduction strategy:
  • Plug 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))
Subset FunSet True Passed
785cbaa9681d97976b36c6286c27d9ae14a182de TLC with reduction strategy:
  • Plug 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))
Subset FunSet False Passed
e44c451658c3388a771c46f2e25dc37a0dddd211 TLC with reduction strategy:
  • Plug 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)
Subset RecordSet True Passed
e8cb21d6f3349b84e8fb45c5e4d72a2904a09a67 TLC with reduction strategy:
  • Plug 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)
Subset RecordSet False Passed
af2211db2b47700e7480c56998d9cc76389cabb1 Apalache Subset SetDiff True Passed
d4013f0eeb83ba6314adbf3f5404de9f7cf93bb1 Apalache Subset SetDiff False Passed
6964dfa5077cd44a45f13e5920fd4c4905ec4d85 Apalache Subset SetUnion True Passed
59f027414f1dbb2f7dc0ce875465042146735ac6 Apalache Subset SetUnion False Passed
c8db44fef536cb500f9cfd1e6ab56f466602ae99 Apalache Subset SetIntersect True Passed
06af2fd9e08c7907609c5bb6985ef1a372aebffd Apalache Subset SetIntersect False Passed
cbdfb420faaf8ea51f1ce9129a10adeb3919ddcb Apalache Subset IfCond True Passed
25640eb27990e77de0ed147be434580ee252bbef Apalache Subset IfCond False Passed
2fe44aff93c469f446749fb471c8a15a75d56f04 Apalache Subset IfThen True Passed
940869abe45e882178782319844fb5e11e261030 Apalache Subset IfThen False Passed
0cccad69ec8f17c1dc42a31eeede4af6451f6af7 Apalache Subset IfElse True Passed
eb07d8f3ab603e4a01105b37bbdcdc362c54a96c Apalache Subset IfElse False Passed
c6974ce424643138a72979b42cb9e09db2c11294 Apalache Subset Subset True Passed
9933ff964715bffb5a386d7048b99bbe3a8ac2c4 Apalache Subset Subset False Passed
9aac4c2bdf05bc36ef979865a3128fa5ba2c2591 Apalache Subset Domain True Passed
c0be6f023414a7ae2d9036ac8095794c44f70097 Apalache Subset Domain False Passed
a34f149f4fb10369dee39b9cb902dfe823014e47 Apalache Subset Union True Passed
7b0bf74bcaaa888288231c5bb08e79609e36936d Apalache Subset Union False Passed
9f7b2faf48ed2c21d2e9a408a8a2a3ea576a9785 TLC with reduction strategy:
  • Plug 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
Subset NumRange True Passed
39fd24097c00e19e644a2635874622fba0f308ad TLC with reduction strategy:
  • Plug 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
Subset NumRange False Passed
0f411e47d63a89910e209d4eafa94b82231f6f8d TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Subset TlcPermuteFun True Passed
4f8f8e4278179db0650dfebd73ef9eed73f019ea TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Subset TlcPermuteFun False Passed
b87bfdfe18dac67265a3ebb1ab6535ae493fc771 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Subset TlcEval True Passed
ada447683e30b8f0770368ad4443ac74159e2fba TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Subset TlcEval False Passed
0117d385b83c1f9ef9021cf0b3d1305ed5e37923 Apalache Subset BagBagToSet True Passed
8cb1ab9cce73991553892d73f35377df21637959 Apalache Subset BagBagToSet False Passed
3712ce370d712f717cabe95bf0cd9984a9c332de TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Subset BagSubBag True Passed
44d74f513e9f48d235f898b00ec9fc59536cd519 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Subset BagSubBag False Passed
c553c61921282b4161fe4c5d11f1b54e84dc50e5 Apalache Subset SeqHead True Passed
79ec1238cae7457dcead6a72d672ed95c72ff4b6 Apalache Subset SeqHead False Passed