Tests by case feature Def1Recursive; CLI Option: -workers 1

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
ea48db06937a6882ec517073fd3f1414491960f1	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Def1Recursive	OneLineComment	True	Passed	Model Under Test Equivalent Model
dbbdece6aa172cc6b86410d7174151de47c08192	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Def1Recursive	OneLineComment	False	Passed	Model Under Test Equivalent Model
ca57ae4d57ea059491ef11865856749661e06b25	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Def1Recursive	MultiLineComment	True	Passed	Model Under Test Equivalent Model
517aa9d96197f6dd04225f880d2837e573bc9af9	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Def1Recursive	MultiLineComment	False	Passed	Model Under Test Equivalent Model
fcfca5d10ba7a7cb0527488d26d9f687a0c36f84	Apalache	Def1Recursive	BoolTrue	True	Passed	Model Under Test Equivalent Model
715fb92740a8f0ee7b4869c95a8930eb69a55e12	Apalache	Def1Recursive	BoolTrue	False	Passed	Model Under Test Equivalent Model
210328ac8de01513df49f2342922519fca997c0f	Apalache	Def1Recursive	BoolFalse	True	Passed	Model Under Test Equivalent Model
02aa6d744ba3aaeb7a441ba5574862e940ad3a38	Apalache	Def1Recursive	BoolFalse	False	Passed	Model Under Test Equivalent Model
a302768f9f112f9c42bb736771ffba595a8892e7	Apalache	Def1Recursive	BoolSet	True	Passed	Model Under Test Equivalent Model
3461e6c5b2c0e5da5a29a503c815ae60fb68c3d0	Apalache	Def1Recursive	BoolSet	False	Passed	Model Under Test Equivalent Model
968dd79c8b3bc18ac153e19aaf82cd7d8e67c1a3	Apalache	Def1Recursive	And	True	Passed	Model Under Test Equivalent Model
194416f2f0d5974dd004c3538a58bb3bd1eaadc4	Apalache	Def1Recursive	And	False	Passed	Model Under Test Equivalent Model
90ac98052e419c83dd8e635e070f81193ce2e6bb	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Def1Recursive	AndMultiLine	True	Passed	Model Under Test Equivalent Model
baec8af64a5260961d6d763f605d4d40a242aa38	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Def1Recursive	AndMultiLine	False	Passed	Model Under Test Equivalent Model
dfe6fedef438b13056d1e27db406aeef1da57780	Apalache	Def1Recursive	Imply	True	Passed	Model Under Test Equivalent Model
dff62cc1c9a4767b176563e6adce20b221c648a7	Apalache	Def1Recursive	Imply	False	Passed	Model Under Test Equivalent Model
f76acc7f791b910d516d32df3d75eae199426317	Apalache	Def1Recursive	Not	True	Passed	Model Under Test Equivalent Model
c5b5eab4ef1cbe2ac0e61d2a809767679c320b5c	Apalache	Def1Recursive	Not	False	Passed	Model Under Test Equivalent Model
3c86cdcb2ff5181cbadaeb4b9d851d186a38533e	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Def1Recursive	Or	True	Passed	Model Under Test Equivalent Model
372a0cffb3214223c037e15d7a790c4c63b4bc06	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Def1Recursive	Or	False	Passed	Model Under Test Equivalent Model
7b7f14dcbbd8a4ea6702295c5f646b77bd81a711	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Def1Recursive	OrMultiLine	True	Passed	Model Under Test Equivalent Model
0ea28e79d3b6775ee2d548bd1121bafee4222496	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Def1Recursive	OrMultiLine	False	Passed	Model Under Test Equivalent Model
b7281ea8a75cb8a9dede3272aa831ae367b86950	Apalache	Def1Recursive	AndProp	True	Passed	Model Under Test Equivalent Model
91a2820d5aaf07b4a0cf84b31f4b6507651c8642	Apalache	Def1Recursive	AndProp	False	Passed	Model Under Test Equivalent Model
700686892478b230bbe283a468506893a0efaf04	Apalache	Def1Recursive	Boxed	True	Failed: There is a known TLC bug (https://github.com/tlaplus/tlaplus/issues/720), which causes TLC to report an error, when a parameterized operator is used to specify a property	Model Under Test Equivalent Model
f804f1d679b5f3101dd683d0c661e28532e4e8b2	Apalache	Def1Recursive	Boxed	False	Failed: There is a known TLC bug (https://github.com/tlaplus/tlaplus/issues/720), which causes TLC to report an error, when a parameterized operator is used to specify a property	Model Under Test Equivalent Model
ec5f1edf5156b09747a4f67df7c976961abdcb31	Apalache	Def1Recursive	Eq	True	Passed	Model Under Test Equivalent Model
d119d9ccac3dd10ade19e785f4bda997110e23c2	Apalache	Def1Recursive	Eq	False	Passed	Model Under Test Equivalent Model
7e2999f3a8afdacabfa967587d36ca6054f3eb53	Apalache	Def1Recursive	Ne	True	Passed	Model Under Test Equivalent Model
6364753ad08d2c30a0a407391e59a4eaf026ce16	Apalache	Def1Recursive	Ne	False	Passed	Model Under Test Equivalent Model
334adb6f6e8778fd470d27705d44a646703eb57d	Apalache	Def1Recursive	Let	True	Passed	Model Under Test Equivalent Model
eca83004c2c921750bb94f3825d125c8bf0f37ec	Apalache	Def1Recursive	Let	False	Passed	Model Under Test Equivalent Model
235150a026234021497e0f56e62fbe56ea4025c2	Apalache	Def1Recursive	SetEmpty	True	Passed	Model Under Test Equivalent Model
00832a6e0756c644432878905a51f4b6011fcde6	Apalache	Def1Recursive	SetEmpty	False	Passed	Model Under Test Equivalent Model
4300aaba09e14522de4db4d30221f3fde60b74bc	Apalache	Def1Recursive	Set0	True	Passed	Model Under Test Equivalent Model
a9fc7103ba3f9b6b6981fbdf9d0f998bd26b9608	Apalache	Def1Recursive	Set0	False	Passed	Model Under Test Equivalent Model
7949800f588db802aebdbaa2117b87b95f72c854	Apalache	Def1Recursive	Set1	True	Passed	Model Under Test Equivalent Model
152cbbc9f31bb43e0c307360d6e290c01a0bf5a0	Apalache	Def1Recursive	Set1	False	Passed	Model Under Test Equivalent Model
a3eed04f3cf08e82225e6ba461a72d7d304ccb4d	Apalache	Def1Recursive	Set2	True	Passed	Model Under Test Equivalent Model
dce87082448bad2395bae7dcf79b452aabf7b784	Apalache	Def1Recursive	Set2	False	Passed	Model Under Test Equivalent Model
f62e5863c0e3866cf4c503af86b61f72a18c6389	Apalache	Def1Recursive	Fun	True	Passed	Model Under Test Equivalent Model
881dfc2698485c4dc73b1090045ebf5281b8e08b	Apalache	Def1Recursive	Fun	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
c54762180727e8d1156a79721281723e776b88cb	Apalache	Def1Recursive	NotIn	True	Passed	Model Under Test Equivalent Model
21fd4e75a9ee8fa8edcc0e4af46a3c01e63d3851	Apalache	Def1Recursive	NotIn	False	Passed	Model Under Test Equivalent Model
27dc70e56ab9f817e577c041e76a43079ed0be23	Apalache	Def1Recursive	Exists	True	Passed	Model Under Test Equivalent Model
4999f1d5016f12816eaca77be4afb84aa8b2fbae	Apalache	Def1Recursive	Exists	False	Passed	Model Under Test Equivalent Model
c039ab74d4659c127d90b5b8d3fa8d188df9e01d	Apalache	Def1Recursive	Forall	True	Passed	Model Under Test Equivalent Model
6fce7ce8bb78979ffb5a29007cec33d6218f1359	Apalache	Def1Recursive	Forall	False	Passed	Model Under Test Equivalent Model
9b824b758764f835742c9abed0078b062c6ed389	Apalache	Def1Recursive	Choose	True	Passed	Model Under Test Equivalent Model
4d823e5393db24d46c34bdd19072f17a70558599	Apalache	Def1Recursive	Choose	False	Passed	Model Under Test Equivalent Model
0f60f563acb5887dac5fd3ea854667969e0ff023	Apalache	Def1Recursive	Record	True	Passed	Model Under Test Equivalent Model
2a978fcc25641ce3506fab63b4602c0188a2f574	Apalache	Def1Recursive	Record	False	Passed	Model Under Test Equivalent Model
aba3f29205f12f7997bb92b4d5fc9b6ad55e9fdb	Apalache	Def1Recursive	Tuple	True	Passed	Model Under Test Equivalent Model
82321468aacc9743f300ea14e6249f6dc40f76b5	Apalache	Def1Recursive	Tuple	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
dd975a35b914f809a30c9c9dc363290719227a95	Apalache	Def1Recursive	FunApp	True	Passed	Model Under Test Equivalent Model
5beb04191d177ee547b9529dc81502c883b38b32	Apalache	Def1Recursive	FunApp	False	Passed	Model Under Test Equivalent Model
ce7d8a2eeb506a85fd5e5cf024569fd41bff85f7	Apalache	Def1Recursive	Prime	True	Passed	Model Under Test Equivalent Model
633c99ecd42f38e58a7dec16d47b96ab75110cc1	Apalache	Def1Recursive	Prime	False	Passed	Model Under Test Equivalent Model
58b734ae9cba892e4f6c1ec2464462dcf434e03a	Apalache	Def1Recursive	NumZero	True	Passed	Model Under Test Equivalent Model
0537d2675a4d0c411e0701f55db4795139e78121	Apalache	Def1Recursive	NumZero	False	Passed	Model Under Test Equivalent Model
01739315978992a3c394912dcd59eb738c3bb0b6	Apalache	Def1Recursive	NumOne	True	Passed	Model Under Test Equivalent Model
0a077b972c54c3989a9c896e4061fec1771a494f	Apalache	Def1Recursive	NumOne	False	Passed	Model Under Test Equivalent Model
331b588b9f215cec6eef80e7fe40c07c94a33bff	Apalache	Def1Recursive	NumMaxInt	True	Passed	Model Under Test Equivalent Model
8c173dbcf67600a22505bda8273519d17dcd2dee	Apalache	Def1Recursive	NumMaxInt	False	Passed	Model Under Test Equivalent Model
ac2d35e3906084ae60ca10784c5cc6a4dee4516d	Apalache	Def1Recursive	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
af14915c4d4790de1e7d81412fdf3170b6d89bdf	Apalache	Def1Recursive	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
a509918dd6f62e22298a444cdba3378d36c83d63	Apalache	Def1Recursive	NumPlus	True	Passed	Model Under Test Equivalent Model
9322fae92e2a132a739d0c68fe2bd29a7175a788	Apalache	Def1Recursive	NumPlus	False	Passed	Model Under Test Equivalent Model
4c639d9e9d6fc0d811ab6f60755cf3a36946eb93	Apalache	Def1Recursive	NumMinus	True	Passed	Model Under Test Equivalent Model
e2a7c6daefb3c40ede5a509db720f4b44adb45db	Apalache	Def1Recursive	NumMinus	False	Passed	Model Under Test Equivalent Model
b73f88064a200e1429a5858a1e2f4bbca77639b4	Apalache	Def1Recursive	NumMul	True	Passed	Model Under Test Equivalent Model
c3a2c801ff97d3f4e5d62e3bd563f35f2d096560	Apalache	Def1Recursive	NumMul	False	Passed	Model Under Test Equivalent Model
20833862a8282601fc7011f32655cdbdb66db860	Apalache	Def1Recursive	NumDiv	True	Passed	Model Under Test Equivalent Model
83672cb5adca81b1f42a8d4422d6ddf3006640e0	Apalache	Def1Recursive	NumDiv	False	Passed	Model Under Test Equivalent Model
658cd73baef25e62a026c904e85b632f66e0a442	Apalache	Def1Recursive	NumMod	True	Passed	Model Under Test Equivalent Model
4678eeb68bea9397a56794da21b4d1867a29c6ae	Apalache	Def1Recursive	NumMod	False	Passed	Model Under Test Equivalent Model
188d857f706f6b61cdf0ee20f88a63fcbc69081f	Apalache	Def1Recursive	NumPow	True	Passed	Model Under Test Equivalent Model
22fa6042b47f84e0c9eec8978248edf5a9fa7271	Apalache	Def1Recursive	NumPow	False	Passed	Model Under Test Equivalent Model
08b1fbdb9f4831d2bdf936532c76302349377b72	Apalache	Def1Recursive	NumGt	True	Passed	Model Under Test Equivalent Model
3d4426d39f7707c3964d137acf5bd6fb0bf6f8a3	Apalache	Def1Recursive	NumGt	False	Passed	Model Under Test Equivalent Model
36f7a1137b330172072e62a3190472a9fe651ff8	Apalache	Def1Recursive	NumGe	True	Passed	Model Under Test Equivalent Model
3a737475a74b44d12fffaa6cb7ff720eb8e23257	Apalache	Def1Recursive	NumGe	False	Passed	Model Under Test Equivalent Model
778b4ce8f9cfc3c6d692174e8bfa706fddeff4c3	Apalache	Def1Recursive	NumLt	True	Passed	Model Under Test Equivalent Model
cebc7c0850340c2c29f87491840f39e336bddcb7	Apalache	Def1Recursive	NumLt	False	Passed	Model Under Test Equivalent Model
88ec959f852211bfe5aba600991f0712d97c6a45	Apalache	Def1Recursive	NumLe	True	Passed	Model Under Test Equivalent Model
771b166a4b58557ba60e4b6d2f2d168207ddf5a8	Apalache	Def1Recursive	NumLe	False	Passed	Model Under Test Equivalent Model
629562529fe7ce8ea09e79aaf5e724e8b6de7d3b	Apalache	Def1Recursive	DefFun	True	Passed	Model Under Test Equivalent Model
6f321bfd8d14be49a098e4baa424cf270566e307	Apalache	Def1Recursive	DefFun	False	Passed	Model Under Test Equivalent Model
c89dd6244cec70929fdbd0366ec9669aefbe7af6	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1Recursive	LetDefFun	True	Passed	Model Under Test Equivalent Model
c7f5ca208bec615b9bd2c69755f8283afc13a000	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1Recursive	LetDefFun	False	Passed	Model Under Test Equivalent Model
01a2c1535e3e8cecef8ee2898961b14947a72fad	Apalache	Def1Recursive	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
85bf85a104452081d79ae406970d7df494d138a8	Apalache	Def1Recursive	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
3c596faf132bc6b0048b2657e68352988661f914	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1Recursive	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
f7249ddb590466d46bb0666539bd9e6c8e092a38	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1Recursive	LetDefFunRecursive	False	Passed	Model Under Test Equivalent Model
53aad11ab3cf06192ab08dcc1a6c4ccfb281594d	Apalache	Def1Recursive	Def0	True	Passed	Model Under Test Equivalent Model
9469f6ba82df200241f3d0d028516d7011262b04	Apalache	Def1Recursive	Def0	False	Passed	Model Under Test Equivalent Model
e8d6f9a02a56258740b89cbec859ce25d4fabccd	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1Recursive	LetDef0	True	Passed	Model Under Test Equivalent Model
eb073ed5399e2478d26c683bcb83eadfb4d9d9dd	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1Recursive	LetDef0	False	Passed	Model Under Test Equivalent Model
8d7bcd5917e00313967f398d17a9b83fdff9a081	Apalache	Def1Recursive	Def1	True	Passed	Model Under Test Equivalent Model
2d122504c15c2cdf959a7aaaa7345ab7ac052523	Apalache	Def1Recursive	Def1	False	Passed	Model Under Test Equivalent Model
7ffa067b3f84c65ff7fddeebea936a265b717ac0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1Recursive	LetDef1	True	Passed	Model Under Test Equivalent Model
0c551240c23e8d14ba3ec9b19451db8be1d9e408	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1Recursive	LetDef1	False	Passed	Model Under Test Equivalent Model
68c685422c1d6a9b25a471ec4814f2194f2760e8	Apalache	Def1Recursive	Def2	True	Passed	Model Under Test Equivalent Model
a15b7b9d9e7a814b037887455e008564a04cd919	Apalache	Def1Recursive	Def2	False	Passed	Model Under Test Equivalent Model
b25133af006526c055b31d7fee4a400aca7124fb	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1Recursive	LetDef2	True	Passed	Model Under Test Equivalent Model
65b889ce82a4cbbcb390272447b2a67a36644a6d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1Recursive	LetDef2	False	Passed	Model Under Test Equivalent Model
82a20a5ad02ffecf62ec90bfafe0c0ee3dab2c20	Apalache	Def1Recursive	Def1Recursive	True	Passed	Model Under Test Equivalent Model
7c8e3e55e49e5a185e0cca0e20b82e681eedc5a2	Apalache	Def1Recursive	Def1Recursive	False	Passed	Model Under Test Equivalent Model
da8e137936e93f5f28dea840e66a7cb945bee9e7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1Recursive	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
bc1c2f74e0156a7cdf378cf610031873ec7cedd0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1Recursive	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
41b3d1caec5c4dd6c997685acbde82d8a9fb3dbd	Apalache	Def1Recursive	Extends	True	Passed	Model Under Test Equivalent Model
0e5f6767d460ef4ee1521e109208f656f638ac9b	Apalache	Def1Recursive	Extends	False	Passed	Model Under Test Equivalent Model
a925b5b0d4a0f1777f593ad2823ee5609e5d6fc5	Apalache	Def1Recursive	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
9c78881a16eb14bb597af129fce47b879c98532e	Apalache	Def1Recursive	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
8630152294c422865ec47f4a10c52cb45c7e942d	Apalache	Def1Recursive	Variable	True	Passed	Model Under Test Equivalent Model
49ba40a05e63339c434b7be4b41176ce6fc84b3a	Apalache	Def1Recursive	Variable	False	Passed	Model Under Test Equivalent Model
6590bc6e331e5cf454f3f54dabd238f35094fef0	Apalache	Def1Recursive	Constant	True	Passed	Model Under Test Equivalent Model
8435457fb1bdbdf2be5dd269ef5b2709413a967d	Apalache	Def1Recursive	Constant	False	Passed	Model Under Test Equivalent Model
9ce8966b7bc8d72d8033698ab4d3827d448508a2	Apalache	Def1Recursive	ConstantModelValue	True	Passed	Model Under Test Equivalent Model
c8e21d1a308c29d09334d472cbc581d6a1dc835f	Apalache	Def1Recursive	ConstantModelValue	False	Passed	Model Under Test Equivalent Model
045202c75ecda7ecc6c54110937d0be3596357aa	Apalache	Def1Recursive	ConstantRank1	True	Passed	Model Under Test Equivalent Model
e9c2ac4457d1f029b9c9b3d2aac6fbe07e7fe7b0	Apalache	Def1Recursive	ConstantRank1	False	Passed	Model Under Test Equivalent Model
3bd38e4f72fe251a26c24d53950da794a3a57d95	Apalache	Def1Recursive	Instance	True	Passed	Model Under Test Equivalent Model
a10821031f0adc0c8b8d7f8c2e896d3a07bd9db3	Apalache	Def1Recursive	Instance	False	Passed	Model Under Test Equivalent Model
63de6574650c5edce454604cd67e57040960ea33	Apalache	Def1Recursive	InstanceWith	True	Passed	Model Under Test Equivalent Model
563bdbe79e591f6da5737727a778c322ddd9ae18	Apalache	Def1Recursive	InstanceWith	False	Passed	Model Under Test Equivalent Model
0eb0c759e0d6434f60249209fe4174d5384a8ea3	Apalache	Def1Recursive	InstanceNamed	True	Passed	Model Under Test Equivalent Model
5a71a0b801616d1d9b488c3e536843cdbedd9c6c	Apalache	Def1Recursive	InstanceNamed	False	Passed	Model Under Test Equivalent Model
21435816a521e597688c667db0e27beca0f0f89d	Apalache	Def1Recursive	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
fc3a9f17c9d4345e1c96a77ca039e478495b7dff	Apalache	Def1Recursive	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
00a1d44f1d614f6f3ba3251c7372066d55ec554a	Apalache	Def1Recursive	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
eb8053bc41226d1c29c80fef710d2d2aa11d1460	Apalache	Def1Recursive	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
29017165b926c1a20efb7edc01b8f495a02e4d62	Apalache	Def1Recursive	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
e2f93ca905ec16d9a7bed7dc4dd7b96792ee0973	Apalache	Def1Recursive	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
1fbffaf5bf27ce475916d160d84bcc27e13a3fa9	Apalache	Def1Recursive	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
69184d1656bf56f525acdfe14474b88c680737ed	Apalache	Def1Recursive	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
9f7d1a90dec5d11299705f59293ceaed674b23a6	Apalache	Def1Recursive	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
74855f265003c08c7f805ce4988cddb1238d4974	Apalache	Def1Recursive	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
5db2f894c17bf8d0d5b86a42938f14b43cc5cb61	Apalache	Def1Recursive	Enabled	True	Passed	Model Under Test Equivalent Model
f3833f6c9fc832ff8facf17f4d13f01626090635	Apalache	Def1Recursive	Enabled	False	Passed	Model Under Test Equivalent Model
28434f038094674b834dd1bf2c5d5e619dac6f68	Apalache	Def1Recursive	Cross2	True	Passed	Model Under Test Equivalent Model
43892743957ab247cd1fc07582b577688a355124	Apalache	Def1Recursive	Cross2	False	Passed	Model Under Test Equivalent Model
36772aad66772081331eac96ee8bc0d53c6c1224	Apalache	Def1Recursive	Cross3	True	Passed	Model Under Test Equivalent Model
766c91051ae78aa80747ef159b4dc502f470e690	Apalache	Def1Recursive	Cross3	False	Passed	Model Under Test Equivalent Model
ccf0b400bb17640efc4a2881730c709a29b27c55	TLC with reduction strategy: Plug Feature: For finite R replace [D -> R] with explicit function set enumeration; for infinite R replace (f \in [D -> R]) with conjunction (DOMAIN f = D /\ (\A x \in D : f[x] \in R))	Def1Recursive	FunSet	True	Passed	Model Under Test Equivalent Model
edd1098e51d722aa51da6da3c4bf355d788449d0	TLC with reduction strategy: Plug Feature: For finite R replace [D -> R] with explicit function set enumeration; for infinite R replace (f \in [D -> R]) with conjunction (DOMAIN f = D /\ (\A x \in D : f[x] \in R))	Def1Recursive	FunSet	False	Passed	Model Under Test Equivalent Model
0d85bab6f7349c0829438061a50ec4837553cdf3	TLC with reduction strategy: Plug Feature: For finite R replace [field : R] with explicit function set enumeration; for infinite R replace (f \in [field : R]) with conjunction (DOMAIN f = {'field'} /\ f['field'] \in R)	Def1Recursive	RecordSet	True	Passed	Model Under Test Equivalent Model
f0bc94d957d88d85fe1bc88d149cd8b560d7caed	TLC with reduction strategy: Plug Feature: For finite R replace [field : R] with explicit function set enumeration; for infinite R replace (f \in [field : R]) with conjunction (DOMAIN f = {'field'} /\ f['field'] \in R)	Def1Recursive	RecordSet	False	Passed	Model Under Test Equivalent Model
f7d3056d42f9865e7bc1b86fc2b931aebc7264df	Apalache	Def1Recursive	SetDiff	True	Passed	Model Under Test Equivalent Model
52c7556a15efad7a07cb2efc0dc424fc484a3bb5	Apalache	Def1Recursive	SetDiff	False	Passed	Model Under Test Equivalent Model
d68fd2407b2f9657802fa8075bf0feab31052f53	Apalache	Def1Recursive	SetUnion	True	Passed	Model Under Test Equivalent Model
5d3f27821a0a0dfec20bc7256be8973f35720ba5	Apalache	Def1Recursive	SetUnion	False	Passed	Model Under Test Equivalent Model
9cd1fec336442448eedd63db555565062ad9ec1b	Apalache	Def1Recursive	SetIntersect	True	Passed	Model Under Test Equivalent Model
de9bf1fce12fe1bcb0d91d9951b8190faa99b66d	Apalache	Def1Recursive	SetIntersect	False	Passed	Model Under Test Equivalent Model
10d34e8ac77a2d48cebc6c502e3c451172e59ddd	Apalache	Def1Recursive	SubsetEq	True	Passed	Model Under Test Equivalent Model
b6336fa9f27ea140e1b4a2ed40401fda1ce59c19	Apalache	Def1Recursive	SubsetEq	False	Passed	Model Under Test Equivalent Model
8de65950fe8a5727fcb888d5b98eea238f9a636d	Apalache	Def1Recursive	IfCond	True	Passed	Model Under Test Equivalent Model
5a9fe16142f8b2dae886e7d3d71cba13807e5402	Apalache	Def1Recursive	IfCond	False	Passed	Model Under Test Equivalent Model
32df71760d0d32777e1c1118d40a96a652a70560	Apalache	Def1Recursive	IfThen	True	Passed	Model Under Test Equivalent Model
57c72688c75b5de8d71cbbadafd74cf72e674c2b	Apalache	Def1Recursive	IfThen	False	Passed	Model Under Test Equivalent Model
3e58506fad9a3813147923c7e65ee095b1775bad	Apalache	Def1Recursive	IfElse	True	Passed	Model Under Test Equivalent Model
4cdd296859d7ccfd66597a51a85fd895d226a0c2	Apalache	Def1Recursive	IfElse	False	Passed	Model Under Test Equivalent Model
3275cd3597ee9b6c3e392c23a647ae90a0ef4291	Apalache	Def1Recursive	Subset	True	Passed	Model Under Test Equivalent Model
003923df3d4b0a247ba52aadf6459c5ad19ed97f	Apalache	Def1Recursive	Subset	False	Passed	Model Under Test Equivalent Model
63b38980542b218032898ffb27e1be81b1906561	Apalache	Def1Recursive	Domain	True	Passed	Model Under Test Equivalent Model
e5e6127489ca52b92d98fd6be8f676e715783e25	Apalache	Def1Recursive	Domain	False	Passed	Model Under Test Equivalent Model
2ff8edfc592708981f8941ccb26a072ce2c04893	Apalache	Def1Recursive	Union	True	Passed	Model Under Test Equivalent Model
4cb9910c30cd66b8375b664a7023d8f225fdf8f3	Apalache	Def1Recursive	Union	False	Passed	Model Under Test Equivalent Model
6902edbd8b2fe372ca580316541ec47dce199fe7	Apalache	Def1Recursive	Unchanged	True	Passed	Model Under Test Equivalent Model
22293de36917c31c810aa5422c57c8d9e051915d	Apalache	Def1Recursive	Unchanged	False	Passed	Model Under Test Equivalent Model
f3510acd94a463ff0af76c9cd00c8f877c33ab1e	Apalache	Def1Recursive	Equivalence	True	Passed	Model Under Test Equivalent Model
9eb5c1f78288b77c4e3e86cbafa574769189aab4	Apalache	Def1Recursive	Equivalence	False	Passed	Model Under Test Equivalent Model
c0d4035af84e13a484eb769313d03a909a7c9a6e	Apalache	Def1Recursive	StringEmpty	True	Passed	Model Under Test Equivalent Model
642268eb65e1ae3491095d60aaa4c9f787815f90	Apalache	Def1Recursive	StringEmpty	False	Passed	Model Under Test Equivalent Model
b8bdbeb2de673325bdae4b65bfa11038880b265e	Apalache	Def1Recursive	String	True	Passed	Model Under Test Equivalent Model
881754f3a17fcca2292bb55d2747c225e5ea8446	Apalache	Def1Recursive	String	False	Passed	Model Under Test Equivalent Model
b34ee9f48191a1654473a4d379b78bcf37cb325c	Apalache	Def1Recursive	SeqLen	True	Passed	Model Under Test Equivalent Model
5683094fbad7e8f223c0eca18a30cb44c0c53e62	Apalache	Def1Recursive	SeqLen	False	Passed	Model Under Test Equivalent Model
a440b597d076dfc4c8afe9104af07e3693312dc9	Apalache	Def1Recursive	SeqConcat	True	Passed	Model Under Test Equivalent Model
2e736f7bd7d690f0cdd219b7bec248d8c134dc1f	Apalache	Def1Recursive	SeqConcat	False	Passed	Model Under Test Equivalent Model
f167c50ea629db74e9e78749218b223cf2542368	Apalache	Def1Recursive	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
77400583aac0950cef55082320bbd8153fb317f7	Apalache	Def1Recursive	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
9dcdb183ff7cdf0e9e80794e442a6c76d608f8eb	Apalache	Def1Recursive	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
74a5a24884b13752a41718f3afc455d7112f1a06	Apalache	Def1Recursive	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
1db2f61c0f91fc72bf0743968cb3abcca4ae41ce	TLC with reduction strategy: Plug 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	Def1Recursive	NumRange	True	Passed	Model Under Test Equivalent Model
75fa8d9e39928d60365a315017b4061cb608d0a9	TLC with reduction strategy: Plug 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	Def1Recursive	NumRange	False	Passed	Model Under Test Equivalent Model
2748b69fe1f68b3da7d9de1f6610c02ee6534213	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Def1Recursive	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
8f1475065551560fc2e98165b7d5d77550a9a593	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Def1Recursive	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
9405c8665d0d2ddda72f0bd44f4cde33c905054a	TLC with reduction strategy: Plug Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g \|-> IF u \in DomF THEN f[u] ELSE g[x]]	Def1Recursive	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
5ecf6c3cf94308e1004c8d4e1c35dab4592bdec3	TLC with reduction strategy: Plug Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g \|-> IF u \in DomF THEN f[u] ELSE g[x]]	Def1Recursive	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
c2d3a4264ea95cf8fce198e02e5649097bf12593	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Def1Recursive	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
5fd8ec35101c1d4b8eb3479157e00fc024c29c86	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Def1Recursive	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
3d40efc753dc3a4e28fdcd923a14e189bc1f92c1	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Def1Recursive	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
35b336ff3c168643c3dcac8a84a26a82c13e9ea2	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Def1Recursive	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
20d33143ccdd4fc6dac2efde9476ab40515dbf6e	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Def1Recursive	TlcEval	True	Passed	Model Under Test Equivalent Model
10518aaa86c8de6ceb8ef65225a93706a7f987ea	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Def1Recursive	TlcEval	False	Passed	Model Under Test Equivalent Model
df8d95dfca95377dab11c414eef973ac9f56108b	Apalache	Def1Recursive	BagBagToSet	True	Passed	Model Under Test Equivalent Model
63d10da56c302536a7eff89125c028d80f9e9482	Apalache	Def1Recursive	BagBagToSet	False	Passed	Model Under Test Equivalent Model
88f9572c5fc9c0224e48491c81f9f83a12aadf01	Apalache	Def1Recursive	BagSetToBag	True	Passed	Model Under Test Equivalent Model
d62a77460de7dbd08f4b9c7b36a09de912577d9d	Apalache	Def1Recursive	BagSetToBag	False	Passed	Model Under Test Equivalent Model
a72d0c7c6a98cc6577a3321576bcc855dd0d6ae8	Apalache	Def1Recursive	BagBagIn	True	Passed	Model Under Test Equivalent Model
dd8be872b7f2a8310418419dd0e7b4679cf14f40	Apalache	Def1Recursive	BagBagIn	False	Passed	Model Under Test Equivalent Model
77a5c2365295dff134ed184d5018e563ab9c952d	Apalache	Def1Recursive	BagEmptyBag	True	Passed	Model Under Test Equivalent Model
11ad2dbb7ac47f433cd0a6ffad03f14feb736186	Apalache	Def1Recursive	BagEmptyBag	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
7e859f7e2f794699aa3e07899630fa46342eab26	Apalache	Def1Recursive	BagBagSub	True	Passed	Model Under Test Equivalent Model
679d43b7d9a25a541ec2feaaaf94b9231357b0e3	Apalache	Def1Recursive	BagBagSub	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
44b43a0a9b370c9569c9d6356ce7fe31a195dfe6	Apalache	Def1Recursive	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
d69a55bcd39808b434b7ac956276322a8705be71	Apalache	Def1Recursive	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
db64182d14a08568215935110e60a08bb75b328f	Apalache	Def1Recursive	BagBagUnion	True	Passed	Model Under Test Equivalent Model
7595766e1c6f3059a7b994da463d3ceb92f7e943	Apalache	Def1Recursive	BagBagUnion	False	Passed	Model Under Test Equivalent Model
101c5149b0cc557afc286001a5ab3760737832f2	Apalache	Def1Recursive	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
59f3d81a04e4e4f531bed54ac43a09213771d783	Apalache	Def1Recursive	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
07297c33b96d883d4bcebd276a838a875e33c8a2	Apalache	Def1Recursive	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
9f41deb79db5d0cb5a614c71711f73d149e5e72c	Apalache	Def1Recursive	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
7999ea96d14d50aaf222ee26c423b91a0de017d9	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Def1Recursive	BagSubBag	True	Passed	Model Under Test Equivalent Model
f94d6e1c009392129e03105ea6010979c0ed99e1	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Def1Recursive	BagSubBag	False	Passed	Model Under Test Equivalent Model
70072c1d261301b9d06d2b3b4ac71e7c4628107b	TLC with reduction strategy: Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)	Def1Recursive	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
f308dc4b1aac34c6d2d25c139f7f1d516a5964d8	TLC with reduction strategy: Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)	Def1Recursive	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
97b6fd0943d29ff5179f5ca59282d870bc5b1068	Apalache	Def1Recursive	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
2ba5741ab43ac89e1210854dbad5380afc71d01a	Apalache	Def1Recursive	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
c21b7b266cac30622435f3814e911619f20be3ce	Apalache	Def1Recursive	SeqHead	True	Passed	Model Under Test Equivalent Model
d3f3b939dbaf69f2786a4571f0a995cb503713bc	Apalache	Def1Recursive	SeqHead	False	Passed	Model Under Test Equivalent Model
dfabd37ef951872c6c08a76034ccacfe67f05f31	Apalache	Def1Recursive	SeqTail	True	Passed	Model Under Test Equivalent Model
e1ce7892e98235af8bd53547fb12b6c4f8d5f82b	Apalache	Def1Recursive	SeqTail	False	Passed	Model Under Test Equivalent Model
7837d3a3c9e20ba820c6c317097ed5594a8b1d08	Apalache	Def1Recursive	SeqAppend	True	Passed	Model Under Test Equivalent Model
ddac5f95754cd18c7d01ae810128898457962e80	Apalache	Def1Recursive	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

Tests by case feature Def1Recursive; CLI Option: -workers 1