Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
aa4ef39b749874988479c96a1324c7871b5d2c5d Apalache And Def2 True Passed
6dcc60029d0cea4c5c45304f60734cfb15f549cb Apalache And Def2 False Passed
d4e06baef553664c4c41646bc4132d9863ef65e7 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Def2 True Passed
99983b509d61c3480182bb40e025aa154c7fdde1 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Def2 False Passed
31311ac47f01c6494d39d37fab81d4acfd0de839 Apalache Imply Def2 True Passed
f63e3f15c0d423af8444f26064af79693b1ba363 Apalache Imply Def2 False Passed
982f8bbdac0120ddae993c091069ffc79db12c8c Apalache Not Def2 True Passed
f4c60e78bc32b29757682e4fb664cb53e8f147b0 Apalache Not Def2 False Passed
e5aa0644c9a60bd1cfb588b2b006e6da18edcd77 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or Def2 True Passed
a4f53dc92debee69c5db09489274df8dd1e5f71e TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or Def2 False Passed
97c04d1ddb54458a6470c50095a464ddb680e165 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine Def2 True Passed
e642337155564a7733ce21e4efc01d8085fd7a40 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine Def2 False Passed
fe50757c5a64d680855efceec1cc66b052f4bd3e Apalache AndProp Def2 True Passed
41a965e576e91e672aab096c5d3fa53792f70072 Apalache AndProp Def2 False Passed
c3f5c6d16edfbd3fff1d0ae72497be509162e899 Apalache Boxed Def2 True Passed
ffc34a613b07d794ba2591c96b5608d17cdc7d7c Apalache Boxed Def2 False Passed
f7ca9deee1143895dc69528429eab2acf6c105f6 Apalache Eq Def2 True Passed
e4aef93ffeac4ac0914392e56e5dffd7c5a93bc2 Apalache Eq Def2 False Passed
9534e30ec7a02a3fbde7f99dbf0a1067ce6b5e25 Apalache Ne Def2 True Passed
b281c41573a8d0adcd5bc6ebbefdc446da9bb115 Apalache Ne Def2 False Passed
2bfa6d0efb91e4e2988c58991e90e7e94e25dce7 Apalache Let Def2 True Passed
6642b7ef676e4fce8c79a71f721d97821c4f203f Apalache Let Def2 False Passed
d95765a8db80243da51105083e87e19a0f37a595 Apalache Set0 Def2 True Passed
12fc8aa7a896f6f9b52381c674089f38c05af8d4 Apalache Set0 Def2 False Passed
b50920704e1cfdd25832393160dccb1f33b522b0 Apalache Set1 Def2 True Passed
f85e5ca88ab30d7c0a90715046dd34e538b5df24 Apalache Set1 Def2 False Passed
e96926c72504148b336a55bd0b72879b45e7b958 Apalache Set2 Def2 True Passed
2562f5dfdabc0247d0dde1209ecfeca775be2c82 Apalache Set2 Def2 False Passed
7c4ed8c5075c91e80cb8c263163482d3fd91c5d2 Apalache Fun Def2 True Passed
c20f2180ae28b9955139954199755eaa40bd6714 Apalache Fun Def2 False Passed
58d315a33fe7a045f11041383ffac95950871ef3 Apalache In Def2 True Passed
4fd2b68fadbdf91e0a53d5417ab9720a5340678c Apalache In Def2 False Passed
43ed8451074f0ab1942092d54d48a61af14d9c2e Apalache NotIn Def2 True Passed
8483cf6cc7528fd6da1a16c34ca4d12e62cd3451 Apalache NotIn Def2 False Passed
85543fd52d0f7c1090c89f03ed7dbf00d81e11d0 Apalache Exists Def2 True Passed
a717a6c24356db1fdd31e4b40c734fed474dd7ac Apalache Exists Def2 False Passed
cba538ce8e7825c1e188fa668c7e8abe854c727d Apalache Forall Def2 True Passed
98e9ca9a5aeb690ba6cf81eede0cf8f726c2f39a Apalache Forall Def2 False Passed
9c2125e41f7f29f49a6c96de332e4a3029302bd5 Apalache Choose Def2 True Passed
594a463c072881f39829053f730476d56f4a1791 Apalache Choose Def2 False Passed
bee1db56ef48265793131d5aec92b39e093ffe28 Apalache Record Def2 True Passed
3f976ce0089c4e5dca2da301184ab590d6830bb2 Apalache Record Def2 False Passed
4751cb731462ecee57901c19b11f6b57a6587a9b Apalache Tuple Def2 True Passed
ff032577c389c4da86ae4d08fe4d16f122470d74 Apalache Tuple Def2 False Passed
e64b2c2d8d53445c217da31db104755109233305 Apalache FunApp Def2 True Passed
578c3c391d87cd6f567ac3457e15ccbfc8115656 Apalache FunApp Def2 False Passed
06f837501c9227f0c648381e9c5f8c4d7af0aa95 Apalache Except0 Def2 True Passed
ad5a41ae7698c30f5b3acc2767e628dac9311d60 Apalache Except0 Def2 False Passed
ee7385550b265d9d8239f4ab04973faeada0fcc4 Apalache Except1Fun Def2 True Passed
4012a4729ea572c4d238ed10d37e228c8a926858 Apalache Except1Fun Def2 False Passed
0d27a76a14fbf2b465cb54ac7629f2d7c5576c48 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Def2 True Passed
62a1c5aeabdc10219bc8dbcb5280a26b0f2a5832 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Def2 False Passed
8d9c3779c6cf47582ce60b36a4f99388cfb8d789 Apalache Except1Rec Def2 True Passed
75410612e8b7b909b9cc0ea41e2711521006dd29 Apalache Except1Rec Def2 False Passed
165aa9260733a59479d2aacfbfaee920b0511682 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Def2 True Passed
6da3775d8f55315afcc07552e960d788dfe19c1b TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Def2 False Passed
d8963097b687979a00553418837d111b14b9a7cb Apalache Except2Fun Def2 True Passed
d0364a8a072b3266e393831a336f70998cec24ab Apalache Except2Fun Def2 False Passed
af369351db77c902c0a0cc71ffedc7aeefb80ef7 Apalache Except2FunTuple Def2 True Passed
79d2e3bb1fd4fb42152492d73b9bce49e26fb98a Apalache Except2FunTuple Def2 False Passed
8e41d91557dd22de764761ac00b124cca83eb93a Apalache Prime Def2 True Passed
628a25f71006e8201ea85990c6ab391e66b78b47 Apalache Prime Def2 False Passed
70a70a956964b08ef349826232b956994a459395 Apalache NumUnaryMinus Def2 True Passed
3a429bbc398895c82d6300f077df02c0a64e567a Apalache NumUnaryMinus Def2 False Passed
22caf39533dee6f60fe255c5eed0c5f7cc587c60 Apalache NumPlus Def2 True Passed
e0375b3cce12f7fdb74a32fe35df2a084e2c4c43 Apalache NumPlus Def2 False Passed
69741fcf4fd38bdb979925cd3fccece7deb8087b Apalache NumMinus Def2 True Passed
013f0806fca5e0d090c74006944f0deb9c52bb01 Apalache NumMinus Def2 False Passed
4f3569d80da10aa68f73c8787d87070f7b4ab412 Apalache NumMul Def2 True Passed
dc877a2f0200183a75fc520e39ccf19639d8853d Apalache NumMul Def2 False Passed
0d1b6f1ecda216f921a069ed6efc287e8e6af3d7 Apalache NumDiv Def2 True Passed
1452ed5c8c5922bedf6c018a77e549c71d8d4af4 Apalache NumDiv Def2 False Passed
677d5821fcfad107bf60150ff505c2b9b686bdda Apalache NumMod Def2 True Passed
936c288407d898217a48823d193d5dcdd582efde Apalache NumMod Def2 False Passed
d2e9d251deaa8de45237ebaf54ff54eae05d3d86 Apalache NumPow Def2 True Passed
e3bd57ca9292cccc9f643f92a949cca7100001d7 Apalache NumPow Def2 False Passed
fab6b77e1aee441627a9c3849e0289d809132e01 Apalache NumGt Def2 True Passed
ef9ca72a9fdce64a6ac215b551cb94c75aebc898 Apalache NumGt Def2 False Passed
a96d1bf7758f0559b1ab8d92c4acbeafec207f13 Apalache NumGe Def2 True Passed
d3b280da2a0497584b68e5c90451751ebabed631 Apalache NumGe Def2 False Passed
1c73f4d06307960153a2b7ee55c41f90a2a7e84a Apalache NumLt Def2 True Passed
96a448df20a8c399c54a914f30c4b95d1b45955e Apalache NumLt Def2 False Passed
229549edaa895b859feffb343ce4bd83e6cf7a28 Apalache NumLe Def2 True Passed
024fe68d7fbfe80bfaf4014a73fe76eb8115f995 Apalache NumLe Def2 False Passed
6e55401c42f4fcae01244ec8eea4e4c2c10366eb Apalache DefFun Def2 True Passed
a5bf943ddd0a707286b93c513ea9883e5ae25de2 Apalache DefFun Def2 False Passed
a363bb196346b01771ccb04216ad963fca3d6504 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Def2 True Passed
358b96cf4a88f9da57271cc6398b0c00d155a428 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Def2 False Passed
1cd83a2eec22979a53f62734c65f797017619052 Apalache DefFunRecursive Def2 True Passed
1049ebaa785a422f1d9f94c0517d14c394f4c551 Apalache DefFunRecursive Def2 False Passed
f1c27695092f2e035980c9e6bee4dc3b759089f0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Def2 True Passed
bb2b24cd74dee514659de57a3d19730a2007576b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Def2 False Passed
8aabee0c8ceff3c4296289f4a1b4897df6db5f11 Apalache Def0 Def2 True Passed
ff8d44090b86ec26ee3983a5c4143c1a830b76c8 Apalache Def0 Def2 False Passed
ff491a5774a36c50bf715f7dfebe6e2ce9b330da TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Def2 True Passed
06dcd5ecc0a80fe22dcfa603a49c135fc91d607b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Def2 False Passed
b5a8f3729171786c285d9fae888241458cfb7e06 Apalache Def1 Def2 True Passed
0f4561daf026474cac9e3740f26cec098a665e47 Apalache Def1 Def2 False Passed
74e06541e1686027f4f31d54a172a008a02c7cac TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Def2 True Passed
f4263cb9246c64f20e729ce9928712c844a7e23a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Def2 False Passed
9610d77a0d777dea600be2d3618395459dc4b4af Apalache Def2 Def2 True Passed
655f96f3e676dc265de8e30d5d4a1dd8bb349f28 Apalache Def2 Def2 False Passed
c78cd0ca983e433ea11f43200b1a4e18ff054ada TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Def2 True Passed
5f85b72dfa0dcc52366c80b005ab58f13009280b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Def2 False Passed
68c685422c1d6a9b25a471ec4814f2194f2760e8 Apalache Def1Recursive Def2 True Passed
a15b7b9d9e7a814b037887455e008564a04cd919 Apalache Def1Recursive Def2 False Passed
2d85bd2021b52055c86c05d85f14f46d1a63586e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Def2 True Passed
05dae5c86c0065b1a51a69472b8a31a4e61e4551 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Def2 False Passed
f09513aca719e5bde83731b36d8317fd8e3c8638 Apalache Extends Def2 True Passed
5ff9c7c0050587edeb466cf1bfb1196b2956871a Apalache Extends Def2 False Passed
2ddfbf6efda9a6f5a4cc93aa652b3c55fd868343 Apalache ExtendsInDifferentFolder Def2 True Passed
4835880620cc9414523dd88354adf7208fa20e40 Apalache ExtendsInDifferentFolder Def2 False Passed
96e9bdf90875cde60047f9575495e341c2b0f24d Apalache Variable Def2 True Passed
61828218d656a0b93c097c8d2871773881defeac Apalache Variable Def2 False Passed
04e5082f0b47424273b1d315aeceae783cdbef5a TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Def2 True Passed
4a8e1964cdf34fac492c4d8c43a0a31b5ce4fa13 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Def2 False Passed
b208dd8c9d7355f1d676f55376a0fe7d1c5d71fb Apalache Constant Def2 True Passed
efb9d7f91e75d64800f03b83d3a921b92441cca2 Apalache Constant Def2 False Passed
91cf33386adfe311cbaffdf5acc1d5d283acf463 Apalache ConstantRank1 Def2 True Passed
5cbc86142d5db0fe1b4980971771a5e17925a79b Apalache ConstantRank1 Def2 False Passed
5b12f80cda7d4aa88062d59f10e9645db959641c Apalache Instance Def2 True Passed
307ba445f804d7cd7d824622c6fa6a8aeea8cbcf Apalache Instance Def2 False Passed
33454474641e6faf4c693dd272d82f2b1e5d6be4 Apalache InstanceWith Def2 True Passed
78c9aa430d96728ba7e82bd603823ec0499819e9 Apalache InstanceWith Def2 False Passed
2fc0caef96f7f1ea553c7acbc6f78de97e25d534 Apalache InstanceNamed Def2 True Passed
194e8481f33be4f73da1823b24ae53d6e0c5ac3a Apalache InstanceNamed Def2 False Passed
3a84b7f3cf91ac144f880abb18f8a6d6a40976b1 Apalache InstanceNamedWith Def2 True Passed
ea7c2932ee998ec99dbd44f226e29d9684ed3738 Apalache InstanceNamedWith Def2 False Passed
fea179969cd69f005f246e093f3e342c63a4c73d Apalache InstanceInFolder Def2 True Passed
6b928684f5bb023c1a49f929e66a30ce51e2e625 Apalache InstanceInFolder Def2 False Passed
dc018d4d893ef729ed2ae0143303af256202eedb Apalache InstanceWithInFolder Def2 True Passed
000f1769f8301f37ed9af589c935fca660287fe2 Apalache InstanceWithInFolder Def2 False Passed
8fd5678e0dc0f70e6438767719118ea41ff8f1b9 Apalache InstanceNamedInFolder Def2 True Passed
c813ad5decdfa824c310fa2bf800bd959577f4c5 Apalache InstanceNamedInFolder Def2 False Passed
709b00c4deccd45b53ec19ab5d120f7194288f9f Apalache InstanceNamedWithInFolder Def2 True Passed
1e94e55e9eecb60f40e1f1c8232b617ab70fb2e6 Apalache InstanceNamedWithInFolder Def2 False Passed
eeaf65775f20b8101f178629769c22c2e7cc08c7 Apalache Enabled Def2 True Passed
61b95e5676fb4955608a018415df0f59c84348b2 Apalache Enabled Def2 False Passed
102fbc98a065890d073b027a591d1aaa72756f14 Apalache Assume Def2 True Passed
e0fa808a7c3a757fd3d50fc7d0c0ffb3fd840434 Apalache Assume Def2 False Passed
b03d721c8648a8b123cb5efbe1d5da2b9ec98a68 Apalache AssumeNamed Def2 True Passed
59259bb91e54399bf48f04b7cc475b36712188b9 Apalache AssumeNamed Def2 False Passed
7b7b1b08c561ff596fd9d781f05e1bf01fc3d656 Apalache Lambda Def2 True Passed
805110db68ab2e2e981419691ed073181d4b7a8e Apalache Lambda Def2 False Passed
23a25efae439db8bbfe2762d91971020b3f61a81 Apalache Cross2 Def2 True Passed
1e85842e19e658c00a3413a0c709beb38c7bd386 Apalache Cross2 Def2 False Passed
0e3279fa43dadf21da83199ca0a0eee02da44265 Apalache Cross3 Def2 True Passed
37a98b0d942f7fdc9c01e2519c60baeeb2123544 Apalache Cross3 Def2 False Passed
e6393b4707a81cc68973b303163aa68e3fb595e2 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 Def2 True Passed
7237df7cafc04f6e640ca39facae6553b7bf05be 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 Def2 False Passed
cfea69d196ad2a6921824d8e224dc90531d72724 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 Def2 True Passed
4d28e866288176552537a8ff89ecd26a771922b4 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 Def2 False Passed
38bdc35b84aaa00ab5993c7014f890def2003480 Apalache SetDiff Def2 True Passed
bcea28c4466a51d465c42a76c4f2038361bfda9f Apalache SetDiff Def2 False Passed
0bd115e9b3208672778437822324a0b246046ec9 Apalache SetUnion Def2 True Passed
af44278dd663c965a2f0af35d0b02c32d32344f5 Apalache SetUnion Def2 False Passed
ef50fa1a72a3bbd3fc97c0dc12dd60aad7c6f0df Apalache SetIntersect Def2 True Passed
42cf292128112374af165d98037855f7dedd1f11 Apalache SetIntersect Def2 False Passed
4d722f586a057525ac8f029eb68b9db8c4b41f13 Apalache SubsetEq Def2 True Passed
65043bf0b4d7dc9e6fa755fc73b41994ad0e5a82 Apalache SubsetEq Def2 False Passed
bf2637f44401f43e81f1e97617e00766ce7fc698 Apalache IfCond Def2 True Passed
2c5174f3111f74f00b760ca3958876b7f562e5b3 Apalache IfCond Def2 False Passed
162ba192ebeec5565c78f0b53588485b4fa199fb Apalache IfThen Def2 True Passed
11af74c09e7730e15ec20b091e012d82a5e9b856 Apalache IfThen Def2 False Passed
38585163e5f69f08f98bc3e3ea24b8b3c8bde3e2 Apalache IfElse Def2 True Passed
1d53b240829344b8ca0d23471f34421bb31a0023 Apalache IfElse Def2 False Passed
6376a0ef7c275da79ac517a84905647c8ef38b82 Apalache Subset Def2 True Passed
2ccfccc029853ebebc1c8a7451177ea406176059 Apalache Subset Def2 False Passed
fff4468113eae0559c5a792ca78355367ed33425 Apalache Domain Def2 True Passed
4c5ca1368833b812036911d0f564a76a11eee105 Apalache Domain Def2 False Passed
9ffbb855b191e10d083a4b51a3d3e4134cfaf750 Apalache Union Def2 True Passed
9a068fca2d2a5e47cde60ac165f2a1df6162497c Apalache Union Def2 False Passed
838959dc26a00232bf6e13ebe06325ba71fd7f27 Apalache Unchanged Def2 True Passed
e00a2330640d07f707c26438aee9918dc7b50f63 Apalache Unchanged Def2 False Passed
d45462ebfe2a5f1b3e3a9e6935f68fb113b865ec Apalache Equivalence Def2 True Passed
8a8da4feee826239624636cb1a22b007031c707d Apalache Equivalence Def2 False Passed
b3ed065c786cb83a62f8a2bd5d4d82d04c781467 Apalache SeqLen Def2 True Passed
b1b996b0c2162ff4413f1ab403c739f13581bcda Apalache SeqLen Def2 False Passed
427fb155d2e6b2e39158ede1e06a7eb0adfba8ce Apalache SeqConcat Def2 True Passed
a7c8ef5a9e29ec9e210102ca28869f9e8c247e12 Apalache SeqConcat Def2 False Passed
d6f90c8af35fce14e979de7c6d3936fcda3c19e5 Apalache SeqSeq Def2 True Passed
4d70dfc137ff755e229efe2d0de12fd717d2adaf Apalache SeqSeq Def2 False Passed
4b59acb993bdc0735df59382cb429ec484510ad5 Apalache SeqSelectSeq Def2 True Passed
72fce6444c7ad77bbfe5ca0379dd9634d04d2204 Apalache SeqSelectSeq Def2 False Passed
a397cd65a10e1a946ff46d597d99fed54f7e056a Apalache SeqSubSeq Def2 True Passed
78df63a1cd3c18a3ba9028100be58a65990ef9be Apalache SeqSubSeq Def2 False Passed
7973a89a00c2c0debf606007c09a5d0b1f96eb2e 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 Def2 True Passed
da584d9492a4c4fb9fafc6034b5b29e38ac0b070 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 Def2 False Passed
65539af9c5c3bf57d4a2cce2491019e85dab0815 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Def2 True Passed
4d7882b2fa713badeb19539c19b1ce559699b579 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Def2 False Passed
d49790e0e965fe483e614157465f435686a51b58 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 Def2 True Passed
313c688e69048a626b0be77c89a3c481793b286b 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 Def2 False Passed
4b9f4c8277ebb93052eb4a4e2da693a3fb942ae3 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Def2 True Passed
ccb0183917efde3adf5dbf9c78792d88aacfe60d TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Def2 False Passed
73f71fed5844446f8292e3511cc8d45c2e54e53d TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq Def2 True Passed
ddca2d65a3b3856b73f230b9fea0966b36916894 TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq Def2 False Passed
b542f5e901a416bc6029511480f9423e7cab1a82 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Def2 True Passed
7ecac8cbf17fc5af00967d7fc8864cd548b3ab2e TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Def2 False Passed
7c3c227648568a2bc4a4124520b0f9337090a2ff Apalache BagBagToSet Def2 True Passed
a1ccd5b49e31144c3824048e3350646487d03bb0 Apalache BagBagToSet Def2 False Passed
57ae6837b39bde8a5860401912f6fd035d3b654f Apalache BagSetToBag Def2 True Passed
680d8f38cec84c6f069dcf524beb61df62b1fed1 Apalache BagSetToBag Def2 False Passed
74a300f00bb4db378359931a93f53ad14890142e Apalache BagBagIn Def2 True Passed
62352e796d995a65bff58134c979cb09eab6a574 Apalache BagBagIn Def2 False Passed
6bcef2f0ee04e728c76b8206666f5ec3c9887e74 Apalache BagAddBag Def2 True Passed
b58f17b2d2d0ec0c297cee62d4c1dba1e16fdaa9 Apalache BagAddBag Def2 False Passed
fa12f64e3b8aa820a300106f6cb5ebcdc3a4a87f Apalache BagBagSub Def2 True Passed
a8322ee7805329595b70cb2bea92ca14f99c51c4 Apalache BagBagSub Def2 False Passed
4d1dfa6c0d4380414fa56414f79eab8c07fd2943 Apalache BagCopiesIn Def2 True Passed
57d807ac5e3869bb52c59f1c28a99c1c3f8dae20 Apalache BagCopiesIn Def2 False Passed
ada400d94054ec6839df5fae7d379caf454ad87b Apalache BagSubsetEqBag Def2 True Passed
c45bb74d072285df93f95d0f4a3774dc3e804631 Apalache BagSubsetEqBag Def2 False Passed
8c321cf1c02fe241cecc4b84079804a3a0331af9 Apalache BagBagUnion Def2 True Passed
a406b953b8b197b735c4c963b1fbf6a20acc7975 Apalache BagBagUnion Def2 False Passed
de3ef5c0bbaf34e6aea82b39de93b1ba95e2cdc6 Apalache BagBagCardinality Def2 True Passed
1d047777306bb6b9d566700f25a72f2b4cfff1cc Apalache BagBagCardinality Def2 False Passed
0407ee6b9e34dac129677f937e10dca4a61dfe5f Apalache BagBagOfAll Def2 True Passed
dbb96dd8bf099b9c8d38dad2e1784a75f543345a Apalache BagBagOfAll Def2 False Passed
f301c5277dd714944eb349606f2fbbd7028e6177 TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag Def2 True Passed
3139774c41d979a19fdb1a9cf2f9ff4ec59a9234 TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag Def2 False Passed
2f67b0de460d09772a05d9c3154d75cac289f8d5 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 Def2 True Passed
38475eacd2c8bb169404d63e9ed11e8081de08ee 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 Def2 False Passed
f77f8d552df19db0c3497e817568ffc1d7105b30 Apalache FiniteSetsCardinality Def2 True Passed
d1d91d8816935689798cc04622d8c71a3671b1c6 Apalache FiniteSetsCardinality Def2 False Passed
4b2f0ea10e9f41536bde2e9cd98fb0605c9e8aaf Apalache SeqHead Def2 True Passed
8f56feff41c9a75902a9d4be10fa81b55ee1049b Apalache SeqHead Def2 False Passed
617589e423d3766568aac482534a172146bc6810 Apalache SeqTail Def2 True Passed
b20f244d07b99324e28da88368479902e6b99147 Apalache SeqTail Def2 False Passed
dd6817bb25f008609b2fd2c345546c2dbcef1de6 Apalache SeqAppend Def2 True Passed
1be1c58b17eeb3e221dd314901f0d64ae4b10eaa Apalache SeqAppend Def2 False Passed