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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
df8676b4148b62a371d682eaa1103c2cb1cec466	Apalache	Eq	Set0	True	Passed	Model Under Test Equivalent Model
80ac7e6c5beddd5bf14b43b87a8dfdb77dad27f7	Apalache	Eq	Set0	False	Passed	Model Under Test Equivalent Model
2356ed16cbed5e34073e7ccd31557c01ced73a35	Apalache	Ne	Set0	True	Passed	Model Under Test Equivalent Model
7e0fa81d489891f1fa557177a7c636f6aef09987	Apalache	Ne	Set0	False	Passed	Model Under Test Equivalent Model
36e11df36d388fa59151f8a030f1007a58342517	Apalache	Let	Set0	True	Passed	Model Under Test Equivalent Model
8323236f5fb44f69c7a667c9203d492dcfe665ce	Apalache	Let	Set0	False	Passed	Model Under Test Equivalent Model
114a7aef3f2619e6d3f6559c225bc16771bdb870	Apalache	Set0	Set0	True	Passed	Model Under Test Equivalent Model
962b5fd24388c100f1258ef545038ba8a77a0bc8	Apalache	Set0	Set0	False	Passed	Model Under Test Equivalent Model
cbf43bd7f0d18532cc30df47d0217cc7ac3d05a4	Apalache	Set1	Set0	True	Passed	Model Under Test Equivalent Model
bc83e8836a024c2edc01e79afd2174f713cdbdc1	Apalache	Set1	Set0	False	Passed	Model Under Test Equivalent Model
4920420437000010f862ca566172e38a39a201c2	Apalache	Set2	Set0	True	Passed	Model Under Test Equivalent Model
50218a0e287364d2df68b3780add12ba39d1af0e	Apalache	Set2	Set0	False	Passed	Model Under Test Equivalent Model
a1aa4f5125ff5795670a52c962a2190b79287556	Apalache	Fun	Set0	True	Passed	Model Under Test Equivalent Model
8f5a0aea682f1a626e32f0f961958ca55227f6ce	Apalache	Fun	Set0	False	Passed	Model Under Test Equivalent Model
c46c61075a4d602e80010bc78e4b92ec34325533	Apalache	In	Set0	True	Passed	Model Under Test Equivalent Model
1e49103a311dfff02566df214836a6b5862c2248	Apalache	In	Set0	False	Passed	Model Under Test Equivalent Model
d11404f3b4786cd29d05ea884b0aa522973e361c	Apalache	NotIn	Set0	True	Passed	Model Under Test Equivalent Model
e4143e9807728913681bbf5b9b73226f933c26a1	Apalache	NotIn	Set0	False	Passed	Model Under Test Equivalent Model
a0aa8de41ba3d17af97d3b78ad58fa35dd730177	Apalache	Record	Set0	True	Passed	Model Under Test Equivalent Model
9e9d4be7eb08651c77771d3644825106523aaf98	Apalache	Record	Set0	False	Passed	Model Under Test Equivalent Model
b08c66c4aef9f7fecb2a8e1a42412cf13899e924	Apalache	Tuple	Set0	True	Passed	Model Under Test Equivalent Model
c2baf01312a74714378bc1c384c85b47b3545310	Apalache	Tuple	Set0	False	Passed	Model Under Test Equivalent Model
b0ce8dfd3f3cec0ae3691beb4906940e2f9a4a70	Apalache	FunApp	Set0	True	Passed	Model Under Test Equivalent Model
db7f49afb903b4fe40c339f60dc48885694c8023	Apalache	FunApp	Set0	False	Passed	Model Under Test Equivalent Model
ae98c0d2d80f264310eb14a91e82566aa236f906	Apalache	Except1Fun	Set0	True	Passed	Model Under Test Equivalent Model
3123b3aa3fa4019eba684e06c73745f5cfc02a08	Apalache	Except1Fun	Set0	False	Passed	Model Under Test Equivalent Model
02bcd673303a4721a0afcae7d0516ea6a178c6c9	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Set0	True	Passed	Model Under Test Equivalent Model
53fb9046306988dc9eb766a4cb91692b46645c50	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Set0	False	Passed	Model Under Test Equivalent Model
2b5d55448f3826280fb92d5fc49b4279d30da452	Apalache	Except1Rec	Set0	True	Passed	Model Under Test Equivalent Model
1d6eebba78f50e68da37384e790c9f62371ce336	Apalache	Except1Rec	Set0	False	Passed	Model Under Test Equivalent Model
12e976241a925f92783d85c1d01eca79bc6b1904	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	Set0	True	Passed	Model Under Test Equivalent Model
0bb29fa0c52da06c3bbc4d54205c9594090219a9	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	Set0	False	Passed	Model Under Test Equivalent Model
c77bbdec6d25a53364d1009ec91509c0bbad86b5	Apalache	Except2Fun	Set0	True	Passed	Model Under Test Equivalent Model
e5ca6213871e4d37bea4a9f51d18b628cb5fc876	Apalache	Except2Fun	Set0	False	Passed	Model Under Test Equivalent Model
d72cf3a5f56c1e34eb60fb377acbf6964fa5d57f	Apalache	Prime	Set0	True	Passed	Model Under Test Equivalent Model
e0ee75982ec63c577a1d5756cd0bf0d248df535b	Apalache	Prime	Set0	False	Passed	Model Under Test Equivalent Model
cd84e5dbb291b16a7587dde3644074fce16fa6f0	Apalache	DefFun	Set0	True	Passed	Model Under Test Equivalent Model
6280c3402c19df8d5695596492b9a0a805c28319	Apalache	DefFun	Set0	False	Passed	Model Under Test Equivalent Model
857cb621310c3e7fcc7ef51c26950f977d80e372	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Set0	True	Passed	Model Under Test Equivalent Model
0f83dcdb0977052510ff5f48e1dc1117dcf5d0eb	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Set0	False	Passed	Model Under Test Equivalent Model
7eda246306da60eea3d3ce7ddf9bf1e5a904e585	Apalache	DefFunRecursive	Set0	True	Passed	Model Under Test Equivalent Model
529ccb927295e8b18e393dffca7c111512f7f28e	Apalache	DefFunRecursive	Set0	False	Passed	Model Under Test Equivalent Model
d038477c3db9b9ff366055f0faba1711da24023f	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Set0	True	Passed	Model Under Test Equivalent Model
090e46c391b7d4cadd3f2cc3405740e1754a76bd	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Set0	False	Passed	Model Under Test Equivalent Model
d7cc5d35faf695c1be9691620b2f3a43f98776b4	Apalache	Def0	Set0	True	Passed	Model Under Test Equivalent Model
55cd503b0ddcf598306b7ea35f1a2aa5e7d2b9b5	Apalache	Def0	Set0	False	Passed	Model Under Test Equivalent Model
a82b1d18c9afdd6a101762cee7a03af041805693	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Set0	True	Passed	Model Under Test Equivalent Model
3148ce013e5f5003dfc5995235854febfcc99b11	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Set0	False	Passed	Model Under Test Equivalent Model
e28bd3a42e058f717b04c127a4def461a6d4ec74	Apalache	Def1	Set0	True	Passed	Model Under Test Equivalent Model
85f62bff8d39d8b6577236ce3fd23e1635784e0a	Apalache	Def1	Set0	False	Passed	Model Under Test Equivalent Model
100f0c611bcbf784fd75c683e36b8d2598fea499	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Set0	True	Passed	Model Under Test Equivalent Model
1022e6ab381588b76e515d41a995011d1a996ccb	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Set0	False	Passed	Model Under Test Equivalent Model
2545cf28d8031d7e8c93561044460763941e58de	Apalache	Def2	Set0	True	Passed	Model Under Test Equivalent Model
1ab507a02834e94a51d2ef7d0485ff8fd3b528f0	Apalache	Def2	Set0	False	Passed	Model Under Test Equivalent Model
7fe1d24d6540ee50c028320ca4be749f1aeeb5fa	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Set0	True	Passed	Model Under Test Equivalent Model
e56436740982a7ed1bd0c53757e9a8fa5a70f818	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Set0	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
8f009ce4d816f7dcde91a7f401a65a0a7ca37108	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Set0	True	Passed	Model Under Test Equivalent Model
e5a2b5e27a004ec66a74451f663b188556b4f830	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Set0	False	Passed	Model Under Test Equivalent Model
a2c9cd2320f461e506be5829247eb6ab616deefc	Apalache	Extends	Set0	True	Passed	Model Under Test Equivalent Model
d6e40edc922855431616966479d563d254dda5b8	Apalache	Extends	Set0	False	Passed	Model Under Test Equivalent Model
091459321091746587a278aa57da309396916887	Apalache	ExtendsInDifferentFolder	Set0	True	Passed	Model Under Test Equivalent Model
e1802a19373b7c9235a41096a3bbff79613cd203	Apalache	ExtendsInDifferentFolder	Set0	False	Passed	Model Under Test Equivalent Model
05e02dd226b1f8121e81c0cdcea7ab70c0ddd4e7	Apalache	Variable	Set0	True	Passed	Model Under Test Equivalent Model
0b9ba2af832b73206291defbbb4969a34fafedf2	Apalache	Variable	Set0	False	Passed	Model Under Test Equivalent Model
4bcb9866e3ce422b3183b9d337dae9a303540bda	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Set0	True	Passed	Model Under Test Equivalent Model
b8aaf9503cf9b50ac118bf45c2c4b6fd6a8b5ff3	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Set0	False	Passed	Model Under Test Equivalent Model
94582b58d0f8c6100467a78f5f863059fa20fe8b	Apalache	Constant	Set0	True	Passed	Model Under Test Equivalent Model
e11683bdc34bda821efc34d168b4a2d9747ff3f1	Apalache	Constant	Set0	False	Passed	Model Under Test Equivalent Model
778d644674d61cb383e2f14969dcf1c18ebcee8e	Apalache	ConstantRank1	Set0	True	Passed	Model Under Test Equivalent Model
ac0bf5fc0c1fd283149bbd191e69a471e1553d80	Apalache	ConstantRank1	Set0	False	Passed	Model Under Test Equivalent Model
6a3467296e07e13d29ef9babb265919c2b7fe42f	Apalache	Instance	Set0	True	Passed	Model Under Test Equivalent Model
6ddde844cff30cee7dad1ffbc2f6d42435aaa148	Apalache	Instance	Set0	False	Passed	Model Under Test Equivalent Model
76de8229193da9c3aa9e29eee3712946e1231559	Apalache	InstanceWith	Set0	True	Passed	Model Under Test Equivalent Model
55b77b9b5b3de207688dee48d6d6933eb6c97190	Apalache	InstanceWith	Set0	False	Passed	Model Under Test Equivalent Model
8780301f113c87bfca74b29a97a50a17c80dd14b	Apalache	InstanceNamed	Set0	True	Passed	Model Under Test Equivalent Model
c22637c220c384bd5a59a6f4cd106294178a30fb	Apalache	InstanceNamed	Set0	False	Passed	Model Under Test Equivalent Model
50a9ad68ceac9a0f4fed7425360f0c8823b48337	Apalache	InstanceNamedWith	Set0	True	Passed	Model Under Test Equivalent Model
9a4800d129b7c2ac92cf9d01046a764932aff5b5	Apalache	InstanceNamedWith	Set0	False	Passed	Model Under Test Equivalent Model
544ce0daaf75c17dc0e95fa47f603f928a35a842	Apalache	InstanceInFolder	Set0	True	Passed	Model Under Test Equivalent Model
6d0452982ec02bb1f0fa54c7e918dd1c78042c4b	Apalache	InstanceInFolder	Set0	False	Passed	Model Under Test Equivalent Model
187d9d5bfbb043055bd5bfde04555d048fb335cd	Apalache	InstanceWithInFolder	Set0	True	Passed	Model Under Test Equivalent Model
f14e18909fc592cc8dd39871e894601a1ce1a962	Apalache	InstanceWithInFolder	Set0	False	Passed	Model Under Test Equivalent Model
53f7517ec0eed26d3e1d5f6001bd411767142b67	Apalache	InstanceNamedInFolder	Set0	True	Passed	Model Under Test Equivalent Model
5105fbe6cce4fafd09d6071bf731c491daeabce7	Apalache	InstanceNamedInFolder	Set0	False	Passed	Model Under Test Equivalent Model
7f6553d0c12d4851ae6ba2fdf73b44989c176be5	Apalache	InstanceNamedWithInFolder	Set0	True	Passed	Model Under Test Equivalent Model
aa11e0544d2048dc4c657c82e64a2de90a18ecb6	Apalache	InstanceNamedWithInFolder	Set0	False	Passed	Model Under Test Equivalent Model
13ad0e1b4c7c1b82acf5d5d3f9e9203943f86156	Apalache	Lambda	Set0	True	Passed	Model Under Test Equivalent Model
d9b0dfb56c67f141e1e074f3844ca7a12571175f	Apalache	Lambda	Set0	False	Passed	Model Under Test Equivalent Model
060d17e968e35e68a41bb80760fea03b69780273	Apalache	Cross2	Set0	True	Passed	Model Under Test Equivalent Model
7cef224664596db717b3d40a0eca5f102931677d	Apalache	Cross2	Set0	False	Passed	Model Under Test Equivalent Model
f8a180468bb04ad0b7d7d5f98d18df64e40ef531	Apalache	Cross3	Set0	True	Passed	Model Under Test Equivalent Model
1d4dfda69dd30ddd48f1133bd45b41c5e38cba38	Apalache	Cross3	Set0	False	Passed	Model Under Test Equivalent Model
725fbe61378035c2dc753c47775abec4db215861	TLC with reduction strategy: Case 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))	FunSet	Set0	True	Passed	Model Under Test Equivalent Model
8e54d065d1bd555176c5d62e7e1f517a8bcfd9e7	TLC with reduction strategy: Case 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))	FunSet	Set0	False	Passed	Model Under Test Equivalent Model
16d4b1a9929d55153b84e7cf2a2c59466d6ede69	TLC with reduction strategy: Case 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)	RecordSet	Set0	True	Passed	Model Under Test Equivalent Model
22d342818d7053d49e5af7786e8e7ffd68247a87	TLC with reduction strategy: Case 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)	RecordSet	Set0	False	Passed	Model Under Test Equivalent Model
0b8aec9e34e98a278a42d22c2e56ef0e86156b19	Apalache	SetDiff	Set0	True	Passed	Model Under Test Equivalent Model
ea2dcf4cad53060cdc1b55d4dda28ed6ef99466d	Apalache	SetDiff	Set0	False	Passed	Model Under Test Equivalent Model
0950d10ef4ed2cfba026a51abb51d597db0a81ac	Apalache	SetUnion	Set0	True	Passed	Model Under Test Equivalent Model
b97e032ee820f9f383fbe98aa26e6cb59d80f6ac	Apalache	SetUnion	Set0	False	Passed	Model Under Test Equivalent Model
8969c28e71b9d810d8325f5d6f9dd64a9e3e2f13	Apalache	SetIntersect	Set0	True	Passed	Model Under Test Equivalent Model
532740fb8b3d4e97b776f2d6fb5e1bd6991fef8c	Apalache	SetIntersect	Set0	False	Passed	Model Under Test Equivalent Model
383b6071b147d15a6b5b76b19f1aa092aed663bd	Apalache	SubsetEq	Set0	True	Passed	Model Under Test Equivalent Model
fe452adee410e9797eedec6ffc8e46ddcd9ed069	Apalache	SubsetEq	Set0	False	Passed	Model Under Test Equivalent Model
f4b0f5587d39953f1cea52921a8d246e5603e321	Apalache	IfThen	Set0	True	Passed	Model Under Test Equivalent Model
5d6efe4fc8aeff15400b743d4848506f82312e88	Apalache	IfThen	Set0	False	Passed	Model Under Test Equivalent Model
05f6979663158709885af89e0786faf4cd44cdcf	Apalache	IfElse	Set0	True	Passed	Model Under Test Equivalent Model
70625b95c7967e121363a65a20f03d361e80a027	Apalache	IfElse	Set0	False	Passed	Model Under Test Equivalent Model
c733a3960b2a7027cbc1379a6bdc558c0e810e4f	Apalache	Subset	Set0	True	Passed	Model Under Test Equivalent Model
f45826c075a56deb8b9ac414eb59b6080dc260ba	Apalache	Subset	Set0	False	Passed	Model Under Test Equivalent Model
be1eb05fb3885333dc464afa6e64ecbf61e2b5fd	Apalache	Union	Set0	True	Passed	Model Under Test Equivalent Model
966939c6aeadbac5b9f2bdaf59559802248ca34e	Apalache	Union	Set0	False	Passed	Model Under Test Equivalent Model
d84b4bed8c9f0c555dcfc34d913adb28a3112bd0	Apalache	Unchanged	Set0	True	Passed	Model Under Test Equivalent Model
cbc4a5be7cd7c7ef205fd62932ac4ca7765f910c	Apalache	Unchanged	Set0	False	Passed	Model Under Test Equivalent Model
b5523b7f65e9f4e4ccbcdda14c64222f335f95ac	Apalache	SeqSeq	Set0	True	Passed	Model Under Test Equivalent Model
49ee8b08393433b9723837f44f8db0358c7ea917	Apalache	SeqSeq	Set0	False	Passed	Model Under Test Equivalent Model
3cb2de7433d36ae76d2145d270c968e083b87496	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Set0	True	Passed	Model Under Test Equivalent Model
b2b107980030e30bdba65df4f4cb96a067df1011	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Set0	False	Passed	Model Under Test Equivalent Model
ba99548442a8cb03a738f94e280ca709b7f5201e	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	Set0	True	Passed	Model Under Test Equivalent Model
eab7eb8d73b3f48fc0e18f64279603385880ac87	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	Set0	False	Passed	Model Under Test Equivalent Model
de4c4534207d2012501613fb65919f61bd81be9e	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Set0	True	Passed	Model Under Test Equivalent Model
49af65d821d972d55d954e3600e02036580bf1b3	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Set0	False	Passed	Model Under Test Equivalent Model
94251b430ea317767e4cfb38f92bc27c2cbedbd8	Apalache	BagSetToBag	Set0	True	Passed	Model Under Test Equivalent Model
8425d44e99397e49ba32cecb030d284648649b73	Apalache	BagSetToBag	Set0	False	Passed	Model Under Test Equivalent Model
5a47102a50f6a2b85e3c4fa214b8226d60f81863	Apalache	BagBagIn	Set0	True	Passed	Model Under Test Equivalent Model
caf95fd3ebbc088fc3dc1b20a22dcde934f55851	Apalache	BagBagIn	Set0	False	Passed	Model Under Test Equivalent Model
9475c853ca51d7e90836a24e1cbaa948f86ee9f9	Apalache	BagCopiesIn	Set0	True	Passed	Model Under Test Equivalent Model
2046c7839c61a99d16bb8616b025076300879189	Apalache	BagCopiesIn	Set0	False	Passed	Model Under Test Equivalent Model
5a01c026c6d1455da238d22c892d909a9910fc7d	Apalache	BagBagUnion	Set0	True	Passed	Model Under Test Equivalent Model
0a77192f1209c77135c9307377a80e0ddd332a74	Apalache	BagBagUnion	Set0	False	Passed	Model Under Test Equivalent Model
0d3d81fd2f07d4f7198dfb3c7a81bdce26b7d29f	TLC with reduction strategy: Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)	FiniteSetsIsFiniteSet	Set0	True	Passed	Model Under Test Equivalent Model
2d4d3d4bd250d78285058878d7bb5cfff4b2f9ad	TLC with reduction strategy: Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)	FiniteSetsIsFiniteSet	Set0	False	Passed	Model Under Test Equivalent Model
2f9dc7282e611192a5b895b85902a15321eb780e	Apalache	FiniteSetsCardinality	Set0	True	Passed	Model Under Test Equivalent Model
18b8d8adcc61fbc1c349d2f43e5068e669ede0a8	Apalache	FiniteSetsCardinality	Set0	False	Passed	Model Under Test Equivalent Model
2c4de9576975e5081fd6297a0a249aba8346f5af	Apalache	SeqAppend	Set0	True	Passed	Model Under Test Equivalent Model
4cf1f6bf20572f3b913b17621a91abf0f448ea7d	Apalache	SeqAppend	Set0	False	Passed	Model Under Test Equivalent Model

Index

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