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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
e1425f3fa0f71ae3499af100fe43bd7f10ee1d1f	Apalache	Eq	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
ef72445567d59f1721435b76621c1c115d1b9e81	Apalache	Eq	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
61a58b2c8f689e1e9c6b8e435b49b9942d128c55	Apalache	Ne	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
1c69fae13596082628109db1e0b8344f5c27ad4c	Apalache	Ne	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
c3830ff7be1cb535755aa840c37a65d5472ecc13	Apalache	Let	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
2ee1fefefb74a4ec3d14ac1e498344d2a9642626	Apalache	Let	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
ac896e83e8365df29abf99e05feff0a4718ea36a	Apalache	Set0	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
6c03dd6aa75f99884b07856447652d0d8b147ca9	Apalache	Set0	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
834cb20e8d8a2051bbb1beeef825ecfe85db5b92	Apalache	Set1	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
4e07ca76c44d5b9315c0a130f543b8099167d578	Apalache	Set1	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
5043f4bf5fc3a13074e6db0ea8d53c712cefb818	Apalache	Set2	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
f6b48973e8c215b2cc665ac9afe961a7c14655dc	Apalache	Set2	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
0673c09fc77a8a672e2efb6255ff612f218a72fc	Apalache	Fun	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
b183ff148aecae3de8cbbc450b4d8712bad38c51	Apalache	Fun	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
bfa6f38bfa13479af99b8d1db3fbf6eff718e527	Apalache	In	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
988f9dfcb931dbf41c37f4ad3ee117b4192c8ec4	Apalache	In	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
97e36ce3e2db04397b59abb3e93b08bb55457c33	Apalache	NotIn	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
bc31f19b0733049898ebd4695a0f56856655e6f1	Apalache	NotIn	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
fd52c919c075b6290c469206ebfbaf27b2e4a960	Apalache	Record	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
b7be877b02803d1fe79ecb85f327f74b2d763709	Apalache	Record	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
1d808d807512bb234edc0f452869be1d0ef9179e	Apalache	Tuple	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
6520a8e766e47c4930f21ba3d9503a730ee10e35	Apalache	Tuple	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
1b06560ffe26f6cdf10c2b31451ec9d0cf474e0f	Apalache	FunApp	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
8a29f3886efafa76d70822293f32964f07b2eb4f	Apalache	FunApp	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
16bee4a98e257be6c991772adced0280e86bf8b7	Apalache	Except1Fun	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
098a15eecfa858e56bb76eec74fb803ac5e0466f	Apalache	Except1Fun	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
36a99cc38f09c4a7fe89d28d7a0a0292b34f4539	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
24434e6b402c6e369d57852570ffb6e557e257c9	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
094a395228a36d3a8f1ea03e4851227a2f49592a	Apalache	Except1Rec	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
01316e662e7e805167811bfd8e52857a47d93e71	Apalache	Except1Rec	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
eed693444d269bd9daceee69572c58e51769b172	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
92d676869c2cbd11f158fe4027c94659f0d81854	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
0e691a2f82666d16689670ca162a33b9d2e3b547	Apalache	Except2Fun	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
61affb31eb22a75de483c9c783a20f66c54da51e	Apalache	Except2Fun	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
bcb753006be14353a16802995ab98c94da602821	Apalache	Prime	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
44718cbd4de81f59ed0f967a1b22aec35467eecf	Apalache	Prime	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
8d2b24dfe7d8a7a231b5e071dade3f713fea548c	Apalache	NumUnaryMinus	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
8dd3e9cca3191bcb058bcbe1c54d018acf16beae	Apalache	NumUnaryMinus	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
ef02f20bdeb792a14546ca5bc9482d2a6924c72b	Apalache	NumPlus	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
b5166404d67c9e59c7cd4a430170727640aaab4b	Apalache	NumPlus	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
c9011a765ce6b68bacf673e7f5ea00d77134fa7a	Apalache	NumMinus	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
5dadfdb3df29d9110e63c6e6f71857af781063ed	Apalache	NumMinus	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
9fd73ae663065944ce0902f19a78c5b1e07073b8	Apalache	NumMul	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
4bb4335e9dd5a8a5ff52cfab1ff3cef222e9cc1d	Apalache	NumMul	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
7e770f59485440c62f0e5ce0b940a3f20fcafa02	Apalache	NumDiv	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
53601410354685e301650c76efb93f6e867c16ef	Apalache	NumDiv	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
3ba3eeabab839c2523a95a2952107d49e439816b	Apalache	NumMod	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
5ac176185505d32570e1eab0b716239304dc2eee	Apalache	NumMod	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
995032f8a18a15e696d50d5717f53181634eba53	Apalache	NumPow	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
d196ea4aea1d1ce5ca83cccabe55184a583dda10	Apalache	NumPow	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
84497a51a33722a6b31242ed5704cc86ec2dd942	Apalache	NumGt	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
282a7eb6ac428d412631fe118e8eb303dfd86f4c	Apalache	NumGt	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
0e7db8e73220464a8980115add9fd96207634bd6	Apalache	NumGe	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
f8f360ca984a9b84a1343e43ad253f37474ba755	Apalache	NumGe	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
cdb4f49a9aab11b2a8d6df06e14c0cebb5a048f4	Apalache	NumLt	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
38e73bf2c39253d8fdf7ca396007914eb2c2a51f	Apalache	NumLt	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
5f5bf7eb73e3ac72d67855c50883478acfae3265	Apalache	NumLe	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
b454859da6680ced172ab0307fbdc64886e69502	Apalache	NumLe	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
acfeb0182f3261c1d3cabcc4cb73c2323b8c7ecb	Apalache	DefFun	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
d9d4490783bb4b75709b957b15f35d34e695f8b7	Apalache	DefFun	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
340ab6b11a1e8e043d1d4193f2ca22110945aec2	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
6ebeacc3568e4de68856ecd0f35951092e212686	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
bffa6456f94044090b28db18179e9caba4dc5288	Apalache	DefFunRecursive	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
8c2c34ead88b6ff3a8ced57cf3258ed2ce35648b	Apalache	DefFunRecursive	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
94810192e8e5d7f6804a2acbfa70d97e69728798	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
1e28c6e194df4a344ba5fbba96339e3f2c791f16	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
311f6859c1607a730bc93a3ef446e8ca81cce8e0	Apalache	Def0	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
e58480c2811072d8b7ea2dbcd31c6e373818e873	Apalache	Def0	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
f8512358057eea792a75b5cb6e650709de609926	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
eb7ed5011355a206f7feb5f85529a473f8886c3c	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
dc89be145e573921bdfe81ccf7ce1f6550485cfe	Apalache	Def1	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
c10560ac6b3b4cb9ffa7a7d3cccba20b81c7333e	Apalache	Def1	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
0815a071e4db7bddd1fa99ee63d291482ac68689	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
c12a66768c7580a6259bb7cd471150fa63e92302	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
794a0a57b654e7fc936842924c8326fe1b5ec947	Apalache	Def2	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
2470cd751c9848ce76997be47277ee1eeef5f45e	Apalache	Def2	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
27a2486fb9f99b915ce8608363cc69afe246fa24	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
faaa723f1b7429e258c2870e2d2a3aa3afb2da37	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
cba51148f928e13be9d1c75d65ad8c15f9207d87	Apalache	Def1Recursive	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
030599a89cc25d3272c63fc511fdcd4b671fa6da	Apalache	Def1Recursive	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
b1bde81490b89f13af6da695ef5859e22ee61d91	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
a66ea9e129c184fad4d814a39e903bdee8117714	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
2cf9cc564e8f8a9be33b9df0cb0c5c517a3020ef	Apalache	Extends	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
291fc14fb3d550de58933a5fa3eb00e075f32894	Apalache	Extends	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
9b87b6cd1f98975f975d6c2d5750a3751312e0dd	Apalache	ExtendsInDifferentFolder	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
a6f8aba1afa96e6a041c7f608c15f8e7f8460a58	Apalache	ExtendsInDifferentFolder	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
c93e10768399b57fffddf729ab6830e1b8816c71	Apalache	Variable	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
1927f43a9337aab927d103b33b1b2e619b08af78	Apalache	Variable	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
f633d7e2bc8e03dea9456005cd8ff2ba7861ea17	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
f9fc0f496381918fd872c0544d0d0e29cc63f0b0	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
08d1c2553eafae97d344e4a85be329ae2fc5c63b	Apalache	Constant	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
d464eb65551fadf7d43a2b093d63fbe045aca0ee	Apalache	Constant	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
e5b8c4e60391f68fa9daf81e13483163389fa1d0	Apalache	ConstantRank1	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
b26e4ed9c98d86cf82708d2e68d0a033750a60e6	Apalache	ConstantRank1	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
fb53116d3a28d1b2146222fb65bfa0291812cfd9	Apalache	Instance	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
665a20750e116452ad854746a925c147307ff099	Apalache	Instance	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
ef6ad8d28baca88fc26dc6e909b76000a9bed07b	Apalache	InstanceWith	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
dbe3c72ad7875b39b4c35d308baa03f2b3ab2697	Apalache	InstanceWith	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
f61ab99b45ebf804dbd38379e7339706c034cb93	Apalache	InstanceNamed	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
0a414da1d1c61fc120a453489b8070d60de5e779	Apalache	InstanceNamed	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
9dd04fdc59c50e20955dbe0738e4a66cf3c8761a	Apalache	InstanceNamedWith	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
dfed379bed297e5f212a37a271f66140a6cd34dc	Apalache	InstanceNamedWith	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
4ef46eb1e686231b1e6dc0516cda7fd8d97e016f	Apalache	InstanceInFolder	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
eb95a4ca1a0240f967ded8bc86302809dfbb2dfe	Apalache	InstanceInFolder	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
f850685db6ae66c8714c936c25ed0c37c9750e9b	Apalache	InstanceWithInFolder	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
55035f0b953cd44c9a1f14fefb920c090f79369c	Apalache	InstanceWithInFolder	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
c1513ad270fc2cc2f77cfee1905025ccb711d8c7	Apalache	InstanceNamedInFolder	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
0f1393827173edacf41573df97c66185b36eee13	Apalache	InstanceNamedInFolder	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
691762633f4aa070a9e2408160e61080a427a6d0	Apalache	InstanceNamedWithInFolder	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
22418e4a1a875502c5e0040718701a3e741a4eea	Apalache	InstanceNamedWithInFolder	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
53b21611f3e1d7519b07a5d7ae9b73dd8a1b1c1a	Apalache	Lambda	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
31ed1fec7a29d68fc5c5025ff08787ef4ae0ac74	Apalache	Lambda	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
f0f05917f283b2487f0b3d277d6953573f3cb57c	Apalache	IfThen	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
6742b65d6a183cfca3f0dfd6b39db87fa6371f50	Apalache	IfThen	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
840f17061d73be69488359f9475160aa5b75c418	Apalache	IfElse	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
5964270592fc50d8963d0e0602997f82f4d2eba1	Apalache	IfElse	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
fa24b8eba8669bce889812250925a2ce3622721c	Apalache	Unchanged	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
1a189c172d156041819f94c8ce6a002e97ecdfc8	Apalache	Unchanged	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
186a484931432d9055cc55ea9908f4b619eb4e68	Apalache	SeqSubSeq	BagCopiesIn	True	Failed: TLC requires the second argument of SeqSubSeq to be in domain of the sequence, which doesn't include zero, and returns an error otherwise. BagCopiesIn returns zero, because there no such value in the bag, therefore TLC reports error. Apalache always returns some sequence and doesn't crash in such situations	Model Under Test Equivalent Model
1e51fed60a710cf8752f73c807de2510e96a90fe	Apalache	SeqSubSeq	BagCopiesIn	False	Failed: TLC requires the second argument of SeqSubSeq to be in domain of the sequence, which doesn't include zero, and returns an error otherwise. BagCopiesIn returns zero, because there no such value in the bag, therefore TLC reports error. Apalache always returns some sequence and doesn't crash in such situations	Model Under Test Equivalent Model
92905afa993e630b46584b46cb37e10298d0b478	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	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
1bac6aea5a0456b5c46296d800e2585a119fc7cb	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	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
d782b0534496b00eec09cf76d302aa09dd2a8940	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
77cf6eb6b1481e73b81c525166104c6e0243a66d	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
d453895b60081fc31df46e4ef7768ae7c3aaddd9	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
6bc1b7538c2327cce6a917695d3757a034b34c3f	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
335bfb67a2caaa7a326b42b83210f223bf266ff7	Apalache	BagBagIn	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
a9fa70648bac5ca6b512659afaba7372d0a31bcc	Apalache	BagBagIn	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
248dd0bdfd4d1a8d65317ae39f5868e57dbb0607	Apalache	BagCopiesIn	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
3d5e7aaf259e2f1f2cbbe7ba7fa6ef4326239ae2	Apalache	BagCopiesIn	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
99d5eff4a4cbb8622aad56d88dc33431af500482	Apalache	SeqAppend	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
3f3bc4449993b88c0b423a6bb7f1108dc1eff338	Apalache	SeqAppend	BagCopiesIn	False	Passed	Model Under Test Equivalent Model

Index

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