Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
faa402e407ab2fec4af7c107a220abfdad5e40f7 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Extends OneLineComment True Passed
b0c41c51410c5e5a6373fe903ed75f24c2213e06 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Extends OneLineComment False Passed
f9adad3b073c132c2bd9d1e66b00090c040c8066 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Extends MultiLineComment True Passed
4bfac3cbc79cb2cf95a3e2344a0e0578fb923e1c TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Extends MultiLineComment False Passed
209961d76ec119d32404fbc3a14062b979f3e5e0 Apalache Extends BoolTrue True Passed
1cafdbd56ead47c82b87c5ec3e1a1c84fd67b168 Apalache Extends BoolTrue False Passed
88c476bb25fc0ef88528f3ca2d1310e62ba4f0f8 Apalache Extends BoolFalse True Passed
cb5fb8a47995de121669249b25eff0f08b7d00bd Apalache Extends BoolFalse False Passed
0651f6147d0b61acc5545d60399f0fe1b0e52e7c Apalache Extends BoolSet True Passed
2245364448dbc150e1bc1a915a4f55d02516d4a6 Apalache Extends BoolSet False Passed
406190758dcc7efdb123a6a5c64254e29e6fe9fb Apalache Extends And True Passed
46c37ea8efb181c2c05f4c212d90a656af29f541 Apalache Extends And False Passed
fe9af42f0b9c2e15887909dc86bec4ea0a78ba25 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Extends AndMultiLine True Passed
61beb5672f0e0dc888e13231c4d93df161a8f58e TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Extends AndMultiLine False Passed
62fdddffadb373726853a76a4bc304b282a61ca1 Apalache Extends Imply True Passed
bd5c2875439e8855e5e5dfe8508cc7ca5b570d25 Apalache Extends Imply False Passed
f01d366758a3b1f9a433129099f1e6856f749ab3 Apalache Extends Not True Passed
f68c8a06103223a2253b68cf4fca5f626efe425d Apalache Extends Not False Passed
30b3691afa2770c7a8fc1c3ce53cca5aa02d4fa7 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Extends Or True Passed
a5fe71d96396d83fbda6e4ee5879dfff62497b13 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Extends Or False Passed
342004cf1e0128120088af6b2f064dc13b666e6d TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Extends OrMultiLine True Passed
69b1d578199c573867e5efb3e11a3eb3937ec13e TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Extends OrMultiLine False Passed
f197aead88ecd9b6395c675756e5e8b9030d2f97 Apalache Extends AndProp True Passed
24d1bde564f50c84d9018953fb417644c2a53f0d Apalache Extends AndProp False Passed
052642b4cfee537268d3edb8edf7e58e9a029404 Apalache Extends Boxed True Passed
72dec714091cd80f822b8ea041cf81dc3d738963 Apalache Extends Boxed False Passed
21744d92c1fc76e2617e966908652de16f7abec6 Apalache Extends Eq True Passed
5e0b4fc63d2dade4aea9beef7e423c845ee1205d Apalache Extends Eq False Passed
9890d52aa2d5ba55eab5dffd32f266713a4242b6 Apalache Extends Ne True Passed
e6ad78a6e54360696eb09e82d93e6da0e8d638d6 Apalache Extends Ne False Passed
5f55331a470819da7a81cc4250fd750a3b32f053 Apalache Extends Let True Passed
43fc56cc479dabaaa2eaae8e832ecea11f759d1f Apalache Extends Let False Passed
d60604a88533b03a164accb7f4a3854172a03c91 Apalache Extends SetEmpty True Passed
011f0e65ab518576a6b02d4468348d0299828cb8 Apalache Extends SetEmpty False Passed
a2c9cd2320f461e506be5829247eb6ab616deefc Apalache Extends Set0 True Passed
d6e40edc922855431616966479d563d254dda5b8 Apalache Extends Set0 False Passed
269bb933c8f2508763ee7b13574e33e7078d3b52 Apalache Extends Set1 True Passed
5f83f5318246759db76315b0f148cec2bf05d113 Apalache Extends Set1 False Passed
5e58fbca4ab3db3d3cf322a56ac9f4b531020b33 Apalache Extends Set2 True Passed
2237141ba951d1fdb99969226b6fe5d8c88cefcc Apalache Extends Set2 False Passed
5be6f9f3cf932cbec81ff17e0a26868d3dc11465 Apalache Extends Fun True Passed
1d99c917cff8e08467d85e1f9308aec4c35cabc3 Apalache Extends Fun False Passed
36ca1d41b354aefccfb6441f49109267be26b3c1 Apalache Extends In True Passed
8b6658339e843d01a744d25f91c6684ed338a55b Apalache Extends In False Passed
05f59a8ff0114ca8e6d3286050d0f1756e195625 Apalache Extends NotIn True Passed
b946b97866900b336ffd63a5f948901a0e08b05a Apalache Extends NotIn False Passed
0a47c83c6d3c2dd6fbc68210e76f96ef1554a002 Apalache Extends Exists True Passed
423373703102bb2454985190a03855d721be2114 Apalache Extends Exists False Passed
30117a181956a04b1f762281d888d2f1c8a2938b Apalache Extends Forall True Passed
0ee4517f2df7d247b28ff3f9bdd64ffd5a5946a3 Apalache Extends Forall False Passed
2964e4a0845ce6dcd4b4967fc22a5d01cf3ce6c9 Apalache Extends Choose True Passed
4669481b5565e1a5e34ddac19b4a415d3a9f3dfd Apalache Extends Choose False Passed
3854419efd901532dde23526370eb4a383829fbd Apalache Extends Record True Passed
b1ebd05e5f5743fbf29bc4f25e7ce8fbe8527e66 Apalache Extends Record False Passed
167ea0182532b1914be49c23b5e53cb8889ee64c Apalache Extends Tuple True Passed
24636a1d619b596789821882f88860d459574f77 Apalache Extends Tuple False Passed
6bfc89f35adeb4b5405bbf59934f2b3810ebd9de Apalache Extends TupleEmpty True Passed
5dd23dda1364fa607a8daa54a466fcbf6eaee180 Apalache Extends TupleEmpty False Passed
288ce0d50a32933e81ad223741072f472a0f958a Apalache Extends FunApp True Passed
2110d7bb699f3b7ec75d82d76dec6bca70165444 Apalache Extends FunApp False Passed
7efd268c753744c702e379df0b3c767008a70a38 Apalache Extends Prime True Passed
34fe9e0017efe7813239a698b2b006f500da800e Apalache Extends Prime False Passed
0c947f6be722e1708a343e9c3bb5aee94203ff23 Apalache Extends NumZero True Passed
c6108499531c5ecf98ba0431e002482ec69b115f Apalache Extends NumZero False Passed
8efb344c627c96f75ae532e38120071b111eddb1 Apalache Extends NumOne True Passed
28351410ec6f8f8378b9c45fadf5624ea2e40426 Apalache Extends NumOne False Passed
54c6ce476428484a30d8a5812f0cb07e6dff318f Apalache Extends NumMaxInt True Passed
ccdb5df595e64803eec146e165c5b73968710a7d Apalache Extends NumMaxInt False Passed
8a1dad81b0dd59923db726098cdc6adc89f90164 Apalache Extends NumUnaryMinus True Passed
52b65a65cd0c260918b6ae4d17fd309c4d26bdbe Apalache Extends NumUnaryMinus False Passed
2f04536befc2c16ee7c090d6a696bd139d443ea4 Apalache Extends NumPlus True Passed
14b04bd99c8a5e611e972979e20d3489f7dcbe9f Apalache Extends NumPlus False Passed
8aa84de537691605a2a2b25ff486224e8e17196f Apalache Extends NumMinus True Passed
9b01fc8958fb82c30b186ba07b5004ff8203c15e Apalache Extends NumMinus False Passed
3bc1afeaf27559c8aa33309a25ea9007f824f91e Apalache Extends NumMul True Passed
d57e2951917ab367f50516c27178440abff445d9 Apalache Extends NumMul False Passed
1de3898ffb58a2baf5a43f3e0cfebbaf892d7172 Apalache Extends NumDiv True Passed
3c91e880f8f6424161cae9342a8def4a0217413c Apalache Extends NumDiv False Passed
5f2b2e25d45d94da39b9022d72a6ef56db86abe0 Apalache Extends NumMod True Passed
ab576775ef08c270045b9c9982ae01c346eda7ce Apalache Extends NumMod False Passed
e4af7ad04ff96a622d1ef57cfe7dd8c302fc0e6f Apalache Extends NumPow True Passed
f820ad4abceb5314a0b10c5277abf925868a53a5 Apalache Extends NumPow False Passed
fad8bcb34f60ba270711e03af58afa600918af7a Apalache Extends NumGt True Passed
d5a67ff778daa840de90b295964c726d631667b1 Apalache Extends NumGt False Passed
13a8a6f1def2a46a87b2c6155ece0953ebdb3c02 Apalache Extends NumGe True Passed
eb6a5a3f284b744898bf85a3cff6bea0df3bde75 Apalache Extends NumGe False Passed
b1a65f024dbf7ec31f565d8a567492113f9ae367 Apalache Extends NumLt True Passed
a512185c70b2dbab3d09cc710453d631aa9aa7e5 Apalache Extends NumLt False Passed
b67480410d705cd43ece20a4c3130dd57d83017d Apalache Extends NumLe True Passed
bf4df8f866b89f9e811173550b96bb2c99c31a96 Apalache Extends NumLe False Passed
c2c58ef63d24336493a3ceee7fc3c6434bcc7181 Apalache Extends DefFun True Passed
1c743de51991559b997a71fcfc8274a3201b17a0 Apalache Extends DefFun False Passed
cbd069699fc7ca6c817d466c8b95df5cff48fdab TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Extends LetDefFun True Passed
e820c6c290304ec089ce2a61bb6b64c511dec17b TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Extends LetDefFun False Passed
60198255058df2b00c2886c5457845fae429cb14 Apalache Extends DefFunRecursive True Passed
fb105c45970cf4186c713527ff1cd484a1c755c5 Apalache Extends DefFunRecursive False Passed
446a31d2274d729319fbfaa9c7fe4de20db851b3 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Extends LetDefFunRecursive True Passed
99451c9f8654ca014a37f7bfd5b4ff946f6bfae2 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Extends LetDefFunRecursive False Passed
4cbdb4d63a9c75088b5c332e4584671138f6a616 Apalache Extends Def0 True Passed
77ba17d0643520e0d028f7debee8307770100fe7 Apalache Extends Def0 False Passed
3bf8083574989ee37a54d29b73855352df2dbe06 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Extends LetDef0 True Passed
49f7d963bd5f64ee0c424b035832f8f052a9604d TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Extends LetDef0 False Passed
3383029495256d671d509a01a06a46c4437a188b Apalache Extends Def1 True Passed
8de2eaabae95f3177bf0dd2d28b01c63fdffdba9 Apalache Extends Def1 False Passed
d8e0518f4570a7224c2f7ee3861423bb420b812b TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Extends LetDef1 True Passed
6907d45a54563f248102ca20067a0c7b3ed4d2a4 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Extends LetDef1 False Passed
f09513aca719e5bde83731b36d8317fd8e3c8638 Apalache Extends Def2 True Passed
5ff9c7c0050587edeb466cf1bfb1196b2956871a Apalache Extends Def2 False Passed
d598a7de186acdc73a558307f59cb1f8bd83dd49 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Extends LetDef2 True Passed
e8c0d3151a57b62238f0970ded4fa0e597a42467 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Extends LetDef2 False Passed
ad350d3276f2811a955f2ed53b2d61e74d974b0e Apalache Extends Def1Recursive True Passed
0e765c0f5a0cbe9294217c021f8944f82cd204ed Apalache Extends Def1Recursive False Passed
60c63100cafe9312f5dff005951222424c966e14 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Extends LetDef1Recursive True Passed
f27c869ef46dbaa7fc58f7a25a8bf506ec1147aa TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Extends LetDef1Recursive False Passed
a32398b489af72ef5d1362aaebae8170f2827f5f Apalache Extends Extends True Passed
ded3010d8e584e836162660f692c581814676aec Apalache Extends Extends False Passed
b89ff633d3ae7344138b5d61159fb0c5e1899535 Apalache Extends ExtendsInDifferentFolder True Passed
d30d358844ff68492aa1ba105e9990097f7cff6a Apalache Extends ExtendsInDifferentFolder False Passed
d2d1586262dc84fabea6709f77e99e6ab3793a8f Apalache Extends Variable True Passed
6b5a2c468b8eef15b74a6f933c562e9c853f5622 Apalache Extends Variable False Passed
40b95583b4ee7d7aa8ed8204305bd3df04185bb2 Apalache Extends Constant True Passed
e136c58ac07edcf0a0bd809c89ee4850538b13fd Apalache Extends Constant False Passed
99b29fb34566965e20fc2501b0c8eb1735f3bc92 Apalache Extends ConstantModelValue True Passed
e010d841b4c42de25e834080c6eaf8c9b85a40ed Apalache Extends ConstantModelValue False Passed
161eb8e7b9a295a940a1ef7dc53569b3e469e123 Apalache Extends ConstantRank1 True Passed
41752ce9a53801934478a858ef85513e5f0ad5b9 Apalache Extends ConstantRank1 False Passed
7373bb312482ca573cf40ca19e6a9b38d698b2e3 Apalache Extends Instance True Passed
3aaccce3b42ea3cb479d96fe61ae3879bb451a67 Apalache Extends Instance False Passed
341990fdd50c65810f7b4662a912f757755c0a1f Apalache Extends InstanceWith True Passed
95c37a7650145fad961d76280d8b52660e53ee2b Apalache Extends InstanceWith False Passed
28ae19035281e3f0500cb9d0edb8c5f68757aacf Apalache Extends InstanceNamed True Passed
53ac7fd6e0b6a66c8f0ad10d728dabb6a92503aa Apalache Extends InstanceNamed False Passed
a5b48543d9fcb16c5c791d4b917f58b87549efab Apalache Extends InstanceNamedWith True Passed
42ff7457cd658b73ad7f0f63ca2ffb0232c13483 Apalache Extends InstanceNamedWith False Passed
d9ddcaccec233c092259739d809fb7b1f5109a3b Apalache Extends InstanceInFolder True Passed
7db4e3ba5fca3b1ff8199d2c3c11ddd1bbec59e1 Apalache Extends InstanceInFolder False Passed
ff85237e6132478d33246ccd9e6abbbd04f8b73f Apalache Extends InstanceWithInFolder True Passed
bf142383dfd348681b7c68e3188ed2035502663d Apalache Extends InstanceWithInFolder False Passed
8eb175cc1c46a360c47da0d91fe8783a8dbb1a72 Apalache Extends InstanceNamedInFolder True Passed
aa7188334e1c581ddb6cda7d78274be201436fa0 Apalache Extends InstanceNamedInFolder False Passed
582d4a67e868e233c7801af15753aa47e5bd4e90 Apalache Extends InstanceNamedWithInFolder True Passed
f62b248d9d7f2eff3ad9164b8bff6da589e53d49 Apalache Extends InstanceNamedWithInFolder False Passed
baca5dba3dc837c06c7b8db4d43da1acfe5f41e4 Apalache Extends Enabled True Passed
ee9eb0f42bae269968a65ec5e185bcd179158bd0 Apalache Extends Enabled False Passed
d0f929d244e399d8f39bf19cd29e00689977d12d Apalache Extends Cross2 True Passed
96cf90c5c513b5578dce2a717210591de61084cf Apalache Extends Cross2 False Passed
b56e0dfc9c4ef0d674a3d8fb5b98629bdcd6f862 Apalache Extends Cross3 True Passed
fdcbccd6c2970ccf31385bfd113063212e4b8ce0 Apalache Extends Cross3 False Passed
70b4a873d920ba7b32911e571e0df2daabe9e6d8 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))
Extends FunSet True Passed
db80032574598790f56b3fb404e62401e1ac5c9b 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))
Extends FunSet False Passed
1cb2200b81d2548dc01b314bcd12b72a3a3ceca8 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)
Extends RecordSet True Passed
ddc1a3fbc434c3e29fb83437ed1bad672f87a557 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)
Extends RecordSet False Passed
f24e460193c487421099d8c84dad8e60d829c52e Apalache Extends SetDiff True Passed
df8bbc623592723a18bf1361a9ab9b3423e8a505 Apalache Extends SetDiff False Passed
7477576fc592a21247905ddf890929cb2e65e813 Apalache Extends SetUnion True Passed
d4e8aa6bc54f41f181017ec82ef1da8f23b3580a Apalache Extends SetUnion False Passed
6dd75ef0e30832e3beef311f95ab9c11da5975e9 Apalache Extends SetIntersect True Passed
5bfdf14ab1b0f5a5dd1e8c3cbf7348b5caa576de Apalache Extends SetIntersect False Passed
9adee1aa885cac38fbe8ee0f009e542d191c2fe6 Apalache Extends SubsetEq True Passed
1f49285e532031a60a80eb3072a1af443129ee64 Apalache Extends SubsetEq False Passed
35b88692b5b310323a371efb494d0970c9b954f7 Apalache Extends IfCond True Passed
1473b360373edc360e034bcbf5b8e2b5f6c76649 Apalache Extends IfCond False Passed
c7583d3aa82ba816d06d847da04fdf9f4b41aa2b Apalache Extends IfThen True Passed
2a01d19d962001616465c9456dfc4b91049d4573 Apalache Extends IfThen False Passed
be234495e4854b5c1e9c78329ce91258ce28030c Apalache Extends IfElse True Passed
443373a8334263bb0de395337cd8189bb970930c Apalache Extends IfElse False Passed
9ac34bae1e04b44d090f547bc7c831e49f2e36ef Apalache Extends Subset True Passed
72f542fa240887e788d0fb6f7e812491788cb593 Apalache Extends Subset False Passed
0bb2149e8465f60010d7f2840d25a7edde1d0d88 Apalache Extends Domain True Passed
14a8b886d46ef85f1c48370bcfca97c31bce7208 Apalache Extends Domain False Passed
6b1f6b5dc02ed678ca3532711549758738db274d Apalache Extends Union True Passed
05455c56cecdd452500e6bf0025a97cb81d80e5b Apalache Extends Union False Passed
015fdf54556b508beb16eb4d526e2924ea072539 Apalache Extends Unchanged True Passed
439c7efde190d6c04c11f4d3217f68cfa0e59322 Apalache Extends Unchanged False Passed
ad62ea61f2b7e73a7186df2688e2de4a280bf5c4 Apalache Extends Equivalence True Passed
dab843f18af465dcd34abfbcac5adeead85b320a Apalache Extends Equivalence False Passed
30b859637798cc8e8c978b973f7e2310d91873ed Apalache Extends StringEmpty True Passed
2116ecd68e0469e81637252103f38779743a447c Apalache Extends StringEmpty False Passed
b840e1d5b1973bcbcb0efc1c2e9b558f21cc4433 Apalache Extends String True Passed
c19cd6e3473851e254e84a5341dee91734a6c73f Apalache Extends String False Passed
76b3a644a9a50a2079173628478ad9de0128e0b5 Apalache Extends SeqLen True Passed
df78ec29c6c60576d25b50bf80203f7074e5717a Apalache Extends SeqLen False Passed
ce9f9c8c04bb2368bc91b85085e339a4996c3924 Apalache Extends SeqConcat True Passed
0ec2d3af8c76e950333bcdaab025392c58c37fb1 Apalache Extends SeqConcat False Passed
61d55e5c3342d3def03cc5597cdbfbb709771efc Apalache Extends SeqSelectSeq True Passed
ab60f89af34fbea7ab6fbab26d5ffa881d96b3b4 Apalache Extends SeqSelectSeq False Passed
1801562e1dae14dc821747f02e1c749292663733 Apalache Extends SeqSubSeq True Passed
8808bc2a7ef0bd92e0f1fe587c34f23947f364b3 Apalache Extends SeqSubSeq False Passed
00e3b7c501562baa5a158bea28bfefa0c5f9bf73 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
Extends NumRange True Passed
0a333378495afc48e1351f2433b50f797f5c0bc6 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
Extends NumRange False Passed
72e7ec6e6c0b5b4b947c2f645f5f6629764a028b TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Extends TlcSingletonFun True Passed
c24b6f88923731f1a158116512a8c4166a1cfba1 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Extends TlcSingletonFun False Passed
ca4c8f50cf310bea51af0a2c6fee615b6a57f7ff TLC with reduction strategy:
  • Plug Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g |-> IF u \in DomF THEN f[u] ELSE g[x]]
