Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
063a3e15d2f5b71c40f6be2cb679d41efc5cc364 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Lambda OneLineComment True Passed
b14cee145e0b9b3965c96f1abc6d3fa857814302 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Lambda OneLineComment False Passed
0b2e0ce649567fc1f36c9b614f78c19a9ca89a4a TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Lambda MultiLineComment True Passed
1aab90aba709b5f678ba2447f4c9834e2ba9f4fd TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Lambda MultiLineComment False Passed
1656b0239965b32e9e8d836d3075b2d55d15c59a Apalache Lambda BoolTrue True Passed
be724b3106283d090b05ec11a25a31d5c064a05c Apalache Lambda BoolTrue False Passed
98f6a57bd6736530c61a3d28468e53305c2e1ba7 Apalache Lambda BoolFalse True Passed
50ea1e9f54ff3874c4e28ef3cab6e925a226ea5e Apalache Lambda BoolFalse False Passed
d2d9b20bc670c5cc255988f0329661b2a6f01d65 Apalache Lambda BoolSet True Passed
9e128778ad2caef95476d398dab68de35eacc864 Apalache Lambda BoolSet False Passed
fb0ea992400043826e0e2dd293af5a5a42d7b976 Apalache Lambda And True Passed
b1acdc641bd2ed8f01824b87a2c588f9ba3c2b3c Apalache Lambda And False Passed
46445949b0e87133a8641c23e5fbc244d3caf689 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Lambda AndMultiLine True Passed
154d4bb5f4bf87dd5f213811d778390693820520 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Lambda AndMultiLine False Passed
010406c9841522b35a1f7b4d04e15e8718786064 Apalache Lambda Imply True Passed
f57a3015ea236f861ce0316d18b6b19909279d14 Apalache Lambda Imply False Passed
5ad8f1468be36eb0fd6b3108fed35827132cf032 Apalache Lambda Not True Passed
f7b76d27b6954261b997535d72efcbe60aa6d13e Apalache Lambda Not False Passed
90d9739bd1d6afe8cae660f6ebbcda3911a58b87 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Lambda Or True Passed
fec5d9cc99c80bb0ba6f7ae1b0f33a3112449845 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Lambda Or False Passed
1ef347f4354a39cf223212284b51745863760157 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Lambda OrMultiLine True Passed
84e2dc3090f15ce856f9590f927d56456a5f45ed TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Lambda OrMultiLine False Passed
b4b5c11bcafc3902f696b5cd9f1bb5abde17e5df Apalache Lambda AndProp True Passed
f303aa5e42691b3a13ccb23436d27cc53f9d5e88 Apalache Lambda AndProp False Passed
b25a22e9df9367b51dc51b5adb0e198e943d03b5 Apalache Lambda Boxed True Failed: TLC does not support boxed operator in LAMBDA expressions and reports an error
4435a5467f708d6ab63fc8edd9966dbc27a3e96e Apalache Lambda Boxed False Failed: TLC does not support boxed operator in LAMBDA expressions and reports an error
6f6bc9d9e74963b03c2eeba8bedfd12e348b721c Apalache Lambda Eq True Passed
7321a06c816ecda5c3e5847a4d3fecfe4d7fde0e Apalache Lambda Eq False Passed
cf1048a911bac5be62eefc006ac411ef8209a8ea Apalache Lambda Ne True Passed
006c59cdc786749b10209a9d48ba1f4362787c5f Apalache Lambda Ne False Passed
e5b044149ebbc21ca8f7114d6f8631bb447f2f5f Apalache Lambda Let True Passed
3494b027929168b299115d7adeb0f3df138f5b90 Apalache Lambda Let False Passed
d049425cd6bb270ca61ac3036abd179e62176759 Apalache Lambda SetEmpty True Passed
b68078ed13fd785ba530c0d7322fd8a146a1fe5b Apalache Lambda SetEmpty False Passed
13ad0e1b4c7c1b82acf5d5d3f9e9203943f86156 Apalache Lambda Set0 True Passed
d9b0dfb56c67f141e1e074f3844ca7a12571175f Apalache Lambda Set0 False Passed
4ff48ca21a2c9f563f26a0ed04075d01bb8b11f4 Apalache Lambda Set1 True Passed
f7f35d0f2c1656563160891fb6fe4437f3ace7ea Apalache Lambda Set1 False Passed
b052856fdc1197c0286c38af0ab2dd9b4b0d9069 Apalache Lambda Set2 True Passed
97d58d460bec5e3095423f307cdb356c01e4b86f Apalache Lambda Set2 False Passed
bced6d61a750336a1bb1800ef7b9ff39b4a4eb3e Apalache Lambda Fun True Passed
b20f547cd73d14029dd8a25497d15dc57b58bf0c Apalache Lambda Fun False Passed
119cfef18be70ffeeea9496ef7a8f9ae7e919d3f Apalache Lambda In True Passed
a409c2089a4afd620edb783886b5edea39e5712c Apalache Lambda In False Passed
e39dbb7195c8a96f29a1a2de2afe73930f9ffc31 Apalache Lambda NotIn True Passed
47c7f0a48d4a3518ea936f4e8d3e0da5b30947de Apalache Lambda NotIn False Passed
1c15a66f277e42aa838b9487b12a49b4c0437648 Apalache Lambda Exists True Passed
dfd76f2a8d6583bbca288d3899cc11993ca62ffd Apalache Lambda Exists False Passed
949fcede39d65c8eef26c1ffbe56060063ee5200 Apalache Lambda Forall True Passed
7253c14011ca84f19048909b1d9df5b96d19db5d Apalache Lambda Forall False Passed
0a6094d460eeaabea885a1f97183b3f37c3662b4 Apalache Lambda Choose True Passed
d8fc305124c2318d1510ecd1f1ec812786dbede0 Apalache Lambda Choose False Passed
c2148e1070e84860a6e477cc52f1770ed5975b2e Apalache Lambda Record True Passed
0b4f2e07d2ade199f863843227aed14cb065bc54 Apalache Lambda Record False Passed
e67225c10934de7f67643beff679f77226bcbefb Apalache Lambda Tuple True Passed
61fbc9c06ab9dffeff64e6867b9a3ba761d1c3e0 Apalache Lambda Tuple False Passed
185a73404334cb2f9e93e476ff531f47fad99872 Apalache Lambda TupleEmpty True Passed
607dff5c04cb01163a580e28374c9136baa21a2b Apalache Lambda TupleEmpty False Passed
b1f0968dd4ef50f6a1cf115d9c56af374d1b0b50 Apalache Lambda FunApp True Passed
f9ab8fb3290e9453e641cadb92e78c8e8177f56b Apalache Lambda FunApp False Passed
4f6d34b2623b6b74fd6b9a72113b95da12a6dad8 Apalache Lambda Prime True Passed
2bf67c952db7a50a385bd35e229daefd3e34023e Apalache Lambda Prime False Passed
4f037cab30a446cd1af0984c53b748a4cd6d4507 Apalache Lambda NumZero True Passed
b3888c7d7fae718d6e70e51bdc33553dadf24417 Apalache Lambda NumZero False Passed
55ad1d527879be5e780f9c8655f6c04e0d3e3cb9 Apalache Lambda NumOne True Passed
418fd1632906fb710e49a119641a9e892047caf2 Apalache Lambda NumOne False Passed
c976fccd4d4cf00ae5758a9ce7e8931113ccecfe Apalache Lambda NumMaxInt True Passed
38c035989d9623ce390c96c280033ff33d650bd2 Apalache Lambda NumMaxInt False Passed
d01bb0ce92d5b7372ebc49eeb17c9074a7bbe1b6 Apalache Lambda NumUnaryMinus True Passed
1a617722fb6f59fdf5fc5787726cd30d0dd623a7 Apalache Lambda NumUnaryMinus False Passed
4571513c699248c168df867bf2c4cfc355287f90 Apalache Lambda NumPlus True Passed
fcb8f41d88a7a60e1197bb57358f2a61426a4dda Apalache Lambda NumPlus False Passed
083298025451bcd0e04800f65757f1d9844dc397 Apalache Lambda NumMinus True Passed
5f2cb5a0acff8f9f425b02fd3aaa84df0e0917a2 Apalache Lambda NumMinus False Passed
9ccc73628963b299db19045ba8557228ef3576eb Apalache Lambda NumMul True Passed
4aad55266094d1833b1941fb79311bc2542a3726 Apalache Lambda NumMul False Passed
d5b755a83e33f168695b28ff21b9726e7934bee6 Apalache Lambda NumDiv True Passed
28c4b90b18bb68985e6a31975954bb1ae0190d28 Apalache Lambda NumDiv False Passed
678d8edc903445263cef0afa6dd828b446b66f34 Apalache Lambda NumMod True Passed
4b941f265e044c8e38db6ef8fbe24a8414cef261 Apalache Lambda NumMod False Passed
4a423a76e9b8533fbc40d6217e9169c58c51496a Apalache Lambda NumPow True Passed
c7435930673c1081b99de6794e782ac470c52f12 Apalache Lambda NumPow False Passed
2a10bd4e62da01fe7ca9c77c8d782f9d005238c7 Apalache Lambda NumGt True Passed
683afa699c6e77b736a23a5041608c2b8d12ecf7 Apalache Lambda NumGt False Passed
3dc1cb0f989d7336a9a089e9530987fb8e245fd9 Apalache Lambda NumGe True Passed
ce1d352d570b31f00f85d6a1a3660a9e47051065 Apalache Lambda NumGe False Passed
cb377b74dfae58e33736184529ecc4428c162af1 Apalache Lambda NumLt True Passed
2db6a90a4cd4b21be80108cae2ccfc2159138446 Apalache Lambda NumLt False Passed
95076204d44a1b19800909bcdf610de37bf719a5 Apalache Lambda NumLe True Passed
73a69490d1df50d7dc08068048ee01099a57333a Apalache Lambda NumLe False Passed
ecfc7e6190d3defc85533c240473818e6937efa7 Apalache Lambda DefFun True Passed
1314ba482e7acd652918e39adf695faa171094ae Apalache Lambda DefFun False Passed
c046ee0870cc236f990ce24be32770e72860a833 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Lambda LetDefFun True Passed
d27b975951bc90629f63cba8c5f8851ac99e729b TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Lambda LetDefFun False Passed
2af28ccb72f493e69ca3800a5041c18f6bdd4260 Apalache Lambda DefFunRecursive True Passed
02ddfc57ce01c103363a0a1cf063abc4598e1be5 Apalache Lambda DefFunRecursive False Passed
97ba3cba73522dfc5b52435b6b0eaef64c33d127 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Lambda LetDefFunRecursive True Passed
d8592b55b603e05ade93373c3434be8b12b939a7 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Lambda LetDefFunRecursive False Passed
d0053f0cdc817691f3254a35ddec2773ec03829b Apalache Lambda Def0 True Passed
1820c57576a136644d91285d1888966692206231 Apalache Lambda Def0 False Passed
9922d82ea7173e762e2e989afe0807ba64d03c95 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Lambda LetDef0 True Passed
e01f86a296d09584b56d0ed8c080a09602c86549 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Lambda LetDef0 False Passed
43c602a079fe36f4da4643b1b13ed9c2b924ce99 Apalache Lambda Def1 True Passed
81e5d55607dbfc17b8985585bb9bf6a51691cfb0 Apalache Lambda Def1 False Passed
30d02dc13d60f833ff4787c14c692e2346a9016d TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Lambda LetDef1 True Passed
fd1705e06244008c69077eb943a6b7e19464c71b TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Lambda LetDef1 False Passed
7b7b1b08c561ff596fd9d781f05e1bf01fc3d656 Apalache Lambda Def2 True Passed
805110db68ab2e2e981419691ed073181d4b7a8e Apalache Lambda Def2 False Passed
67c30e614e6e1a25207d190c0eddf02b363b8a3a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Lambda LetDef2 True Passed
5147c313e07a72bbe05488fa41aa79ff32b8b417 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Lambda LetDef2 False Passed
5eb32f0d3462e2ffd44a89695634d67a5e5e6638 Apalache Lambda Def1Recursive True Passed
71aaeac7d39d7ac19820ac5e6aa484a08372fdb6 Apalache Lambda Def1Recursive False Passed
af938c3c43bd463301c339a470d339d48311ba70 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Lambda LetDef1Recursive True Passed
749a3b29eff22c98423cc18fc423ca8b1a580cb9 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Lambda LetDef1Recursive False Passed
fab917075bf9c7b6e224e39e49801446ec36a739 Apalache Lambda Extends True Passed
90a6e439286370ec6fa739e9c5d35fd19f98c261 Apalache Lambda Extends False Passed
2a0b1ac91a696089c245734815869dd6cedb75a6 Apalache Lambda ExtendsInDifferentFolder True Passed
adf18be2adea5151f3bfce5ddffea290864ad917 Apalache Lambda ExtendsInDifferentFolder False Passed
357ea49b57aae256b86ec2af0baba61b4f0f4370 Apalache Lambda Variable True Passed
2ad7365971ed588f0e8f3aca69f2ad7c52df153e Apalache Lambda Variable False Passed
29046a9cfee3dc21eac4e7c5ad8ac79d014e5a72 Apalache Lambda Constant True Passed
ee5e539f73b8d1769896b7544bf62a436e09f99b Apalache Lambda Constant False Passed
3b5001dde714b93021887b1d766d2ffec63ee68b Apalache Lambda ConstantModelValue True Passed
da709d3f87e246d84fd2f1771a8076f518f7d9de Apalache Lambda ConstantModelValue False Passed
c6ba49d5151b7cbcd08913b38dff4d4463e9b7a0 Apalache Lambda ConstantRank1 True Passed
10c7023c1764d1225b9ce4e7607cba5d23b2a7b9 Apalache Lambda ConstantRank1 False Passed
ae1b44cf1437005b3f2599e35059851ad9883f5c Apalache Lambda Instance True Passed
f2b94d36c82925faa00720c2ea8aafce3233474d Apalache Lambda Instance False Passed
b0768969d06c4b44bf5cb8297ee1348fe9c3c169 Apalache Lambda InstanceWith True Passed
2861d8281b46e34c223fe37e3f317b4f580fc87f Apalache Lambda InstanceWith False Passed
926e194aa44ad22596584e18706deec1b246a656 Apalache Lambda InstanceNamed True Passed
8a76fe061c38794313224e2f1cb91e0ca6b61ab2 Apalache Lambda InstanceNamed False Passed
25cc50f9c786a5183f518bbc48ca74a572856bf5 Apalache Lambda InstanceNamedWith True Passed
be995b813cb36b978dd658f491ea68b931cbce48 Apalache Lambda InstanceNamedWith False Passed
0b59c51b50e4a12864b87acc13b8b922bfb10d8d Apalache Lambda InstanceInFolder True Passed
c58f648f764357c8c836e7374d85feeb8e15a980 Apalache Lambda InstanceInFolder False Passed
0390fd122a523087ba03338d7dbe1facf4162da9 Apalache Lambda InstanceWithInFolder True Passed
5b68d2bc2d3c37e4619667aa75d4395b15ea0076 Apalache Lambda InstanceWithInFolder False Passed
94497c0355235c8197c6da0cfab8aef61a77e181 Apalache Lambda InstanceNamedInFolder True Passed
e8902f2d8f017fc8d229fe28efac46821fb09f4b Apalache Lambda InstanceNamedInFolder False Passed
2617267928950c16d62404c430b31040da9002c4 Apalache Lambda InstanceNamedWithInFolder True Passed
defe866cb13c185d3a26a0b76cc0556beb17f9ae Apalache Lambda InstanceNamedWithInFolder False Passed
73edbe7175e12de4586e6310055719ae987ce291 Apalache Lambda Enabled True Passed
d55b0c31529dbe4d78f6378a6bb966e5d0750b0b Apalache Lambda Enabled False Passed
f64a4b1d07b2c43b922294aaa4c6073014cebc59 Apalache Lambda Cross2 True Passed
68690b8f3bb2b9d820a7a3082649336792bc46b9 Apalache Lambda Cross2 False Passed
2644b2fcc898546239e2c01119da9e6e5c4263d9 Apalache Lambda Cross3 True Passed
1260f84d403f42607c8924b12716e0d37f88cb7a Apalache Lambda Cross3 False Passed
fb795918afc1cda730e792fc2e0659d5416a1ccb 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))
Lambda FunSet True Passed
b472b50080703cbbe26fd70db6d83905ac9eb920 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))
Lambda FunSet False Passed
357bede6315bae19fc00250b83d711370b404920 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)
Lambda RecordSet True Passed
c778c4714705bc535a29b9f200bb07465ed3c463 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)
Lambda RecordSet False Passed
7af318eb39c338456cbf3569f27a60376fb548e2 Apalache Lambda SetDiff True Passed
4efdea427cff715e94672671f3e1ba5222b820ba Apalache Lambda SetDiff False Passed
b6d4207eac7a977ff5e708d03510a9f7782963c0 Apalache Lambda SetUnion True Passed
a49973b821c6f57549e62c6adabe6619688f6bbf Apalache Lambda SetUnion False Passed
bfe77d387705ab469d206bc0d0910be74e19d6c3 Apalache Lambda SetIntersect True Passed
92dc77c10af5fa5e0e020cccb69ae9529b6e4979 Apalache Lambda SetIntersect False Passed
810e4cd5b6144041cacbed11d236e25c8aab94ee Apalache Lambda SubsetEq True Passed
b88c56bab7c072e947cb6b764adb0c76d673a401 Apalache Lambda SubsetEq False Passed
2fdf684ea85e2b34300e50c19c52aebcca5c5f76 Apalache Lambda IfCond True Passed
5587653c7e3f831fd71521693ea4de354fcb2863 Apalache Lambda IfCond False Passed
eea10d4f6ee8cd0589ded205014124380cc11c06 Apalache Lambda IfThen True Passed
669d94e6929ed4d122641457b3989b83f3b759f9 Apalache Lambda IfThen False Passed
65f4905de6665fb7023d95f856a64d9e98051ba7 Apalache Lambda IfElse True Passed
86d3ceaf6260ef6a5d1052cb8a536f3531e3d90c Apalache Lambda IfElse False Passed
fc4aaa7686f17d7b9a5657a59fb45e2dda60d514 Apalache Lambda Subset True Passed
967ccbc3d512b486f99bc819f4f3049cacdb4d0a Apalache Lambda Subset False Passed
a1a941f533080657135a40448b5de865d7d64165 Apalache Lambda Domain True Passed
e2f4f79bee5c04415b74fd793f750f12adc1a400 Apalache Lambda Domain False Passed
9c7d4576581c44e25042dd80f4efaa3974c70779 Apalache Lambda Union True Passed
00be486b5f180738018bddb970be89411b8a10cd Apalache Lambda Union False Passed
c71b3aad5adf026cc0a3cf684c3a5070f75034f7 Apalache Lambda Unchanged True Passed
7d6727edfcb332796350e9c10d51c2aea06fac23 Apalache Lambda Unchanged False Passed
f1243afefb39647974c6a0262cf630f0ae92b029 Apalache Lambda Equivalence True Passed
86bbf869e3f3e207d05aac038a876df17ca43a7a Apalache Lambda Equivalence False Passed
5a00370243b1ee34165f5aeb13c0308e6f4b9317 Apalache Lambda StringEmpty True Passed
947608e75dddcb170fc69962e43607d9f702e04b Apalache Lambda StringEmpty False Passed
fd85efdc9e2981d715c4a86fcdfc172c34c7dd55 Apalache Lambda String True Passed
dbea79b52dea60f567a8ec5b5478730b8fde6d00 Apalache Lambda String False Passed
6d839b8f4eae3cfdb796e9c333674d30b4ea3b51 Apalache Lambda SeqLen True Passed
e638e36c7f68d7eaef2d6f3b263e0b83e29eddd9 Apalache Lambda SeqLen False Passed
c8eafb801d4efa0159cbafd28b802fde48ec4106 Apalache Lambda SeqConcat True Passed
83188a46e6111cf1e7960b0d779c66f31f829c3d Apalache Lambda SeqConcat False Passed
bd15ecf3f087dd933cb121156e68458ec9676b56 Apalache Lambda SeqSelectSeq True Passed
36ce90cb715e0c4aecb36002c0e6d2a15291534c Apalache Lambda SeqSelectSeq False Passed
ba23acc8a21bd5b779fc279212bce57065f15678 Apalache Lambda SeqSubSeq True Passed
21e4bff41ac722653d677797e949f4b8e1a62479 Apalache Lambda SeqSubSeq False Passed
e2ad287bf697741930c05ef04436a43d0684fea6 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
Lambda NumRange True Passed
c8a359508b0988d08d057afcb75479edf41a35c7 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
Lambda NumRange False Passed
04bf02a3f7ab1281965d76c0a814e35195b106c0 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Lambda TlcSingletonFun True Passed
5987bf986e8700cdb26c324dd4168251b58f7fb6 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Lambda TlcSingletonFun False Passed
5dd00e1480f3caaa9edb4708174de031d7a4fa91 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]]
Lambda TlcExtendFun True Passed
dca746bfb474e76a9d3fd16cfdf9c88d6c3d97a1 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]]
Lambda TlcExtendFun False Passed
cb5f382ec001fb8267ed2955759b565fdb9615ab TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Lambda TlcPermuteFun True Passed
438c19e3e606d5a64f66d1e6f9dfd7b98d37ddff TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Lambda TlcPermuteFun False Passed
bdcda349ffecfde46ee45938e3712d87cf7d4988 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Lambda TlcSortSeq True Passed
73a09f1779c15d27394617e988ccd472769d9e55 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Lambda TlcSortSeq False Passed
95cfafb2d46d111fb7082455114a0c02404f42be TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Lambda TlcEval True Passed
cda654c44e128b9c8b0eba6a1ba4d8b1e05cbbc3 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Lambda TlcEval False Passed
8356e3f4413058fe1c27b744540907f455e2ac2d Apalache Lambda BagBagToSet True Passed
bac3ac78de6e0a2c72f66e7e499be62a616a8c0b Apalache Lambda BagBagToSet False Passed
8d5c835a0dd06cf8c9055d11e11155d89af78d99 Apalache Lambda BagSetToBag True Passed
63b06297133db179066d9984609f7782499d6cc1 Apalache Lambda BagSetToBag False Passed
fac7e309a67a799e682f0939b26e5b2a71f8c3b8 Apalache Lambda BagBagIn True Passed
139704ca64b5a0a0376b1a8b4694c7ace507fcf4 Apalache Lambda BagBagIn False Passed
a8fd79e07f3ddf1ff68ead857053e84537de4d4e Apalache Lambda BagEmptyBag True Passed
a16b30616c002b2f029533df6998cd1a18bb4d21 Apalache Lambda BagEmptyBag False Passed
49546f45ddb118725ac9ff4322929436debba9f1 Apalache Lambda BagAddBag True Passed
e5e279aa5f6d2cd1b33c779693aef4b8da5beded Apalache Lambda BagAddBag False Passed
bb287ef0c69b8548cb935edeb1358f01e2d57298 Apalache Lambda BagBagSub True Passed
b1562b25af6a5e8eec4be939342a9bd3b333ae1f Apalache Lambda BagBagSub False Passed
53b21611f3e1d7519b07a5d7ae9b73dd8a1b1c1a Apalache Lambda BagCopiesIn True Passed
31ed1fec7a29d68fc5c5025ff08787ef4ae0ac74 Apalache Lambda BagCopiesIn False Passed
af17cdf2f0c846829cba4c72278a60820b579ae4 Apalache Lambda BagSubsetEqBag True Passed
99e3bc8c325c181aa5118180988ff7f19993ce97 Apalache Lambda BagSubsetEqBag False Passed
5b728aac08f5a3b58deb68f7ec1cf12b1f4faff1 Apalache Lambda BagBagUnion True Passed
e4fb27e48a68ee231b8d6caf31bd8335d91356c5 Apalache Lambda BagBagUnion False Passed
d2502e6d696e5f69b2c905dca189dfeb7c6ad259 Apalache Lambda BagBagCardinality True Passed
12cca94b33ef81e3d045cee8bd2285b6309a057f Apalache Lambda BagBagCardinality False Passed
a942cb994b060c986d3539229be6624a7369353f Apalache Lambda BagBagOfAll True Passed
62465e21897a7ed58669acdf4a6652647f1c3d30 Apalache Lambda BagBagOfAll False Passed
e4f49c13a9b0c5d9987001929c86cad03de2373b TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Lambda BagSubBag True Passed
c07ada86138f8c99e807958f7d70d4b1593a2fb1 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Lambda BagSubBag False Passed
bfca393c69a91a7336e49655c7cc19f0d244461f 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)
Lambda FiniteSetsIsFiniteSet True Passed
cce936c6701ae43d0f8060145bd261044db5dfef 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)
Lambda FiniteSetsIsFiniteSet False Passed
132acd7b7f8569209a706546cb3f4cf202136e21 Apalache Lambda FiniteSetsCardinality True Passed
1b0d15d96d968d062ea73813fcaac94c278d0216 Apalache Lambda FiniteSetsCardinality False Passed
1e334cc10209c1a49f6068eea29a76583db52562 Apalache Lambda SeqHead True Passed
317db677952e94852a94b893e8d241a06f4c0015 Apalache Lambda SeqHead False Passed
aa79f780f6eb83e1cba719393893d7191024c3dd Apalache Lambda SeqTail True Passed
21a5186cd3a2538fcd392b321177293bd85b446c Apalache Lambda SeqTail False Passed
12870e229ab7b1dd272be62a6bd5194f45ce514d Apalache Lambda SeqAppend True Passed
76cb6beacea18c4b2a75114dc1a79a34fc644e47 Apalache Lambda SeqAppend False Passed