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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
14674c082bef6f2fe6b5d5aad1e729e74dca1358	Apalache	Eq	NumMinus	True	Passed	Model Under Test Equivalent Model
58e88970ffd2351740c3833b0b50847dd063507a	Apalache	Eq	NumMinus	False	Passed	Model Under Test Equivalent Model
5dd1d0f59bc967d91f488b8a3f68cb209093fccb	Apalache	Ne	NumMinus	True	Passed	Model Under Test Equivalent Model
fb4adf120868f0a35f614fe61e4168b1f3410b58	Apalache	Ne	NumMinus	False	Passed	Model Under Test Equivalent Model
0f48895547aaddf330d1f0f2e8ad57880f9dd6a9	Apalache	Let	NumMinus	True	Passed	Model Under Test Equivalent Model
016ffa323fdb78bce685fc198637e57189e01ac8	Apalache	Let	NumMinus	False	Passed	Model Under Test Equivalent Model
9cabf640d93535a2d8ce12308948fac6c694c453	Apalache	Set0	NumMinus	True	Passed	Model Under Test Equivalent Model
6626ec8c649b248de16b6b6fe4c404c0c0dadcae	Apalache	Set0	NumMinus	False	Passed	Model Under Test Equivalent Model
5e7360188f4960869519128f7a7e32e86015e841	Apalache	Set1	NumMinus	True	Passed	Model Under Test Equivalent Model
d70845bdf1515400ffc5eb565a67e5bb1e3ba378	Apalache	Set1	NumMinus	False	Passed	Model Under Test Equivalent Model
fbb2429a42e7c5dc7eb774dac9a3cf721d53c2a1	Apalache	Set2	NumMinus	True	Passed	Model Under Test Equivalent Model
9560d180d50fe40ec3b0c8a07296f711b147754e	Apalache	Set2	NumMinus	False	Passed	Model Under Test Equivalent Model
91733ba01a1a93f4d247ddb3a8c79069e627f046	Apalache	Fun	NumMinus	True	Passed	Model Under Test Equivalent Model
093310b4d1c33f7fdf8e210372558d89b9f1d826	Apalache	Fun	NumMinus	False	Passed	Model Under Test Equivalent Model
12a4cd713f1c7df713f05bad92ec840134a615b2	Apalache	In	NumMinus	True	Passed	Model Under Test Equivalent Model
a76d9fe04c247e53dd4c44c75e0187b92d0d5342	Apalache	In	NumMinus	False	Passed	Model Under Test Equivalent Model
f53d9de520c115fcef40b3d1571670f4c00c8978	Apalache	NotIn	NumMinus	True	Passed	Model Under Test Equivalent Model
a84171984250ffcd162b652761f2e4d17ef67ac8	Apalache	NotIn	NumMinus	False	Passed	Model Under Test Equivalent Model
b98e85873adee1f90dc5f4db155db4380683a622	Apalache	Record	NumMinus	True	Passed	Model Under Test Equivalent Model
42fd0408e639f5880c25300b20aaae903f966716	Apalache	Record	NumMinus	False	Passed	Model Under Test Equivalent Model
0b233e8419db3e846bfd82db33ca1408739a9378	Apalache	Tuple	NumMinus	True	Passed	Model Under Test Equivalent Model
be4be70842a44a17016c4f8c9c6fdc38c3bd5141	Apalache	Tuple	NumMinus	False	Passed	Model Under Test Equivalent Model
a31f9bcd399333c0decb2ce898ae4fd104fc2785	Apalache	FunApp	NumMinus	True	Passed	Model Under Test Equivalent Model
90b4cc25e9eb76d984d71b9def47ee0c853cb7e4	Apalache	FunApp	NumMinus	False	Passed	Model Under Test Equivalent Model
eeb29330a616dbd2b2f74ebc648d38225115cfea	Apalache	Except1Fun	NumMinus	True	Passed	Model Under Test Equivalent Model
03683e438f54e5da32328fdf0bdce41951f58dcd	Apalache	Except1Fun	NumMinus	False	Passed	Model Under Test Equivalent Model
c51e2c72870ed27e0cf19768c32bb9cf3ff2a434	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	NumMinus	True	Passed	Model Under Test Equivalent Model
9839dd355a822915590eba1584f36a6471142e59	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	NumMinus	False	Passed	Model Under Test Equivalent Model
a24724c83bfa85a3a7d1845cc26237c352e592c4	Apalache	Except1Rec	NumMinus	True	Passed	Model Under Test Equivalent Model
729fc29d4cb467c6cdeba40177d02330ceb629fb	Apalache	Except1Rec	NumMinus	False	Passed	Model Under Test Equivalent Model
577b94c287e464a01111a680d04b33d29a8a7078	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	NumMinus	True	Passed	Model Under Test Equivalent Model
ff1ac7f0568b4f90c73c268e8bf34a1c9e17ad3e	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	NumMinus	False	Passed	Model Under Test Equivalent Model
a346609af44e95d044e6cf3c4a57195218f07dcb	Apalache	Except2Fun	NumMinus	True	Passed	Model Under Test Equivalent Model
0ddbbba13e9bfc69a8b582222d46057df6df4608	Apalache	Except2Fun	NumMinus	False	Passed	Model Under Test Equivalent Model
2a05258c1ede9cb6b51ac36d6dcc68e52fd9f7ba	Apalache	Prime	NumMinus	True	Passed	Model Under Test Equivalent Model
fa5ae43a057c017e5c6a2780639780fc21a36f74	Apalache	Prime	NumMinus	False	Passed	Model Under Test Equivalent Model
41eaad9147596315fd5db51ba77d0bb735ba20ad	Apalache	NumUnaryMinus	NumMinus	True	Passed	Model Under Test Equivalent Model
597177f7bc1989feb3f6fe86af53fefd48ee1be6	Apalache	NumUnaryMinus	NumMinus	False	Passed	Model Under Test Equivalent Model
946fa57c64e88bbc74d1631d35b5068b8dc69f04	Apalache	NumPlus	NumMinus	True	Passed	Model Under Test Equivalent Model
8d1f8809f9ea9fbe74c9c90e103c5e72a9994e72	Apalache	NumPlus	NumMinus	False	Passed	Model Under Test Equivalent Model
455ab83e76acdaa242d9f3f34b2365cdb6693d07	Apalache	NumMinus	NumMinus	True	Passed	Model Under Test Equivalent Model
ff4afdf1f35fbbb1b904765aeafeef943e1db27b	Apalache	NumMinus	NumMinus	False	Passed	Model Under Test Equivalent Model
23ff9d7e2ef088372c5431c643dd1727e6659aee	Apalache	NumMul	NumMinus	True	Passed	Model Under Test Equivalent Model
389e65dfba868f00e51fa3ae26334b77a7ffd33e	Apalache	NumMul	NumMinus	False	Passed	Model Under Test Equivalent Model
1bd59be9744def68a5e7fc853b20a70c6ee273e3	Apalache	NumDiv	NumMinus	True	Passed	Model Under Test Equivalent Model
aee3ce09fa97d6dd41a3cedec71f57f30233dc6a	Apalache	NumDiv	NumMinus	False	Passed	Model Under Test Equivalent Model
bb81417638c3742d7d624b045e734ead2d8fdf66	Apalache	NumMod	NumMinus	True	Passed	Model Under Test Equivalent Model
41212285b57240391d51f09c3a9e38c6971e7a0d	Apalache	NumMod	NumMinus	False	Passed	Model Under Test Equivalent Model
e2a4a78b19c4b1b8c829854eb63e4cf6284952bc	Apalache	NumPow	NumMinus	True	Passed	Model Under Test Equivalent Model
cd5b2e23b40c26f57d27823a50a634fead20f560	Apalache	NumPow	NumMinus	False	Passed	Model Under Test Equivalent Model
8d0c929c5261f31432ebb7e0f5358a5bd4c326a5	Apalache	NumGt	NumMinus	True	Passed	Model Under Test Equivalent Model
cf1de4a29dc02a074da0679212c652b0659af2eb	Apalache	NumGt	NumMinus	False	Passed	Model Under Test Equivalent Model
d7b9392b2402129c95a426fb7eb31543ce6942eb	Apalache	NumGe	NumMinus	True	Passed	Model Under Test Equivalent Model
a9c79f36c79adb859f0dce89e93c0b4b9cda2670	Apalache	NumGe	NumMinus	False	Passed	Model Under Test Equivalent Model
e0cc7b8b29d5ef2063d18f0475ec0d59cf72ceeb	Apalache	NumLt	NumMinus	True	Passed	Model Under Test Equivalent Model
e207d2b38fc7a27359e1a4771b5c0faf783477a8	Apalache	NumLt	NumMinus	False	Passed	Model Under Test Equivalent Model
b1864f1e501fda1a19fc7c92204a77e95bef7f11	Apalache	NumLe	NumMinus	True	Passed	Model Under Test Equivalent Model
7eda53a03a9e91d3fd6f6e5866d89618689b7dd8	Apalache	NumLe	NumMinus	False	Passed	Model Under Test Equivalent Model
bea94f2df2397481de05c545d9eb39592c50c511	Apalache	DefFun	NumMinus	True	Passed	Model Under Test Equivalent Model
e96b6108fca0285e60af28f20e0b9eca55505bf9	Apalache	DefFun	NumMinus	False	Passed	Model Under Test Equivalent Model
c2134b41f732b05bf207308a50afb9d829479d68	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	NumMinus	True	Passed	Model Under Test Equivalent Model
3ad0630a5ea9e8ccfb8b291bb2324bd89c88cd71	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	NumMinus	False	Passed	Model Under Test Equivalent Model
6f48ee4f696647e7b28dec30e2d0aa0bb40e9685	Apalache	DefFunRecursive	NumMinus	True	Passed	Model Under Test Equivalent Model
8d609f3e119096a2282f858826ed0ac53d5fb280	Apalache	DefFunRecursive	NumMinus	False	Passed	Model Under Test Equivalent Model
a5e3c57a444e4199672402a2ab4c3a2f6b9778da	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	NumMinus	True	Passed	Model Under Test Equivalent Model
4e5e3622796858d08f71e2281b411e06ca7c256a	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	NumMinus	False	Passed	Model Under Test Equivalent Model
a83e24d3a4fa635ab6f8c7699225fab32c6bbe8b	Apalache	Def0	NumMinus	True	Passed	Model Under Test Equivalent Model
e184cd7717e30451a2590a6456f0a3afad4bc50a	Apalache	Def0	NumMinus	False	Passed	Model Under Test Equivalent Model
3eeccf496c7c621fc80b4880caa10de36caa4ecf	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	NumMinus	True	Passed	Model Under Test Equivalent Model
f67147a0883e31be1bf1dc99274c83a2c6744caa	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	NumMinus	False	Passed	Model Under Test Equivalent Model
afb20ee727ea482b96ae6bd0b7b4a032d882eb25	Apalache	Def1	NumMinus	True	Passed	Model Under Test Equivalent Model
c059369daaa32b840ae754c1904a39691edba538	Apalache	Def1	NumMinus	False	Passed	Model Under Test Equivalent Model
6b3ff0bdaa5e78f28031505a4f8a6ef5168b5201	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	NumMinus	True	Passed	Model Under Test Equivalent Model
90ffed440230a9e59f4d5c9f073b1216c4694c5c	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	NumMinus	False	Passed	Model Under Test Equivalent Model
509f8dea8877904c6adefa3c5e04c1d6fce04d3a	Apalache	Def2	NumMinus	True	Passed	Model Under Test Equivalent Model
b2fab82c17df80d442ef6e2b09ce7f86f227ed50	Apalache	Def2	NumMinus	False	Passed	Model Under Test Equivalent Model
98446430fe34208dbf57e773d77dbc7e33d1e4cd	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	NumMinus	True	Passed	Model Under Test Equivalent Model
8d55abe31ce6b017f1ff44c389ef34b6ba8e7fd8	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	NumMinus	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
c7611e99006ef9ebf54b41f79fc704064c37604b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	NumMinus	True	Passed	Model Under Test Equivalent Model
475b719db7997604076be7578c6eb37b2f886e4e	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	NumMinus	False	Passed	Model Under Test Equivalent Model
8aa84de537691605a2a2b25ff486224e8e17196f	Apalache	Extends	NumMinus	True	Passed	Model Under Test Equivalent Model
9b01fc8958fb82c30b186ba07b5004ff8203c15e	Apalache	Extends	NumMinus	False	Passed	Model Under Test Equivalent Model
6a8825f190c8cc3986be579535ec6ed034e7f5ee	Apalache	ExtendsInDifferentFolder	NumMinus	True	Passed	Model Under Test Equivalent Model
78b74e8ef507e8bde8c9942ad08c0844ee2abf42	Apalache	ExtendsInDifferentFolder	NumMinus	False	Passed	Model Under Test Equivalent Model
d8ec211cb6d6a813bf967a42473f03c3c1cff96e	Apalache	Variable	NumMinus	True	Passed	Model Under Test Equivalent Model
82b14e2052519aa69d829c6dfa8cc69db8e85eed	Apalache	Variable	NumMinus	False	Passed	Model Under Test Equivalent Model
6e5fc3bb0aaead8a212594827ee45e67fe3b1203	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	NumMinus	True	Passed	Model Under Test Equivalent Model
6a7ca2256e10bf4f98366b7263c296a5428f0194	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	NumMinus	False	Passed	Model Under Test Equivalent Model
eda2a051dba74030f9b56b1a96136518c1f48383	Apalache	Constant	NumMinus	True	Passed	Model Under Test Equivalent Model
fe64f6f819ece95d9fe3566a06bbd250f4bc28dc	Apalache	Constant	NumMinus	False	Passed	Model Under Test Equivalent Model
9a891b5e67c5a3177768f95687f97ac818b078cf	Apalache	ConstantRank1	NumMinus	True	Passed	Model Under Test Equivalent Model
df1ef18a0401394424bd685240227dd72950743d	Apalache	ConstantRank1	NumMinus	False	Passed	Model Under Test Equivalent Model
142d1d45d1abb17c2a813773fbf5d9a7d249bad3	Apalache	Instance	NumMinus	True	Passed	Model Under Test Equivalent Model
f7f136c8c6ed7fca1a7e2ae75e8de7eea65731f8	Apalache	Instance	NumMinus	False	Passed	Model Under Test Equivalent Model
2d820ca0d9583aecd0a1acc6982abae5457fc41f	Apalache	InstanceWith	NumMinus	True	Passed	Model Under Test Equivalent Model
ad2af1edb4a8ecc55c67a011c38ed4668fc3ef2e	Apalache	InstanceWith	NumMinus	False	Passed	Model Under Test Equivalent Model
31213eae3b9cf44df022d469b81ad803bbf9aeb6	Apalache	InstanceNamed	NumMinus	True	Passed	Model Under Test Equivalent Model
27b46436afe281a9c43c5f459c9fdd93c4b52e42	Apalache	InstanceNamed	NumMinus	False	Passed	Model Under Test Equivalent Model
4c25e55eed52c0f5632b2e1d99662c14bf720b28	Apalache	InstanceNamedWith	NumMinus	True	Passed	Model Under Test Equivalent Model
7637a52ebe5f74ad3f70f8797698f22f798fd265	Apalache	InstanceNamedWith	NumMinus	False	Passed	Model Under Test Equivalent Model
21b13e4cc8b6a5d9289fdcfc807794b461cc8b84	Apalache	InstanceInFolder	NumMinus	True	Passed	Model Under Test Equivalent Model
2dd88af4c7781e539db5e221d4df52ac78df2156	Apalache	InstanceInFolder	NumMinus	False	Passed	Model Under Test Equivalent Model
5e6c8ac64b2bcf55bceb6ebe5f8db204e4eb70a0	Apalache	InstanceWithInFolder	NumMinus	True	Passed	Model Under Test Equivalent Model
fae894160ee7982851af4e21286d473cd41d26ab	Apalache	InstanceWithInFolder	NumMinus	False	Passed	Model Under Test Equivalent Model
e19241be0e9c38794fa319f037c53f5065dcf6af	Apalache	InstanceNamedInFolder	NumMinus	True	Passed	Model Under Test Equivalent Model
659ee2f2efb589fe215f2564732cc88ffaada9b1	Apalache	InstanceNamedInFolder	NumMinus	False	Passed	Model Under Test Equivalent Model
d2163c5d12e9c50727546c47a9d0aad5e8876f62	Apalache	InstanceNamedWithInFolder	NumMinus	True	Passed	Model Under Test Equivalent Model
bd2bb5f47b64472aabbaa3b2cb462784ff8c1ed9	Apalache	InstanceNamedWithInFolder	NumMinus	False	Passed	Model Under Test Equivalent Model
083298025451bcd0e04800f65757f1d9844dc397	Apalache	Lambda	NumMinus	True	Passed	Model Under Test Equivalent Model
5f2cb5a0acff8f9f425b02fd3aaa84df0e0917a2	Apalache	Lambda	NumMinus	False	Passed	Model Under Test Equivalent Model
6d61d8c6856c421af459afc4bdfa3eca2f6ab53d	Apalache	IfThen	NumMinus	True	Passed	Model Under Test Equivalent Model
68033ef4dc1c444269896118e98822dd2b695b0f	Apalache	IfThen	NumMinus	False	Passed	Model Under Test Equivalent Model
37d27cce609a1df49099ebb4ad86dadc223ab49d	Apalache	IfElse	NumMinus	True	Passed	Model Under Test Equivalent Model
94609f1b020d2a7f2943844f2dce2f87721a8231	Apalache	IfElse	NumMinus	False	Passed	Model Under Test Equivalent Model
74ee154898d690b63ecbc92d31d5d7cd4ed144a0	Apalache	Unchanged	NumMinus	True	Passed	Model Under Test Equivalent Model
9a56759a1619c7e1c001d7a8bbb66535583cec78	Apalache	Unchanged	NumMinus	False	Passed	Model Under Test Equivalent Model
30760c62c4c515dac8cb3b45cf0ece18a2d02e2e	Apalache	SeqSubSeq	NumMinus	True	Passed	Model Under Test Equivalent Model
3352bc8719aede252b6668197d144e9ae8643ec1	Apalache	SeqSubSeq	NumMinus	False	Passed	Model Under Test Equivalent Model
cb1724e1f84a64c7aa81e560946c27390afc8174	TLC with reduction strategy: Case 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	NumRange	NumMinus	True	Passed	Model Under Test Equivalent Model
ebbc2a299fd7bd38c1bce04fd8225a5ba7da397a	TLC with reduction strategy: Case 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	NumRange	NumMinus	False	Passed	Model Under Test Equivalent Model
1154ddfdc2a5ea86f5db13305d7b74b2feff977f	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	NumMinus	True	Passed	Model Under Test Equivalent Model
84b0366f09b40cd2582c3a1b51027fd7f1c9673e	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	NumMinus	False	Passed	Model Under Test Equivalent Model
fa19944bed9315e0e0153734bf2a209e3b9d5b17	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	NumMinus	True	Passed	Model Under Test Equivalent Model
1603baa382256471ce6af3e3be52aea70e39abf3	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	NumMinus	False	Passed	Model Under Test Equivalent Model
325802c817bb12df3ac166de899acb550141d912	Apalache	BagBagIn	NumMinus	True	Passed	Model Under Test Equivalent Model
9d813d5856b6beb10a1a2efcb284c56a4f1a3d70	Apalache	BagBagIn	NumMinus	False	Passed	Model Under Test Equivalent Model
0b203c7ec97ff6af07f1fc15cb70274042d45f6b	Apalache	BagCopiesIn	NumMinus	True	Passed	Model Under Test Equivalent Model
a718a0ad1ed1efd1ee16049a7c394ab822104f31	Apalache	BagCopiesIn	NumMinus	False	Passed	Model Under Test Equivalent Model
5b7f3451c9dd78d1f60e706639458c83d4af1e71	Apalache	SeqAppend	NumMinus	True	Passed	Model Under Test Equivalent Model
2ef3ecc06e9f4092be5bd238d658cf3991e5b65b	Apalache	SeqAppend	NumMinus	False	Passed	Model Under Test Equivalent Model

Index

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