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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
e49446460fd7c9deff05afd65340834998d09572	Apalache	Eq	BagBagSub	True	Passed	Model Under Test Equivalent Model
de1d648b9eced0db6b2aaa02af8aeeae8f3ceee3	Apalache	Eq	BagBagSub	False	Passed	Model Under Test Equivalent Model
138d79cb92388c21dc707ea5ae32bca561dc0567	Apalache	Ne	BagBagSub	True	Passed	Model Under Test Equivalent Model
69807393accd9834879812bd31f211c45cb701ba	Apalache	Ne	BagBagSub	False	Passed	Model Under Test Equivalent Model
25caf1c7ed489bb3b6fa60fd370e47f5f9bb6bd4	Apalache	Let	BagBagSub	True	Passed	Model Under Test Equivalent Model
82f6d680ce095cb724bc905ebf31d315e0cb3e8c	Apalache	Let	BagBagSub	False	Passed	Model Under Test Equivalent Model
1150af6ee5879337be923e3f5f14a089c88f1a8d	Apalache	Set0	BagBagSub	True	Passed	Model Under Test Equivalent Model
89483fa8bf3c16c19a2d0dd816d9b29f95f4cf8d	Apalache	Set0	BagBagSub	False	Passed	Model Under Test Equivalent Model
b65bcc6e4985d9695240be0086fba5fcc5d6bf44	Apalache	Set1	BagBagSub	True	Passed	Model Under Test Equivalent Model
7b835dee793e6f248a28a07250adfac8ab631b86	Apalache	Set1	BagBagSub	False	Passed	Model Under Test Equivalent Model
bf11da463bb437cadbea0497576c20e7c6ed38db	Apalache	Set2	BagBagSub	True	Passed	Model Under Test Equivalent Model
49390e19e232e5742e72ab9b1c1dae93336d23b0	Apalache	Set2	BagBagSub	False	Passed	Model Under Test Equivalent Model
187772d143746fc12a48157ce73925c6c3e7e436	Apalache	Fun	BagBagSub	True	Passed	Model Under Test Equivalent Model
b3ba7960cb9d7b786c03430653f51bf5ab8ab420	Apalache	Fun	BagBagSub	False	Passed	Model Under Test Equivalent Model
dcad1cb4d69f55487422289e1d529fb823b4add1	Apalache	In	BagBagSub	True	Passed	Model Under Test Equivalent Model
ae2970c0b7daf2b84dbe22f24c632e1902c4e848	Apalache	In	BagBagSub	False	Passed	Model Under Test Equivalent Model
f67a815889d8a9b071b9d58489dd203d37581aff	Apalache	NotIn	BagBagSub	True	Passed	Model Under Test Equivalent Model
34b062ca83520cdd6285ffcc61e6f2c718075e8a	Apalache	NotIn	BagBagSub	False	Passed	Model Under Test Equivalent Model
bc95e979dcd6e95aa7ccc116af35723ad4bea8a3	Apalache	Record	BagBagSub	True	Passed	Model Under Test Equivalent Model
c2d3782fae9986a8b0871b2966ff23f3ce8d9d8b	Apalache	Record	BagBagSub	False	Passed	Model Under Test Equivalent Model
2a034421e75788ffb8dcc4261b7d70a6896ff4ee	Apalache	Tuple	BagBagSub	True	Passed	Model Under Test Equivalent Model
4b2b715781f8a6fc232f685b6fea48a1aded8937	Apalache	Tuple	BagBagSub	False	Passed	Model Under Test Equivalent Model
d8bb01b3668b9895b1294825bd7e2fcaefac2711	Apalache	FunApp	BagBagSub	True	Passed	Model Under Test Equivalent Model
3bedc09291e31f10e797079aecd130a413c9130b	Apalache	FunApp	BagBagSub	False	Passed	Model Under Test Equivalent Model
244f71bbe13aead53a9613dd1128747350bdb94d	Apalache	Except1Fun	BagBagSub	True	Passed	Model Under Test Equivalent Model
ba77803b2b68b1ad83a947ea7c26d791753c0856	Apalache	Except1Fun	BagBagSub	False	Passed	Model Under Test Equivalent Model
f5ba2ea6544f61a130af298fd49b495cba3909e2	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	BagBagSub	True	Passed	Model Under Test Equivalent Model
67275d9e329a4931a9c4a31bc271835e6b2e876f	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	BagBagSub	False	Passed	Model Under Test Equivalent Model
1e46f2fd9b6c4b2da5d5a4a6c92fc591de19dd71	Apalache	Except1Rec	BagBagSub	True	Passed	Model Under Test Equivalent Model
e4c310f7ea31752fe0be78ca4a363a6bc7af258f	Apalache	Except1Rec	BagBagSub	False	Passed	Model Under Test Equivalent Model
6d68567234721ec9e60a6863ee09f2fc2fa2d049	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	BagBagSub	True	Passed	Model Under Test Equivalent Model
8abec1250a32c74a5a61487d84ea0933dd65c348	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	BagBagSub	False	Passed	Model Under Test Equivalent Model
22cdbcca7d27a551e89d7cc8a5603b426f255dd2	Apalache	Except2Fun	BagBagSub	True	Passed	Model Under Test Equivalent Model
f8b43af09d73e472b66398e4e1459e625786ae89	Apalache	Except2Fun	BagBagSub	False	Passed	Model Under Test Equivalent Model
924ee53862a58f0165f39bd63e310e6059498cbf	Apalache	Prime	BagBagSub	True	Passed	Model Under Test Equivalent Model
860de1f57c1b30be7d6f6dec855c5e72a409496b	Apalache	Prime	BagBagSub	False	Passed	Model Under Test Equivalent Model
7bac3a35d4f17eb37c0043924071c785879e7365	Apalache	DefFun	BagBagSub	True	Passed	Model Under Test Equivalent Model
27eda85ad4e43b869a1a29a1d2b1159887bb2cdc	Apalache	DefFun	BagBagSub	False	Passed	Model Under Test Equivalent Model
61fc76c6444b7b4618d73be83493b3eecfc6b8df	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	BagBagSub	True	Passed	Model Under Test Equivalent Model
e009020e5c9b689ece0c306c1bef95f5990a2567	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	BagBagSub	False	Passed	Model Under Test Equivalent Model
5e58ee712476857d3f142bb8c51625caf28fa32f	Apalache	DefFunRecursive	BagBagSub	True	Passed	Model Under Test Equivalent Model
21a3d840b519942f932adf9d9894ff5f8f34cafb	Apalache	DefFunRecursive	BagBagSub	False	Passed	Model Under Test Equivalent Model
7c58e70766a02a7eef340bf2510f1cf830c361cb	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	BagBagSub	True	Passed	Model Under Test Equivalent Model
ffb98226156e20acce930f2f5535b27e8e726e03	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	BagBagSub	False	Passed	Model Under Test Equivalent Model
35a7300d73302cec13e0f89a02db13984170dd97	Apalache	Def0	BagBagSub	True	Passed	Model Under Test Equivalent Model
ca4a857bd81604318a89209ca0c3edbfd8e4d09c	Apalache	Def0	BagBagSub	False	Passed	Model Under Test Equivalent Model
6caf08717bca7da2e029433467582c0090685d35	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	BagBagSub	True	Passed	Model Under Test Equivalent Model
ff4ab2eb02998fc0c45e0fbb974dcbb14c43dccb	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	BagBagSub	False	Passed	Model Under Test Equivalent Model
8991a0afa3694735e5a028848f0167bc7741f869	Apalache	Def1	BagBagSub	True	Passed	Model Under Test Equivalent Model
09de55403d23ae491c485532200219cca9cbb42b	Apalache	Def1	BagBagSub	False	Passed	Model Under Test Equivalent Model
14b72d0e07389985d6132e361779baa973cdf49d	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	BagBagSub	True	Passed	Model Under Test Equivalent Model
c657cd04d0caa0602310cafd2c0b2f0a8f60064f	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	BagBagSub	False	Passed	Model Under Test Equivalent Model
92a099dfae86cc51a0413744d542e4319098f79d	Apalache	Def2	BagBagSub	True	Passed	Model Under Test Equivalent Model
8b36b8282d5a155a427a93e4d624a0620058f35f	Apalache	Def2	BagBagSub	False	Passed	Model Under Test Equivalent Model
a21fbf2f7d056d94ce7282b713e9f4b1612e5404	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	BagBagSub	True	Passed	Model Under Test Equivalent Model
7d8af7d6178e20cbd96c4feaeb2937edc725e970	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	BagBagSub	False	Passed	Model Under Test Equivalent Model
7e859f7e2f794699aa3e07899630fa46342eab26	Apalache	Def1Recursive	BagBagSub	True	Passed	Model Under Test Equivalent Model
679d43b7d9a25a541ec2feaaaf94b9231357b0e3	Apalache	Def1Recursive	BagBagSub	False	Passed	Model Under Test Equivalent Model
e26306245ccf8481417232b8a94c3465581590de	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	BagBagSub	True	Passed	Model Under Test Equivalent Model
be8cded459350d695d8b78b5ea8edf0f53f44318	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	BagBagSub	False	Passed	Model Under Test Equivalent Model
5e84bae7e45f16c8fe46d24d4f6abab6766bbc3c	Apalache	Extends	BagBagSub	True	Passed	Model Under Test Equivalent Model
aa173092c68ee074962f67b9224f417c6e7959b7	Apalache	Extends	BagBagSub	False	Passed	Model Under Test Equivalent Model
efe2c04a7c069e404647cfceb10fa7579037c12c	Apalache	ExtendsInDifferentFolder	BagBagSub	True	Passed	Model Under Test Equivalent Model
b1f3f576ba7c220472ec9b2d6d9e6c654b01d300	Apalache	ExtendsInDifferentFolder	BagBagSub	False	Passed	Model Under Test Equivalent Model
1fa666e9b98af3c6bb67e4bcbc28a83d69efb901	Apalache	Variable	BagBagSub	True	Passed	Model Under Test Equivalent Model
c5e5bb478fcbf96c5cd59ea114b3c7f8fee43999	Apalache	Variable	BagBagSub	False	Passed	Model Under Test Equivalent Model
2e26529a34e94e28cb4774b574be7ffabad76a3e	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	BagBagSub	True	Passed	Model Under Test Equivalent Model
37819dcf3a54905004ce4425a5c52bd64b08b8db	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	BagBagSub	False	Passed	Model Under Test Equivalent Model
3b5b96f98f7c04e106d31854ebffe299187a3a96	Apalache	Constant	BagBagSub	True	Passed	Model Under Test Equivalent Model
50a368548e55d753dd3849963846a7ca12787ef3	Apalache	Constant	BagBagSub	False	Passed	Model Under Test Equivalent Model
7ca606a95d793c7379c5d370c645da55f0f168ae	Apalache	ConstantRank1	BagBagSub	True	Passed	Model Under Test Equivalent Model
a02e2969bd33c232695bb09b61385db1f5f1ab6a	Apalache	ConstantRank1	BagBagSub	False	Passed	Model Under Test Equivalent Model
912651bf39212dc32cb87009f70a543f139ed486	Apalache	Instance	BagBagSub	True	Passed	Model Under Test Equivalent Model
8c499572b6a93b6166243aa488e0d6a5f25450ac	Apalache	Instance	BagBagSub	False	Passed	Model Under Test Equivalent Model
6058f214e3144ee6e8be0e2ededaedda26b584a5	Apalache	InstanceWith	BagBagSub	True	Passed	Model Under Test Equivalent Model
f3fabd81bf417b70a29766e903abc96df360a0dd	Apalache	InstanceWith	BagBagSub	False	Passed	Model Under Test Equivalent Model
a3fa1a9d2e2596f73e79e97bcbb5d266401ea8a5	Apalache	InstanceNamed	BagBagSub	True	Passed	Model Under Test Equivalent Model
3db8b5f2f2c04cfc5a1178e1d876fbf87698f8c4	Apalache	InstanceNamed	BagBagSub	False	Passed	Model Under Test Equivalent Model
bb822b8227660e9d489605d2b56545168372d42b	Apalache	InstanceNamedWith	BagBagSub	True	Passed	Model Under Test Equivalent Model
4b8f3110f1c959b141bce488d8107173d51e3d2e	Apalache	InstanceNamedWith	BagBagSub	False	Passed	Model Under Test Equivalent Model
f53fc2a88e7c1f5f6d6ec7d0a8122863bd04cd0e	Apalache	InstanceInFolder	BagBagSub	True	Passed	Model Under Test Equivalent Model
cc0ee4f5074d89ca79b132192ae13f0cc9c6a4b1	Apalache	InstanceInFolder	BagBagSub	False	Passed	Model Under Test Equivalent Model
42b70f7c1bbfc58e3108f42288d3846afa0e482b	Apalache	InstanceWithInFolder	BagBagSub	True	Passed	Model Under Test Equivalent Model
879fa43ac6c5d46463fffeb0298e4846cf2a5da5	Apalache	InstanceWithInFolder	BagBagSub	False	Passed	Model Under Test Equivalent Model
22e687cf597c501326b311a21a06eebe02352e01	Apalache	InstanceNamedInFolder	BagBagSub	True	Passed	Model Under Test Equivalent Model
af1e0b55fe1a884a15a5345cc454a129b17401da	Apalache	InstanceNamedInFolder	BagBagSub	False	Passed	Model Under Test Equivalent Model
18c22880e30199a91739089b824928f9128d2735	Apalache	InstanceNamedWithInFolder	BagBagSub	True	Passed	Model Under Test Equivalent Model
8da64cd1838c8ad3b2fd144b9208466e25419ed9	Apalache	InstanceNamedWithInFolder	BagBagSub	False	Passed	Model Under Test Equivalent Model
bb287ef0c69b8548cb935edeb1358f01e2d57298	Apalache	Lambda	BagBagSub	True	Passed	Model Under Test Equivalent Model
b1562b25af6a5e8eec4be939342a9bd3b333ae1f	Apalache	Lambda	BagBagSub	False	Passed	Model Under Test Equivalent Model
2c7ef9df7611102c9debc9e8f3252fa6fd794156	Apalache	IfThen	BagBagSub	True	Passed	Model Under Test Equivalent Model
c49627f9815736c32c54f7cf8054e65b8b073961	Apalache	IfThen	BagBagSub	False	Passed	Model Under Test Equivalent Model
2210ab1a939a9becaf4999f46dce9e8494bc2bf2	Apalache	IfElse	BagBagSub	True	Passed	Model Under Test Equivalent Model
815dcd6028aacb60433a24933a00a91d75a4866e	Apalache	IfElse	BagBagSub	False	Passed	Model Under Test Equivalent Model
aa8724c23d635152d5d312c0bfccfe9124c55238	Apalache	Unchanged	BagBagSub	True	Passed	Model Under Test Equivalent Model
f14839cca164ddd68daa55b0813a283fc9457b50	Apalache	Unchanged	BagBagSub	False	Passed	Model Under Test Equivalent Model
e07e395d7ca527b11f98d7eedb868a512ae666f0	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	BagBagSub	True	Passed	Model Under Test Equivalent Model
b005280f625632ae29a373479432b403b52c6e8a	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	BagBagSub	False	Passed	Model Under Test Equivalent Model
d2c18668dc7974502653de3fe65bab6d5d37b31d	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	BagBagSub	True	Passed	Model Under Test Equivalent Model
6af294bbde43597451b7c44fce84b03d63de52d2	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	BagBagSub	False	Passed	Model Under Test Equivalent Model
39a48e7c7dec3eddf56aa3cb78bdd2900351e0b0	Apalache	BagBagToSet	BagBagSub	True	Passed	Model Under Test Equivalent Model
1d6a059a23e1a6dbd5b0a5563b1ca953d08f1966	Apalache	BagBagToSet	BagBagSub	False	Passed	Model Under Test Equivalent Model
d58f664ae7121b01ab34a9c54ff21dc643312b25	Apalache	BagBagIn	BagBagSub	True	Passed	Model Under Test Equivalent Model
f872b2dee36aea099fa9f9e4e2d8bb5ebb29586b	Apalache	BagBagIn	BagBagSub	False	Passed	Model Under Test Equivalent Model
6b48dc2b828e6e49b9057df849777567e1babae8	Apalache	BagAddBag	BagBagSub	True	Passed	Model Under Test Equivalent Model
a5f4ed8318161cc98fd022038940dbc05a0857aa	Apalache	BagAddBag	BagBagSub	False	Passed	Model Under Test Equivalent Model
c979b078d51a3e1574de96eae0219a75b0d5cc08	Apalache	BagBagSub	BagBagSub	True	Passed	Model Under Test Equivalent Model
e9f0992cf1b6dbce1a403ad63b9627342e94fba4	Apalache	BagBagSub	BagBagSub	False	Passed	Model Under Test Equivalent Model
d517e5ac78b76de28cd21af16ae3a8b7ce76e5f9	Apalache	BagCopiesIn	BagBagSub	True	Passed	Model Under Test Equivalent Model
644ee08f7a9739386c3c8f8d5cfa47b397594051	Apalache	BagCopiesIn	BagBagSub	False	Passed	Model Under Test Equivalent Model
f52a3447ad8420ba1dbdcec7da13334145867818	Apalache	BagSubsetEqBag	BagBagSub	True	Passed	Model Under Test Equivalent Model
8f6702ea39d337ebcbdeed9b7cf782075e25cf4d	Apalache	BagSubsetEqBag	BagBagSub	False	Passed	Model Under Test Equivalent Model
cd8691c17622d8053b22c86a9022c57ee61cbe6c	Apalache	BagBagCardinality	BagBagSub	True	Passed	Model Under Test Equivalent Model
8d30dc6652b66bc8107ca281a599b6f39ff09575	Apalache	BagBagCardinality	BagBagSub	False	Passed	Model Under Test Equivalent Model
60b399eae46923e195b8ba71afd85d7536c3baa9	Apalache	BagBagOfAll	BagBagSub	True	Passed	Model Under Test Equivalent Model
a9a4e47661677d5222a3026a8a46aed6e52c650a	Apalache	BagBagOfAll	BagBagSub	False	Passed	Model Under Test Equivalent Model
43e902241af4098bb8773ab0ef2b5c6d427533d1	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	BagBagSub	True	Passed	Model Under Test Equivalent Model
a2d19e5ea63c4518c220001824d6fb60d4f30785	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	BagBagSub	False	Passed	Model Under Test Equivalent Model
2c97657fd24d0f83a3d3e341c7bc4117e3efc220	Apalache	SeqAppend	BagBagSub	True	Passed	Model Under Test Equivalent Model
c47a8474c16360839682035abc3107ee11ff891c	Apalache	SeqAppend	BagBagSub	False	Passed	Model Under Test Equivalent Model

Index

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