Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
0375443e581246ce5b03020203726e935c3a8201 Apalache And Extends True Passed
3377aa75cfaf8b0ca8990530f0ac8873d23950d0 Apalache And Extends False Passed
fee56e2c974c7cd8dc36d2c1d3274074dbfe193a TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Extends True Passed
287c1e577d5827224cb2d66bc460266ccafadc69 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Extends False Passed
7149d8928d3555187726ad9694fb836e648a7c44 Apalache Imply Extends True Passed
e3897ec1734a84ba681802b94c068e1f5a59c357 Apalache Imply Extends False Passed
ad7e4718e2e516396910ec9f8ff6d26dc4765ba5 Apalache Not Extends True Passed
dcd11026ccd432bdc0c38f541e014d2abe67244a Apalache Not Extends False Passed
0798bb209a85a00c4b4891301056ae31d131038d TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or Extends True Passed
4784021ed9ef154892694d610d5e5f4aee9d52d2 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or Extends False Passed
db179f39245306288767cd1d669b93779bba09ef TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine Extends True Passed
f04e61c5b616f4d7e4cfec2df92d947713bd84b9 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine Extends False Passed
ca524d2c72adbd53ba435ad7c894daa475f35f48 Apalache AndProp Extends True Passed
b2aa7456548e79d7e10aedb6321c9dfa13608412 Apalache AndProp Extends False Passed
a13a6cc8d4c46a1f9644b1d9f46c06b87e006a95 Apalache Boxed Extends True Passed
e8572f0dfb66c8905da8b0d261324da72f15b281 Apalache Boxed Extends False Passed
f723df95e536c3759a85cdc962b4b98149caafb4 Apalache Eq Extends True Passed
78cd90f2da344a66de5bd2df13554aebe6c429c3 Apalache Eq Extends False Passed
41b59394b1bbefc87323a82c13443df944dc61ee Apalache Ne Extends True Passed
b1c10ad9b7214a12f265c2d1c149d274e1bdf826 Apalache Ne Extends False Passed
d358fd1ad91071d1109faae3b95bf5e94441c78c Apalache Let Extends True Passed
b2ec72c2170b904cc1cdd40f917bcffd88f6fe6f Apalache Let Extends False Passed
f299d375df6795e7106e63e57a9c5f8bf7028e49 Apalache Set0 Extends True Passed
6b979661cc2f97009360049b04c35f125081bad2 Apalache Set0 Extends False Passed
d4666d8bb7f9e857995208bf1a10cae6000d1f7e Apalache Set1 Extends True Passed
e94caee3623b5c63261244453e792af996af6b4a Apalache Set1 Extends False Passed
9aa67a13fbead96b39d1975b93a60034502136a7 Apalache Set2 Extends True Passed
ae4f4e33b43000485db3b2fd01538448d0e5f1c3 Apalache Set2 Extends False Passed
33237baf1a065ca1aba05e538ca4465f610e4be3 Apalache Fun Extends True Passed
a59a818bff3d34cd8d0fc6baf463fb66e20ea80d Apalache Fun Extends False Passed
360b2a1ec0c60c559a938364ae6cd3f4b557b727 Apalache In Extends True Passed
bf703938ab6bb267b734305c14edd225ac9fe637 Apalache In Extends False Passed
4ce3e44eca260fa66c714b054e3f0205994253a7 Apalache NotIn Extends True Passed
c9e90fbce5023c581542c58979f80bd19d204d28 Apalache NotIn Extends False Passed
c5a44c3485e874507261eec8f7b2a24b1c5be4d3 Apalache Exists Extends True Passed
dd57e437e7a69bc6dc200b753bc7625d2b4ed886 Apalache Exists Extends False Passed
9aea2a05ebdcc22fa10790067fe095ef0f2270d9 Apalache Forall Extends True Passed
570daf61db0edd8555598dbbf6c1bbb381e6bae5 Apalache Forall Extends False Passed
5d7a1b4244bd2f8a88143a88b20564caa7916d85 Apalache Choose Extends True Passed
3d1f1d28a9490474d6846a3538a1ae11f4884f92 Apalache Choose Extends False Passed
c96597a1c9615e1b28c36299001893e6c444ef64 Apalache Record Extends True Passed
4ee4699c5b0941da095b4e61b879f3e6303beb28 Apalache Record Extends False Passed
36179da3cdecb255a9b9c64d1083cb6f5b629117 Apalache Tuple Extends True Passed
0f249ff5926d5f8bebd254be3e9354e681610dd8 Apalache Tuple Extends False Passed
09789a68e2d11a49f4af83c64cb8e660d386bf2f Apalache FunApp Extends True Passed
253fad0dfd5c3b12b9e0c6a2eccbce1cb296995b Apalache FunApp Extends False Passed
7b222313bff3c3bdb4d2a61130f16991e4b475bb Apalache Except0 Extends True Passed
1a6f85747bd6ec7f52bf86789154d5d947ba0522 Apalache Except0 Extends False Passed
030cbb70c23305cda0b8148b7e4d40b3ee118d49 Apalache Except1Fun Extends True Passed
243d088743f587f0781c384ec24531ca900d2a63 Apalache Except1Fun Extends False Passed
9ab52fd6ed4a816a5d7e002fc3f5e0090e7065b1 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Extends True Passed
c85d0f3153977a4d10f0ecec398faed870dde25f TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Extends False Passed
e9a928c548ff31d8ca46e5cd351fdc835a5a303e Apalache Except1Rec Extends True Passed
d5bd14947e96ba0ce153bd20e80042e3b26066de Apalache Except1Rec Extends False Passed
e61b7e95607117c568bb00bd0763ed47b1601841 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Extends True Passed
de31847f2a0fde3646b1e41494ab7942e51c2378 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Extends False Passed
af66e6ce6eaadb7c3fed265d81d913802fb91317 Apalache Except2Fun Extends True Passed
975c8f53fd58ea3da82546ac7c67574a2f694a10 Apalache Except2Fun Extends False Passed
3af86e87c757e9c14eab20cb1fb1c00d80a496a2 Apalache Except2FunTuple Extends True Passed
11a6946dabe93ef9c87ffdea95708c4de038b19a Apalache Except2FunTuple Extends False Passed
df8b27c5016687db20ad07bec36da9ed75234493 Apalache Prime Extends True Passed
efb17692fa65794e17987c0948660aafcd9049f9 Apalache Prime Extends False Passed
5642c825ef1bce3fa1fbafccd5d6cfaffae0e750 Apalache NumUnaryMinus Extends True Passed
ace882f368af3daa9310edbe2bda4add383a64fa Apalache NumUnaryMinus Extends False Passed
4874a65ebc078de81e783f03bee530f1e17ee15a Apalache NumPlus Extends True Passed
d1370ab2d19ccf8b764d019a8665c52724a9afc1 Apalache NumPlus Extends False Passed
5fcb9087f403f4fee21045f36ac9365ae1de460d Apalache NumMinus Extends True Passed
a40f3176a18a4bba1e8ca34da4c4a6f45e243615 Apalache NumMinus Extends False Passed
23958bfacab1c83155c6489f333037651c6995e7 Apalache NumMul Extends True Passed
fffd6f4683620da2b85226f59bfa8b9f11c20672 Apalache NumMul Extends False Passed
ca6a3f9a0da445ec7a3f8d903264518a1f7998ac Apalache NumDiv Extends True Passed
e94e5c7c93f3cce7f76d3abe0b9995cf0d8ca0d2 Apalache NumDiv Extends False Passed
d5fac2c1c67d3b5a839b62e5082021e09485a039 Apalache NumMod Extends True Passed
8cd7c2d2fa220cb4fa032ef4da25d26e9dd8e5b3 Apalache NumMod Extends False Passed
f938e2df4c2e08336793c757fc1e21ac18d6c5d3 Apalache NumPow Extends True Passed
e71f9214b11a79b676f4025e80c61ec4752d977b Apalache NumPow Extends False Passed
611df6e90c31489f09e84b842811ffa709989b18 Apalache NumGt Extends True Passed
7a6f5b610f5d22232d25bf1d8f304cc649779698 Apalache NumGt Extends False Passed
659563a7dc01ab40ccc64be9a9e2fe164f07e42f Apalache NumGe Extends True Passed
119d7fb62b2449fcb2278cf20aa6d887d545d6f3 Apalache NumGe Extends False Passed
dff17a8d2ca86102b58f17731cf257303d49f5cd Apalache NumLt Extends True Passed
6adc1bd23b2628e2f2a1975de400efac77249a9c Apalache NumLt Extends False Passed
687d6e2c4170fdd0b1f0f94b3e1a431e99bc97bf Apalache NumLe Extends True Passed
45b5a58eaea7dfc099b2dfd90bdfea7d3e942de8 Apalache NumLe Extends False Passed
e91d91e6b20b22bf3d84d0cbb5dd86a1b81d7d83 Apalache DefFun Extends True Passed
b2608378afe33c3678ae2ab07e57603547bb5a6d Apalache DefFun Extends False Passed
c3b3c630192d024d47ff2d6868a1aadb55b08452 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Extends True Passed
73fd2c63bee22f9c079c22a60f61193d6270076b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Extends False Passed
9356704c2c7b3ad8df0baf5cf8b63e94f04d9746 Apalache DefFunRecursive Extends True Passed
19f4f7e2e3fc070c288c4e9313dd3747e1138ef0 Apalache DefFunRecursive Extends False Passed
0146673d2b505e3ef79e7fbfbff1d2389aa524f3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Extends True Passed
1bfaf8ee13bcbf1deb222e63baf799d753f5eafd TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Extends False Passed
5c046a8d700572a680e1e3e305ad05b381768bc9 Apalache Def0 Extends True Passed
5642eb8009219fd2905e047fbd6d287f73c39de8 Apalache Def0 Extends False Passed
6452f4e62ca9ca96aeb61648f013d1d85067a313 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Extends True Passed
e3dd862656237f7d04f2d2958b64342dee31af0c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Extends False Passed
3a05c928cafecfb4ea48c702f4a942be6fa0db2b Apalache Def1 Extends True Passed
7ec01dbe998b67f509b274a996280e6a44831830 Apalache Def1 Extends False Passed
d300749b4c6c806aade6904cd2271a39535b17b3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Extends True Passed
89b9877d604c025c3fa757659aecb4a06623e889 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Extends False Passed
0b8d3eeb156e6404b8267888b25dd371648440db Apalache Def2 Extends True Passed
c4f42ff1fe38eb7ce257572c612b7d4806cda436 Apalache Def2 Extends False Passed
597d92ce49db58e6a2ec6da73b38cafe95aa15ec TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Extends True Passed
7efcbc502dfd2fd024bc4235b868057d1b83d214 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Extends False Passed
41b3d1caec5c4dd6c997685acbde82d8a9fb3dbd Apalache Def1Recursive Extends True Passed
0e5f6767d460ef4ee1521e109208f656f638ac9b Apalache Def1Recursive Extends False Passed
677da16c7d2d96661306f6eaea472ec12dea3985 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Extends True Passed
47574bd665babdf147c5fe1b48732f316bb5e761 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Extends False Passed
a32398b489af72ef5d1362aaebae8170f2827f5f Apalache Extends Extends True Passed
ded3010d8e584e836162660f692c581814676aec Apalache Extends Extends False Passed
c9079e84aa934d8e0744fd8eb92b00c4be46e221 Apalache ExtendsInDifferentFolder Extends True Passed
b35e1c772868f07ee542542b9a61b3e5575cbe30 Apalache ExtendsInDifferentFolder Extends False Passed
215dcb1741060af98a5a9dd6337c1b22c3fa900b Apalache Variable Extends True Passed
9c6353f435fe3bab0984c71347ddeb27cc14ac72 Apalache Variable Extends False Passed
6fb364928def310f6213d2e426d56208d6051f27 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Extends True Passed
b72d3fe6f28d101949b3ab60c1d52c6417bf3c47 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Extends False Passed
f54e82cd12ebca8df13adf0b4492e28aeb91c1b0 Apalache Constant Extends True Passed
87ba973c9c8b4968e03418b91f0ce102cc3bd56c Apalache Constant Extends False Passed
364fd7e5290c7788d77ecd9f401e9155b876df38 Apalache ConstantRank1 Extends True Passed
469a2d37c1ddd12e7737faa9c362ca3776310cea Apalache ConstantRank1 Extends False Passed
73af86021860395c8f96cbd6fc881bc24a0531d1 Apalache Instance Extends True Passed
2b8a0c85baf99878cab1de17842bac877be092c6 Apalache Instance Extends False Passed
ddb7df94261c8f6ba0d232ebdc74fd0e0b7a6481 Apalache InstanceWith Extends True Passed
4b42d3112150b38b845cc51f71c95d000b00ebfc Apalache InstanceWith Extends False Passed
24efe108013976f4da6626b2a73f9dce0fb55376 Apalache InstanceNamed Extends True Passed
678d1fa456f7bf5219f93e242a0231622c51247a Apalache InstanceNamed Extends False Passed
f7a4cce69af3546ee80899558769ac1821bc9a95 Apalache InstanceNamedWith Extends True Passed
6bad38d208a34582c1dcfbfac5fa836560345c06 Apalache InstanceNamedWith Extends False Passed
d2236251ed23ca0de6014631aa6a5a7c7cfab79d Apalache InstanceInFolder Extends True Passed
65497c5f33bffe003bdd05e1edea72638dfa4bf4 Apalache InstanceInFolder Extends False Passed
dda6b25116e066ef65a2bf69da964829a0530865 Apalache InstanceWithInFolder Extends True Passed
b65b5b58c3e586834b20fa49eeec0107ce4fc9b0 Apalache InstanceWithInFolder Extends False Passed
8ab99f1ea7efb4e2a42257c3ec2dbd3f792f1ab2 Apalache InstanceNamedInFolder Extends True Passed
92074012ab36d5afc260a6b10357086ff8f508b9 Apalache InstanceNamedInFolder Extends False Passed
c7150976d93031246a3117c66b11e0d2804ff605 Apalache InstanceNamedWithInFolder Extends True Passed
c7e6548d127723a5f278c2b684abe49cc86a55e3 Apalache InstanceNamedWithInFolder Extends False Passed
722353afb4de40023b9e0de8fcdbf91729a41ac9 Apalache Enabled Extends True Passed
1412acc3d1e5935323dc84a7eb7e126e6d6ee2d2 Apalache Enabled Extends False Passed
485ecfec173c66c843b7307d6106172e487e64d0 Apalache Assume Extends True Passed
94b0d3fd818fadb3ca859817f838524d06a4f545 Apalache Assume Extends False Passed
7b89b04ed4d372fcb4c3e914122acfae7f0a8cc6 Apalache AssumeNamed Extends True Passed
dc87aa96642ee0bff6a09e3ae9c6d4d57c07bed8 Apalache AssumeNamed Extends False Passed
fab917075bf9c7b6e224e39e49801446ec36a739 Apalache Lambda Extends True Passed
90a6e439286370ec6fa739e9c5d35fd19f98c261 Apalache Lambda Extends False Passed
01ffeb41a587aa3f80262c44d115e3d1369b8baa Apalache Cross2 Extends True Passed
7fd8ce2931f449086cb8eb06da5099f0995ce069 Apalache Cross2 Extends False Passed
9bf4148e9cc53c3f316938841c38159ea2fd73e0 Apalache Cross3 Extends True Passed
d54dd7493ae43634ebcb1c7bd3676e20d46e27d2 Apalache Cross3 Extends False Passed
5401d980199104d28d401215a0ba32dedb152774 TLC with reduction strategy:
  • Case 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))
