Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
f2d20be079db6505dc08d78f49845a6830a28b03 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Variable OneLineComment True Passed
ba11baea47b98ab1d93712760e0b3eea81ba161c TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Variable OneLineComment False Passed
899d5744fa489e4d40f717dd1622b199316d1269 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Variable MultiLineComment True Passed
8b52571534c05b4cad5b2cad831da7a928c0a639 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Variable MultiLineComment False Passed
7e4febb6f33289058b355e3a83f259336ac14d19 Apalache Variable BoolTrue True Passed
538eda2121f0bf826e6e37ac38192c023bcf8189 Apalache Variable BoolTrue False Passed
d416b36d1af6ab925e99be5bed44bb70b599d3c8 Apalache Variable BoolFalse True Passed
06efdd4e789cee241b922d2887db0fa0ad345c07 Apalache Variable BoolFalse False Passed
12cb76c5474f5dd0b38c2650bb45f6b32d077858 Apalache Variable BoolSet True Passed
0fb989112132a24ff3dbe124dc16ffb17fecc993 Apalache Variable BoolSet False Passed
6003c9daf0ae7e2c6a5d623936f30de25e28af91 Apalache Variable And True Passed
81cde0ae2de17771118f160f5f4652eb7b5239cf Apalache Variable And False Passed
2e351f497444f7df3613636f3d94494306e5617a TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Variable AndMultiLine True Passed
8ae6c25b51c5cd18f793c9814312e132eb8e917b TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Variable AndMultiLine False Passed
a2511070d32db117418e3a642f28b1902b7a26e0 Apalache Variable Imply True Passed
484e44f9a42ac6f1d10374053e240616b4e41a73 Apalache Variable Imply False Passed
74b0eb20af7a3683f4d419d0ef7e446440f7c00a Apalache Variable Not True Passed
a3c9baea421b54da7506b64ac43ee5fd608e5f55 Apalache Variable Not False Passed
c42c88756a82a749707e80c12a2b0ff407edf3d4 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Variable Or True Passed
b4ecd0a6c9c359297c58ccbbdeaf75d9fe1152c7 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Variable Or False Passed
b5c5292ce409229553f3da585c1f2233aec07247 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Variable OrMultiLine True Passed
ad702b5fc48328e8c2441b1e07d083140b590354 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Variable OrMultiLine False Passed
4df21a10a1ea6ad141f6f904211acdf1df021c22 Apalache Variable Eq True Passed
a716f14e9631a52d92ec1395765d35d262c7d84e Apalache Variable Eq False Passed
0671d1de782522a7a8089566e97d175f1639d2ee Apalache Variable Ne True Passed
77b972c2a5c537e12f917aa112fe0dfd1048045c Apalache Variable Ne False Passed
0321e7454ac0d76f700030c5d5eb9187602e5738 Apalache Variable Let True Passed
d536ca2e41328507fd41c16a5a3ac078f78f7fd7 Apalache Variable Let False Passed
d9239e55a07f9227671cff71420cf2aa5a3deaac Apalache Variable SetEmpty True Passed
0cdcc18708ee947921a2e27517b01955fa381fa5 Apalache Variable SetEmpty False Passed
05e02dd226b1f8121e81c0cdcea7ab70c0ddd4e7 Apalache Variable Set0 True Passed
0b9ba2af832b73206291defbbb4969a34fafedf2 Apalache Variable Set0 False Passed
068e14de8c80cef3b795aef517cd90ec1cec69f5 Apalache Variable Set1 True Passed
8dc7134a89b38a4e75d7d8b79bc5f43deec4de47 Apalache Variable Set1 False Passed
ee1972068799f60b7c0e62eec03e1e291f3b6d53 Apalache Variable Set2 True Passed
2fb39c6ac66c165c0b3eb059e726250b0e81bca5 Apalache Variable Set2 False Passed
ff752ce9f33347d2bc843dc534051606a0f0ea72 Apalache Variable Fun True Passed
6a763449a6d224d7f64e29e9c3a5d5171fa860f7 Apalache Variable Fun False Passed
6138818309569e97e39ac25b73eb6f0fe94ae04b Apalache Variable In True Passed
927e43645e04879155ebc1d5beab8c02e55485cb Apalache Variable In False Passed
49bd6ff1fbe9b0cc165879a58df924eeb069d71f Apalache Variable NotIn True Passed
58d712a5d5715fa8b8e4c4dc02847b82f9554a3f Apalache Variable NotIn False Passed
1c2790181ecba2cf49b0a6eab1631ae7d062950b Apalache Variable Exists True Passed
b7f65231bec3bf99beaa1818ef07322b803aa7e4 Apalache Variable Exists False Passed
85d52afd980ac26563442675b8155eeb6214998d Apalache Variable Forall True Passed
115e91a5dbd9c8401fc794003d7f9cd861a486df Apalache Variable Forall False Passed
be40b064d635198bb6590eed5835dff08c9b0541 Apalache Variable Choose True Passed
f0bf5794d80440be5f4a5d13b155f10f73781f8f Apalache Variable Choose False Passed
b111614210cd769ae834ae7d91c2ee005f647cf3 Apalache Variable Record True Passed
6d2ad4e5c1d60714d328c14daaeb633db94feaa6 Apalache Variable Record False Passed
418d6bfcc5f4e6933b9b4b59e3155ea660de294e Apalache Variable Tuple True Passed
de7fe238388783b92e0d495dab78416232a6be29 Apalache Variable Tuple False Passed
9e8185e52f209e6075daaed1ada2ea4d5af2fd28 Apalache Variable TupleEmpty True Passed
5bfe95d1d908fee0565cf9ae2518d23b8ebb85b6 Apalache Variable TupleEmpty False Passed
d0c5814f1f71b8891417363f929c869a0945cfed Apalache Variable FunApp True Passed
c45aa20ae6e8a9d79f115e76d90924401b663502 Apalache Variable FunApp False Passed
5a2f5137de28cd777694c8be8b02b4586c1ebccc Apalache Variable Prime True Passed
07510a1cdb125aa4d52ed5152df7c7c7812fb35c Apalache Variable Prime False Passed
c6cf6d229f864e67e50f65835f8a5ea30cc09987 Apalache Variable NumZero True Passed
75435491c479687d294b0622b5cf73971aa3e192 Apalache Variable NumZero False Passed
96ab71f6acb5d21c15f69417c73d68ca91f79fe6 Apalache Variable NumOne True Passed
ef4c933a98525c99d4e1a8ec272133d4872b7eb8 Apalache Variable NumOne False Passed
f0babe7f8183f1877cfc015a744997de14bc1906 Apalache Variable NumMaxInt True Passed
583af8427d40303f1fc81b753b6e448a13603fc5 Apalache Variable NumMaxInt False Passed
d5ea57379872729137812d14395f1eb361d5e45f Apalache Variable NumUnaryMinus True Passed
7b34fdca8e773148c122856c3aa23d140c949a9a Apalache Variable NumUnaryMinus False Passed
d2362395b8492e72777fc5dbfb7dcf5d53765d1d Apalache Variable NumPlus True Passed
415bb74f5124f9c77c487103a0726e2e054d00f9 Apalache Variable NumPlus False Passed
d8ec211cb6d6a813bf967a42473f03c3c1cff96e Apalache Variable NumMinus True Passed
82b14e2052519aa69d829c6dfa8cc69db8e85eed Apalache Variable NumMinus False Passed
4e6d6e5f6fe53df6a4b43d73c5814ce64aa46f9a Apalache Variable NumMul True Passed
d0bbcf79d3ef5d848f8dd1795b057d753bb716ca Apalache Variable NumMul False Passed
59333ecf04add5d25c0fe053b50febb6a014b471 Apalache Variable NumDiv True Passed
4509da9bb30c5deaeefc6427556e524def24bc3e Apalache Variable NumDiv False Passed
6a3dd472327c5b22cc9ba8987b124bf6b211c0cb Apalache Variable NumMod True Passed
e2068398f6655c7c8e297be5f17fcaec3f33fb91 Apalache Variable NumMod False Passed
59f6690f4dec32a64a0968a17c7da9bd2e6a16dc Apalache Variable NumPow True Passed
673b100d8b6615ec161db4da661254cc53c9605d Apalache Variable NumPow False Passed
28a85dd592c8b54bdc74c66253b94c44404795bf Apalache Variable NumGt True Passed
6e324428af5599ea509533a485a2b33d44f56278 Apalache Variable NumGt False Passed
b510461c6013481f881b205551d22b29057fefda Apalache Variable NumGe True Passed
2665c82e450072ba812e7cb6284faa9cc46827cd Apalache Variable NumGe False Passed
ebff17dde351479c5c458dd710df30f0c3ca8a92 Apalache Variable NumLt True Passed
7d1baa793e12958decd188a3b66c0b01c8f648e6 Apalache Variable NumLt False Passed
85caebe5763efd1d38fbfab851bfaf5f6825e239 Apalache Variable NumLe True Passed
64aca7520f430d9b5910de80268082b1a5b836ab Apalache Variable NumLe False Passed
8d7e6329a513afe1797145cd80bb1284a29b2e5a Apalache Variable DefFun True Passed
340a695b045fc96b0821e6661c8fcff2a6fc42b4 Apalache Variable DefFun False Passed
0fa7a4f8ecaaf6ae43e77a14cb15b77deeae2c26 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Variable LetDefFun True Passed
f6d1a8baf12f7f9f09a3931a00be509716af2f87 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Variable LetDefFun False Passed
5ae96488e6fba7d6b024fb03d98165e4641dedf1 Apalache Variable DefFunRecursive True Passed
0bbadb63613a395f4e80e1513b842480d249940a Apalache Variable DefFunRecursive False Passed
cedc7da428ee0d59f45a9d04ae1f6f17376101df TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Variable LetDefFunRecursive True Passed
ebcad52e60f9a5d13c7eac095c828301ea4aab03 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Variable LetDefFunRecursive False Passed
b924c073e84f7612814a3193c3683ed34a03db57 Apalache Variable Def0 True Passed
4b1ebbe89d90935e8a13c11dd7208424a0b251f7 Apalache Variable Def0 False Passed
1b7a0df2533bcf8eba8fd3d57e64c4d9c9793900 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Variable LetDef0 True Passed
d490fb003ce13c15ed501ab51a9d97962051facf TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Variable LetDef0 False Passed
88630e96451b4d23ec98708d9df503df51d2eccc Apalache Variable Def1 True Passed
255df1d3666a8de0744e38b37d79f920f0ab68e7 Apalache Variable Def1 False Passed
10ab602137f588864c9f8dc9ecbb657d63188029 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Variable LetDef1 True Passed
134184522745cb707cb29b3c2f078bf38e6a2a11 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Variable LetDef1 False Passed
96e9bdf90875cde60047f9575495e341c2b0f24d Apalache Variable Def2 True Passed
61828218d656a0b93c097c8d2871773881defeac Apalache Variable Def2 False Passed
c423316aeaf267d09fa52b90aff16923d43e2380 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Variable LetDef2 True Passed
01206232f86997c8a903bf70c2580737bd0a9aba TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Variable LetDef2 False Passed
dead5be7ef8d5cb9528afbb3f19b20d9dfdf3a9c Apalache Variable Def1Recursive True Passed
a736de12a9d62c8a9d24638e9e380e91d4d71f04 Apalache Variable Def1Recursive False Passed
2e1652f34e554310ac423188208696c20f4337a9 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Variable LetDef1Recursive True Passed
b411223600f52a3fc4d449b0c97f931b44f05ded TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Variable LetDef1Recursive False Passed
215dcb1741060af98a5a9dd6337c1b22c3fa900b Apalache Variable Extends True Passed
9c6353f435fe3bab0984c71347ddeb27cc14ac72 Apalache Variable Extends False Passed
a931cf86d4f815759b8b8f9aebca97004a219e29 Apalache Variable ExtendsInDifferentFolder True Passed
732cc3e1de3ded5def2cbac2dd9384e4d7da4b98 Apalache Variable ExtendsInDifferentFolder False Passed
c16eabd8afdbcdcebe22346d6018391367037a8d Apalache Variable Variable True Passed
42335999f496d50501956fc71912bacd871007ab Apalache Variable Variable False Passed
642d376051f55bc6122f93a15ba3eac816dcc3cd Apalache Variable Instance True Passed
cc9c79db36016fa557cc6f446bfe5049695a940b Apalache Variable Instance False Passed
b7a7cf799d688161be3323575fc6fbdc31540388 Apalache Variable InstanceWith True Passed
87d1665d37da92027b21ca67a265a5160e3746e2 Apalache Variable InstanceWith False Passed
fd9fcc93f00d35913474be50828524028f693094 Apalache Variable InstanceNamed True Passed
de9a0415398e0d37d2791ad887a3f89f68d54199 Apalache Variable InstanceNamed False Passed
914d17705aa68d46c6653ccb6481862b9ebcec11 Apalache Variable InstanceNamedWith True Passed
f2bf05a841ffa0a17477c34b60e289e3ca58b38a Apalache Variable InstanceNamedWith False Passed
d9e85090b15f6bfe3796c3ed188347a8ce85d972 Apalache Variable InstanceInFolder True Passed
8a40c16f08575484f82b57a23fe397a8ec6f2a56 Apalache Variable InstanceInFolder False Passed
02e5c25f6244480783782a537c4e89c2d7ed99af Apalache Variable InstanceWithInFolder True Passed
03454f5b5e4b0eb833f2a163dfe23420a92294ab Apalache Variable InstanceWithInFolder False Passed
5228955950ad7b7d64880a77071fedb32f85d63a Apalache Variable InstanceNamedInFolder True Passed
8e2217d332f1c856464325ea84e65c68ecd432f6 Apalache Variable InstanceNamedInFolder False Passed
6229c54f24a829138aa84a95c52f65f96c9b92d3 Apalache Variable InstanceNamedWithInFolder True Passed
e9e3348090f409f7b9777abf4af1b289dd46db85 Apalache Variable InstanceNamedWithInFolder False Passed
52fe08036077e989cf1966566d1219a3c4d91c0f Apalache Variable Enabled True Passed
adcb99211770fe5d91e53b6097965ed1cd0c6816 Apalache Variable Enabled False Passed
3de3fe5ddf31635e703a35918b173fbb54d68130 Apalache Variable Cross2 True Passed
1b2ae0ecaeaa4240569a9bf95987d8f3d4fff0d9 Apalache Variable Cross2 False Passed
fa3b409ea0e1d5fde08da665a5e3d3a1aa09a391 Apalache Variable Cross3 True Passed
dacd6c8fbc004fee508108aa8cf4dc49266f1610 Apalache Variable Cross3 False Passed
1e78998db9f1404d7bade0fb1d40bee86cd4f663 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))
Variable FunSet True Passed
ac879be0c2d5090a5f2562dc8280956fdda4214d 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))
Variable FunSet False Passed
e179b044120c71cf8906e1120768b949c1166be6 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)
Variable RecordSet True Passed
22fd78ce7d6d3265c8af64619d36ee55efb57007 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)
Variable RecordSet False Passed
721684748ebed3dbdc1575a0594dd44e0cd415ba Apalache Variable SetDiff True Passed
5df4b2ac595618f69d1fac8dbf107bdb8f343357 Apalache Variable SetDiff False Passed
9e138b87190f725de575821f3d2083032bc939bd Apalache Variable SetUnion True Passed
9a355e5c17ce57e26ab3bca9ee053978d20ffecc Apalache Variable SetUnion False Passed
876487a05793282bdad832f2784930cbba77b4be Apalache Variable SetIntersect True Passed
41910a2aa0049f892f62371c19cf2b645223e3bd Apalache Variable SetIntersect False Passed
29d425169cd50e7c5ab59bb0ceb4e26acfff825d Apalache Variable SubsetEq True Passed
e750757304eb5003425923b9a189f55c3f2f00a6 Apalache Variable SubsetEq False Passed
47052fda3cb27f6274d90e94a5b46682d79f7875 Apalache Variable IfCond True Passed
51e83f4d5ec7bd6482ec1e05bdc496aed18cedd9 Apalache Variable IfCond False Passed
1ebb22e4a5e73267300e352de4052965b43ebef0 Apalache Variable IfThen True Passed
7bbdb20a1066e67895caad4a557f6df49c98b7b5 Apalache Variable IfThen False Passed
0b4db1d6778afedad51d878b8a8a378a1c9bf290 Apalache Variable IfElse True Passed
bdd121054705452a97d00f18f3471c938aafb474 Apalache Variable IfElse False Passed
d300cc219af6071dee9f30e17ae1d28c62f98173 Apalache Variable Subset True Passed
2e3b8afcd96d5a9caf31227bedfc68bd1d83661e Apalache Variable Subset False Passed
dce02843cf5000aa7661b3b7ef6af6ce87ede82e Apalache Variable Domain True Passed
fc6322cec14b452e58909ae13760653a0f8c78d1 Apalache Variable Domain False Passed
4535a1430129d5284f5479f4ef5478f3aa7beeaa Apalache Variable Union True Passed
59cde515ceccf945193baacbbad0340a11aa3d6c Apalache Variable Union False Passed
d7e47a9a65da7582e4474b6ab50953987c4bbf24 Apalache Variable Unchanged True Passed
0a778f723b0aab9bb385d07c223a5f56e6a90c41 Apalache Variable Unchanged False Passed
de053681a61daed488b06cdec04cd9f3b654a115 Apalache Variable Equivalence True Passed
6147dcdabbe3c9643cf706bae765201b8adcb532 Apalache Variable Equivalence False Passed
5cc79075a76afee39e6140133ee8980be97158fb Apalache Variable StringEmpty True Passed
e08a236c2ae1223f93ba972aee457e413e6eb55f Apalache Variable StringEmpty False Passed
f779d972260603c0c5fee2ed1cd20724c4e04946 Apalache Variable String True Passed
7beb3061237ea1101228243862a00f3fbeea27cb Apalache Variable String False Passed
3b52544e3856149af47e8aa553b60aa31e52311a Apalache Variable SeqLen True Passed
c91432dfde1a0ad852600750e2cc3a5fa8aaa49b Apalache Variable SeqLen False Passed
a4aaa8771973357e394fb75d1d9edaec66196a29 Apalache Variable SeqConcat True Passed
b170c07fcdf4cf6a5be61dd0731c8a6528644e06 Apalache Variable SeqConcat False Passed
9b1d42aa6be75762f1024fdb0b9086c35e247a5b Apalache Variable SeqSelectSeq True Passed
fc83f55d4016f5f6ace639dde98a4fc50fd8ff01 Apalache Variable SeqSelectSeq False Passed
c372de507f484807481b36a95b9ca6c4ab519c28 Apalache Variable SeqSubSeq True Passed
290915a55da39a23ee130dfaefecedfeea941fd7 Apalache Variable SeqSubSeq False Passed
ee83f20fd57fd6a5690b02c5e346647ecfe00318 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
Variable NumRange True Passed
4befae1f3299999c59a7c9727baa3edb3c9f88e9 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
Variable NumRange False Passed
eb38218600c4f661c6cdb38e9d5ee8b0b8ffde32 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Variable TlcSingletonFun True Passed
b6754d547937784874f059f6c7739d7bfa092534 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Variable TlcSingletonFun False Passed
20df195daebbb1f4fdeb37868178f58ec721fe19 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]]
Variable TlcExtendFun True Passed
087cfe26df2b5d0cf167f95ac4fab92276b7835d 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]]
Variable TlcExtendFun False Passed
301487d6b829e8d81c22df0224bb431ca76ddc72 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Variable TlcPermuteFun True Passed
75638a75f1d7c6e248a3a63165f3322073257642 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Variable TlcPermuteFun False Passed
8198b238a6068cae2196ffb339923fe9456d9255 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Variable TlcSortSeq True Passed
dd247ce1253c07764516304f07d53b15f5fababe TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Variable TlcSortSeq False Passed
b1e302d1c4e3d3f49f2ed4049628fb0ff1eb843a TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Variable TlcEval True Passed
db99b6fd288c92474148b85114ba8f9b0d58da62 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Variable TlcEval False Passed
c10d007c75edd273aea8a8ddf2c6571f1d7ff804 Apalache Variable BagBagToSet True Passed
954d3cd0d6e140e4d1997c4213ecd7a8f8eba241 Apalache Variable BagBagToSet False Passed
29305cd2f3ec7fbe400690e4fc9f19d57b814ef5 Apalache Variable BagSetToBag True Passed
77b421a978134b8e602bacebd91b544fa9bf9162 Apalache Variable BagSetToBag False Passed
808a627d7767dd92eb010de2691ea339a731e05d Apalache Variable BagBagIn True Passed
a9626aa5b7aee52309e8128c6a86303025d9a2df Apalache Variable BagBagIn False Passed
751a61f10df4b89345135d022e13edcb951830d4 Apalache Variable BagEmptyBag True Passed
7f2dc1399c2403c5758512a7386b91b5ba014453 Apalache Variable BagEmptyBag False Passed
1003acb66f30064891be98228689f9c2ff382d0a Apalache Variable BagAddBag True Passed
b53839f7c3a08947789b3331787ed5fbe0fa025e Apalache Variable BagAddBag False Passed
1fa666e9b98af3c6bb67e4bcbc28a83d69efb901 Apalache Variable BagBagSub True Passed
c5e5bb478fcbf96c5cd59ea114b3c7f8fee43999 Apalache Variable BagBagSub False Passed
c93e10768399b57fffddf729ab6830e1b8816c71 Apalache Variable BagCopiesIn True Passed
1927f43a9337aab927d103b33b1b2e619b08af78 Apalache Variable BagCopiesIn False Passed
27a2baeb29735ade089c05cbf9423a238179fe97 Apalache Variable BagSubsetEqBag True Passed
53c88fbd79e88e872596d8b063c87335697d9137 Apalache Variable BagSubsetEqBag False Passed
cb2fd141034e7d106d423ffbdfe11fc492715a79 Apalache Variable BagBagUnion True Passed
18a3a6416e7cf23d8e0690eafb814626aa224154 Apalache Variable BagBagUnion False Passed
4c3f24ddeaf03d8a8bd6ce900defaa512a4b2ee4 Apalache Variable BagBagCardinality True Passed
2242331a70147324fe996293027c7fa717e2d8bd Apalache Variable BagBagCardinality False Passed
70b6e93d75d5da89bb39b44140c6586a83e3db45 Apalache Variable BagBagOfAll True Passed
e62a761b8b707827a665ba6e542afddc6f34b8d2 Apalache Variable BagBagOfAll False Passed
e1920c174aab3ca2346eefbc3e1309b3e86a74da TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Variable BagSubBag True Passed
ee9e54d3a1a0f881fe6e2b9804a8c9d7552d1979 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Variable BagSubBag False Passed
9dd563bb65a447eebb78863d8c628de6001058c9 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)
Variable FiniteSetsIsFiniteSet True Passed
8628c5ef91f88a8661eb6ff295db45c6893d3d3f 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)
Variable FiniteSetsIsFiniteSet False Passed
b0ba1fe86da67c5674270b57c69dcc4c0ec9fd2d Apalache Variable FiniteSetsCardinality True Passed
86b56ddb2ff3b1f045b0aea44a33a6d0dd830fca Apalache Variable FiniteSetsCardinality False Passed
da3bdd9bc8655dd66343efc13af4723e6467c696 Apalache Variable SeqHead True Passed
ed7c4bc0d84726a2e945fc4b5024500fb07f89c1 Apalache Variable SeqHead False Passed
79f393b8da8d6af59b3bd053ba0d7b79b77d4da1 Apalache Variable SeqTail True Passed
335668ea5e7c56b604b7c3aaf15d56e16f29a829 Apalache Variable SeqTail False Passed
eee8d174c27c15d3e2c13e9eba0dfa7dff23201e Apalache Variable SeqAppend True Passed
e695c95dd4f4e9cde6408aac71799196e0f45184 Apalache Variable SeqAppend False Passed