Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
ec65a3d33fa36e9652ce723cfc3e5b191a7bc52e Apalache BagCopiesIn BoolTrue True Passed
0d6afb8104f8809e4a4a786b33afd44ae5391c5d Apalache BagCopiesIn BoolTrue False Passed
8d7bcb754c0e6494f62b59dfa1b42b451268d5de Apalache BagCopiesIn BoolFalse True Passed
8d03ceffb86f40cfcac4d718acd3a80e5a00e92b Apalache BagCopiesIn BoolFalse False Passed
2d868dbbcacca010a29169005c96834744b142e1 Apalache BagCopiesIn BoolSet True Passed
8cafa06c3632e434672736fce468de4adfb76a98 Apalache BagCopiesIn BoolSet False Passed
3a82d9cfdf5accabf28a6c47fb850f032c4602d7 Apalache BagCopiesIn And True Passed
2e1a96ab326afdb8b63f3edec07f221e89ec6da8 Apalache BagCopiesIn And False Passed
78dee6ce2bfe819f1b024fbf31ddc4767694ec99 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
BagCopiesIn AndMultiLine True Passed
d9ac6991a4529d55931ae01e59d6276f780c296d TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
BagCopiesIn AndMultiLine False Passed
af182b08ccc1b113045e813baf5bb3237071bb95 Apalache BagCopiesIn Imply True Passed
965816fe065f63e753c10924daf1eee9a53b0a28 Apalache BagCopiesIn Imply False Passed
1169e03b27b98bbecdf0c7c942fe590ca1718650 Apalache BagCopiesIn Not True Passed
db90cea1225a3790afd75c30373d263bbd84d21e Apalache BagCopiesIn Not False Passed
722e4d2697d7de57edd217c16c552c0244b2338c TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
BagCopiesIn Or True Passed
6715336ea8c6932cd8d999ed3a113f505313daa7 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
BagCopiesIn Or False Passed
761d77474cdb8685708bbdb6175781801859686e TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
BagCopiesIn OrMultiLine True Passed
085ddc5d9e80666d2f0b2286071abe234e82131d TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
BagCopiesIn OrMultiLine False Passed
e51e67d891739c5bd4383133199c7ec7b40f031c Apalache BagCopiesIn Eq True Passed
42773645b71a928d5bc7d5395229a9b98d3e8510 Apalache BagCopiesIn Eq False Passed
b6866b7df81bec51ad134cc3cd4a960722f6b650 Apalache BagCopiesIn Ne True Passed
c875e6b543b2007073695a0421d60f88ebc892cf Apalache BagCopiesIn Ne False Passed
dd06f89571a7bb26781a18012e2424f27186e50d Apalache BagCopiesIn Let True Passed
608e429a39c4c056f5423e21c114cc88b5f90a79 Apalache BagCopiesIn Let False Passed
43bd0b074131a28f5cb4e0f1fc8d0dfe2afaf75f Apalache BagCopiesIn SetEmpty True Passed
327a2ff10154688d2a89144e3f3cfc5e810dfa54 Apalache BagCopiesIn SetEmpty False Passed
9475c853ca51d7e90836a24e1cbaa948f86ee9f9 Apalache BagCopiesIn Set0 True Passed
2046c7839c61a99d16bb8616b025076300879189 Apalache BagCopiesIn Set0 False Passed
d4a6455baaef4269b33ea0c2b443824658377e18 Apalache BagCopiesIn Set1 True Passed
4b79093d89016ad3d5f43247ce52dd15f0035ea8 Apalache BagCopiesIn Set1 False Passed
79668250b8ac79f6ef785994b82da5228caff788 Apalache BagCopiesIn Set2 True Passed
3d53272c51c6b1931122621f9c4c5c498c113b94 Apalache BagCopiesIn Set2 False Passed
d160b61ef5542c04d281a122a7497ace9684b5b5 Apalache BagCopiesIn Fun True Passed
fc2dcfed35857d166ed5909733f9eb9e65440fce Apalache BagCopiesIn Fun False Passed
830ecd07a32098af9df98ecccd8dbae164634f22 Apalache BagCopiesIn In True Passed
e2735497b5f3bc31afa252dd4da1cb560b986c0b Apalache BagCopiesIn In False Passed
6ff1380f6ccf78ea9aaada46429509318c46cb07 Apalache BagCopiesIn NotIn True Passed
c9f8edb56d94b27490be53520b0e36571cbb3f11 Apalache BagCopiesIn NotIn False Passed
b43eb8152fd3ea55ac44d95c0f08761f59dabce9 Apalache BagCopiesIn Exists True Passed
92787ffd3eeac7ba3337057ab4bb0a51e74f97cb Apalache BagCopiesIn Exists False Passed
4b53c3ab2d6357e699cf8e6e162cd6e2980e7b23 Apalache BagCopiesIn Forall True Passed
b4169eaa2a7e00cf51202eaa16571d1e0b893688 Apalache BagCopiesIn Forall False Passed
791fe90e9483f2f7c4159fd0a6633e3b20d34ea7 Apalache BagCopiesIn Choose True Passed
89dfdca03d883084e4b003aee35bc736507069a7 Apalache BagCopiesIn Choose False Passed
754fcb8fbb2a61d87a0be929be062ec88dcc32a2 Apalache BagCopiesIn Record True Passed
e515311532f73e6fb7b810fedd267fe9382a413a Apalache BagCopiesIn Record False Passed
1002a8df762d636feec4b13ccaee1a5177d272f2 Apalache BagCopiesIn Tuple True Passed
dfb0ab0d24f3bcae6c7f19d41a170ec236a7ad3e Apalache BagCopiesIn Tuple False Passed
fbc8648f55a5d8f85a6bdd3b04d6849f9b8aad47 Apalache BagCopiesIn TupleEmpty True Passed
aecd7d68091f02a33e2a53e5f7fa5d38e9f99e87 Apalache BagCopiesIn TupleEmpty False Passed
c527780735c501397962aeea1099213bd005c679 Apalache BagCopiesIn FunApp True Passed
132c3cc01502f7f9d2daf955967181e22012b655 Apalache BagCopiesIn FunApp False Passed
8fd41b6e52b97610e4b1e3d4fb671cfdf04d7828 Apalache BagCopiesIn Prime True Passed
3d93e0c452ba5649d8923ea5d76c9e19bc307451 Apalache BagCopiesIn Prime False Passed
5066eb5f262ed1fd89bdc0f583e920d9f9bb8fa3 Apalache BagCopiesIn NumZero True Passed
a2f2ae232cd328d3cafdb12ee75165ce63936257 Apalache BagCopiesIn NumZero False Passed
e84c62255bbde8825f7dc74fc79f8b6d7856fc18 Apalache BagCopiesIn NumOne True Passed
0e0f3b46ef92aa775c88ace0e1983c655c3550b9 Apalache BagCopiesIn NumOne False Passed
49129014f18cedd1ac8cd4b99deb533dee50268c Apalache BagCopiesIn NumMaxInt True Passed
17302d00b1b3ae07cbdf18d852c1efc7dd4eb890 Apalache BagCopiesIn NumMaxInt False Passed
dc47072e9a5d0c53f7805c827839f5272b3bce78 Apalache BagCopiesIn NumUnaryMinus True Passed
7c591b6eb92a29f89e5480e5592d5a19d73ed500 Apalache BagCopiesIn NumUnaryMinus False Passed
dacd59d802b3f01c9b9c91381388f1b303b770d4 Apalache BagCopiesIn NumPlus True Passed
645c9049bff29ea4c502a174ec599dba71d25e6e Apalache BagCopiesIn NumPlus False Passed
0b203c7ec97ff6af07f1fc15cb70274042d45f6b Apalache BagCopiesIn NumMinus True Passed
a718a0ad1ed1efd1ee16049a7c394ab822104f31 Apalache BagCopiesIn NumMinus False Passed
5175a2429f0d31886f8bea3cc5cd689961f1f33b Apalache BagCopiesIn NumMul True Passed
103596a67c37e92cc9062cc2197448d5586520eb Apalache BagCopiesIn NumMul False Passed
953b369a04a1beae9702a444036d72a575f42e69 Apalache BagCopiesIn NumDiv True Passed
3d13a0d53f50d3722af338b2b03ef215f227033d Apalache BagCopiesIn NumDiv False Passed
2dd86e93b41db3fff110085ee54d3d3cffe4610c Apalache BagCopiesIn NumMod True Passed
d7dec039060f36405ca70c7e24bd86120c4e6cda Apalache BagCopiesIn NumMod False Passed
bc77c97d4a1265166ea5fc55675eced5aced28df Apalache BagCopiesIn NumPow True Passed
b72199cfc670dbf3ad2bce3d1004628edc11ff25 Apalache BagCopiesIn NumPow False Passed
7a2f5696ca1a250fada82d4e5c83392bb153e283 Apalache BagCopiesIn NumGt True Passed
c34230f4b3a682f02f9d8150331c9f494ab873cf Apalache BagCopiesIn NumGt False Passed
db8997d8fca980e10f1519028ef96c1b910416f6 Apalache BagCopiesIn NumGe True Passed
2b2dc5b1512f53ac8218182c0d76856a8aa32931 Apalache BagCopiesIn NumGe False Passed
59bcf38d1cbfba6a150b6ecb967d59e0c31fc6c8 Apalache BagCopiesIn NumLt True Passed
2480c6198ef885d259f22d55b9b21a86085a0a83 Apalache BagCopiesIn NumLt False Passed
18a68265094bce70008cd091474ce7bfb1091096 Apalache BagCopiesIn NumLe True Passed
b58c9d0389b09a868261e971ecc988b8dd7bbab6 Apalache BagCopiesIn NumLe False Passed
88daaaf0d0f6c02befb4d28b8204aeb99b446ae9 Apalache BagCopiesIn DefFun True Passed
c6df6a44c549eea9dba2afeb8aa517a994ad5416 Apalache BagCopiesIn DefFun False Passed
8965c1d6ad1f1e75e62e723ab53b33e85dc0f086 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagCopiesIn LetDefFun True Passed
d88a88c03b682c2dd9cc738b38c6d6cfe31de539 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagCopiesIn LetDefFun False Passed
87dfd319b5c7b40396e7bddd4c665065e4ae0010 Apalache BagCopiesIn DefFunRecursive True Passed
651f4a6d02ec7619bf8cd271b4232460af61b1c3 Apalache BagCopiesIn DefFunRecursive False Passed
50913b6d5f35fcf1e31ee6bef92a38d74d45a87d TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagCopiesIn LetDefFunRecursive True Passed
bb78e9d6ebd2523cd8600a7c2eefa564d2147f29 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagCopiesIn LetDefFunRecursive False Passed
a25754b86422c8242f0fee263d970dcbe0f1ff37 Apalache BagCopiesIn Def0 True Passed
2817e27b38b522238e4add041976330bb85247a7 Apalache BagCopiesIn Def0 False Passed
ec8a1b540ccf3add5894a120777f6b36f5b362f0 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagCopiesIn LetDef0 True Passed
d60e267dee738dc3dd46e84967ea831e2526dd55 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagCopiesIn LetDef0 False Passed
3f687bd4a13259edf54131dd5a2c592b0f74018b Apalache BagCopiesIn Def1 True Passed
3b3db5746e3f19723a63733372be65a4f495f690 Apalache BagCopiesIn Def1 False Passed
82282a7e91569de6f9805d4d5ed41b85fbed37cd TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagCopiesIn LetDef1 True Passed
46f637d1d6c14d2493985f13a54d0e0850eafadb TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagCopiesIn LetDef1 False Passed
4d1dfa6c0d4380414fa56414f79eab8c07fd2943 Apalache BagCopiesIn Def2 True Passed
57d807ac5e3869bb52c59f1c28a99c1c3f8dae20 Apalache BagCopiesIn Def2 False Passed
3e06ab9afdb162a5e7276c37cc2befb0b3b957a5 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagCopiesIn LetDef2 True Passed
adb63d78295f32cd9eacbae8e6410c94ee69eee6 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagCopiesIn LetDef2 False Passed
f496a23e7470916c577de4b377a269ac8d286b6d Apalache BagCopiesIn Def1Recursive True Passed
9315ad91c045501d95d1738110e5993b72a172a5 Apalache BagCopiesIn Def1Recursive False Passed
5adb859c88e8ad263d6d3b90af739947fa8aa9b1 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagCopiesIn LetDef1Recursive True Passed
b0fb087f2d6ab1b8935e9d045ac91abb91fa98b7 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
BagCopiesIn LetDef1Recursive False Passed
5f0e5981d2f0cbc328bb16053787edf936315177 Apalache BagCopiesIn Extends True Passed
9f722718ea6c0c4ec1cec8a4bbbb2eab20fa33ea Apalache BagCopiesIn Extends False Passed
c5f2766d6ffade35db3f399956d9c90ed2d906f2 Apalache BagCopiesIn ExtendsInDifferentFolder True Passed
9ced19d1af49eb6dac4cbeea75afe0dbb0d0e2b6 Apalache BagCopiesIn ExtendsInDifferentFolder False Passed
19982dd3f3bbe49e6f9997da8583553f53532dbb Apalache BagCopiesIn Variable True Passed
c34461ef9eba35b2971803560038cf625bb7bdcc Apalache BagCopiesIn Variable False Passed
c3d2edb952172246e5ea5b1f32a81d1cb05ca4f7 Apalache BagCopiesIn Constant True Passed
403afdaf9e85aa88d03515a2527cfbd965bf5842 Apalache BagCopiesIn Constant False Passed
f34adaa74819d3488d298413ef823ad5e8c25bf2 Apalache BagCopiesIn ConstantRank1 True Passed
6bc2d828549a21ad2f510cc8f8a43634f43baf73 Apalache BagCopiesIn ConstantRank1 False Passed
4d7c0da52dd94b8d62bcea236c4077f91b1fd8f8 Apalache BagCopiesIn Instance True Passed
cfd2bf1155b84558b00e06885609b82b80464813 Apalache BagCopiesIn Instance False Passed
0c97877c70881da257b183c0fc65c96a443f7d39 Apalache BagCopiesIn InstanceWith True Passed
1c64f88d80905802564d11544944177507547f2e Apalache BagCopiesIn InstanceWith False Passed
d14efc8fbe0cbc57bf7d08c87d75d645aecef084 Apalache BagCopiesIn InstanceNamed True Passed
e6a79687ea39095ccd49eba78d7d0dce1134cdf6 Apalache BagCopiesIn InstanceNamed False Passed
124df8786197a189015c3ec21d27ef08c07b6c89 Apalache BagCopiesIn InstanceNamedWith True Passed
4d0afcf0ccd5f3770dae3f26a79123ed1fefdd94 Apalache BagCopiesIn InstanceNamedWith False Passed
9e9f378ae7eca07990804401e983dc49c386a7da Apalache BagCopiesIn InstanceInFolder True Passed
f5be4877d76947989e1bc3eedd49b6a345a95871 Apalache BagCopiesIn InstanceInFolder False Passed
9dd337971dcd2e24043eb8d57715bd780f8d0cb4 Apalache BagCopiesIn InstanceWithInFolder True Passed
a8c38a330cff997f16d79ccce2df5b29824a3d23 Apalache BagCopiesIn InstanceWithInFolder False Passed
94e36b8c69a016cfb114107a9120548c6b973f28 Apalache BagCopiesIn InstanceNamedInFolder True Passed
9e7e95d49fccd285dff3ab93c72cb3c164662a09 Apalache BagCopiesIn InstanceNamedInFolder False Passed
d66eb2e507d4de435f4d110be3fbbc397955ec76 Apalache BagCopiesIn InstanceNamedWithInFolder True Passed
94a5371e66834fe55cfaae4e8b30903a150e1b8d Apalache BagCopiesIn InstanceNamedWithInFolder False Passed
1e5c678abc2ccf994fcb78126d47917be1def97b Apalache BagCopiesIn Enabled True Passed
22322f9b29aea600301f18fee459d64a2ab151bf Apalache BagCopiesIn Enabled False Passed
9f4ad3704bbed4a1f92f766050fd58f7f5b30d9e Apalache BagCopiesIn Cross2 True Passed
9c34d873f8872cec0c7fe8d304892a3c9b04ba2e Apalache BagCopiesIn Cross2 False Passed
f323229ddd342866daba2bc2fc30faebf9d5ec36 Apalache BagCopiesIn Cross3 True Passed
b061f0e1eab43908db2c12e7ee97217e08e0eb81 Apalache BagCopiesIn Cross3 False Passed
6335099ccd5a043d3be1da3dd49ed49213ac5e2e 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))
BagCopiesIn FunSet True Passed
fc219987149ed3c84fd523f59152b8ea0ffc9154 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))
BagCopiesIn FunSet False Passed
9cdbd71f2ea720e9722aee253d0770dc46fb4e09 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)
BagCopiesIn RecordSet True Passed
d5d108a08331acfea0f89bb1b74ec86db282c99f 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)
BagCopiesIn RecordSet False Passed
010178edd971f947b5ce135150b0c37d6ca68c2c Apalache BagCopiesIn SetDiff True Passed
d9256cb8c3bdd39a7376885a30d6669a7335e0a7 Apalache BagCopiesIn SetDiff False Passed
0f746aaa6b16e050296ddfa7fa7fd534be16bae4 Apalache BagCopiesIn SetUnion True Passed
68f9090e3fd59715b5a2a90e5ce229da90462f24 Apalache BagCopiesIn SetUnion False Passed
067fcf6465bb0f6ea9314840dcd7f3ac9f159307 Apalache BagCopiesIn SetIntersect True Passed
24fc965fa0c972ee519f4180b831223156b9ec24 Apalache BagCopiesIn SetIntersect False Passed
51e2a3bf3f83336a838d5b8e28909c4e9750bcce Apalache BagCopiesIn SubsetEq True Passed
5e6fb77fa9d409153f881d10e79bfc16c5547075 Apalache BagCopiesIn SubsetEq False Passed
64e84d862cdf200adf50882a18175b1170e2e1d7 Apalache BagCopiesIn IfCond True Passed
3340b46b19064cc549d33367fa4cb4d8fbea40c2 Apalache BagCopiesIn IfCond False Passed
8214d61640649851eb68d03881f7490635b1b118 Apalache BagCopiesIn IfThen True Passed
a288ecad7d590b7af714c53efea251434c6e9689 Apalache BagCopiesIn IfThen False Passed
64b1e63d26fa6f038e9ae54b23e5cd75bf40eb12 Apalache BagCopiesIn IfElse True Passed
3b03be7350b8092c53a7a06e9d71ce6fc15650c8 Apalache BagCopiesIn IfElse False Passed
37e9c39aeeee048ddf741307d268c67a25924431 Apalache BagCopiesIn Subset True Passed
ae0496c2c7728c771ce55f94648bcab7813a8156 Apalache BagCopiesIn Subset False Passed
158e1bb9298e8aca03107539c6e447ab6eee8779 Apalache BagCopiesIn Domain True Passed
c627d3091c15abd341b43da003cc590353d93e7a Apalache BagCopiesIn Domain False Passed
6cd2c419ce199eba5c2ba85146b95493cf18c1a4 Apalache BagCopiesIn Union True Passed
ca003a15f08ae1c0f59fce17dd5b27cc5f1df4dc Apalache BagCopiesIn Union False Passed
6dd5f2e81d606fafb5c19547fe8835c2fc8857ed Apalache BagCopiesIn Unchanged True Passed
aecf496aa551d07b8a1a4cfdb6ec839113362d9a Apalache BagCopiesIn Unchanged False Passed
c47b2e63586af1e6c821e326aa3d5d614108be74 Apalache BagCopiesIn Equivalence True Passed
60d600d20efd8aa8499fbf7b5f9e5f5fcc66b829 Apalache BagCopiesIn Equivalence False Passed
7b5828d4c57d84309deae05ec849464ce40cced9 Apalache BagCopiesIn StringEmpty True Passed
c755da72902a2752947d0f8ad11db6ec837b10db Apalache BagCopiesIn StringEmpty False Passed
55cbe3a94637d6a244c7879c3789b2bc701acfa4 Apalache BagCopiesIn String True Passed
1b2534c753806f8af528afcca79be1487c40bec3 Apalache BagCopiesIn String False Passed
1a6fefa205832080f90ea5dc3cbd60553d3fb1ed Apalache BagCopiesIn SeqLen True Passed
24f4ae86d2f0533b3adcaea6d63cf2a25a95d4f6 Apalache BagCopiesIn SeqLen False Passed
860f2a257ddadf77100e87713fcf90be4e6be456 Apalache BagCopiesIn SeqConcat True Passed
d63a6ce51a8521f2961b93bc9c6af9bb06ca2c25 Apalache BagCopiesIn SeqConcat False Passed
7bc86b360c40434cf594fcbf5bbe371175e8642c Apalache BagCopiesIn SeqSelectSeq True Passed
7fe35e46ca6a3441c618cb094071f6069ed4cb9e Apalache BagCopiesIn SeqSelectSeq False Passed
d97b603d7e6e211464bf024efdbccfae5e3aeb07 Apalache BagCopiesIn SeqSubSeq True Passed
b6dd34ebf54c2ff9c215ba86fa255a1e6eb7f83f Apalache BagCopiesIn SeqSubSeq False Passed
aca0add3e102218196e7d8674d4366856b6c30c6 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
BagCopiesIn NumRange True Passed
f7f9bd939f22e3d3e2199ab95813ed083a605337 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
BagCopiesIn NumRange False Passed
e178cfe7ec37acb26c994f1a350aba49fce6d08a TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
BagCopiesIn TlcSingletonFun True Passed
73ecacae094305bdf3f4bc4b630e1e2384129572 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
BagCopiesIn TlcSingletonFun False Passed
a9db3b955c9145268579e5c8b399d0cb63995202 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]]
BagCopiesIn TlcExtendFun True Passed
2cb9d5988534212b66f55663a52d1839067f7cbb 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]]
BagCopiesIn TlcExtendFun False Passed
0504becd7b691663b1dfbe5334446d7a0d8c3032 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
BagCopiesIn TlcPermuteFun True Passed
f6d6122d2fb046e17fe0dc54cf6fc5e2645360fb TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
BagCopiesIn TlcPermuteFun False Passed
487116da511b79b4df6daa7bdfd068c7d6701c11 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
BagCopiesIn TlcSortSeq True Passed
142a0b0370cb1f1fe4bd0e4147062181f5aa7a2d TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
BagCopiesIn TlcSortSeq False Passed
a524b277f4e52d96458cbd365906ee4c5d3c327b TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
BagCopiesIn TlcEval True Passed
8cb4e20d05400a508dd6e29078ae362d4ce55829 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
BagCopiesIn TlcEval False Passed
37618e89283d54113165153e66ab03f00e7e5d61 Apalache BagCopiesIn BagBagToSet True Passed
aacc8f3142c0fbd8e70fec6b0ac8caced655a656 Apalache BagCopiesIn BagBagToSet False Passed
ace6f427c74e7327a60ecc9ced1fb0993ce85f77 Apalache BagCopiesIn BagSetToBag True Passed
231de6979fc63d59c46594b5e1f2ac786be3b7dc Apalache BagCopiesIn BagSetToBag False Passed
169a6cab64268ef8b0c42340dcd355f3e43eb092 Apalache BagCopiesIn BagBagIn True Passed
c5972abf9176f0b7d20f076e3a3be7e168b7056e Apalache BagCopiesIn BagBagIn False Passed
7b2fb6e3c6bfb4715f11f14b80ca8e41540a6860 Apalache BagCopiesIn BagEmptyBag True Passed
1abcc0d5f1f5e0c5a82f45fb87301caf600c0568 Apalache BagCopiesIn BagEmptyBag False Passed
ff10050919c0a2fafef6ca91176410966a38db62 Apalache BagCopiesIn BagAddBag True Passed
ca154db16a8790924f484c66fc57241f36884ecd Apalache BagCopiesIn BagAddBag False Passed
d517e5ac78b76de28cd21af16ae3a8b7ce76e5f9 Apalache BagCopiesIn BagBagSub True Passed
644ee08f7a9739386c3c8f8d5cfa47b397594051 Apalache BagCopiesIn BagBagSub False Passed
248dd0bdfd4d1a8d65317ae39f5868e57dbb0607 Apalache BagCopiesIn BagCopiesIn True Passed
3d5e7aaf259e2f1f2cbbe7ba7fa6ef4326239ae2 Apalache BagCopiesIn BagCopiesIn False Passed
39096a4a891dba562befea5f63bd9317f5de5249 Apalache BagCopiesIn BagSubsetEqBag True Passed
955f1168b418a6c6d52f3875e627430f22ac3a38 Apalache BagCopiesIn BagSubsetEqBag False Passed
de68b5a14e19f4552667cd6b001abb684b0c1b8a Apalache BagCopiesIn BagBagUnion True Passed
0504b0e2c7c2c1a28053fa199307bd509b8d0600 Apalache BagCopiesIn BagBagUnion False Passed
6ff02df167f76debce07d6446a7a6af3746462d2 Apalache BagCopiesIn BagBagCardinality True Passed
05bd89c325349cfb429367e483236db1baf52f61 Apalache BagCopiesIn BagBagCardinality False Passed
8bdf992f15296589e3f0797cc776a2c91c9d3cc7 Apalache BagCopiesIn BagBagOfAll True Passed
82ff8f807bb712164585c3b01e7e645957fde280 Apalache BagCopiesIn BagBagOfAll False Passed
7ee189e2808d7b4c8b5019bc2eaaea6ddc21a924 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagCopiesIn BagSubBag True Passed
8e01f5bf3a8e5081fd4978a5bb44a784b2c6efce TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagCopiesIn BagSubBag False Passed
1f8d4632d9bf07598ecd06cac05a0674062b7223 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)
BagCopiesIn FiniteSetsIsFiniteSet True Passed
2bdb73f4efeba63a2bf6c868d9695b33bb89dde3 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)
BagCopiesIn FiniteSetsIsFiniteSet False Passed
c2b4e895f0d1da9b728b287fef6db3b63dc81126 Apalache BagCopiesIn FiniteSetsCardinality True Passed
73f046e7c9bacbea0db4d9b10412fa054edc5e29 Apalache BagCopiesIn FiniteSetsCardinality False Passed
2ed56604f22a37b2562d5a1020525609bc48bdaf Apalache BagCopiesIn SeqHead True Passed
345eb41ed90abddf0f789e8b38542d866ff63263 Apalache BagCopiesIn SeqHead False Passed
729b78b06674f78af88a2673e381762ecabc4296 Apalache BagCopiesIn SeqTail True Passed
8a59a936d229623297fe4709831f4718c4b37920 Apalache BagCopiesIn SeqTail False Passed
87aec7f9340ef0713dc2970f8b32cd9196992683 Apalache BagCopiesIn SeqAppend True Passed
6f03802da4baf4b4447024e528c5da1897f55784 Apalache BagCopiesIn SeqAppend False Passed