Extends TlcExtendFun True Passed
52e0062cd02602b8df71f6a9dca5a0180b3518ed TLC with reduction strategy:
  • Plug Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g |-> IF u \in DomF THEN f[u] ELSE g[x]]
Extends TlcExtendFun False Passed
f7f858a5bf04954e2a26c43e33efb80e53509d72 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Extends TlcPermuteFun True Passed
f7f17fa7c0a08994a1431b232a5a1436f011e7cf TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Extends TlcPermuteFun False Passed
86ea0b23bde2bdfad4a74b80677b47feab9212d2 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Extends TlcSortSeq True Passed
faf8409945a08edda67359e10e7de12baba8d17a TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Extends TlcSortSeq False Passed
62422f8b177e33e9806813c14c7e3c04e50a80ab TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Extends TlcEval True Passed
7dd737740d89752d6ae8983c6862f843fb86d8e9 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Extends TlcEval False Passed
a02232e451e0f9461cb22178e4fe28f75c41e761 Apalache Extends BagBagToSet True Passed
6f8834d165e6b457d484feeb5dcfff26a1b6c552 Apalache Extends BagBagToSet False Passed
a942c24bfc3743b216b334d1efb81ddb7e38f8a4 Apalache Extends BagSetToBag True Passed
ebf946fab7e8bc876a78ada30103356661000aef Apalache Extends BagSetToBag False Passed
adc8441965ad261d3a19da0736c6bf48a5607695 Apalache Extends BagBagIn True Passed
bd10699b3df8ac83fb0349de4adc98fe7d54b532 Apalache Extends BagBagIn False Passed
7d7927fced4c4f7efcfd8f4c3bc260266bedb29f Apalache Extends BagEmptyBag True Passed
496d3d9ba84406b284edcf6e192c93e25b421d86 Apalache Extends BagEmptyBag False Passed
94fc5b41a2b2c64520172a0c077be040817439e7 Apalache Extends BagAddBag True Passed
6fc061a289a816148ebe870b8a88b3541857d5e4 Apalache Extends BagAddBag False Passed
5e84bae7e45f16c8fe46d24d4f6abab6766bbc3c Apalache Extends BagBagSub True Passed
aa173092c68ee074962f67b9224f417c6e7959b7 Apalache Extends BagBagSub False Passed
2cf9cc564e8f8a9be33b9df0cb0c5c517a3020ef Apalache Extends BagCopiesIn True Passed
291fc14fb3d550de58933a5fa3eb00e075f32894 Apalache Extends BagCopiesIn False Passed
70db327844b371cc77954067a813e034da5efeac Apalache Extends BagSubsetEqBag True Passed
ac2c3d0aede589bd568a98e66b23e70f260d2239 Apalache Extends BagSubsetEqBag False Passed
16c9e2ecf63d945ec527004990179c2f79dd0cdb Apalache Extends BagBagUnion True Passed
79872fde454c1b86ff81843c00852d4393c36042 Apalache Extends BagBagUnion False Passed
cf49aaac889c1bd56be3a56456a546214f5d3dd0 Apalache Extends BagBagCardinality True Passed
29f7512890e8c87e405547233a5baba3426ff0fb Apalache Extends BagBagCardinality False Passed
8fa72b476877aed1137dc37bc0112127c28beaf0 Apalache Extends BagBagOfAll True Passed
0c37cc504d1492bc78df4c8ad2bd6e760a7d3fc9 Apalache Extends BagBagOfAll False Passed
c40f606b1c15852c51f511c6f8d3fb36c7c11aa5 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Extends BagSubBag True Passed
dd8a1c196637cab6224f146f7739f18e88fabc24 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Extends BagSubBag False Passed
5c18f4e8a4849021d8043aecfb8deec6d2a7af19 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Extends FiniteSetsIsFiniteSet True Passed
e99029868d67cf964a40863df4cb1d44644d76f6 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Extends FiniteSetsIsFiniteSet False Passed
fda09763757f5b065ee1f20f3015191e6fb2b678 Apalache Extends FiniteSetsCardinality True Passed
1f6616c385352eca1555e33d7aea448a46fa2dbf Apalache Extends FiniteSetsCardinality False Passed
26c0653faab3ca94d1ce46f7324f243c8efea767 Apalache Extends SeqHead True Passed
947bd84d55b0f34200deb00925204e76aac65e29 Apalache Extends SeqHead False Passed
ccea100c75194e28894bf8a1a82ac17be47391b8 Apalache Extends SeqTail True Passed
d358346462a1f7de9a26a78453b22345b3b75b69 Apalache Extends SeqTail False Passed
c2af88fda02c482911205b5fc5492c6e9b6fcfd2 Apalache Extends SeqAppend True Passed
338c5b3c662899db1b98877458ab0e3f4ade9832 Apalache Extends SeqAppend False Passed