FunSet Extends True Passed
e2a9ce26b2d29b6876eb69f22ea6a6dc11689c19 TLC with reduction strategy:
  • Case 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))
FunSet Extends False Passed
459dd0bd16fb835030d7efca9cfe0b0a055fd5a9 TLC with reduction strategy:
  • Case 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)
RecordSet Extends True Passed
39767adb0d545caa6314f4ee426e737c965aed36 TLC with reduction strategy:
  • Case 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)
RecordSet Extends False Passed
5d2384957665aefd9de98dffba13a76a36ad2ad5 Apalache SetDiff Extends True Passed
f78c94f89abde0d721cac27ff78f552d4fb98214 Apalache SetDiff Extends False Passed
6f0070786a657af571a4ee6e6061ec5f9458df4a Apalache SetUnion Extends True Passed
483094d398d354b4019a31c0c6e57abacf57064b Apalache SetUnion Extends False Passed
ed6bfc24c625fbe3bdc0e7df33fd6170ee30c4bb Apalache SetIntersect Extends True Passed
d01517a85db6714368cabbb79b5f40ca21af9538 Apalache SetIntersect Extends False Passed
0a956c2a26b94132fa471b107ec0bc6035abec9a Apalache SubsetEq Extends True Passed
0530807e6873569c97b650a249df02bc1b78324f Apalache SubsetEq Extends False Passed
0d62280f29ee3a503876586887d3f02e57352ee6 Apalache IfCond Extends True Passed
cf516f5eba9730933f4948746e426aa3ec76ee0c Apalache IfCond Extends False Passed
9a2cf0232f6e66126e146d2d787e5cde2b1e96a4 Apalache IfThen Extends True Passed
0a0dbb9a2f9d7c961d05594c18da391a83bf6ea7 Apalache IfThen Extends False Passed
fb4ad2d84c8abd2c33caf5f4c527607c876a17a6 Apalache IfElse Extends True Passed
e02a97146499d08d4026fecdf845982cd9e690ef Apalache IfElse Extends False Passed
0fd6ebbc31be4bd5ba3d55e7cc49558e033e2e27 Apalache Subset Extends True Passed
7987ab43351df8ed2c58b4aeb0a7e27ffbd73444 Apalache Subset Extends False Passed
ee6600a9430a8c44da73a966ab031bbcc3b80951 Apalache Domain Extends True Passed
1dd07f515015b1b5a13faadd5021f29c6f0fb729 Apalache Domain Extends False Passed
e2a0ad1f42e44a159617ecfbb2b1355d78cd33b3 Apalache Union Extends True Passed
310d37d4b80221fe2480d2caa68ef543cfa7e281 Apalache Union Extends False Passed
1f779cceb6b95e6b39a910b5a9b29c6395bbbfea Apalache Unchanged Extends True Passed
4920126b5eb2d33531f80b789c8c4717d136447c Apalache Unchanged Extends False Passed
ffd4be9e0febfe6aeec8385c411509c42354850c Apalache Equivalence Extends True Passed
0bdd8c93f8efd89c284f82d4608374643dc10fda Apalache Equivalence Extends False Passed
928d965ea2821b84db04353eac82d668534954d3 Apalache SeqLen Extends True Passed
696c7f76457f4188aeeb64be638e8ce90005bc07 Apalache SeqLen Extends False Passed
ef61f3f5357ea429fa096de4b902d22616d3161f Apalache SeqConcat Extends True Passed
5ae85cc470ef7bd4d87f6f9a0614f94f38dce9b3 Apalache SeqConcat Extends False Passed
b408013220f41c3ac51f85fa1f905bc7471dfdcb Apalache SeqSeq Extends True Passed
52748114d4b5a738c5ae24859baef457dfdcba88 Apalache SeqSeq Extends False Passed
c34089e71929adda29774a9ba104fe5627fc5a2e Apalache SeqSelectSeq Extends True Passed
cbe386b4436e8d63e57ee1808efcc5ad735a022e Apalache SeqSelectSeq Extends False Passed
3cb53ffc8e44fb3e779ebbf234500b755454049b Apalache SeqSubSeq Extends True Passed
8c3f7bcf7a53442e254b8ee1a7f0a733ad93b28d Apalache SeqSubSeq Extends False Passed
ff7363ffc91d2ca02a8881ff1b596f908fbe6ea6 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 Extends True Passed
3253d4bdcbabe7eb1be2d07786df51c37155407d 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 Extends False Passed
4b33431f9b4e1db68af11accbce627f1b1b174e5 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Extends True Passed
9175e9f24cc269609be6d51bffcf9377bd87b082 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Extends False Passed
de87f66215e716349d95d84cc8988afff4a089f0 TLC with reduction strategy:
  • Case 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]]
