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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
2e89a8e866b2efdaf2a4ffd5b82b0b1f7763980f	Apalache	And	In	True	Passed	Model Under Test Equivalent Model
5fc6ed7a397571c4f92cb75a88d66a04cb279098	Apalache	And	In	False	Passed	Model Under Test Equivalent Model
980caae626e2a6ed380ec18fd5e373284c51391e	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	In	True	Passed	Model Under Test Equivalent Model
8b1651bdd2b21c1ef98cb337e037f28cfbc00b3b	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	In	False	Passed	Model Under Test Equivalent Model
5514ca0c928c8c4656d8b3fc1c4a61ec934aa5cf	Apalache	Imply	In	True	Passed	Model Under Test Equivalent Model
aa8aff67a4537dae1cf8a94add4097b419c40f76	Apalache	Imply	In	False	Passed	Model Under Test Equivalent Model
bab431f0527ec6403e9e58eda301114f7ce55a19	Apalache	Not	In	True	Passed	Model Under Test Equivalent Model
74848245c7e45b65eb9e251b121981efd4032bbc	Apalache	Not	In	False	Passed	Model Under Test Equivalent Model
31290e5539d0ca4dcc682fe486e57a9c16c504ff	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	In	True	Passed	Model Under Test Equivalent Model
01601f9f43cc5c3670b541df67dc530040b2091c	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	In	False	Passed	Model Under Test Equivalent Model
7b922fde50f8e61e1dff9afbb353b204a3faa1f2	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	In	True	Passed	Model Under Test Equivalent Model
737a4577f99665a2a50af9af0a95d6078dca96e2	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	In	False	Passed	Model Under Test Equivalent Model
166b6ede1ae86eef81f9f35ac56d3c4b222aaafc	Apalache	AndProp	In	True	Passed	Model Under Test Equivalent Model
f99568c29398ee9cfed0f395341f1d81bac50f5d	Apalache	AndProp	In	False	Passed	Model Under Test Equivalent Model
97b8af6056eea606778c7466e634daa804fec346	Apalache	Boxed	In	True	Passed	Model Under Test Equivalent Model
b5068b95871d29cd358a0f6f3c9c95e4fbd700f5	Apalache	Boxed	In	False	Passed	Model Under Test Equivalent Model
ae87cf7c2498a847095de10fbad6d4d50cc7247e	Apalache	Eq	In	True	Passed	Model Under Test Equivalent Model
260c32951c09e042a65e3a7d68d9a2ab80e3f013	Apalache	Eq	In	False	Passed	Model Under Test Equivalent Model
a4a4c5af03db6cbc0492d253fd866d453b77f3a6	Apalache	Ne	In	True	Passed	Model Under Test Equivalent Model
30650ace5d22e82c512662f715bed398512d4adc	Apalache	Ne	In	False	Passed	Model Under Test Equivalent Model
7b381ca36d140705ea9dc070980d745f1ba39463	Apalache	Let	In	True	Passed	Model Under Test Equivalent Model
f0741947d3e4de05021b66e226547ca656a15efd	Apalache	Let	In	False	Passed	Model Under Test Equivalent Model
0c75d253f0230c2bd0aa1535a09457778a3d8230	Apalache	Set0	In	True	Passed	Model Under Test Equivalent Model
8145565c6c4fe5f1b8314ca0f0c52a7e45601285	Apalache	Set0	In	False	Passed	Model Under Test Equivalent Model
93ea9a9abe6015ac5acc4d53a46885af2b8b8588	Apalache	Set1	In	True	Passed	Model Under Test Equivalent Model
a79f613b9a4e9a221269d99cb05167b44c6b0ff0	Apalache	Set1	In	False	Passed	Model Under Test Equivalent Model
58cefc6e1e01dea6bba6d673d5fa242f8bc107e7	Apalache	Set2	In	True	Passed	Model Under Test Equivalent Model
4789a949d0fd33ce514cb1505af0a78ed8311ace	Apalache	Set2	In	False	Passed	Model Under Test Equivalent Model
6ac7f65417e4b3efa35364e2281ad8ccbf50b3c7	Apalache	Fun	In	True	Passed	Model Under Test Equivalent Model
9dfbc161d2e6f5bcfff2002bac037715117c72a6	Apalache	Fun	In	False	Passed	Model Under Test Equivalent Model
8523c13373a905b4738c273826f5e084b5c7462d	Apalache	In	In	True	Passed	Model Under Test Equivalent Model
d8ed2719b115301a59d67bc356a2585710e7b19c	Apalache	In	In	False	Passed	Model Under Test Equivalent Model
f5e4a112dd60cbc93dcc8cee4f91d9433e8c7396	Apalache	NotIn	In	True	Passed	Model Under Test Equivalent Model
70a0c955a70634dd26e1202780a60d2e609776e1	Apalache	NotIn	In	False	Passed	Model Under Test Equivalent Model
ca671148bca3af9e5b425b0f4cb3f8c23fc449d4	Apalache	Exists	In	True	Passed	Model Under Test Equivalent Model
d31001880926a1e6aa491e29ea925f2ae2485247	Apalache	Exists	In	False	Passed	Model Under Test Equivalent Model
7d041623fc348da6204e1afa23c78fbf5d0d497d	Apalache	Forall	In	True	Passed	Model Under Test Equivalent Model
43221f8838b935ecfc8b5e9bcbcdc77c02122350	Apalache	Forall	In	False	Passed	Model Under Test Equivalent Model
14f7225190b3860604eaaf2d517639397379de06	Apalache	Choose	In	True	Passed	Model Under Test Equivalent Model
6210b34c8e9f740a3f13328d0dcbc64a9679f997	Apalache	Choose	In	False	Passed	Model Under Test Equivalent Model
ef04c07e4ae6183d8cf048356622b21ea27569cd	Apalache	Record	In	True	Passed	Model Under Test Equivalent Model
1b0bd6e7ba997e3271e1730b0ff8c325af4caf36	Apalache	Record	In	False	Passed	Model Under Test Equivalent Model
25c21ddc7b263b9d3a65fc8806effc34c3831dd0	Apalache	Tuple	In	True	Passed	Model Under Test Equivalent Model
95f8301dd719ec48a1bd7285189b7ee0e5077f40	Apalache	Tuple	In	False	Passed	Model Under Test Equivalent Model
7c2f0eea16f0a3767241e0672894b1f14d00929f	Apalache	FunApp	In	True	Passed	Model Under Test Equivalent Model
e7c9545ed582dacb8b30a60267c81fc1fa82e9d3	Apalache	FunApp	In	False	Passed	Model Under Test Equivalent Model
c9bf9079b3157217cad6b02b760b7fba7c839524	Apalache	Except1Fun	In	True	Passed	Model Under Test Equivalent Model
7979e69b39cc831ae05cc48be4bc6e0b98326eaa	Apalache	Except1Fun	In	False	Passed	Model Under Test Equivalent Model
ecfb8d89905707823f157148a4694e5fea7404e8	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	In	True	Passed	Model Under Test Equivalent Model
209e6876a8747b7ddfaa03a643cce5cc4257b661	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	In	False	Passed	Model Under Test Equivalent Model
b92e286f4787c9d70fdd4a432b849fc4914e114c	Apalache	Except1Rec	In	True	Passed	Model Under Test Equivalent Model
6a4d36e8081d526eed8569af1782c4db3fdda5f0	Apalache	Except1Rec	In	False	Passed	Model Under Test Equivalent Model
2efd7beca87334798dda1a5dea5618acac1d1551	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	In	True	Passed	Model Under Test Equivalent Model
659118eb57c456f05ec9daabefbcc8f75877a58d	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	In	False	Passed	Model Under Test Equivalent Model
76b839f27367c1ce788174b0197f77fde6fb5a8d	Apalache	Except2Fun	In	True	Passed	Model Under Test Equivalent Model
11e423f23d2aeb001b24ac7fe72055065e985599	Apalache	Except2Fun	In	False	Passed	Model Under Test Equivalent Model
484a2d81e558f65312905ada7fb21c5ecc05a7dc	Apalache	Prime	In	True	Passed	Model Under Test Equivalent Model
129665e100479fde152207dae67277269a079c21	Apalache	Prime	In	False	Passed	Model Under Test Equivalent Model
07c363524226feed1247f53028afc3a7ca13ec8c	Apalache	DefFun	In	True	Passed	Model Under Test Equivalent Model
117ed40d8372f63a2c8f32ef4336b4615ebfa434	Apalache	DefFun	In	False	Passed	Model Under Test Equivalent Model
ef3231dce5011fc5bb40ff8ee57ab0a1293f0d1b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	In	True	Passed	Model Under Test Equivalent Model
b006c82f553328d4c2e93e4ed2550f39bf438505	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	In	False	Passed	Model Under Test Equivalent Model
7aabbd2a2f4dc2b1b7610dbf6c9012b1d372c4de	Apalache	DefFunRecursive	In	True	Passed	Model Under Test Equivalent Model
43d58a61606b246753858acd1bba14cffbd4518f	Apalache	DefFunRecursive	In	False	Passed	Model Under Test Equivalent Model
27201a4e35c07c7db4379d54a4204e81fd049255	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	In	True	Passed	Model Under Test Equivalent Model
1c5af45cbd53dd13501d697ec06ced9204fcc9e0	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	In	False	Passed	Model Under Test Equivalent Model
c6586b007ff925a410c136f41648c9789c919392	Apalache	Def0	In	True	Passed	Model Under Test Equivalent Model
3300083a8a9e41228986ca7e423ec71232d0a324	Apalache	Def0	In	False	Passed	Model Under Test Equivalent Model
d2e56eab8e683b1c45e2a4e16d36d7e1dae28eee	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	In	True	Passed	Model Under Test Equivalent Model
e29733d95adaad3d6ba4a43b7ab2cffa8f837f30	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	In	False	Passed	Model Under Test Equivalent Model
8c48c2ce27d95e36026732cf344aa00772584b4d	Apalache	Def1	In	True	Passed	Model Under Test Equivalent Model
cc55cd2c6f00d2200a27dcba102b2684c7d4fe6b	Apalache	Def1	In	False	Passed	Model Under Test Equivalent Model
9a52dcd1e30e61a805ade484b67cca247ad2abc0	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	In	True	Passed	Model Under Test Equivalent Model
c36225bfb4e713319b427040c483ffab2ce5d460	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	In	False	Passed	Model Under Test Equivalent Model
1f755318f0bd448374ff1c22eb15853614eff938	Apalache	Def2	In	True	Passed	Model Under Test Equivalent Model
9cbc475e0720aa5ebb65fd265719ce36fb1a5198	Apalache	Def2	In	False	Passed	Model Under Test Equivalent Model
7e9c9ef4f3c645a18241474d07be77950f64edf2	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	In	True	Passed	Model Under Test Equivalent Model
7784d91f84968b4b1536ce4ef6f0bd7a0cc81f5e	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	In	False	Passed	Model Under Test Equivalent Model
0f87d0e406b657c5cf22e96b06e02644c6a36d62	Apalache	Def1Recursive	In	True	Passed	Model Under Test Equivalent Model
db971ab073b63102af9c732edc9a0291d50a9024	Apalache	Def1Recursive	In	False	Passed	Model Under Test Equivalent Model
4d499529bf560c032fee4f409bbd1a027485de43	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	In	True	Passed	Model Under Test Equivalent Model
bb0147efa47f826a6cb7bb82bfb6928dd91b20d5	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	In	False	Passed	Model Under Test Equivalent Model
36ca1d41b354aefccfb6441f49109267be26b3c1	Apalache	Extends	In	True	Passed	Model Under Test Equivalent Model
8b6658339e843d01a744d25f91c6684ed338a55b	Apalache	Extends	In	False	Passed	Model Under Test Equivalent Model
76c8fe40fcf1a7dbd58e223516b0bffd55818c97	Apalache	ExtendsInDifferentFolder	In	True	Passed	Model Under Test Equivalent Model
aafbbe3100184fa74a97be5be39fde35a2613ea0	Apalache	ExtendsInDifferentFolder	In	False	Passed	Model Under Test Equivalent Model
6138818309569e97e39ac25b73eb6f0fe94ae04b	Apalache	Variable	In	True	Passed	Model Under Test Equivalent Model
927e43645e04879155ebc1d5beab8c02e55485cb	Apalache	Variable	In	False	Passed	Model Under Test Equivalent Model
e572aaa3ee794cca7b5219a488532590a144ce9d	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	In	True	Passed	Model Under Test Equivalent Model
529eb1e828143a892fca4eefeec32229423c599d	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	In	False	Passed	Model Under Test Equivalent Model
a93ecc1de2e1d9139a8f0617738558bda9e4720e	Apalache	Constant	In	True	Passed	Model Under Test Equivalent Model
9792170799911ca4b153dab021dec9c0ad241cf4	Apalache	Constant	In	False	Passed	Model Under Test Equivalent Model
fa18214ca2017d550e6469c2efa06acb4c1731de	Apalache	ConstantRank1	In	True	Passed	Model Under Test Equivalent Model
26c5555bdb0620134e583e2246a3ac360c77f8c4	Apalache	ConstantRank1	In	False	Passed	Model Under Test Equivalent Model
d9630b8fbec2e412972b6f77874857725307d242	Apalache	Instance	In	True	Passed	Model Under Test Equivalent Model
c146271feea511d59c106c6a9a1c4902bf7ddf7b	Apalache	Instance	In	False	Passed	Model Under Test Equivalent Model
656c1c18edec5fcb1ab99330ac9e0146933a0b6b	Apalache	InstanceWith	In	True	Passed	Model Under Test Equivalent Model
3f9c84f45229f1ee34bc97e77c5492b2c52f2b32	Apalache	InstanceWith	In	False	Passed	Model Under Test Equivalent Model
478d4596bb87fa7396f562a7ff3d96cb657e7a08	Apalache	InstanceNamed	In	True	Passed	Model Under Test Equivalent Model
68f7fcda358247c7e02ed87f083ea64b96f1190b	Apalache	InstanceNamed	In	False	Passed	Model Under Test Equivalent Model
819879b7357b026d839599f318896c744b532b47	Apalache	InstanceNamedWith	In	True	Passed	Model Under Test Equivalent Model
b67688d59f7302e5ae7816682700cf3f9cf34bb9	Apalache	InstanceNamedWith	In	False	Passed	Model Under Test Equivalent Model
08c0a3cef343a293bd5eb808323c8ed6c442250f	Apalache	InstanceInFolder	In	True	Passed	Model Under Test Equivalent Model
17b4bc90e6523eb871546b558b687b327054e523	Apalache	InstanceInFolder	In	False	Passed	Model Under Test Equivalent Model
0f3b96564806556be4bc7ba75844b4c9a52f1d8f	Apalache	InstanceWithInFolder	In	True	Passed	Model Under Test Equivalent Model
95dd7265bb6c171f74ce9a9a5112c07cdd6759c2	Apalache	InstanceWithInFolder	In	False	Passed	Model Under Test Equivalent Model
72430ba799d7e991343ed8aa272dcc6dbd8a3d27	Apalache	InstanceNamedInFolder	In	True	Passed	Model Under Test Equivalent Model
87c4f56facabc325157bf8b843a66181163050e3	Apalache	InstanceNamedInFolder	In	False	Passed	Model Under Test Equivalent Model
79a558b72a90f7c5879d4e4cdbdf813b5794b33a	Apalache	InstanceNamedWithInFolder	In	True	Passed	Model Under Test Equivalent Model
3a31ed015eff9aadb607520b5aee39cc7d3e0415	Apalache	InstanceNamedWithInFolder	In	False	Passed	Model Under Test Equivalent Model
3a087653ffaf5703b7ce8f0954e0e219f4600430	Apalache	Enabled	In	True	Passed	Model Under Test Equivalent Model
d522fa0077ce34b9baa0845f943182947054c342	Apalache	Enabled	In	False	Passed	Model Under Test Equivalent Model
698f0e719536ac2bed8efd376ca9432b55f31c06	Apalache	Assume	In	True	Passed	Model Under Test Equivalent Model
05c24fc729ea07bea57b84b0865c23bc77ea84eb	Apalache	Assume	In	False	Passed	Model Under Test Equivalent Model
3b5389fffedb4facda477ca0b4614f784040ebe7	Apalache	AssumeNamed	In	True	Passed	Model Under Test Equivalent Model
6ac1cd850e7be5a94c180a272bc2defe606d5db8	Apalache	AssumeNamed	In	False	Passed	Model Under Test Equivalent Model
119cfef18be70ffeeea9496ef7a8f9ae7e919d3f	Apalache	Lambda	In	True	Passed	Model Under Test Equivalent Model
a409c2089a4afd620edb783886b5edea39e5712c	Apalache	Lambda	In	False	Passed	Model Under Test Equivalent Model
184800cab8abc4ece178fd7f14a7c0d0eb651e2e	Apalache	IfCond	In	True	Passed	Model Under Test Equivalent Model
95ee28ba014e76e9a21441249b9d0c5848ae5409	Apalache	IfCond	In	False	Passed	Model Under Test Equivalent Model
8d63379d117ad8fae6a020881feb54ec1242dd5e	Apalache	IfThen	In	True	Passed	Model Under Test Equivalent Model
4e7a377ea14ca4e1667f872d4ea2e0f03f9dc816	Apalache	IfThen	In	False	Passed	Model Under Test Equivalent Model
7e0e6c6367e98c1e3ddfa3c53f78785f92c81c11	Apalache	IfElse	In	True	Passed	Model Under Test Equivalent Model
a393f0a6ba4fb73d123e90b644b9294c8b2218a9	Apalache	IfElse	In	False	Passed	Model Under Test Equivalent Model
362d84ef158476d53f6f31fc2ca7ed41436a90fc	Apalache	Unchanged	In	True	Passed	Model Under Test Equivalent Model
d455de00f151cc556105cea8c81303cc547f6d6a	Apalache	Unchanged	In	False	Passed	Model Under Test Equivalent Model
c6f407b962fa3a6b4eab9706d38d15e2f10bc48b	Apalache	Equivalence	In	True	Passed	Model Under Test Equivalent Model
5be8ca6e7903f8db6ce41995a5c6f2279d359c8a	Apalache	Equivalence	In	False	Passed	Model Under Test Equivalent Model
7f5f68f8fc05a57bbf326c85ce0c41305984e8ba	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	In	True	Passed	Model Under Test Equivalent Model
f7bcd11eba114332e43ac64863566c56b0171223	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	In	False	Passed	Model Under Test Equivalent Model
8fc650f5986df8b8ca0b35c9afff46ffbfe4e2af	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	In	True	Passed	Model Under Test Equivalent Model
fae292342b0a93dd6f8378fee1a544aea0b78a3b	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	In	False	Passed	Model Under Test Equivalent Model
e4f06c366f747d6c7a566cf49286bebc5f8d35df	Apalache	BagBagIn	In	True	Passed	Model Under Test Equivalent Model
6be8d7d2a9474e354eddf55f963688f3f2bfc387	Apalache	BagBagIn	In	False	Passed	Model Under Test Equivalent Model
830ecd07a32098af9df98ecccd8dbae164634f22	Apalache	BagCopiesIn	In	True	Passed	Model Under Test Equivalent Model
e2735497b5f3bc31afa252dd4da1cb560b986c0b	Apalache	BagCopiesIn	In	False	Passed	Model Under Test Equivalent Model
690cd76285ff0ebed61765d49a7f958f35077805	Apalache	SeqAppend	In	True	Passed	Model Under Test Equivalent Model
800a857faf98ac3d3f7aec8b8727ea07108e50e4	Apalache	SeqAppend	In	False	Passed	Model Under Test Equivalent Model

Index

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