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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
3db8c45c9d7b192d7c849a7611ebbb9dbecf9775	Apalache	Eq	TupleEmpty	True	Passed	Model Under Test Equivalent Model
416f30977f6e439a0041f5bd79d68bbdfbc9a105	Apalache	Eq	TupleEmpty	False	Passed	Model Under Test Equivalent Model
ff8264c8788b987d8ceeae5c9fe674c2b0eadcee	Apalache	Ne	TupleEmpty	True	Passed	Model Under Test Equivalent Model
98ce93f6470fcd30f6e3884132d097d5db2d22bc	Apalache	Ne	TupleEmpty	False	Passed	Model Under Test Equivalent Model
74340ccc150151054ac448024f270aac209e1866	Apalache	Let	TupleEmpty	True	Passed	Model Under Test Equivalent Model
065cfac74aea21d7813618399a487289721f761f	Apalache	Let	TupleEmpty	False	Passed	Model Under Test Equivalent Model
04c17e8e6fe23e008726c1f1a138b2c99c061762	Apalache	Set0	TupleEmpty	True	Passed	Model Under Test Equivalent Model
d22e31d8a26163360beaba40c15e41e22ccbe605	Apalache	Set0	TupleEmpty	False	Passed	Model Under Test Equivalent Model
1ca15cb78ccce5c4aa28082908f5915db44c8511	Apalache	Set1	TupleEmpty	True	Passed	Model Under Test Equivalent Model
c688f9afd2742389d9bfdb29f9e42007078cb554	Apalache	Set1	TupleEmpty	False	Passed	Model Under Test Equivalent Model
2f3c2a45d5c517d708597199587dbd7adeafcd4c	Apalache	Set2	TupleEmpty	True	Passed	Model Under Test Equivalent Model
4336372eae4ce5073eff1b008b1526ca1b94642a	Apalache	Set2	TupleEmpty	False	Passed	Model Under Test Equivalent Model
51872252506a4907c074671105543e77a0913a0d	Apalache	Fun	TupleEmpty	True	Passed	Model Under Test Equivalent Model
3bf475748e78ba6e28824f0214ae59c073a897c2	Apalache	Fun	TupleEmpty	False	Passed	Model Under Test Equivalent Model
4a813a1da83a1b10f959a2ca13a47d0663c64393	Apalache	In	TupleEmpty	True	Passed	Model Under Test Equivalent Model
254b1b243c78d8d78ddb8176f743de81d7a86a99	Apalache	In	TupleEmpty	False	Passed	Model Under Test Equivalent Model
92de7ad93e782ea946b028177a1e837b67cc6845	Apalache	NotIn	TupleEmpty	True	Passed	Model Under Test Equivalent Model
8dc2e5e62a8dbe721e419a054e108f3670532901	Apalache	NotIn	TupleEmpty	False	Passed	Model Under Test Equivalent Model
5d1927e8e06e9155ce839317f0d8275624e648e7	Apalache	Record	TupleEmpty	True	Passed	Model Under Test Equivalent Model
1b9c7a4807d03b5b96931a787370bff7c37a5b11	Apalache	Record	TupleEmpty	False	Passed	Model Under Test Equivalent Model
17449fd4c0dd45f3cf5cad552efb781790e05592	Apalache	Tuple	TupleEmpty	True	Passed	Model Under Test Equivalent Model
b741e539363c40365ac130044551e310649128bf	Apalache	Tuple	TupleEmpty	False	Passed	Model Under Test Equivalent Model
cdf78ceed0b53146c6672f9140c27fd4bb68da5b	Apalache	FunApp	TupleEmpty	True	Failed: TLC reports an error if there is an attempt to apply a function with value not from its domain. Apalache is unable to detect such situation and returns arbitrary value.	Model Under Test Equivalent Model
a4604139020fc219015253d4a621cfdf1a4c7cef	Apalache	FunApp	TupleEmpty	False	Failed: TLC reports an error if there is an attempt to apply a function with value not from its domain. Apalache is unable to detect such situation and returns arbitrary value.	Model Under Test Equivalent Model
1b80418d75c0f0644d7909116df20d2ce863a964	Apalache	Except0	TupleEmpty	True	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
ea53af8dd5d5e1b94168ffe2b33a00e5becc32a0	Apalache	Except0	TupleEmpty	False	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
7d01c8c08b1d4cac9bd7a4720a4a4d2e0c555a1e	Apalache	Except1Fun	TupleEmpty	True	Passed	Model Under Test Equivalent Model
d01631db577a1df9c2f5239961068655ff62863a	Apalache	Except1Fun	TupleEmpty	False	Passed	Model Under Test Equivalent Model
abd2dd74ff60d37877d27b7f0d9aa57906247b12	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	TupleEmpty	True	Passed	Model Under Test Equivalent Model
e54fa567606b320a65d10581f199f4bc1cae558f	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	TupleEmpty	False	Passed	Model Under Test Equivalent Model
923f322eb292dbe2463c2f6d4092865171621cc7	Apalache	Except1Rec	TupleEmpty	True	Passed	Model Under Test Equivalent Model
67bc1c9b696bbacbe53d04b8f45123d770aa1fbd	Apalache	Except1Rec	TupleEmpty	False	Passed	Model Under Test Equivalent Model
9ddb5f14afa6043d8e7669abc805b487234618bf	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	TupleEmpty	True	Passed	Model Under Test Equivalent Model
4833a5a7a1178f5e36ca9127915b4ef2442a073f	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	TupleEmpty	False	Passed	Model Under Test Equivalent Model
448986f8c3af71d94441b2eb16632370d9df7dde	Apalache	Except2Fun	TupleEmpty	True	Passed	Model Under Test Equivalent Model
0a81e6a66a869be46fdad839df19f379c9316c32	Apalache	Except2Fun	TupleEmpty	False	Passed	Model Under Test Equivalent Model
a0efb9330fa37c6b054b34d1fadff967b9f38813	Apalache	Prime	TupleEmpty	True	Passed	Model Under Test Equivalent Model
666d51a01d1e37c3c4fa42b282e6966bd04804ff	Apalache	Prime	TupleEmpty	False	Passed	Model Under Test Equivalent Model
c086dca0bde6d0c05a585b74ff98c91e21250626	Apalache	DefFun	TupleEmpty	True	Passed	Model Under Test Equivalent Model
4f370fe07ccf538abd51622c24ebc16fa0c93b19	Apalache	DefFun	TupleEmpty	False	Passed	Model Under Test Equivalent Model
234936037c911c27784692dbdc5a83f8fb349f85	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	TupleEmpty	True	Passed	Model Under Test Equivalent Model
078fda8e72fbcc55f215f4dafaa8aa89970f7941	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	TupleEmpty	False	Passed	Model Under Test Equivalent Model
e6b9d839bc2f3b2b2092e03f9f82ff7ff23e4837	Apalache	DefFunRecursive	TupleEmpty	True	Passed	Model Under Test Equivalent Model
8988e401be36fb37b932328e362f40faa56a0534	Apalache	DefFunRecursive	TupleEmpty	False	Passed	Model Under Test Equivalent Model
45b6049de8b1003d89eee910bee9710b1bc96e0b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	TupleEmpty	True	Passed	Model Under Test Equivalent Model
f20f2d736932d05103262ac0603fcf873224170a	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	TupleEmpty	False	Passed	Model Under Test Equivalent Model
4733ac85afd94283d51cb406abe269ee0d5676cc	Apalache	Def0	TupleEmpty	True	Passed	Model Under Test Equivalent Model
8d1710d39938ea4d0e10696eae390a342923333d	Apalache	Def0	TupleEmpty	False	Passed	Model Under Test Equivalent Model
09ef2acb4e296a01c1607e433d9719d1b0c9864b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	TupleEmpty	True	Passed	Model Under Test Equivalent Model
21a33231ddeee88e8cf2d4ea68c3410dfdc5ef1a	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	TupleEmpty	False	Passed	Model Under Test Equivalent Model
b8377c78ae8df4c710eefc8c2b147982de7edaae	Apalache	Def1	TupleEmpty	True	Passed	Model Under Test Equivalent Model
ec5b32414851a72be5fece50ddc0b0af6e71dcdc	Apalache	Def1	TupleEmpty	False	Passed	Model Under Test Equivalent Model
abc58d2dacbdc205b8aa69aa9b46376877daf85a	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	TupleEmpty	True	Passed	Model Under Test Equivalent Model
d26d8b5d4d5ccdb9066da33cb89050d95ad3d41e	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	TupleEmpty	False	Passed	Model Under Test Equivalent Model
8a5bfdecc0ddf65cfbbd26285176bbb76f542b3d	Apalache	Def2	TupleEmpty	True	Passed	Model Under Test Equivalent Model
c1fc90a14deb9ad9611717d07906ef2835c41004	Apalache	Def2	TupleEmpty	False	Passed	Model Under Test Equivalent Model
a1f4441bdb8e3a2942c0e032a68c9181f2d9caa7	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	TupleEmpty	True	Passed	Model Under Test Equivalent Model
8f0c93a2f301edf4095bf3f274313ed4b3c33974	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	TupleEmpty	False	Passed	Model Under Test Equivalent Model
c72e9b8d6949694e49d3b25b3be73d1894898c3e	Apalache	Def1Recursive	TupleEmpty	True	Passed	Model Under Test Equivalent Model
27679c921134ee2ae41585124ab040173ed11975	Apalache	Def1Recursive	TupleEmpty	False	Passed	Model Under Test Equivalent Model
f67d54ea054081fe06fc319f017c3f2fe8b82e2e	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	TupleEmpty	True	Passed	Model Under Test Equivalent Model
f29e3ace815e581ad572a83e2fd9359124fd85fe	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	TupleEmpty	False	Passed	Model Under Test Equivalent Model
6bfc89f35adeb4b5405bbf59934f2b3810ebd9de	Apalache	Extends	TupleEmpty	True	Passed	Model Under Test Equivalent Model
5dd23dda1364fa607a8daa54a466fcbf6eaee180	Apalache	Extends	TupleEmpty	False	Passed	Model Under Test Equivalent Model
6263942d6dd82178bb59fb458c90518e1a64910a	Apalache	ExtendsInDifferentFolder	TupleEmpty	True	Passed	Model Under Test Equivalent Model
c91d3a46f2f38e3bc470ad2e556e0bf00ebd4ae4	Apalache	ExtendsInDifferentFolder	TupleEmpty	False	Passed	Model Under Test Equivalent Model
9e8185e52f209e6075daaed1ada2ea4d5af2fd28	Apalache	Variable	TupleEmpty	True	Passed	Model Under Test Equivalent Model
5bfe95d1d908fee0565cf9ae2518d23b8ebb85b6	Apalache	Variable	TupleEmpty	False	Passed	Model Under Test Equivalent Model
edb9c21ef7840c1e19a4bbc082765b9b5c84dc81	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	TupleEmpty	True	Passed	Model Under Test Equivalent Model
4216af29431218cd70686905e06693171ae3c83d	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	TupleEmpty	False	Passed	Model Under Test Equivalent Model
ce38612b87f91d04b1ce82f26d1f14b5b11b7847	Apalache	Constant	TupleEmpty	True	Passed	Model Under Test Equivalent Model
f3d91be799b0d7e8bee63cc480356f03f77b03ce	Apalache	Constant	TupleEmpty	False	Passed	Model Under Test Equivalent Model
84aebb5c09f7c82a7075b11566375092ed970003	Apalache	ConstantRank1	TupleEmpty	True	Passed	Model Under Test Equivalent Model
b01d182f6ad1eec22dd7384dd2588ae01b86d9c8	Apalache	ConstantRank1	TupleEmpty	False	Passed	Model Under Test Equivalent Model
ca955c468330e0ed59e12c7b67b71a05858b1b09	Apalache	Instance	TupleEmpty	True	Passed	Model Under Test Equivalent Model
4e6893f1e1616be8d79a6029b47d06ccd707490a	Apalache	Instance	TupleEmpty	False	Passed	Model Under Test Equivalent Model
d54e0190c8bb867239c0c628ebdaf9ec9b8c8bee	Apalache	InstanceWith	TupleEmpty	True	Passed	Model Under Test Equivalent Model
becc20ead3c0be05d0e56aa6820d1ef8e60ee913	Apalache	InstanceWith	TupleEmpty	False	Passed	Model Under Test Equivalent Model
133f6b0a6fd5ce96d31aae5d7ae71bf83d09fc3a	Apalache	InstanceNamed	TupleEmpty	True	Passed	Model Under Test Equivalent Model
61cfbcdb9ca2dab663313ae82adf36190430a137	Apalache	InstanceNamed	TupleEmpty	False	Passed	Model Under Test Equivalent Model
9cf4cf676a308016161fe2e020860325fb88863f	Apalache	InstanceNamedWith	TupleEmpty	True	Passed	Model Under Test Equivalent Model
7c5a45a69073e336fef59d8a53022d28c1230603	Apalache	InstanceNamedWith	TupleEmpty	False	Passed	Model Under Test Equivalent Model
aedb93fccecef095d3799887b4a1a46c70b4796b	Apalache	InstanceInFolder	TupleEmpty	True	Passed	Model Under Test Equivalent Model
5377dd4f6b21bb422b30abfdb8cb02eb64c241a7	Apalache	InstanceInFolder	TupleEmpty	False	Passed	Model Under Test Equivalent Model
d374d362e26246e359a410d5e512ff9b54169d86	Apalache	InstanceWithInFolder	TupleEmpty	True	Passed	Model Under Test Equivalent Model
3330539dc1ff2112709a31621956e469df99aa80	Apalache	InstanceWithInFolder	TupleEmpty	False	Passed	Model Under Test Equivalent Model
d1bc8e43089ba78da9013efbcd372a2a7a3ef85e	Apalache	InstanceNamedInFolder	TupleEmpty	True	Passed	Model Under Test Equivalent Model
7becab07361b860b25d2e12846cdbc01f6cc022f	Apalache	InstanceNamedInFolder	TupleEmpty	False	Passed	Model Under Test Equivalent Model
6780860c707a3edf1cf9f186ee02b00f3d7fd634	Apalache	InstanceNamedWithInFolder	TupleEmpty	True	Passed	Model Under Test Equivalent Model
c4ee4f8bbb9a8e2ea6c2aacc9f7404e3ccae1a74	Apalache	InstanceNamedWithInFolder	TupleEmpty	False	Passed	Model Under Test Equivalent Model
185a73404334cb2f9e93e476ff531f47fad99872	Apalache	Lambda	TupleEmpty	True	Passed	Model Under Test Equivalent Model
607dff5c04cb01163a580e28374c9136baa21a2b	Apalache	Lambda	TupleEmpty	False	Passed	Model Under Test Equivalent Model
4eb3d2768d1257ee2fbacfbcedc387788836cafa	Apalache	IfThen	TupleEmpty	True	Passed	Model Under Test Equivalent Model
34acba4f3333b637de07190e280134a2d8d8403a	Apalache	IfThen	TupleEmpty	False	Passed	Model Under Test Equivalent Model
f0a7101d75a73811af424c96f610be999f645649	Apalache	IfElse	TupleEmpty	True	Passed	Model Under Test Equivalent Model
46da69983fcee6b3fab5fa9f39026c3707896e1d	Apalache	IfElse	TupleEmpty	False	Passed	Model Under Test Equivalent Model
67c5b0e7e0e2c53660b8766c4f85fa7ef4197250	Apalache	Unchanged	TupleEmpty	True	Passed	Model Under Test Equivalent Model
2feba8bd6617b2c53760fef8e4fa118e8fac3ff8	Apalache	Unchanged	TupleEmpty	False	Passed	Model Under Test Equivalent Model
fb172ada74afa0f04cc114ea6b7b1e937b9dbfd7	Apalache	SeqLen	TupleEmpty	True	Passed	Model Under Test Equivalent Model
c2c4e8ad95f86d3553bf58b73ec3cf24f6b77e3b	Apalache	SeqLen	TupleEmpty	False	Passed	Model Under Test Equivalent Model
831bfbbf14bf0c3d22f99117b611d86d7dd187f9	Apalache	SeqConcat	TupleEmpty	True	Passed	Model Under Test Equivalent Model
7acc549d089fe981f6e13852e93fa5b9a2ef6b1b	Apalache	SeqConcat	TupleEmpty	False	Passed	Model Under Test Equivalent Model
e94a681743512ecb0c0e618227c7a5a99367d41a	Apalache	SeqSelectSeq	TupleEmpty	True	Passed	Model Under Test Equivalent Model
9a54e89f41a04d94d2ea5b3992997498d5e67f49	Apalache	SeqSelectSeq	TupleEmpty	False	Passed	Model Under Test Equivalent Model
241439717be0ec493be023b444bdb8c4262c80ed	Apalache	SeqSubSeq	TupleEmpty	True	Failed: TLC requires the second argument of SeqSubSeq to be in domain of the sequence and returns an error otherwise. Apalache always returns some sequence	Model Under Test Equivalent Model
40db46ac9db7ea5895d1f9d252f78ddbeed1317f	Apalache	SeqSubSeq	TupleEmpty	False	Failed: TLC requires the second argument of SeqSubSeq to be in domain of the sequence and returns an error otherwise. Apalache always returns some sequence	Model Under Test Equivalent Model
88aadf19af2a0e12207bab28432286b686070bbf	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	TupleEmpty	True	Passed	Model Under Test Equivalent Model
5ed3242a3333a410e46f1aad715e766df023863e	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	TupleEmpty	False	Passed	Model Under Test Equivalent Model
d96e2d8a814848784d216e8671a0f35ec3fff6af	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	TupleEmpty	True	Passed	Model Under Test Equivalent Model
1a5e179cf6dd818a3c94debffde46e5942412b11	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	TupleEmpty	False	Passed	Model Under Test Equivalent Model
4277d9a1dc0ec7d7672508f04d60df470613409d	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	TupleEmpty	True	Passed	Model Under Test Equivalent Model
3408691c0aa395996e323bd7c9f0cb303c35aae9	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	TupleEmpty	False	Passed	Model Under Test Equivalent Model
fd7d0fc11000c07671dce387f991a92f94da4e8f	Apalache	BagBagIn	TupleEmpty	True	Passed	Model Under Test Equivalent Model
99e9f719fa23590c2e96925435d7bf5ec4563ff2	Apalache	BagBagIn	TupleEmpty	False	Passed	Model Under Test Equivalent Model
fbc8648f55a5d8f85a6bdd3b04d6849f9b8aad47	Apalache	BagCopiesIn	TupleEmpty	True	Passed	Model Under Test Equivalent Model
aecd7d68091f02a33e2a53e5f7fa5d38e9f99e87	Apalache	BagCopiesIn	TupleEmpty	False	Passed	Model Under Test Equivalent Model
4cf1156e005f4d434d61c44c22b5fa2461c7235e	Apalache	SeqHead	TupleEmpty	True	Failed: Head of empty sequence results in error in TLC. Apalache is unable to detect such an error and instead returns arbitrary value	Model Under Test Equivalent Model
13b8a5df936f0a06bfc14d43a657bcbec061b694	Apalache	SeqHead	TupleEmpty	False	Failed: Head of empty sequence results in error in TLC. Apalache is unable to detect such an error and instead returns arbitrary value	Model Under Test Equivalent Model
cd16e1f8c4d71514b565193260eedc22a3183858	Apalache	SeqTail	TupleEmpty	True	Failed: Tail of empty sequence results in error in TLC. Apalache is unable to detect such an error and instead returns arbitrary value	Model Under Test Equivalent Model
fc8253e6317e8891a7069c098f558350613a8404	Apalache	SeqTail	TupleEmpty	False	Failed: Tail of empty sequence results in error in TLC. Apalache is unable to detect such an error and instead returns arbitrary value	Model Under Test Equivalent Model
0f13194c40f0e06801e17e8ecc47eb526fd5731c	Apalache	SeqAppend	TupleEmpty	True	Passed	Model Under Test Equivalent Model
d5d1fff76a91fb83ac119f7f009df62e450ac195	Apalache	SeqAppend	TupleEmpty	False	Passed	Model Under Test Equivalent Model

Index

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