TlcExtendFun Extends True Passed
391485e7d515691280f28b333ebc9bc41af64a8e TLC with reduction strategy:
  • Case 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]]
TlcExtendFun Extends False Passed
5741b3274c3ef0a573e7d061c66772ad71946086 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Extends True Passed
5ed145ce14d7dafe35d150a6d1308cf9342079d7 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Extends False Passed
a77119fe40013fb0f5076ccf8f302dc8f1c73e0e TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq Extends True Passed
be376dfc1c714e997f1c9e371dca4bd8839f131a TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq Extends False Passed
a37cc50090020204b66541da975409e1679600b8 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Extends True Passed
fc2200fe3ebf038d03c648c2dee5468d62938d94 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Extends False Passed
1fb2f55ff3d5133ab4c4852af1779d4570d6645d Apalache BagBagToSet Extends True Passed
21cb2794f384b9c8f1adb4011162f6239a487586 Apalache BagBagToSet Extends False Passed
fbd7e981f5c2210d644268193ce3f0e4dd9e2c11 Apalache BagSetToBag Extends True Passed
77864d38cbe95f33db2aea76d5358d4733a538a8 Apalache BagSetToBag Extends False Passed
26df4596c3d5cb0f9928c6df9d54c0f88a2fc7c6 Apalache BagBagIn Extends True Passed
9c3b8f042db29354d5ef77e0f716390596b19eae Apalache BagBagIn Extends False Passed
71b23a76bb24c26f7e6f3ae58f5ccfe12c900fb9 Apalache BagAddBag Extends True Passed
735658c4d22dd9fca38a0d489dde236ae492130f Apalache BagAddBag Extends False Passed
8f6ee2441a30227769391f2a9116507926b5bb2b Apalache BagBagSub Extends True Passed
7eebb734cdfe9e54fc44236f0f005ce3df5cfeac Apalache BagBagSub Extends False Passed
5f0e5981d2f0cbc328bb16053787edf936315177 Apalache BagCopiesIn Extends True Passed
9f722718ea6c0c4ec1cec8a4bbbb2eab20fa33ea Apalache BagCopiesIn Extends False Passed
eff029001a44653d3c352665ef5658a9d8084d84 Apalache BagSubsetEqBag Extends True Passed
a3faa2b1553e8793fa9d0a608faeef4b1c66d637 Apalache BagSubsetEqBag Extends False Passed
24b397137bf6333a14ccf6bf28bf878923bbe099 Apalache BagBagUnion Extends True Passed
58283c6ce33508ccae9fbc38b6b82d21d7487be2 Apalache BagBagUnion Extends False Passed
019ec733c84fbfaff99adf18f35cb1ddd3d11f26 Apalache BagBagCardinality Extends True Passed
b35e2d013f787db86ea9856e623898f6e61358de Apalache BagBagCardinality Extends False Passed
a4b91c2d05e89e7b72b18f66c14cee22322a3493 Apalache BagBagOfAll Extends True Passed
8cedf1aaff38ba7e7628f3fc7ab7d071bd369c89 Apalache BagBagOfAll Extends False Passed
2ea57f321c11cb30dfedd53b0c9af9838e981192 TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag Extends True Passed
a0321dad2794decb341917b51a031ace6e40ae6e TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag Extends False Passed
5219d6ce7d173820d7770a2b0c909d890dce727f TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Extends True Passed
e6777e30ea0c9985959ec80f11ba8337c1c80c65 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Extends False Passed
4053c7ecddc80f794079e80c2187476dbed9b9bb Apalache FiniteSetsCardinality Extends True Passed
07205014ae306ad63a8da0742346c619ec05a170 Apalache FiniteSetsCardinality Extends False Passed
932542e0e7f2ee86c458f2cc2708d19ebecba9bd Apalache SeqHead Extends True Passed
e08c4b0481469d9695d89d7d2645e0097213659e Apalache SeqHead Extends False Passed
a355a1c9608e8301f8e8872d508ebdf822c053c8 Apalache SeqTail Extends True Passed
5a178e8825307b268484a32f18dbe285502b2abf Apalache SeqTail Extends False Passed
47c5bf199cba955df25cf6de2b0146a85e65a666 Apalache SeqAppend Extends True Passed
6015397de20adb63929ea20b6d054cce32c7f2cc Apalache SeqAppend Extends False Passed