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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
b3121404907b39cf50f5e33916c9260e230d0525	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Boxed	OneLineComment	True	Passed	Model Under Test Equivalent Model
56f864d30dfd27a4541e669b26aa42ceebd73bbf	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Boxed	OneLineComment	False	Passed	Model Under Test Equivalent Model
303fd18bbdcd5e7edb6418e6ddb3278e426c706d	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Boxed	MultiLineComment	True	Passed	Model Under Test Equivalent Model
d877e69ea6d20e257a02e837820ed19072e56860	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Boxed	MultiLineComment	False	Passed	Model Under Test Equivalent Model
d0a7c23000693b09257a8dea9df735df7fa026e3	Apalache	Boxed	BoolTrue	True	Passed	Model Under Test Equivalent Model
6c7647dbc8a1cefb4283fa783b7bcb969c6918e6	Apalache	Boxed	BoolTrue	False	Passed	Model Under Test Equivalent Model
18ddd500ad3cdf75c329f317c645e11736267539	Apalache	Boxed	BoolFalse	True	Passed	Model Under Test Equivalent Model
400e779330355fb4567b4013e6d1cbb419ef41a8	Apalache	Boxed	BoolFalse	False	Passed	Model Under Test Equivalent Model
957bd8e1bbc932665fd6eb9b16b500a8c904418c	Apalache	Boxed	And	True	Passed	Model Under Test Equivalent Model
f726da81f621df9985a4e1da54729db8a35b6d3e	Apalache	Boxed	And	False	Passed	Model Under Test Equivalent Model
a036bfc2b99a7f58376bbffa0687a381e1233dbd	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Boxed	AndMultiLine	True	Passed	Model Under Test Equivalent Model
3530c92ddb47c2812c03545c3ff195290b8db27e	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Boxed	AndMultiLine	False	Passed	Model Under Test Equivalent Model
41dc2bb0967d518d99b39ec0d6f46e96e0abb077	Apalache	Boxed	Imply	True	Passed	Model Under Test Equivalent Model
a062804b2defdc1b79aa11b15bf4ae56d447daa5	Apalache	Boxed	Imply	False	Passed	Model Under Test Equivalent Model
8e712d990298a151ad1f71678cb02e37794cbbc0	Apalache	Boxed	Not	True	Passed	Model Under Test Equivalent Model
c9de56110cfd3efb6e8ebb4c809d52589c981530	Apalache	Boxed	Not	False	Passed	Model Under Test Equivalent Model
b50cbc7ef84a896832ef699858f5b2cd6886b95b	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Boxed	Or	True	Passed	Model Under Test Equivalent Model
a7e7dbd874596fe80d879afaedcc740b851d47f8	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Boxed	Or	False	Passed	Model Under Test Equivalent Model
3b67886b27e2d8dd9a40cc9d0c25254627c8a3dc	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Boxed	OrMultiLine	True	Passed	Model Under Test Equivalent Model
ba72f70e0f383f34a8f5d8294b1b0d054eb04a88	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Boxed	OrMultiLine	False	Passed	Model Under Test Equivalent Model
2852d4672fbbbc58463216c51c39b5632460d80e	Apalache	Boxed	Eq	True	Passed	Model Under Test Equivalent Model
f51f9aea340264bd12e2cb37f1277dd478368208	Apalache	Boxed	Eq	False	Passed	Model Under Test Equivalent Model
e6da0caf30ef69f0771e3aba043842f4ee1ccbf2	Apalache	Boxed	Ne	True	Passed	Model Under Test Equivalent Model
b14409249d126a97263422863370eeae25106306	Apalache	Boxed	Ne	False	Passed	Model Under Test Equivalent Model
1d44351a2f715b9df8ef545eb2a4e1061383d592	Apalache	Boxed	Let	True	Passed	Model Under Test Equivalent Model
c377f00ef97672465349b8c2b33ac1e66445e903	Apalache	Boxed	Let	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
ff2f68ebbc4c52472570c2751600e9ee97e41850	Apalache	Boxed	NotIn	True	Passed	Model Under Test Equivalent Model
2e74565d7dc68e62f66fa24f461dadf96fba7125	Apalache	Boxed	NotIn	False	Passed	Model Under Test Equivalent Model
1efb29054d4663c82ada6ab74a50566fb1e84c32	Apalache	Boxed	Exists	True	Passed	Model Under Test Equivalent Model
730dca1655c1e9a5243b2c91dc2158e8f106f46f	Apalache	Boxed	Exists	False	Passed	Model Under Test Equivalent Model
52c1177686336382ca015e68a7733848c96dcff4	Apalache	Boxed	Forall	True	Passed	Model Under Test Equivalent Model
838b0f401f8a7e52bd76661440681648d9efd3ba	Apalache	Boxed	Forall	False	Passed	Model Under Test Equivalent Model
e5758ae7a6ceb8eb382aaea28174384423cf3f8a	Apalache	Boxed	Choose	True	Passed	Model Under Test Equivalent Model
335b4ae42f4553e41a7ec5375355817aa99882ed	Apalache	Boxed	Choose	False	Passed	Model Under Test Equivalent Model
c09e7b8a6b55e00c3fe286a884d6a7ba476ac139	Apalache	Boxed	FunApp	True	Passed	Model Under Test Equivalent Model
9d0983c008e2934a23d43d22dd2a4a89a89c68e3	Apalache	Boxed	FunApp	False	Passed	Model Under Test Equivalent Model
ad42606209e55850cf2b9a2aa99ccd818f109dba	Apalache	Boxed	Prime	True	Passed	Model Under Test Equivalent Model
4ce214492980ee32823fee5af6a49349cb527302	Apalache	Boxed	Prime	False	Passed	Model Under Test Equivalent Model
baa1623ee8f3c71d85c4712e288821866f7c3118	Apalache	Boxed	NumGt	True	Passed	Model Under Test Equivalent Model
fa7f77edc0d52838d16f8c1a2da75917ea018a6d	Apalache	Boxed	NumGt	False	Passed	Model Under Test Equivalent Model
580cc5054162ac762ca187b6d2be7f71ade7dc46	Apalache	Boxed	NumGe	True	Passed	Model Under Test Equivalent Model
9882f5be469bdce7a83b5c3c06d01d4efb115574	Apalache	Boxed	NumGe	False	Passed	Model Under Test Equivalent Model
352f0b2253b09d55fced54926e613d8447554aa0	Apalache	Boxed	NumLt	True	Passed	Model Under Test Equivalent Model
c86203091a1c904777952b546db16ac85d1519d5	Apalache	Boxed	NumLt	False	Passed	Model Under Test Equivalent Model
69c9a1a5b1e754da0b68329670bbe717c6a0dd76	Apalache	Boxed	NumLe	True	Passed	Model Under Test Equivalent Model
43f99a58ed2064d27de53673d69150131eb6206c	Apalache	Boxed	NumLe	False	Passed	Model Under Test Equivalent Model
a725ad75a005e64b0b48f4ec335ce2fe3583bdcd	Apalache	Boxed	Def0	True	Passed	Model Under Test Equivalent Model
8d36fa76205a24e00b0928119ad850f1e7549dd1	Apalache	Boxed	Def0	False	Passed	Model Under Test Equivalent Model
297e429514e63ac1cc3d96c79b2fce61f6ddb1a1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Boxed	LetDef0	True	Passed	Model Under Test Equivalent Model
f748ef89933ce74001770331e80c4cac10208706	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Boxed	LetDef0	False	Passed	Model Under Test Equivalent Model
12dd1d403cc57e218c24568939cd3afbb8e7b017	Apalache	Boxed	Def1	True	Passed	Model Under Test Equivalent Model
a3837a41512caf13a5baeabada4b8e20e5a6268f	Apalache	Boxed	Def1	False	Passed	Model Under Test Equivalent Model
2ca77bd09110b995bca94957efa186b967580e2d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Boxed	LetDef1	True	Passed	Model Under Test Equivalent Model
b6fc1b610ec47a76ea2e4bbb396861382b5e9e58	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Boxed	LetDef1	False	Passed	Model Under Test Equivalent Model
c3f5c6d16edfbd3fff1d0ae72497be509162e899	Apalache	Boxed	Def2	True	Passed	Model Under Test Equivalent Model
ffc34a613b07d794ba2591c96b5608d17cdc7d7c	Apalache	Boxed	Def2	False	Passed	Model Under Test Equivalent Model
74a930912efac3cf8bb023cee05237cac4ce01ff	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Boxed	LetDef2	True	Passed	Model Under Test Equivalent Model
ef98d4ec8b8ca4e52fa33535608a20ff123d2b05	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Boxed	LetDef2	False	Passed	Model Under Test Equivalent Model
fa54cf770fbdf63592adea26535523cd2e0629e2	Apalache	Boxed	Def1Recursive	True	Passed	Model Under Test Equivalent Model
08349c57d402705385349c3cbb94153e3d807016	Apalache	Boxed	Def1Recursive	False	Passed	Model Under Test Equivalent Model
0c655edcc503554e218ad77446259f1261a12590	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Boxed	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
0b0e739cec219f80033de3e5a850e0f9078dcf5a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Boxed	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
a13a6cc8d4c46a1f9644b1d9f46c06b87e006a95	Apalache	Boxed	Extends	True	Passed	Model Under Test Equivalent Model
e8572f0dfb66c8905da8b0d261324da72f15b281	Apalache	Boxed	Extends	False	Passed	Model Under Test Equivalent Model
a56666a78cb3b65a43751bd2570746834ab66550	Apalache	Boxed	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
f999a1d92d5c3ad10729358e479c16de96a81e34	Apalache	Boxed	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
3eb0adb89f6f11b762b9d63fa7df4a9baa9b012a	Apalache	Boxed	Variable	True	Passed	Model Under Test Equivalent Model
14f01ad00bc7f600dd277a0cbb6c9e9bc2319d20	Apalache	Boxed	Variable	False	Passed	Model Under Test Equivalent Model
e3e620a621b1859c385ec33aae610cfd4000de4d	Apalache	Boxed	Constant	True	Passed	Model Under Test Equivalent Model
6ac7d4b5cabe51e2ddb400b0acb32fda2b04604a	Apalache	Boxed	Constant	False	Passed	Model Under Test Equivalent Model
505c1b9a11ed4b846e55dc0b8cc74630901c54ce	Apalache	Boxed	ConstantRank1	True	Passed	Model Under Test Equivalent Model
eb64378a777339054d56c3738555bce24607f832	Apalache	Boxed	ConstantRank1	False	Passed	Model Under Test Equivalent Model
9c01d0a7d100027c262e290cac89c56fa958c36e	Apalache	Boxed	Instance	True	Passed	Model Under Test Equivalent Model
d6c66f1ff4f072fea78d3da207e6036ae123db90	Apalache	Boxed	Instance	False	Passed	Model Under Test Equivalent Model
d24733ffcfca18a58edc295918d9617a2a592d39	Apalache	Boxed	InstanceWith	True	Passed	Model Under Test Equivalent Model
8ad6082405eebe737a9a8e0b9fb38281daa1e42b	Apalache	Boxed	InstanceWith	False	Passed	Model Under Test Equivalent Model
c9f7a08f65c8ed0bd66ad782512db27d2a304784	Apalache	Boxed	InstanceNamed	True	Passed	Model Under Test Equivalent Model
ad0325f35e2ae8974d6a3df27d767d1d18c1c272	Apalache	Boxed	InstanceNamed	False	Passed	Model Under Test Equivalent Model
93f3599377817c421746587fd54425340cff6b49	Apalache	Boxed	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
64e4fe86146bf3ad4deaa5caf0ee1099a7f85ea1	Apalache	Boxed	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
23a1e48936162fbf7f03da783377e8171ca812f3	Apalache	Boxed	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
c00db02bd250e2775f379d8828dc693cd9e2bfda	Apalache	Boxed	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
ecad16289a759e3e804ed52c411bd6b752c1b74d	Apalache	Boxed	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
64c8543668825330d61e3bff76523ca33385dce3	Apalache	Boxed	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
63ee3898e0d4bb3e2debd0ab0f26d024c61ac2ce	Apalache	Boxed	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
62b7d69d096561b5466040c86ca880930b68fe1c	Apalache	Boxed	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
b0fe40fde623c9d9c4419ea152d80d18e8883ad4	Apalache	Boxed	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
267f9c2cd2323c791702349101d27532af780d7f	Apalache	Boxed	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
d67380be4c97193e5b9424e3f2758cf9757049c7	Apalache	Boxed	Enabled	True	Passed	Model Under Test Equivalent Model
a330ada29638053d6d848105e521c38692ec8e2f	Apalache	Boxed	Enabled	False	Passed	Model Under Test Equivalent Model
aa084976132c09075335eee320a7e8b1d1c3d9cf	Apalache	Boxed	SubsetEq	True	Passed	Model Under Test Equivalent Model
039feda9b875ebcf1684f699d36a6d537e8ac28e	Apalache	Boxed	SubsetEq	False	Passed	Model Under Test Equivalent Model
5faa9f34e5510ffd2a34dad415a0035b1d16c6ab	Apalache	Boxed	IfCond	True	Passed	Model Under Test Equivalent Model
970e8369f5c4b3b4322d8639d02ceaf603cd742c	Apalache	Boxed	IfCond	False	Passed	Model Under Test Equivalent Model
abca9a517043807e3f682aa3b11028a6ecbfc8eb	Apalache	Boxed	IfThen	True	Passed	Model Under Test Equivalent Model
e7cc64aaeac8d15ed47bd16df9891ef0913a2991	Apalache	Boxed	IfThen	False	Passed	Model Under Test Equivalent Model
0abd39340aa146373597822fbd89237a6303bb6b	Apalache	Boxed	IfElse	True	Passed	Model Under Test Equivalent Model
6be131d8c4c20d78d053221b45af214bbfb42610	Apalache	Boxed	IfElse	False	Passed	Model Under Test Equivalent Model
7c2ed4461da22534f7594451f65f5c682484d3dd	Apalache	Boxed	Unchanged	True	Passed	Model Under Test Equivalent Model
615a11ccec6fd5633d9f5c6d512e31c7d10284ee	Apalache	Boxed	Unchanged	False	Passed	Model Under Test Equivalent Model
dfa0b127d89373c12c5ac44f80bec467a6ba1d9c	Apalache	Boxed	Equivalence	True	Passed	Model Under Test Equivalent Model
11218e5d82908d48d893c1b1fb3009029e1bfb23	Apalache	Boxed	Equivalence	False	Passed	Model Under Test Equivalent Model
7996a17cf1179191b80a9ddc63e915a3210d31d5	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Boxed	TlcEval	True	Passed	Model Under Test Equivalent Model
edd8c8c31f154e9a42e0af5aefd9bc7c152de8b3	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Boxed	TlcEval	False	Passed	Model Under Test Equivalent Model
071c3923265ed35ccf799af3174b45e2f93a8d4b	Apalache	Boxed	BagBagIn	True	Passed	Model Under Test Equivalent Model
31ba79d1ace67d5f76f143087dba4a6043382917	Apalache	Boxed	BagBagIn	False	Passed	Model Under Test Equivalent Model
68fdceca048e91228295d0ae5fbc9c7d4a3a908c	Apalache	Boxed	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
4d51a649f02d42d07ed97a6a48da5903dce91cca	Apalache	Boxed	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
4496829a996f0a1bb19b1707a5c956d29113dfe4	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)	Boxed	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
6a67605b7dab093c1370c68926e420c70671d75a	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)	Boxed	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
a039d377f222bd5139495635171f287de96eceea	Apalache	Boxed	SeqHead	True	Passed	Model Under Test Equivalent Model
8dc65aca6f913aa1b4e5941812a157f2ae906461	Apalache	Boxed	SeqHead	False	Passed	Model Under Test Equivalent Model

Index

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