Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
c8eb4b6a4ae416728b2c31cf6fffdf5b6c73930c Apalache And FunApp True Passed
cc14e5033924706b44e2fc209680c59b1362ad9a Apalache And FunApp False Passed
3b078d8ba9ca3012b8cf18e24299de44d7b94fe7 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine FunApp True Passed
deaae78b3e85232f4aa9ba79d1a8fed51e05d139 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine FunApp False Passed
2beac356ab1631cbebf69a5e374b661f37d01eff Apalache Imply FunApp True Passed
d928ef064cc04996938fed8308f827f32f64efca Apalache Imply FunApp False Passed
c6e6ba9cc8b45e000f2bcef68b8963fa71ecb6bb Apalache Not FunApp True Passed
17b802026ef628c00fc70fa61922186f152d9b45 Apalache Not FunApp False Passed
a271dc27d29ae659a361845f72787f1eee68a87c TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or FunApp True Passed
89b0d45578fc1860c96ac0fc1d8e0d6b4ab97a04 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or FunApp False Passed
d094aa46382e2e8b1f4be7a19c5e20b17f65571c TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine FunApp True Passed
33aca9ff7b1ec74d66c50f18e602114f491b9bf8 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine FunApp False Passed
68d4ba16ed078ae915d8d650479f2ceb714347d4 Apalache AndProp FunApp True Passed
ba74835a1a078068183ddb5291d259d942ad302a Apalache AndProp FunApp False Passed
c09e7b8a6b55e00c3fe286a884d6a7ba476ac139 Apalache Boxed FunApp True Passed
9d0983c008e2934a23d43d22dd2a4a89a89c68e3 Apalache Boxed FunApp False Passed
d6bade8a45f80452d15f94be0501a0d23fdfdddc Apalache Eq FunApp True Passed
431784ed49fca48bef28c80891b0c7cbbcc498bb Apalache Eq FunApp False Passed
9de6f6043e944227ec5db202ef34e6ef06f2c4d8 Apalache Ne FunApp True Passed
1cfd4cf6aee16fb39c2a4c12f41ae225820a4d8c Apalache Ne FunApp False Passed
d75d4f484312da2e4d3d65d88c2af3cba1b323a7 Apalache Let FunApp True Passed
f7a56637239b89afe0a7b7b28a294aca64f620ac Apalache Let FunApp False Passed
e3e4395aec1cfc495133a60b613b93898c5cd965 Apalache Set0 FunApp True Passed
c81026f1a282e5f06661838f32b9ca6e69951bcf Apalache Set0 FunApp False Passed
b7112a156649efe74ed2a8bb0a80652cbcde792c Apalache Set1 FunApp True Passed
c5988a2fb21b7c3f69aae5d5ba0b50043bdbe199 Apalache Set1 FunApp False Passed
7b4ff9a807b6edf739146496479f1d28edab96ab Apalache Set2 FunApp True Passed
931b7f830096ccd52670e5b89dbb1d3124420e09 Apalache Set2 FunApp False Passed
64245786aea3ffbb4474022802d71bcb6a016c0d Apalache Fun FunApp True Passed
146b7f85ac5e63e4b55ee87e4a8b3b457f7322c4 Apalache Fun FunApp False Passed
b5017e2b23dc4eabdca6ed9bfd2d5932d6ff2327 Apalache In FunApp True Passed
eb2624d37d6ec8b3539f965362fe21b7e03e2c42 Apalache In FunApp False Passed
7f3ef8eae2543873ea1d99546632eea57ccbb110 Apalache NotIn FunApp True Passed
2951045f6c5a1779e228d9a70107cf8d12b68e53 Apalache NotIn FunApp False Passed
1afe202b8279350f0e888eceb1cadbdb80690cf4 Apalache Exists FunApp True Passed
3d9808f9c8b886d0fc71ea37fd4d9695c4f147d9 Apalache Exists FunApp False Passed
257ffa40d61b51c75dadcec9d665d1c87f07c858 Apalache Forall FunApp True Passed
67aee127ee35313d309f7d5fc74f9fa8bab6ffef Apalache Forall FunApp False Passed
5f7e166c77dc6a3e74fb480b6e119cf58b0e3420 Apalache Choose FunApp True Passed
d5b4ca944a18fe4a68327e76a630f85c4ce0838b Apalache Choose FunApp False Passed
3a89e1c6f54d52364a6a206ac49eb3a17c58cc0c Apalache Record FunApp True Passed
18d8809d3e388d5c4c13fac278e0c9a14f9c25cc Apalache Record FunApp False Passed
a0155333d2e85b9d251af31d65674989009b9196 Apalache Tuple FunApp True Passed
5a99b3df741b170146560c947c208649f16eb956 Apalache Tuple FunApp False Passed
59601f7b08f17e976629808295cd70a7f75a0502 Apalache FunApp FunApp True Passed
24c5e73972831495bea5a070456a0373496d6e0f Apalache FunApp FunApp False Passed
86fe0ed35a238c5bfbf25555ffee23ba61b41614 Apalache Except0 FunApp True Passed
edca9210011f2eabc4038615724698115b515db4 Apalache Except0 FunApp False Passed
8bcf8d2e40cd3c08a7b8196b8827ffcdfa873198 Apalache Except1Fun FunApp True Passed
35232392003964841d9b3a4219e9f3ce6a539083 Apalache Except1Fun FunApp False Passed
0230394b8f02c83c09003725042b0d1a87781753 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt FunApp True Passed
728ec11f801fe3194f99781e5ea666a64662a8d1 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt FunApp False Passed
4a04820fa02a60cedf65f02c0f68c597ec1e2b20 Apalache Except1Rec FunApp True Passed
81617e59678ac0ef84d67598c22dc5dcfd73cb0a Apalache Except1Rec FunApp False Passed
0d86c41cc570be91822501075cb0acb7956b8842 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt FunApp True Passed
edf93fdcd1e43ed1ccc2a5218b1cc1388905fa7c TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt FunApp False Passed
ef1c7ef93bc7d143e99ba4d007e3ef42333cf0a0 Apalache Except2Fun FunApp True Passed
5769f6de4ee36e32098e7ec0f0367a1a8dd09f93 Apalache Except2Fun FunApp False Passed
8a929cd4d1e6eee662af912019a348a5610b5256 Apalache Except2FunTuple FunApp True Passed
40b0289af3c0b1c7a9ca25d040d1a0433690f86a Apalache Except2FunTuple FunApp False Passed
b83c84bf2b6236a7c98fbaa9a3d35376cc2b44d4 Apalache Prime FunApp True Passed
618b1a5b58ac8b0227968f15105080bb21083176 Apalache Prime FunApp False Passed
72ce7d919e1c50d98bd417af17e3ba35b6af5949 Apalache NumUnaryMinus FunApp True Passed
d28e4ed94f4b6c7967075ac9ded598a0d57c4057 Apalache NumUnaryMinus FunApp False Passed
8bab4baa6098053ed6ee390490a6cdbc4450d7f3 Apalache NumPlus FunApp True Passed
3f34d00430f4518b73720877c3b02056b7b89f52 Apalache NumPlus FunApp False Passed
ff633f99178f89f73bae17fa93dbb0b0c5ce6887 Apalache NumMinus FunApp True Passed
f8d3fc4edfb2c4c811d1fe490c3ab6d21ad0e73c Apalache NumMinus FunApp False Passed
9f9b03e9a735d37d524f60e5daa6acd41153a2fe Apalache NumMul FunApp True Passed
540c4e6401b9dc41775ccd9426a03815f9173502 Apalache NumMul FunApp False Passed
9f6d048e5bceb75acc0e4d97b141de194ac763c5 Apalache NumDiv FunApp True Passed
1cfda8c959a81902cbee921d6722767aa688ff09 Apalache NumDiv FunApp False Passed
4601ab57aacd7c6614a8dccb2f5f2c6ce3a5aabe Apalache NumMod FunApp True Passed
bc345174118b6d8f5226ccd7e1458d546e8595dc Apalache NumMod FunApp False Passed
4a8c62c338abb2fd4634ba8404d0330aad37df7b Apalache NumPow FunApp True Passed
ff80e41e5e05f9bb9056ed6bef0c21051859db0c Apalache NumPow FunApp False Passed
d31ba9b574abab71c8056e4344e549a51632eb0f Apalache NumGt FunApp True Passed
e5fb607fd0960f53056a31e8a4f1c375e16bbd41 Apalache NumGt FunApp False Passed
4dbd1fcae8b653a16686da95b6272597981a6480 Apalache NumGe FunApp True Passed
fef0de07550b8533bfb87309ecc6868f1c915e56 Apalache NumGe FunApp False Passed
2c675d0f32721e6dae9caf2cb5106714a4d1f162 Apalache NumLt FunApp True Passed
95f5f89d7fd2cd5dff1d53442db46ab80f2351c9 Apalache NumLt FunApp False Passed
4b5a47a65d344d105b9c04c112c4d3372e616890 Apalache NumLe FunApp True Passed
93c4f9ae8ba91977ecaa8c571cbaab9a35c29ade Apalache NumLe FunApp False Passed
823ab31ad4e2e7a1b475452dcba1927581c56aa1 Apalache DefFun FunApp True Passed
36f489eab67c1a4f9ae630db78a7d1da1ea81e63 Apalache DefFun FunApp False Passed
554a52588a2cb65e72260b4fa4e547faaf04843d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun FunApp True Passed
d7ebc22fe5587c379de453b2b621d370b2848a66 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun FunApp False Passed
3e7315a992423620a8bd852efb8c1b762f3c4ec3 Apalache DefFunRecursive FunApp True Passed
b1bc2179919ee546bc1e157b92e71fc1bdac6d62 Apalache DefFunRecursive FunApp False Passed
f55f22b22a673f7fe25bf93f148224af808f006e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive FunApp True Passed
ec46b7577f7dddf9735e2d6cdded8f280c51b53f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive FunApp False Passed
5b77d086dfb866aca7379c43d7e5164bc0c66bb1 Apalache Def0 FunApp True Passed
faabc0be7fc4de0d30a5e564bc3db099e60d6026 Apalache Def0 FunApp False Passed
45826a23aae893d4615f6fe74ef600d6118a5820 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 FunApp True Passed
9ac299359336c8651641f268228a23f063e870b4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 FunApp False Passed
64c6d0c61889ab297ad6087a6b99c45551a49140 Apalache Def1 FunApp True Passed
f2ff4ced1bc3454ee9bde30fe0b92bbe3f32522e Apalache Def1 FunApp False Passed
1bbf8ed3327362487cbe044624fe9050992b5c7b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 FunApp True Passed
89e33cc6fdf3c8d8a72aafe991ddd7d8106d1f03 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 FunApp False Passed
c19975da39e34f7b3588eb2125ab2a45a24146f3 Apalache Def2 FunApp True Passed
ce222959d11e319a65228d6aecb20f19814a9e45 Apalache Def2 FunApp False Passed
c899c492a028973f24bdb55b2e142d8065790578 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 FunApp True Passed
0d92f3cd35ba1f305291d36bb2501b1cb5aacdaf TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 FunApp False Passed
dd975a35b914f809a30c9c9dc363290719227a95 Apalache Def1Recursive FunApp True Passed
5beb04191d177ee547b9529dc81502c883b38b32 Apalache Def1Recursive FunApp False Passed
7d427b6f4e7587a3a2534381e016ba222f1734ac TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive FunApp True Passed
7eef74d9bda63b2ae416625acd217527600421a3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive FunApp False Passed
288ce0d50a32933e81ad223741072f472a0f958a Apalache Extends FunApp True Passed
2110d7bb699f3b7ec75d82d76dec6bca70165444 Apalache Extends FunApp False Passed
b39d7d406b3b51b3a67403df8ccda29ade0fe540 Apalache ExtendsInDifferentFolder FunApp True Passed
390afb91e260510de5fabbfd255faa7fc8a04ad6 Apalache ExtendsInDifferentFolder FunApp False Passed
d0c5814f1f71b8891417363f929c869a0945cfed Apalache Variable FunApp True Passed
c45aa20ae6e8a9d79f115e76d90924401b663502 Apalache Variable FunApp False Passed
8c9c79e59d7faa6da50fe801ea0b2a8acedffb3b TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude FunApp True Passed
56baf1f66c452bdcc2221f517e8ee7a23dabbb75 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude FunApp False Passed
8638b27ed04a1d7c223dc426ca92b21a4130bd6a Apalache Constant FunApp True Passed
21067629af377f84c64dd04e827e81ae2588bd09 Apalache Constant FunApp False Passed
4b75764c20ae5159dbfaa69837e77a84f26911dd Apalache ConstantRank1 FunApp True Passed
ef9377292acc5d253a71f7d64ef3bf93178e7c8e Apalache ConstantRank1 FunApp False Passed
eaff91da5e11b5c8de104da3b4880b66d481f226 Apalache Instance FunApp True Passed
ffcde4ecaf0d200e0e6650490ad8b9d7438b04af Apalache Instance FunApp False Passed
1d0512e93678c1e25d5d23cb7ec850f40c91300e Apalache InstanceWith FunApp True Passed
ce18e80eb80a2004ba684907b757d6398eb96ac8 Apalache InstanceWith FunApp False Passed
20c9382428b4070e89fb1a47ce7e1edfec247a8b Apalache InstanceNamed FunApp True Passed
94cd6add36c7a22f2f337c12b9192ee5f5b3dbf4 Apalache InstanceNamed FunApp False Passed
c57f4b77031d05d2c0fb3772ecd2be017097ca7c Apalache InstanceNamedWith FunApp True Passed
209db169dafa30e228c61c32ac503829e10ff61c Apalache InstanceNamedWith FunApp False Passed
04eef732ca3ff126c030f21ec67d03170b253960 Apalache InstanceInFolder FunApp True Passed
c2e58424e8d152d735c6989f53fbd40a028978a2 Apalache InstanceInFolder FunApp False Passed
e735aecad907abce60044e6a051c46f3ff8e5eaa Apalache InstanceWithInFolder FunApp True Passed
c0dd5e3634db13824cf1cd1e3f6b557cc246f33c Apalache InstanceWithInFolder FunApp False Passed
a816a8137d11b4e92bea9cdfc897730d42b350f3 Apalache InstanceNamedInFolder FunApp True Passed
05e2b7b5ee2dca6f641a9e4eb558d6e3da3ab9d0 Apalache InstanceNamedInFolder FunApp False Passed
a5029fd9355272b0931f650568c5050022576eef Apalache InstanceNamedWithInFolder FunApp True Passed
cc147fa56c0d290f2cfe8e343732f8c396cbc653 Apalache InstanceNamedWithInFolder FunApp False Passed
d860b9838009d08e00a4f786bf315d75c6729874 Apalache Enabled FunApp True Passed
18297d8e53a5b775d1ec919c7915392d73380937 Apalache Enabled FunApp False Passed
5bcc00b89787c3fe878e67d2898bdbc850db657c Apalache Assume FunApp True Passed
22821b66d469783b5f9e59603976b212fe2abcdb Apalache Assume FunApp False Passed
c41814cda2ff58ac1f000b0b27fa24d88f5ec46a Apalache AssumeNamed FunApp True Passed
041a1bcc54aca37da3cc4c81ddf22b513dd4eb21 Apalache AssumeNamed FunApp False Passed
b1f0968dd4ef50f6a1cf115d9c56af374d1b0b50 Apalache Lambda FunApp True Passed
f9ab8fb3290e9453e641cadb92e78c8e8177f56b Apalache Lambda FunApp False Passed
fdfa418691a20e5c656af2925596b20e5cdce8f0 Apalache Cross2 FunApp True Passed
82129ce4035cab735eb5ed5bdd53eba66a6f6e62 Apalache Cross2 FunApp False Passed
e12f3d0e069b2349d89456f10f5d181cf436b723 Apalache Cross3 FunApp True Passed
373ee57578f9dbee487b9129afa62a4b01a7a00c Apalache Cross3 FunApp False Passed
8a538005b64639745d5f0eda5f4fb2d2f536b3b5 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 FunApp True Passed
a2bdece0b4b6e939cc7a258e0eb0377109437f1d 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 FunApp False Passed
4e53c6742c600569b9342d373d22f3f4cd3d9c02 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 FunApp True Passed
e31c1b88b4a9c49c083446176c79ee40cd0b5f60 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 FunApp False Passed
379aa8f13a9aa6f3f2edd4efb2b70d8de007df51 Apalache SetDiff FunApp True Passed
47d5ab33a19e8d82e6f69220c7c7b2cce8b2c03e Apalache SetDiff FunApp False Passed
2334b461227c5033cfa96043f5c3480bf12947e5 Apalache SetUnion FunApp True Passed
878e6246a2793dcc6f39a39a443cca1eebe52406 Apalache SetUnion FunApp False Passed
3bda1ba1ac3aa738b34fbbaf8339432f8a2e79d6 Apalache SetIntersect FunApp True Passed
2845245673c9d45b794ade2935c53697d6f296cd Apalache SetIntersect FunApp False Passed
d77a7fd0a37a947ea3971429251c2ec5898c6d60 Apalache SubsetEq FunApp True Passed
2bce7e58419c27b80304836a633e0781f00f02b6 Apalache SubsetEq FunApp False Passed
acdeb4dfe1a94d7e9585a83fb87273222bfa1e5d Apalache IfCond FunApp True Passed
f783886a101a14537297d7230d04c8395d296be7 Apalache IfCond FunApp False Passed
a65d058a75557f37b20b1248befb98ea90b04035 Apalache IfThen FunApp True Passed
b8aededf6a3a52a2121bc057c0a24d9369735106 Apalache IfThen FunApp False Passed
1e7c2f09a55503d3845ba876ad917dcdec175ebb Apalache IfElse FunApp True Passed
8fd35c0f435dd5688e1aeedcc61bdd986bf6262b Apalache IfElse FunApp False Passed
d0936637cbcefebd5ebeb809d18e89ede242e431 Apalache Subset FunApp True Passed
a2de11ccda1c91256262683343a34602e349dd63 Apalache Subset FunApp False Passed
2b78423e2bfe6f581cda515f9951cfec1ef565db Apalache Domain FunApp True Passed
5086daa513c9bef3509fb6e6f389aa4ee9a60d98 Apalache Domain FunApp False Passed
a79139f9adbab2fd4a9ab9439274fb3730d6b639 Apalache Union FunApp True Passed
84044592f93191b589b9bd01fd6a67f6a2549dfa Apalache Union FunApp False Passed
1614c9eb8dd255a743c7b103504fcd7d5bdf71e2 Apalache Unchanged FunApp True Passed
731b346250042a577830d007f2652c3d3e2e8539 Apalache Unchanged FunApp False Passed
f1487128ab2e1f4a7d3f84d25645eb2a0022cfde Apalache Equivalence FunApp True Passed
5e1051133f0a4c8e61551168bb3a4e2597b5eb57 Apalache Equivalence FunApp False Passed
0121151b97e7d8fdbad378e76411ea05af876205 Apalache SeqLen FunApp True Passed
b45fabb14491b1ce522272dab28b8b16078a2eab Apalache SeqLen FunApp False Passed
bdc7443e61cadaf366e4c5f45d639365a701337f Apalache SeqConcat FunApp True Passed
2e484f42d8b8188ce72cfefc8a9d1e34e7904d27 Apalache SeqConcat FunApp False Passed
77f4ab894d81ad331b09e0294b6c9b18513a9558 Apalache SeqSeq FunApp True Passed
99dcf86c0aff4b7d6b0cb1a6393ba6cbd2713677 Apalache SeqSeq FunApp False Passed
24aa86637a74c5cb90d46bd597e32eac04c77c95 Apalache SeqSelectSeq FunApp True Passed
fd444ebe62f0c49c2f8447407655191cd4ad1be0 Apalache SeqSelectSeq FunApp False Passed
1ed5b3da6d2d149d6755d064826b322541a10192 Apalache SeqSubSeq FunApp True Passed
90959f858809186b8b95d65774dc90fe5e8034ef Apalache SeqSubSeq FunApp False Passed
0ddf01d76eb4ba6121495ae875cd13aa875e4b87 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 FunApp True Passed
398c89b0fe89f1cac6dedbe45b0159c84ce9614d 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 FunApp False Passed
37035be2293f5a3e47d48d221a2a40f24fd77609 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun FunApp True Passed
bbb168686f7273460df767f7c67a4484e374b452 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun FunApp False Passed
884bc6926eab116cb4a542b67085c4617f96a5bc 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 FunApp True Passed
4c85a3e7be3ab3ee7a64e9acc01eaff6ca3779c7 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 FunApp False Passed
c577d052dc08e84aff43fe6741f212bdf3c60447 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun FunApp True Passed
e18f3384c1014c2fc4f1c9950001300c8a070861 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun FunApp False Passed
c910307e4edb67dea697b2cccd84ab8a3f2d7d87 TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq FunApp True Passed
e74804270deb5c49d2dfefb1d7cca31d17a377ed TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq FunApp False Passed
825209bb144690adf846e9ce2206cb9b59329e38 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval FunApp True Passed
52f4d985da8ad334d8cb3f59e0d96d0f662e39f4 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval FunApp False Passed
3106ec571d436d8e6711bd1587620998706caf28 Apalache BagBagToSet FunApp True Passed
7a1e26defba44155b7ae32cf1835f0519bccc2a4 Apalache BagBagToSet FunApp False Passed
63aa7c3b28ff4b79c154ab8d7bcd2bc1bc5277d7 Apalache BagSetToBag FunApp True Passed
52cdfc4c21ee2e286265b16a960c9358fe84afbe Apalache BagSetToBag FunApp False Passed
2daffb1b933b69ed250dc989d8b5e6f28a430334 Apalache BagBagIn FunApp True Passed
75b8eaaac068a75f78e200de325043cd4d4c990c Apalache BagBagIn FunApp False Passed
c086cbf2ec63b0e1fc9dba0f0a1295581aeb1b60 Apalache BagAddBag FunApp True Passed
c9cf81e95496fa146c9917063262e52e94b26fa3 Apalache BagAddBag FunApp False Passed
461959f5a9c61407e45c86b0ee978df494fa5333 Apalache BagBagSub FunApp True Passed
5430459ee2687c0cecf71420c1089f126e2351fe Apalache BagBagSub FunApp False Passed
c527780735c501397962aeea1099213bd005c679 Apalache BagCopiesIn FunApp True Passed
132c3cc01502f7f9d2daf955967181e22012b655 Apalache BagCopiesIn FunApp False Passed
99fd89fbb9033dfd95690e00bc94e0d83c23320c Apalache BagSubsetEqBag FunApp True Passed
9d4cd06dd44589676a40a4741b3013fd96826146 Apalache BagSubsetEqBag FunApp False Passed
ca29cc94ebc293d94c6bee44862f61627dd3cbb9 Apalache BagBagUnion FunApp True Passed
3a8dcd1054088c6030b151749f34d01c49d7b83f Apalache BagBagUnion FunApp False Passed
345adcd94c4128f3757138a6b3cb392d0675b86c Apalache BagBagCardinality FunApp True Passed
2c8196e264c0e81ba09266ed4caeb54875bd5674 Apalache BagBagCardinality FunApp False Passed
def7dda91d500256ef537b463471e65669348af8 Apalache BagBagOfAll FunApp True Passed
644ec63f5aa2bf8bdd70ed22875700bec0222690 Apalache BagBagOfAll FunApp False Passed
34f3b4446852c406a62f3f0742bd043bfcde7486 TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag FunApp True Passed
6bb2c1830c5f5dd419c4da79d8a56e5dbb8360e8 TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag FunApp False Passed
0fe06d0d0975eb64eb1181d7c5af492e57b453ed 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 FunApp True Passed
b2edbd7ffa504c52fb573d52c4707cad807d3b7b 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 FunApp False Passed
4383172109379fff727555eea72c6090df62385e Apalache FiniteSetsCardinality FunApp True Passed
38e8fff75cd8009ad5dd2754e324591c18a49b27 Apalache FiniteSetsCardinality FunApp False Passed
1f99f4330840e72d380adea6072f0bea17dc0e11 Apalache SeqHead FunApp True Passed
9b4f3daaeec7064f41ceed4bfc3ec388904b431f Apalache SeqHead FunApp False Passed
9f236c2cdfc3f61718dd9a83223065b2ab3998e8 Apalache SeqTail FunApp True Passed
453969ff0097c6115f554d24437b4766129da1c4 Apalache SeqTail FunApp False Passed
c99aaf97a4af299b3048a49875271f6ab749fc92 Apalache SeqAppend FunApp True Passed
50e1a313ba783a27967dc405c4e8923936ac99b2 Apalache SeqAppend FunApp False Passed