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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
c61675e65b6356999dfb1ed4ef3d92c14b5711e2	Apalache	AndProp	Boxed	True	Passed	Model Under Test Equivalent Model
745765a375a9b1c3ef0767ddaa55d26ef88e45df	Apalache	AndProp	Boxed	False	Passed	Model Under Test Equivalent Model
a8ada6aa9cb0fd5000402744c25d5cf284f41a9c	Apalache	Def0	Boxed	True	Passed	Model Under Test Equivalent Model
4935456101a16ee9b74c367dd4027ceebff20f5f	Apalache	Def0	Boxed	False	Passed	Model Under Test Equivalent Model
ebfc33eff1b8ad16fe92ed6a179ac451d0dac89e	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Boxed	True	Failed: TLC expects temporal properties to be specified directly without using operators or LET expression. Otherwise it reports an error	Model Under Test Equivalent Model
a1dc6ecff969a30f8b2a4fd310b4f54b0b3ff77a	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Boxed	False	Failed: TLC expects temporal properties to be specified directly without using operators or LET expression. Otherwise it reports an error	Model Under Test Equivalent Model
b2764bdde952b581ea57a9b4cc3c9d15e04cefa9	Apalache	Def1	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
41b3104fca3384e9525d42ba801375965de689db	Apalache	Def1	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
d369dc83ff2a09bdbbf5ebead912c851aa096528	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Boxed	True	Passed	Model Under Test Equivalent Model
c37e9ee02851013fa72d288184b7b1a3cab45c0d	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Boxed	False	Passed	Model Under Test Equivalent Model
147e8a4cffe636b65800f847b08f93ff7768dd49	Apalache	Def2	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
1374059dc9765e9c8f151f32751f7a17f4a2d57b	Apalache	Def2	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
94f8afacdb326515d95ee73277d0a8f12d187457	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Boxed	True	Passed	Model Under Test Equivalent Model
080a286036b7f56e8556efe40e4fc912b6301a94	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Boxed	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
75f83294cead81b6012d98ea4142802f78b15106	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Boxed	True	Passed	Model Under Test Equivalent Model
3b978ee554c9c5e9c8158e0e67df45ea398b4fa9	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Boxed	False	Passed	Model Under Test Equivalent Model
052642b4cfee537268d3edb8edf7e58e9a029404	Apalache	Extends	Boxed	True	Passed	Model Under Test Equivalent Model
72dec714091cd80f822b8ea041cf81dc3d738963	Apalache	Extends	Boxed	False	Passed	Model Under Test Equivalent Model
07cf92a69ba15065f723f0fe3f6e22b82140e87b	Apalache	ExtendsInDifferentFolder	Boxed	True	Passed	Model Under Test Equivalent Model
902c9a9f621293aca17d082f4ad123ad2878bab7	Apalache	ExtendsInDifferentFolder	Boxed	False	Passed	Model Under Test Equivalent Model
fd627611942b61adefde3cecbcacc97cd9d4d1a7	Apalache	Instance	Boxed	True	Passed	Model Under Test Equivalent Model
1c5fa0b2541edd2c1b3ec001fb3e5331340d4e1b	Apalache	Instance	Boxed	False	Passed	Model Under Test Equivalent Model
eaf8bed47c2b7f94cbb557da51843f52f9873764	Apalache	InstanceWith	Boxed	True	Passed	Model Under Test Equivalent Model
5fe91b38b2fe929aed990be9a56277105a895b5d	Apalache	InstanceWith	Boxed	False	Passed	Model Under Test Equivalent Model
106e4e5d76ebe2452a837b0ecec271056b4fd784	Apalache	InstanceNamed	Boxed	True	Passed	Model Under Test Equivalent Model
c4200822c384b072608860631901593bdf92f4b4	Apalache	InstanceNamed	Boxed	False	Passed	Model Under Test Equivalent Model
f294dd7429cf496f3ff00cab841b7f48328ff3bf	Apalache	InstanceNamedWith	Boxed	True	Passed	Model Under Test Equivalent Model
47736123732736417ced77fc1faa5bd42998bf68	Apalache	InstanceNamedWith	Boxed	False	Passed	Model Under Test Equivalent Model
1b4216a7ab5daffc73083539173cfca30daf33a2	Apalache	InstanceInFolder	Boxed	True	Passed	Model Under Test Equivalent Model
bbe3bb113211b03733be16a4f65b7deef3a0eb85	Apalache	InstanceInFolder	Boxed	False	Passed	Model Under Test Equivalent Model
bfc48051fcd7e92a679b97f22e8573f01604d8fe	Apalache	InstanceWithInFolder	Boxed	True	Passed	Model Under Test Equivalent Model
56d09189ef479c722e4a752c75b036ff6b84ef07	Apalache	InstanceWithInFolder	Boxed	False	Passed	Model Under Test Equivalent Model
26f8703a6a7ca411894224b0481c25ddcda299cf	Apalache	InstanceNamedInFolder	Boxed	True	Passed	Model Under Test Equivalent Model
ff6aa72151841db6e1fd055b2d43d639796a181f	Apalache	InstanceNamedInFolder	Boxed	False	Passed	Model Under Test Equivalent Model
df8a8afaccb442ccb643cee241d9ac8daa2aa4d9	Apalache	InstanceNamedWithInFolder	Boxed	True	Passed	Model Under Test Equivalent Model
2ebf13488a0d8422d34fc28af9466daae170dd65	Apalache	InstanceNamedWithInFolder	Boxed	False	Passed	Model Under Test Equivalent Model
b25a22e9df9367b51dc51b5adb0e198e943d03b5	Apalache	Lambda	Boxed	True	Failed: TLC does not support boxed operator in LAMBDA expressions and reports an error	Model Under Test Equivalent Model
4435a5467f708d6ab63fc8edd9966dbc27a3e96e	Apalache	Lambda	Boxed	False	Failed: TLC does not support boxed operator in LAMBDA expressions and reports an error	Model Under Test Equivalent Model

Index

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