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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
b3c57f522af3095a0aa277488f4433f5faf43bba	Apalache	Eq	BagAddBag	True	Passed	Model Under Test Equivalent Model
6475e2f78eac85fd0150e5920f7569dfb1282495	Apalache	Eq	BagAddBag	False	Passed	Model Under Test Equivalent Model
62c0e5ba9bce4283db93f9d169688d0f0ff2b2c6	Apalache	Ne	BagAddBag	True	Passed	Model Under Test Equivalent Model
0c18bffa619bdf9f60cf84c6cbc614219ed6cd41	Apalache	Ne	BagAddBag	False	Passed	Model Under Test Equivalent Model
f0f402d524c72d2a7358609147c1786c12a28e94	Apalache	Let	BagAddBag	True	Passed	Model Under Test Equivalent Model
0bae3fa75bece1818bbf711094d21015064b9c18	Apalache	Let	BagAddBag	False	Passed	Model Under Test Equivalent Model
c1ccc5652abeb0908e354627bb5100eb6025ea49	Apalache	Set0	BagAddBag	True	Passed	Model Under Test Equivalent Model
ebec4dc5ee2e2c52252d7df2683c81399027c10e	Apalache	Set0	BagAddBag	False	Passed	Model Under Test Equivalent Model
994008ecda961f4099b38b89fda1ce3ce0172d72	Apalache	Set1	BagAddBag	True	Passed	Model Under Test Equivalent Model
4c28d1a34a40af972d936d4a312367665993b27a	Apalache	Set1	BagAddBag	False	Passed	Model Under Test Equivalent Model
1d1aee41449d508ddd6057fe467e27b1a503b727	Apalache	Set2	BagAddBag	True	Passed	Model Under Test Equivalent Model
2f25031558d677a488f75df75cb6376e35343c88	Apalache	Set2	BagAddBag	False	Passed	Model Under Test Equivalent Model
cdd2891c4df14c9d5fcb760935125aeedb6c1bde	Apalache	Fun	BagAddBag	True	Passed	Model Under Test Equivalent Model
16db5598f742e3717874e28e10611b951d4db07b	Apalache	Fun	BagAddBag	False	Passed	Model Under Test Equivalent Model
54c429176f802513382b1de8fca37f9677f00386	Apalache	In	BagAddBag	True	Passed	Model Under Test Equivalent Model
bac715ef484bbda92309906006d1ef286babc8f0	Apalache	In	BagAddBag	False	Passed	Model Under Test Equivalent Model
5bb01155d3a480fef100ab57975a6f5b3637c061	Apalache	NotIn	BagAddBag	True	Passed	Model Under Test Equivalent Model
2341b81761195c44b0e387fb202df94acb778c13	Apalache	NotIn	BagAddBag	False	Passed	Model Under Test Equivalent Model
257506345a5c1e89d2e6905959aabc7738dcf01a	Apalache	Record	BagAddBag	True	Passed	Model Under Test Equivalent Model
fada54d7040c7c92a79835e0ee6c798851f1401d	Apalache	Record	BagAddBag	False	Passed	Model Under Test Equivalent Model
021f8c50e8371900a1abea679a0d917e44e83812	Apalache	Tuple	BagAddBag	True	Passed	Model Under Test Equivalent Model
ff288f228b8c035c78c34a30aafb319cfa71b7ba	Apalache	Tuple	BagAddBag	False	Passed	Model Under Test Equivalent Model
f0d24236e85213de58209150c9a2b7026054b067	Apalache	FunApp	BagAddBag	True	Passed	Model Under Test Equivalent Model
4647a19da70966815dfab16ae201b783b4e5edfb	Apalache	FunApp	BagAddBag	False	Passed	Model Under Test Equivalent Model
69b5ae1002c0d70f81d662210ed6e7fdbe295ffc	Apalache	Except1Fun	BagAddBag	True	Passed	Model Under Test Equivalent Model
9cf64b251fda08ff33aeb404b61215ef7e12f5e7	Apalache	Except1Fun	BagAddBag	False	Passed	Model Under Test Equivalent Model
7bdeb3915b6ac89e36d9d29393e5a0636f9912e2	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	BagAddBag	True	Passed	Model Under Test Equivalent Model
a5c30f32ce7e37cd30026effa779b415318d6ff0	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	BagAddBag	False	Passed	Model Under Test Equivalent Model
a06a5e4f8acace964e89b0cf273098d17a26ec28	Apalache	Except1Rec	BagAddBag	True	Passed	Model Under Test Equivalent Model
6c561403cb560803a5b0c48c4e0588cdf73f2fe2	Apalache	Except1Rec	BagAddBag	False	Passed	Model Under Test Equivalent Model
49e1472f024eaf1f76603d4428c2f02ea6a1ec13	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	BagAddBag	True	Passed	Model Under Test Equivalent Model
baba7737c1675d392fc1020f55da47dc8d210389	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	BagAddBag	False	Passed	Model Under Test Equivalent Model
e24195bcbd3c0c3f2c9cbfcc57ba440e167efb33	Apalache	Except2Fun	BagAddBag	True	Passed	Model Under Test Equivalent Model
486711dcce9cfde36b76c3efa3496fe8636e880d	Apalache	Except2Fun	BagAddBag	False	Passed	Model Under Test Equivalent Model
5b0759a2d8e250dba3b063411c1d205d17ac40d3	Apalache	Prime	BagAddBag	True	Passed	Model Under Test Equivalent Model
0e3ff9b055b0c58d4bf595cea45ae6739e3ae0d9	Apalache	Prime	BagAddBag	False	Passed	Model Under Test Equivalent Model
e17295fab81042728240a858a4f0e28bdcf2d95a	Apalache	DefFun	BagAddBag	True	Passed	Model Under Test Equivalent Model
f806d69a59cd82428dc742ad51269cd0b0eb9290	Apalache	DefFun	BagAddBag	False	Passed	Model Under Test Equivalent Model
786f42cff3b332be04395dc77d5d8ebf97a30309	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	BagAddBag	True	Passed	Model Under Test Equivalent Model
94aaba9486fc20f5e430401e7e765519a1a3848d	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	BagAddBag	False	Passed	Model Under Test Equivalent Model
5d4eee7ea5ab787fd117bc031c0ee981c1d705d2	Apalache	DefFunRecursive	BagAddBag	True	Passed	Model Under Test Equivalent Model
1a5de9a89bbe60612c3afa1f5e73c7e0c5c7acbb	Apalache	DefFunRecursive	BagAddBag	False	Passed	Model Under Test Equivalent Model
9e57dccfe1ca67b129cdd031f7c3bc1b4bf4f209	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	BagAddBag	True	Passed	Model Under Test Equivalent Model
f96b8674bb4c4a28710bf6251411d0e7c7deb509	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	BagAddBag	False	Passed	Model Under Test Equivalent Model
ee31d4b700056aa1e38b5b2c86c3f23beb6ce403	Apalache	Def0	BagAddBag	True	Passed	Model Under Test Equivalent Model
5abffac19786d48e6e048f2f3276f71a451e9b5e	Apalache	Def0	BagAddBag	False	Passed	Model Under Test Equivalent Model
8d8347dd300a827ca02c44044fbab8d94dea61cf	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	BagAddBag	True	Passed	Model Under Test Equivalent Model
a3e6b7c17e630f03f2dce4af84e6359a45c90282	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	BagAddBag	False	Passed	Model Under Test Equivalent Model
ec63c8d7c5492b58a7367bc8869b3a66562134e2	Apalache	Def1	BagAddBag	True	Passed	Model Under Test Equivalent Model
0104fb2908fa8fe66c86e0b1f279e81cb16cfdce	Apalache	Def1	BagAddBag	False	Passed	Model Under Test Equivalent Model
0738ccae2bf4e13a0309e22a08169bb68dbe08a5	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	BagAddBag	True	Passed	Model Under Test Equivalent Model
96896d96d1ad803c361f0924609183c5f89cf604	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	BagAddBag	False	Passed	Model Under Test Equivalent Model
2cba9ab9392ace3128d3eaffa9f21b58da1354ca	Apalache	Def2	BagAddBag	True	Passed	Model Under Test Equivalent Model
815dd45f2c34e92bf06a24c1ba86de0ef2ee45b0	Apalache	Def2	BagAddBag	False	Passed	Model Under Test Equivalent Model
31ba213488f001af7dcf64ab0445e8c7a4be4948	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	BagAddBag	True	Passed	Model Under Test Equivalent Model
a3157fb8ae3d0c348de9819b3e8a11593da63fb2	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	BagAddBag	False	Passed	Model Under Test Equivalent Model
14f3237a6bd28d376a01e07234312fc2b377900d	Apalache	Def1Recursive	BagAddBag	True	Passed	Model Under Test Equivalent Model
0f3c0b4d00a45469f818e234d2558dcad0596e16	Apalache	Def1Recursive	BagAddBag	False	Passed	Model Under Test Equivalent Model
597daf1ebdf2a4d086de9e2c85ce83d7704ba90b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	BagAddBag	True	Passed	Model Under Test Equivalent Model
9adb729733855062b26fdb357db088f7a4fa3da2	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	BagAddBag	False	Passed	Model Under Test Equivalent Model
94fc5b41a2b2c64520172a0c077be040817439e7	Apalache	Extends	BagAddBag	True	Passed	Model Under Test Equivalent Model
6fc061a289a816148ebe870b8a88b3541857d5e4	Apalache	Extends	BagAddBag	False	Passed	Model Under Test Equivalent Model
984ff48d14db02f27af01c18cc20c0858dbe5341	Apalache	ExtendsInDifferentFolder	BagAddBag	True	Passed	Model Under Test Equivalent Model
046d93251a7b403da0ceca8a1564983d11865f61	Apalache	ExtendsInDifferentFolder	BagAddBag	False	Passed	Model Under Test Equivalent Model
1003acb66f30064891be98228689f9c2ff382d0a	Apalache	Variable	BagAddBag	True	Passed	Model Under Test Equivalent Model
b53839f7c3a08947789b3331787ed5fbe0fa025e	Apalache	Variable	BagAddBag	False	Passed	Model Under Test Equivalent Model
8088fb2f6dde037259b11299348abd04449843c6	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	BagAddBag	True	Passed	Model Under Test Equivalent Model
3d772dc90d307f4ee25df7642c080f60f96834ab	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	BagAddBag	False	Passed	Model Under Test Equivalent Model
8c2ef6d5380ef988bf72664ad21ec8a1e482a83a	Apalache	Constant	BagAddBag	True	Passed	Model Under Test Equivalent Model
a19f71e372c56bbad6fea128be6e7d9a2665fde9	Apalache	Constant	BagAddBag	False	Passed	Model Under Test Equivalent Model
39b6aa268b05017ad13c7b4069c7074c1c013c36	Apalache	ConstantRank1	BagAddBag	True	Passed	Model Under Test Equivalent Model
92b059001b7a533e548ec2fcfab7a09565dfb21a	Apalache	ConstantRank1	BagAddBag	False	Passed	Model Under Test Equivalent Model
bbe135c47abca2e7381323d3194075be56669e6a	Apalache	Instance	BagAddBag	True	Passed	Model Under Test Equivalent Model
a29533b018b98f2b9ebfd8a767392974b5682d43	Apalache	Instance	BagAddBag	False	Passed	Model Under Test Equivalent Model
9fe062ab339a13d3011bc9d52f08ce29df2f2184	Apalache	InstanceWith	BagAddBag	True	Passed	Model Under Test Equivalent Model
fe1a9a76438f27823c4b2c5cfbc3aec196f866ca	Apalache	InstanceWith	BagAddBag	False	Passed	Model Under Test Equivalent Model
c3d72341235c6ff5beaa054ecfc60f0858f23300	Apalache	InstanceNamed	BagAddBag	True	Passed	Model Under Test Equivalent Model
622d2cf11e59df273c823505b2449ab51ea5ef2c	Apalache	InstanceNamed	BagAddBag	False	Passed	Model Under Test Equivalent Model
bf53a0789a5f44ab36660a2b4a4a71d1c0484f3f	Apalache	InstanceNamedWith	BagAddBag	True	Passed	Model Under Test Equivalent Model
156eb8dd5afe4abbfa3c5d13a7109663fc49313f	Apalache	InstanceNamedWith	BagAddBag	False	Passed	Model Under Test Equivalent Model
36ad4750b9334476600647d3181fdb32d3a66b32	Apalache	InstanceInFolder	BagAddBag	True	Passed	Model Under Test Equivalent Model
47ddcb7e45677ab79b72ffdd9eafae858efe24b6	Apalache	InstanceInFolder	BagAddBag	False	Passed	Model Under Test Equivalent Model
88acbd0a5f54e3d7e67e9817b089fad930e81ef0	Apalache	InstanceWithInFolder	BagAddBag	True	Passed	Model Under Test Equivalent Model
8c345af952e5da3e2b0a4617ac97e061c8b723a9	Apalache	InstanceWithInFolder	BagAddBag	False	Passed	Model Under Test Equivalent Model
88832846d5a932e3bdf84b80eb2945d28a943cc5	Apalache	InstanceNamedInFolder	BagAddBag	True	Passed	Model Under Test Equivalent Model
1f9d8d184c3ecda07ea16e1861c75e2d3244fa0e	Apalache	InstanceNamedInFolder	BagAddBag	False	Passed	Model Under Test Equivalent Model
c1b9621cc5db95862ab6c15d190168ce8c6a8256	Apalache	InstanceNamedWithInFolder	BagAddBag	True	Passed	Model Under Test Equivalent Model
b4b092288fad02635ba7aa1ef58c138dc1ad4927	Apalache	InstanceNamedWithInFolder	BagAddBag	False	Passed	Model Under Test Equivalent Model
49546f45ddb118725ac9ff4322929436debba9f1	Apalache	Lambda	BagAddBag	True	Passed	Model Under Test Equivalent Model
e5e279aa5f6d2cd1b33c779693aef4b8da5beded	Apalache	Lambda	BagAddBag	False	Passed	Model Under Test Equivalent Model
68d97566390bfdce7caaf29e3a70042e5eb8886d	Apalache	IfThen	BagAddBag	True	Passed	Model Under Test Equivalent Model
f73ddea4869f352588737dab6155b2d9b0bf4439	Apalache	IfThen	BagAddBag	False	Passed	Model Under Test Equivalent Model
e8dfcfde3552ba6dfccf3def6ec470f319adb180	Apalache	IfElse	BagAddBag	True	Passed	Model Under Test Equivalent Model
e80e6cfc4b2b91bee4d7ab13b9efea6f1e0365f8	Apalache	IfElse	BagAddBag	False	Passed	Model Under Test Equivalent Model
0a2302f7e188dce196fde2874bc57052ad1c47b9	Apalache	Unchanged	BagAddBag	True	Passed	Model Under Test Equivalent Model
0449dc412abec44b1e8ab4f15e8cdb89dff32c30	Apalache	Unchanged	BagAddBag	False	Passed	Model Under Test Equivalent Model
f25fb87ed65c2a1f1ff97542450b95ece87572aa	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	BagAddBag	True	Passed	Model Under Test Equivalent Model
5723973cc784f316a191e42dec755e4ed0193c73	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	BagAddBag	False	Passed	Model Under Test Equivalent Model
d67911051c9c651e433e70a30837fff383397329	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	BagAddBag	True	Passed	Model Under Test Equivalent Model
ceff100202cec479c28aa6a03620a12f3a7462aa	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	BagAddBag	False	Passed	Model Under Test Equivalent Model
6a5da93d5fb3bd1a632fc0afe5a6c03f3a8f4e3d	Apalache	BagBagToSet	BagAddBag	True	Passed	Model Under Test Equivalent Model
49323f79bd0a968e44cbc5d30609ca2be14536be	Apalache	BagBagToSet	BagAddBag	False	Passed	Model Under Test Equivalent Model
70c7a755b1d71f82960470792e9775bf7fde87be	Apalache	BagBagIn	BagAddBag	True	Passed	Model Under Test Equivalent Model
fd517c28e9447c76e59e414f1bb00112fb0e6cda	Apalache	BagBagIn	BagAddBag	False	Passed	Model Under Test Equivalent Model
e323867835a073fcd574bfdbfb288b9fd08607a0	Apalache	BagAddBag	BagAddBag	True	Passed	Model Under Test Equivalent Model
bc00e0731b7e1716f1955f34f7a7b3f835bb1748	Apalache	BagAddBag	BagAddBag	False	Passed	Model Under Test Equivalent Model
f4703045e6c47e1e7923cb1ded5392086cd2856b	Apalache	BagBagSub	BagAddBag	True	Passed	Model Under Test Equivalent Model
8a68c7c78f96b1e5b4c4248dfd344f7d88a8f4e3	Apalache	BagBagSub	BagAddBag	False	Passed	Model Under Test Equivalent Model
ff10050919c0a2fafef6ca91176410966a38db62	Apalache	BagCopiesIn	BagAddBag	True	Passed	Model Under Test Equivalent Model
ca154db16a8790924f484c66fc57241f36884ecd	Apalache	BagCopiesIn	BagAddBag	False	Passed	Model Under Test Equivalent Model
b7fa955a21c9de87fc01ed28cf19b677a884d5ad	Apalache	BagSubsetEqBag	BagAddBag	True	Passed	Model Under Test Equivalent Model
abbc722ea95534af760e51898e442ddfe273b4e4	Apalache	BagSubsetEqBag	BagAddBag	False	Passed	Model Under Test Equivalent Model
ae38bc7c7c4cfa52cd5264831324d25c7f67bc39	Apalache	BagBagCardinality	BagAddBag	True	Passed	Model Under Test Equivalent Model
38e804e2e71908fabb5a97fd48c108def1fc562b	Apalache	BagBagCardinality	BagAddBag	False	Passed	Model Under Test Equivalent Model
9d113836c266bcf4f0eb889cbc2947d403ec0e2b	Apalache	BagBagOfAll	BagAddBag	True	Passed	Model Under Test Equivalent Model
36197f22623de61d467477058dc6cfc96ca974a9	Apalache	BagBagOfAll	BagAddBag	False	Passed	Model Under Test Equivalent Model
f1ef9749d53055f1aa137dacd4ea3ff10403e624	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	BagAddBag	True	Passed	Model Under Test Equivalent Model
e2e7fc38975fe77fac3fb0d09f1e78c7cf089d97	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	BagAddBag	False	Passed	Model Under Test Equivalent Model
10f0a9fbab58139d5099325c9bb87b51e330e269	Apalache	SeqAppend	BagAddBag	True	Passed	Model Under Test Equivalent Model
3398c2ce7e5325f10eabff09a05af23fac690954	Apalache	SeqAppend	BagAddBag	False	Passed	Model Under Test Equivalent Model

Index

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