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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
dbfcc200b7b5d5d897666f508e01198ef89799a4	Apalache	And	NumLt	True	Passed	Model Under Test Equivalent Model
b544b2a2610aea053f9ebc112e5817c5ac54e1c0	Apalache	And	NumLt	False	Passed	Model Under Test Equivalent Model
6c09f7599e00ed307aa3f9dfca8d9db14efbec9e	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	NumLt	True	Passed	Model Under Test Equivalent Model
aaab018c611942fe08e4d2410aaeb877d724429b	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	NumLt	False	Passed	Model Under Test Equivalent Model
186b2094302b35566614e03b91aaf32250326f30	Apalache	Imply	NumLt	True	Passed	Model Under Test Equivalent Model
b8b6b16410dcd82d374d531ae9b1e88a189c0c69	Apalache	Imply	NumLt	False	Passed	Model Under Test Equivalent Model
8aa6d9c1353b13fc0c71f0fcc7dc7d23dc3a24be	Apalache	Not	NumLt	True	Passed	Model Under Test Equivalent Model
6b00e17b7c1121738bcdb3ddb31e55a7a2285086	Apalache	Not	NumLt	False	Passed	Model Under Test Equivalent Model
3acdec195df2e6eccc6c309f999dd38e76c0faa3	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	NumLt	True	Passed	Model Under Test Equivalent Model
8f36d078950a43713af3de00916312cb0599bff1	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	NumLt	False	Passed	Model Under Test Equivalent Model
118747476eeb3078e34b56164877a1338e6cc641	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	NumLt	True	Passed	Model Under Test Equivalent Model
946399894364c1a7440b8f672d7e23e82142f739	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	NumLt	False	Passed	Model Under Test Equivalent Model
5d4f779840f28eb36f7fcafc972beb9f9576b813	Apalache	AndProp	NumLt	True	Passed	Model Under Test Equivalent Model
d3aea441146d286bfb3aee5b706aed22abc9b7fd	Apalache	AndProp	NumLt	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
3beadce93403e76d4ea1eeff315bb6a3a6fe1b2b	Apalache	Eq	NumLt	True	Passed	Model Under Test Equivalent Model
b4bf76bb15fc9b89705b523bc0db82fb41287bce	Apalache	Eq	NumLt	False	Passed	Model Under Test Equivalent Model
a8026af34acd8bb277677227918be077e2469e33	Apalache	Ne	NumLt	True	Passed	Model Under Test Equivalent Model
0f2f5e0fcf89024e193b5f6367dbf2c490ebc016	Apalache	Ne	NumLt	False	Passed	Model Under Test Equivalent Model
cc54e75bca07f9d7874c527e00ed7d307d6b4a10	Apalache	Let	NumLt	True	Passed	Model Under Test Equivalent Model
4bdaa0e6e14f7fc1a06adaf4c81a286e89ab0fe5	Apalache	Let	NumLt	False	Passed	Model Under Test Equivalent Model
e578cbe4aa33d56439df95625a0a855206776a06	Apalache	Set0	NumLt	True	Passed	Model Under Test Equivalent Model
4c3da86a660970c2b069ce8d0f627554fab1d0d9	Apalache	Set0	NumLt	False	Passed	Model Under Test Equivalent Model
115a707d8e721b7136ede392d08e7c08707c89df	Apalache	Set1	NumLt	True	Passed	Model Under Test Equivalent Model
d69ae1c4f19b344403261bd9c70fe68004a2403d	Apalache	Set1	NumLt	False	Passed	Model Under Test Equivalent Model
579671e26c1e711e2fd12017f4b6b45289c20cb0	Apalache	Set2	NumLt	True	Passed	Model Under Test Equivalent Model
b0344fa00be8fef63fe709200fc8742b0473cbdb	Apalache	Set2	NumLt	False	Passed	Model Under Test Equivalent Model
be1037788e1d703d3ddeba3148ba693724ca22d0	Apalache	Fun	NumLt	True	Passed	Model Under Test Equivalent Model
b7f8dd8155cb8ba8db20c360f304b8ac7ddc289d	Apalache	Fun	NumLt	False	Passed	Model Under Test Equivalent Model
e782b396c01ade52ec36c29ae3e11c7bbfd42677	Apalache	In	NumLt	True	Passed	Model Under Test Equivalent Model
4e4d878300abf0b284143e72d7e4773b0a92b827	Apalache	In	NumLt	False	Passed	Model Under Test Equivalent Model
d8c613e4be161f4fd4830a2f29cf52de16192727	Apalache	NotIn	NumLt	True	Passed	Model Under Test Equivalent Model
9005776bde260a9919c8852c3fb9adc5f81597f3	Apalache	NotIn	NumLt	False	Passed	Model Under Test Equivalent Model
d9e6c2419e17befe5cde1219bdc69d68543f93e9	Apalache	Exists	NumLt	True	Passed	Model Under Test Equivalent Model
b3a724c3da44c5814b219578f7c42d1bc00b0b61	Apalache	Exists	NumLt	False	Passed	Model Under Test Equivalent Model
d2e99d01d8d847bdee5f549882748bad193c0c4f	Apalache	Forall	NumLt	True	Passed	Model Under Test Equivalent Model
bd55da018eda1a3a5003227028f123b16708297e	Apalache	Forall	NumLt	False	Passed	Model Under Test Equivalent Model
55f95aef57f44226000613b2eae7fb71e80ed346	Apalache	Choose	NumLt	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
05c14cc9b8e2d432a5d3b33fe26833d1bbcaa14c	Apalache	Choose	NumLt	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
809b63927e68661a5bcf8fcf971900906dfd9f52	Apalache	Record	NumLt	True	Passed	Model Under Test Equivalent Model
8ee6f9a95cf73216c3e4423f27c8d31c2b66ed19	Apalache	Record	NumLt	False	Passed	Model Under Test Equivalent Model
ac60bcaa95408d9495234fe8c6fd85dc6228d742	Apalache	Tuple	NumLt	True	Passed	Model Under Test Equivalent Model
a8fba3ed69add55e55362f5c5f2ecfd4e4917887	Apalache	Tuple	NumLt	False	Passed	Model Under Test Equivalent Model
cc309cfc6dc96e88c5e0eaa2019910f52801bcb6	Apalache	FunApp	NumLt	True	Passed	Model Under Test Equivalent Model
dac95254c399a40dfbc8920dd951e93424a4338d	Apalache	FunApp	NumLt	False	Passed	Model Under Test Equivalent Model
19fa160f1e84b949cd357094c9e9064427c5116c	Apalache	Except1Fun	NumLt	True	Passed	Model Under Test Equivalent Model
7babeac9df52c31b58707fc7902ddf2d01f2621c	Apalache	Except1Fun	NumLt	False	Passed	Model Under Test Equivalent Model
522476124269a095b141b85c7a04df409e64c3b1	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	NumLt	True	Passed	Model Under Test Equivalent Model
70f9ac805e1235d8accef11d0ac23b1eb7b36050	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	NumLt	False	Passed	Model Under Test Equivalent Model
998e33ae50a792339e9476539b73c356d5d72cca	Apalache	Except1Rec	NumLt	True	Passed	Model Under Test Equivalent Model
a43b7bd6f818db366b58e6aed36ee1a3f44b00a3	Apalache	Except1Rec	NumLt	False	Passed	Model Under Test Equivalent Model
159f3636265793e81b1088f9026c745df489559d	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	NumLt	True	Passed	Model Under Test Equivalent Model
d6f77dcd5e891de0299529e9730f02490d13b480	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	NumLt	False	Passed	Model Under Test Equivalent Model
ef7e7c852958ccbf037d9fbf754d2f36a7d606ec	Apalache	Except2Fun	NumLt	True	Passed	Model Under Test Equivalent Model
a93b6407373617676617f5c2a15145a07bbcae0a	Apalache	Except2Fun	NumLt	False	Passed	Model Under Test Equivalent Model
11e3e5127ab0d409b1abbe500de4f9a1d7aca0d2	Apalache	Prime	NumLt	True	Passed	Model Under Test Equivalent Model
e7eab39752639c9bc1dc46a69520f5998dce1b3c	Apalache	Prime	NumLt	False	Passed	Model Under Test Equivalent Model
c91ca7f4e9cd4117c53823d4b1303f16fea9f0c0	Apalache	DefFun	NumLt	True	Passed	Model Under Test Equivalent Model
29d0fb0d8d9c622c966929f9a1772866411803f7	Apalache	DefFun	NumLt	False	Passed	Model Under Test Equivalent Model
8e40faef99fc42c249a8aa1c4d5d884d0d78f9a3	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	NumLt	True	Passed	Model Under Test Equivalent Model
9f783e2668a949c22b3bef377230c576de575402	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	NumLt	False	Passed	Model Under Test Equivalent Model
3d9bc0b6fcec7851fce503e644961f735262a89e	Apalache	DefFunRecursive	NumLt	True	Passed	Model Under Test Equivalent Model
632886c136ec945e1140dc9b701a6f81ca926e74	Apalache	DefFunRecursive	NumLt	False	Passed	Model Under Test Equivalent Model
6b0176f387433f963e7c3ff9dd9c116cb28a2886	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	NumLt	True	Passed	Model Under Test Equivalent Model
fa7800b2cd7cf11b4d88936e29edd78aa861f7d9	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	NumLt	False	Passed	Model Under Test Equivalent Model
3fb3403e09d1b16a6a774a3f37517dd1566bd4a8	Apalache	Def0	NumLt	True	Passed	Model Under Test Equivalent Model
dde129b89db0ac3c6bcdd805525d3f5a87190ed8	Apalache	Def0	NumLt	False	Passed	Model Under Test Equivalent Model
bc45ec19919a9f7c2bd4837a8eb161be60d0c7c8	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	NumLt	True	Passed	Model Under Test Equivalent Model
f60b455cc782fe3e0bfe6142e6e4b8c33036929c	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	NumLt	False	Passed	Model Under Test Equivalent Model
8240736cf52e014cfe3fd3f26da1c8282f379483	Apalache	Def1	NumLt	True	Passed	Model Under Test Equivalent Model
98be8f91718090dd076575b78e168fdd0991a726	Apalache	Def1	NumLt	False	Passed	Model Under Test Equivalent Model
2f06a69402ad8aa34a2de559e50b69dc165b24fc	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	NumLt	True	Passed	Model Under Test Equivalent Model
7461545bc20fd4b7e0f6b16c4df07f0b4f7fcc5f	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	NumLt	False	Passed	Model Under Test Equivalent Model
0ab292c729f6953158d809145c6d25d39b212e73	Apalache	Def2	NumLt	True	Passed	Model Under Test Equivalent Model
863e7e9cf435a1128cff3be4d25915af68421adb	Apalache	Def2	NumLt	False	Passed	Model Under Test Equivalent Model
b125752067c1139fb9c09619a99b01bc6b76f982	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	NumLt	True	Passed	Model Under Test Equivalent Model
c095465afce3c9c5545fd6b980c21a0fe8d7e5fe	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	NumLt	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
cb3b347fd49b06289f6b14d310237cbbf839675d	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	NumLt	True	Passed	Model Under Test Equivalent Model
3b888ffd6f7e2922a53a8e7c12faf5efc27a9a3a	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	NumLt	False	Passed	Model Under Test Equivalent Model
b1a65f024dbf7ec31f565d8a567492113f9ae367	Apalache	Extends	NumLt	True	Passed	Model Under Test Equivalent Model
a512185c70b2dbab3d09cc710453d631aa9aa7e5	Apalache	Extends	NumLt	False	Passed	Model Under Test Equivalent Model
48b316791553fa5b849dc07e096f5e5d35ed4ff6	Apalache	ExtendsInDifferentFolder	NumLt	True	Passed	Model Under Test Equivalent Model
4403477b9dcff1cbd033ff034e705146ba4437c9	Apalache	ExtendsInDifferentFolder	NumLt	False	Passed	Model Under Test Equivalent Model
ebff17dde351479c5c458dd710df30f0c3ca8a92	Apalache	Variable	NumLt	True	Passed	Model Under Test Equivalent Model
7d1baa793e12958decd188a3b66c0b01c8f648e6	Apalache	Variable	NumLt	False	Passed	Model Under Test Equivalent Model
9a9be1f5d6b679f3032e33eac426879175555c46	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	NumLt	True	Passed	Model Under Test Equivalent Model
172f377ee3c29309245b9cb124212ca3ce6de1e5	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	NumLt	False	Passed	Model Under Test Equivalent Model
7f1a8b73a90f31670ed3ced1fe9c431a8bc9d690	Apalache	Constant	NumLt	True	Passed	Model Under Test Equivalent Model
62ceb4f48f76fc3c30e58a9d28e0ee62a0b01253	Apalache	Constant	NumLt	False	Passed	Model Under Test Equivalent Model
2e404789546f7537b2608ec2ed5d6fb5828d1f22	Apalache	ConstantRank1	NumLt	True	Passed	Model Under Test Equivalent Model
a35d5c806b9d0264c4fbdb9085ef3b1123e57592	Apalache	ConstantRank1	NumLt	False	Passed	Model Under Test Equivalent Model
a680ea2612742fc6cc0de8f250849126b2289efb	Apalache	Instance	NumLt	True	Passed	Model Under Test Equivalent Model
f646957b4e2df2e61cc123564aa2493e9cda33a8	Apalache	Instance	NumLt	False	Passed	Model Under Test Equivalent Model
6ecc62cc3804ad5b76b18c0004dde55064548a97	Apalache	InstanceWith	NumLt	True	Passed	Model Under Test Equivalent Model
4a00154f64d1953bfc7615b1a9ddc9b22fbacccc	Apalache	InstanceWith	NumLt	False	Passed	Model Under Test Equivalent Model
4aee3600557ac438eed612a83eeec3c7cd9e0146	Apalache	InstanceNamed	NumLt	True	Passed	Model Under Test Equivalent Model
6ccfa74c435c8049382646737eeb1159dd591ccb	Apalache	InstanceNamed	NumLt	False	Passed	Model Under Test Equivalent Model
3864fc8e03419a8702a5277f3f3194ded89656cf	Apalache	InstanceNamedWith	NumLt	True	Passed	Model Under Test Equivalent Model
12120cc3c318f9e8476354b0730eb38a19476a22	Apalache	InstanceNamedWith	NumLt	False	Passed	Model Under Test Equivalent Model
aaa8d562faead62a4b6ed4b51b3337e77a323cb7	Apalache	InstanceInFolder	NumLt	True	Passed	Model Under Test Equivalent Model
38421bb832d91998c69d283fee258bb0539cd46a	Apalache	InstanceInFolder	NumLt	False	Passed	Model Under Test Equivalent Model
91b07687362d90b46f3be073894b18c001289b42	Apalache	InstanceWithInFolder	NumLt	True	Passed	Model Under Test Equivalent Model
8ba57388d319e0ebebd8446b7330b14d5f8743af	Apalache	InstanceWithInFolder	NumLt	False	Passed	Model Under Test Equivalent Model
cac4c0256e0962bfb10c00f6c7078e2f835206e7	Apalache	InstanceNamedInFolder	NumLt	True	Passed	Model Under Test Equivalent Model
a3b51d441b0563a4f4492b466ce78c6bce7ac793	Apalache	InstanceNamedInFolder	NumLt	False	Passed	Model Under Test Equivalent Model
84aa84f8be39686640c98e766e0c26e6b8485cfc	Apalache	InstanceNamedWithInFolder	NumLt	True	Passed	Model Under Test Equivalent Model
f30b86f932f9a8671d70e089bea093396ee44358	Apalache	InstanceNamedWithInFolder	NumLt	False	Passed	Model Under Test Equivalent Model
b02fbb6db483297294cde6eb5552b2b87a15760c	Apalache	Enabled	NumLt	True	Passed	Model Under Test Equivalent Model
cf0c894e3321de1b21b4d06f5ce01669192a5b17	Apalache	Enabled	NumLt	False	Passed	Model Under Test Equivalent Model
f1071c031b4f44f6105d51e8e7ecd8e09e3ddbb6	Apalache	Assume	NumLt	True	Passed	Model Under Test Equivalent Model
65928f3ce77febe2eb9b193cd546b570c7ba5149	Apalache	Assume	NumLt	False	Passed	Model Under Test Equivalent Model
a798bb9d59ae789e801a03048c95bc10440ff621	Apalache	AssumeNamed	NumLt	True	Passed	Model Under Test Equivalent Model
c03694ff89f17b2f3a0af166dcd89d1af2911e20	Apalache	AssumeNamed	NumLt	False	Passed	Model Under Test Equivalent Model
cb377b74dfae58e33736184529ecc4428c162af1	Apalache	Lambda	NumLt	True	Passed	Model Under Test Equivalent Model
2db6a90a4cd4b21be80108cae2ccfc2159138446	Apalache	Lambda	NumLt	False	Passed	Model Under Test Equivalent Model
79c4aa367ea2b001ea353bc84140bd1b7ce72d06	Apalache	IfCond	NumLt	True	Passed	Model Under Test Equivalent Model
9cb887065553762efa6a124815bb7453e4098bf2	Apalache	IfCond	NumLt	False	Passed	Model Under Test Equivalent Model
88cf1a2c180507fc97050c99f3de09b0c857b5b8	Apalache	IfThen	NumLt	True	Passed	Model Under Test Equivalent Model
490d8d43112cef093579802a76ad489d161e611c	Apalache	IfThen	NumLt	False	Passed	Model Under Test Equivalent Model
5bd94c08f0f0c51fc9590fa982d4c3c8f5067cba	Apalache	IfElse	NumLt	True	Passed	Model Under Test Equivalent Model
98b23bcf54c2ebd93e2492172044442a418b4b43	Apalache	IfElse	NumLt	False	Passed	Model Under Test Equivalent Model
d51b6e8af0eb43caf767f869b585bc87f33239e4	Apalache	Unchanged	NumLt	True	Passed	Model Under Test Equivalent Model
5907748f02e79e4f313d875ec32ba84c19912d8f	Apalache	Unchanged	NumLt	False	Passed	Model Under Test Equivalent Model
333d8c726942949cb3a5d73994cb2cef9c3a174e	Apalache	Equivalence	NumLt	True	Passed	Model Under Test Equivalent Model
0c110d7b39737e177a641bbbdf052dd61106d3d5	Apalache	Equivalence	NumLt	False	Passed	Model Under Test Equivalent Model
87a2e75f06888e342c8ffa31cfe24f1eb93e5c73	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	NumLt	True	Passed	Model Under Test Equivalent Model
eacc8d80d54538d4a31e4faec67f77bc382555b9	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	NumLt	False	Passed	Model Under Test Equivalent Model
e825ec4464a7936d7c4ae5c9558828e2a89de929	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	NumLt	True	Passed	Model Under Test Equivalent Model
c31ae8642f7acd9ace282abd60319f579d913900	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	NumLt	False	Passed	Model Under Test Equivalent Model
226f2691c8bdf2173aa1a16649dc497c576c1dc8	Apalache	BagBagIn	NumLt	True	Passed	Model Under Test Equivalent Model
09e1c189fa451f3309dff711a5677df63d441ffd	Apalache	BagBagIn	NumLt	False	Passed	Model Under Test Equivalent Model
59bcf38d1cbfba6a150b6ecb967d59e0c31fc6c8	Apalache	BagCopiesIn	NumLt	True	Passed	Model Under Test Equivalent Model
2480c6198ef885d259f22d55b9b21a86085a0a83	Apalache	BagCopiesIn	NumLt	False	Passed	Model Under Test Equivalent Model
02996a835390a17dd3a822c83bccdb21eded7420	Apalache	SeqAppend	NumLt	True	Passed	Model Under Test Equivalent Model
baf2c6a5ddf3d0221ba44e932c6cafcd8c6b2820	Apalache	SeqAppend	NumLt	False	Passed	Model Under Test Equivalent Model

Index

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