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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
421d7ef2247747f6fa1597a872e1b320a6571aec	Apalache	Eq	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
d727f8d352e46a01545bfd139593af26421b935f	Apalache	Eq	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
5f2ffc75c0c81fbe341f97f908bccd38576c80ee	Apalache	Ne	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
7919ec292e1542b2c3657ea7885598413717fc9d	Apalache	Ne	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
1e39c54b38f1c210bc3101339d64b314c5d18f49	Apalache	Let	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
51d70c1739dd3421d454d9114f48fe62c8cd2a97	Apalache	Let	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
68cbb81b3ad0c30d5248c1616062c3e011275d1e	Apalache	Set0	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
4e002e12008613e9b17117b896514967f812c559	Apalache	Set0	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
0cac0988b1f4ab31acaa36deec922c1d08ab894b	Apalache	Set1	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
2fbed502e3a08f549f40ecccd11060cb44e669e4	Apalache	Set1	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
abbdb2942fc76771f13103e96ffc295cf59a5012	Apalache	Set2	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
8954901a667a886fa710ae0ce2f0091dc965e3a5	Apalache	Set2	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
f6bd439878d71cafc47e8a5942d93b4628f37b14	Apalache	Fun	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
4bcdf9d5ef58daf3ba13b8e981d4be1377cbe7a7	Apalache	Fun	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
724ec77b75a4b3d3d7462a19c3ef687639a892f5	Apalache	In	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
bacfd70f3ff9f773a48b1cbeb5de4d2bbfcdd39d	Apalache	In	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
a29d04f73297207de9abbd7ca32905a1d10f4502	Apalache	NotIn	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
7e1e9f6b3047d8a460958e22d3b45d2ac8751daf	Apalache	NotIn	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
2d733567f63c274693dcbc943c6f5228c24ac703	Apalache	Record	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
589fb971ad004f577e0418a56bfd387a8bbb0631	Apalache	Record	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
4d09ed4ae74e943d542a8b1a921103fd672539a4	Apalache	Tuple	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
da03cafd367f828bc3a1680c6bbbb236db5cd7ea	Apalache	Tuple	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
5b4da5bef082c27e97fb078d516873e7925563d7	Apalache	FunApp	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
01f1ea86fd7813ffcda2d8bf6acdfdd40a58730c	Apalache	FunApp	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
811966a2c47c4a91a6a3dcdab620f25cdc55d1aa	Apalache	Except1Fun	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
713e40f1da4960fa1db74848b47f290aa91ece84	Apalache	Except1Fun	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
239e980f395344e08d25976003b525675ef72057	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
fdc21a524f48c89d9f6c220e6d9e6223d63bc8ed	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
ad3c745b6b00fb585ff3360c8a52400d7adbf705	Apalache	Except1Rec	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
f4981e4a7614412ca9e44187ba5b9d4f0a9c36f0	Apalache	Except1Rec	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
2b9b69a299b7282069ff27101c0c361ac067a559	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
ce8699241043a1e23f4d3f2dcfe01b9c582a2f8b	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
12f96ecc2c0ef5f04e77ef0cfa7584176a176520	Apalache	Except2Fun	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
8c93eac6fd943e48a87e7a152d1403b864afa847	Apalache	Except2Fun	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
11a447bea9b8df48ab88fdc1d16418f23837425c	Apalache	Prime	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
5a1a8e03ff1988731354026af5dbef5fbdb6c5f9	Apalache	Prime	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
0a8d03fcb25e727f4c614d63fcf41937fe893e5b	Apalache	NumUnaryMinus	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
cb125b4d590e0bf3851d62c958d1f00e4e91f67f	Apalache	NumUnaryMinus	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
38790b93fcde8f20b1d563a85c67bc145581edd6	Apalache	NumPlus	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
dbb452f0a0305a4e2b1da6756e6e305c1a7d4b47	Apalache	NumPlus	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
5d1fdd6aa3bd5c29be8aa6a6c4ed31b7850db614	Apalache	NumMinus	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
678e68828e038e6baa7ffd9c29d43e52c2351fa3	Apalache	NumMinus	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
e7c92f3135962f3b4e2713727d5b8912885aaa24	Apalache	NumMul	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
9b42a0536de22553f94a57a185d45ef7f26b1e20	Apalache	NumMul	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
79f6900fbdb9154d2f46b9f4619ff87011249a76	Apalache	NumDiv	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
8c6c056ea21a0cc0aca42d8655a77bbf5015056b	Apalache	NumDiv	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
e3e90c6a94f754bfc493774e22bdaaab067e9637	Apalache	NumMod	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
7d24f8b4285cd5ef016c484abc35029fe8c40932	Apalache	NumMod	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
a50dfd276946f18e195cb41456ee58705f74974b	Apalache	NumPow	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
aa1189f0a213a57dc032c5271acfc275be3a2989	Apalache	NumPow	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
4c19e5074b0934ac93aa385bebd1aed7c952f0b8	Apalache	NumGt	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
090814785591e95ebafd04b922f5fb9d8ea849d9	Apalache	NumGt	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
85c049c297a90e69774cae317f8b523651316dc6	Apalache	NumGe	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
1dbf378c67f6dd8bad413a08c33d3f7bd68e4d23	Apalache	NumGe	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
4b3d6de118550102a915b5a91368de0b23d9094e	Apalache	NumLt	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
d4a4d0be8035345045dd148819a7ccfec822f1b1	Apalache	NumLt	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
a9d134253d890d4ea8bea34ea28dbd16170969ef	Apalache	NumLe	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
7f9df94aa34ffda458ab884bf01866f3674393e9	Apalache	NumLe	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
a773a91315683b3f8b3612f695441e4b74115196	Apalache	DefFun	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
79b59ff6d5cd94cb8abeeffaa9b28ca8cba38c8c	Apalache	DefFun	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
4348ad8772e8fab211ce6a38fb90915f466707e7	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
b5f30a142a0c1f4465cc90857519d32760ef48fd	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
d4062254342a41dead8441eb270a433741f63b69	Apalache	DefFunRecursive	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
328ac07c48722984c6ca0fd30602a7a3f0b83736	Apalache	DefFunRecursive	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
34c33b5fc3ba79672541989d8b9a7a457f33c514	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
874f366514ad453aa4499d5b90cb26f7246fc009	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
d3c011bb46c57cc177ee95e34879e27b1a7c9035	Apalache	Def0	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
1d04d9b1669f3e43b62e852bcbe9087aecac3925	Apalache	Def0	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
886f3ee3ca2183797c2146a0c9b956cf152df58b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
02567ec778d8f82030dc554d9ee7aab9a057858c	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
8d7c63a76bb49e5308f000d7c8a7b47887ffa122	Apalache	Def1	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
ea93565d5ee7cdd29314748ea9b38a216fe3b8b0	Apalache	Def1	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
5667e7be0ea4f9428721e72a601e1d42efdc9399	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
37f7919f92f0ea1983d276d73cea8c7a3f4b76f2	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
bf3ff4e456d50185c5cf0f31c634f3cd14be5de2	Apalache	Def2	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
a63539ff92a3c29e91d00f59ad61bf6fa7d0d279	Apalache	Def2	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
7b80498de02c943a5975477948258984c9ce6713	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
973363af56eab48fc38bfc7a4cedd553d5d16602	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
101c5149b0cc557afc286001a5ab3760737832f2	Apalache	Def1Recursive	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
59f3d81a04e4e4f531bed54ac43a09213771d783	Apalache	Def1Recursive	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
1ad424329aba3b789cfa570d7d79b441b0cf347a	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
a673fd9de319b65d9a063ebfc3692418586c9341	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
cf49aaac889c1bd56be3a56456a546214f5d3dd0	Apalache	Extends	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
29f7512890e8c87e405547233a5baba3426ff0fb	Apalache	Extends	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
126b633a8e012a4011dce9a96f72bb5ec8ae9d57	Apalache	ExtendsInDifferentFolder	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
8d185a3848235313f72732cc2670c31e35064a73	Apalache	ExtendsInDifferentFolder	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
4c3f24ddeaf03d8a8bd6ce900defaa512a4b2ee4	Apalache	Variable	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
2242331a70147324fe996293027c7fa717e2d8bd	Apalache	Variable	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
64b755e3242f1c52c9aea303e572f7c8d90fd241	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
5638c726b8fa0572040311894fe01b5169d1b8ab	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
1644986eeed9a332b1c5ddfa1b2ebbed7322adca	Apalache	Constant	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
ec769e1e8401fcc95320e805f692ab5c6a15cc9d	Apalache	Constant	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
dee5a636628eeea259793993e68902f5df9a7790	Apalache	ConstantRank1	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
26a79f2b46484d1aa07cd1e4c743f6f15e06c85c	Apalache	ConstantRank1	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
e93368e62a1778829b8017d234b617eeff492728	Apalache	Instance	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
32a0714aa05f2bd10ed6073a1ee58443ee4d4266	Apalache	Instance	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
7968786e1cb073a01514f71ca82acbbcd3294b15	Apalache	InstanceWith	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
1de3c29a126d6ff8243da163e435493c773387a0	Apalache	InstanceWith	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
5be390854e63934acecec1eac1b1116384e6f757	Apalache	InstanceNamed	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
25a5854731c40e04edf6c48e4134964fe2f65838	Apalache	InstanceNamed	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
4b431d6c28d3a04f966a3478304eb5f28044ab79	Apalache	InstanceNamedWith	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
f3d7dc6863a0dd16dc524d43f2ebb16bcc25d9eb	Apalache	InstanceNamedWith	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
ed5cd936078858475e08d5016e90788d2ef06313	Apalache	InstanceInFolder	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
d1bdd00ae7e810a0f684232aabadfa569618b0eb	Apalache	InstanceInFolder	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
e5a2cf5769d86d9771e8d14bbad415c3a684fe58	Apalache	InstanceWithInFolder	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
05156e423c23c7792e35dbfee56327f18f03418c	Apalache	InstanceWithInFolder	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
516cae17b935e1edfc14091e4b7589a421b30f0f	Apalache	InstanceNamedInFolder	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
650bdcced66a4836574e838c0998301afb8a6f6e	Apalache	InstanceNamedInFolder	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
4cf186baa6e2c4d28fd6f71799c78d8a04d18f6a	Apalache	InstanceNamedWithInFolder	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
680829a1c592f37cef10a3f535fc12f607d5ff9d	Apalache	InstanceNamedWithInFolder	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
d2502e6d696e5f69b2c905dca189dfeb7c6ad259	Apalache	Lambda	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
12cca94b33ef81e3d045cee8bd2285b6309a057f	Apalache	Lambda	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
e65ecd5cfaf91020dbcd9b699a34a72c544a54f4	Apalache	IfThen	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
8e03a4ca99a108bd27e1bacf34561fd0f27a628d	Apalache	IfThen	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
c22585e3798855b493f135e6024b98687af2d6d9	Apalache	IfElse	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
810e497ef22193721bfd10389527ac58d8a5d17e	Apalache	IfElse	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
965dc40492d8c5063c701b46463cef5159a9531e	Apalache	Unchanged	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
fcb29ccb383331b23c5ca7e1f39aec4a0400c196	Apalache	Unchanged	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
7149c3fce30b4e7f1113fa456e68f9f91da8b634	Apalache	SeqSubSeq	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
7836a91f9e124b7bea77d0aad9c7cd8eaf8f7da9	Apalache	SeqSubSeq	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
7e24606fd5ededf54c338c22d275e963a65aea0a	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	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
f3adec253491cf9d53d2b410944af4b5bfcafe39	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	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
8a7d051096531b11e8a748048dc53b33013693cd	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
65d9d63f69d9378ab2a5ee5edaba71043cd18352	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
50e08a870a5599aec22fa77894463937883cec30	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
2c5299c6337ea609c5e608eb4a16b85f9fea6e8c	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
d3c333b64f339f2badc57966d235630335651c5f	Apalache	BagBagIn	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
576b7c85e3f215a48928f7003ddf0bae5b51b471	Apalache	BagBagIn	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
6ff02df167f76debce07d6446a7a6af3746462d2	Apalache	BagCopiesIn	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
05bd89c325349cfb429367e483236db1baf52f61	Apalache	BagCopiesIn	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
3da2152f8b5eb2d13101822fb1ef5115975f3395	Apalache	SeqAppend	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
3047795734e383a4caa3f87b39b7865fde69eb07	Apalache	SeqAppend	BagBagCardinality	False	Passed	Model Under Test Equivalent Model

Index

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