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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
bde3dd56526d8c05fcb2533d5604a3971e9b5f9e	Apalache	And	Not	True	Passed	Model Under Test Equivalent Model
b356d2503f38f9bd3ab7d0f5534425ba6f1063c4	Apalache	And	Not	False	Passed	Model Under Test Equivalent Model
f32be84bcb25b678147d2bbe2fa33ab5e139e0f1	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	Not	True	Passed	Model Under Test Equivalent Model
fe0d36f35fa3a18fdaf969c095d824ca0d1a790d	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	Not	False	Passed	Model Under Test Equivalent Model
90f1e67440dc17e354c7f85b66117bdd834f3fab	Apalache	Imply	Not	True	Passed	Model Under Test Equivalent Model
5c4dae6909fe3a7df20b32cbb785953be4a79162	Apalache	Imply	Not	False	Passed	Model Under Test Equivalent Model
306456070cb441c51b54dee95f9e338da4befac8	Apalache	Not	Not	True	Passed	Model Under Test Equivalent Model
067efe3c3b5e6bdf7d0dd9f0c7ca026846a999f4	Apalache	Not	Not	False	Passed	Model Under Test Equivalent Model
72343bdf1061d442c715969692a4a49b39b482f7	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	Not	True	Passed	Model Under Test Equivalent Model
f34111f8e99d4837785a0424248967de04251179	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	Not	False	Passed	Model Under Test Equivalent Model
a5aaa01ef26ef717e4e040efaab4474dba560b80	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	Not	True	Passed	Model Under Test Equivalent Model
a23eccccd6e3104967cd1f5abe594f3f9111bfcc	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	Not	False	Passed	Model Under Test Equivalent Model
b3b9095f903ac03be858ca24df566ed7032db9d0	Apalache	AndProp	Not	True	Passed	Model Under Test Equivalent Model
d399c3ca9ec6c9b75aa5fe4eee8959f029c26548	Apalache	AndProp	Not	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
9ef3a20352e38aeb37af37ad4360a385eac25d23	Apalache	Eq	Not	True	Passed	Model Under Test Equivalent Model
0d0029507005791253d40c91b936f9e9d409c19c	Apalache	Eq	Not	False	Passed	Model Under Test Equivalent Model
9e66e99317be5d9ae88e96ec4f22696c7b784d3e	Apalache	Ne	Not	True	Passed	Model Under Test Equivalent Model
95f55f66cff664863595b3e3bb3ebd26c499685d	Apalache	Ne	Not	False	Passed	Model Under Test Equivalent Model
c85781eb0f6d5a54314ee18d24c81854477a4c70	Apalache	Let	Not	True	Passed	Model Under Test Equivalent Model
bf21403654892c5050acbeedd8bc42af1f006d37	Apalache	Let	Not	False	Passed	Model Under Test Equivalent Model
f9b6889d0f93c692c862a0aa471253c712f911dc	Apalache	Set0	Not	True	Passed	Model Under Test Equivalent Model
61989fb6ae65577da5e525df4fd044abe5eb53e5	Apalache	Set0	Not	False	Passed	Model Under Test Equivalent Model
3b16f950f51ad09bedabb74617d0ca1e92dd29a8	Apalache	Set1	Not	True	Passed	Model Under Test Equivalent Model
ca0013887556fe0cea75e793b6bd83141a98afdf	Apalache	Set1	Not	False	Passed	Model Under Test Equivalent Model
32ced51d7bad6caf609a4c50261bf822dbc2851f	Apalache	Set2	Not	True	Passed	Model Under Test Equivalent Model
e90de7743fb232f037e638ecd064f1865fd68085	Apalache	Set2	Not	False	Passed	Model Under Test Equivalent Model
724817d16dfeb1c71eb7e2e8f0ea743f61693f3c	Apalache	Fun	Not	True	Passed	Model Under Test Equivalent Model
582eaa9b5cd42999fb528e0c49bd603e7db2e5a2	Apalache	Fun	Not	False	Passed	Model Under Test Equivalent Model
c01faef2df5deeee02540c37ff0324097a453d56	Apalache	In	Not	True	Passed	Model Under Test Equivalent Model
808f570465a6ac23e5ae888d79ab1f3a809e2174	Apalache	In	Not	False	Passed	Model Under Test Equivalent Model
1d3bed688f7da90a785f805c0c2433abcc4f0e06	Apalache	NotIn	Not	True	Passed	Model Under Test Equivalent Model
b6b8d714da92b5e48de717609688a8dc6caaad13	Apalache	NotIn	Not	False	Passed	Model Under Test Equivalent Model
328de057e68d8059306b85730850a298641410c1	Apalache	Exists	Not	True	Passed	Model Under Test Equivalent Model
6b9f597b80bd75c11a3077126df645393e3d51b9	Apalache	Exists	Not	False	Passed	Model Under Test Equivalent Model
79715d99ec5ab4d68cb805fdef68335d9bf1e31d	Apalache	Forall	Not	True	Passed	Model Under Test Equivalent Model
559c1fd79ee55a143503d5ea00d5d90bce05f520	Apalache	Forall	Not	False	Passed	Model Under Test Equivalent Model
6f4b6450456ea77d11909cabd20cdee0a7323965	Apalache	Choose	Not	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
f2f82f385106fcf3529bcb41555fcf0e475d4ab8	Apalache	Choose	Not	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
3fa73ca397661e5e35bdd4d53c6064db2bd6f57b	Apalache	Record	Not	True	Passed	Model Under Test Equivalent Model
725db4bdbcd3568800d0757616d00e2edca19aa9	Apalache	Record	Not	False	Passed	Model Under Test Equivalent Model
7fe9cc35ff2736f1900a1d59ffec7fac2f00d4bc	Apalache	Tuple	Not	True	Passed	Model Under Test Equivalent Model
a629994cc4319d21ce547199934c3a8faabff995	Apalache	Tuple	Not	False	Passed	Model Under Test Equivalent Model
3976d45ff757e3f0ee83cce760661b367bfd44af	Apalache	FunApp	Not	True	Passed	Model Under Test Equivalent Model
bb4a571886b0fedc04e67f468956e1de5b2a85b8	Apalache	FunApp	Not	False	Passed	Model Under Test Equivalent Model
f0d887f774e10c62e02b8b9b54d5cfbf0c3956e2	Apalache	Except1Fun	Not	True	Passed	Model Under Test Equivalent Model
591e98ed958b2b6ec167764f6f9c978a93f8a62e	Apalache	Except1Fun	Not	False	Passed	Model Under Test Equivalent Model
aabb28f4a91a27cee1bf8a4fe2e8d4b0c92ec46b	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Not	True	Passed	Model Under Test Equivalent Model
6ef250972d19fcef5184a2549aee94e07bfe0b75	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Not	False	Passed	Model Under Test Equivalent Model
141d59aba9bdc82afd2b9ae0c731c91547115eb6	Apalache	Except1Rec	Not	True	Passed	Model Under Test Equivalent Model
758178f118a885c453c33cf35e5af0137ecb42ac	Apalache	Except1Rec	Not	False	Passed	Model Under Test Equivalent Model
3229fdb09a23b2df7d810559894a7563e672e845	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	Not	True	Passed	Model Under Test Equivalent Model
77be4eef3f4dc78f24a69244aa40274d456be958	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	Not	False	Passed	Model Under Test Equivalent Model
d15ba9c7f0130f3bcdb322ec6f3ed173213393e3	Apalache	Except2Fun	Not	True	Passed	Model Under Test Equivalent Model
8214e1e03135f71d993eaf1f9f96e1b91c62dfda	Apalache	Except2Fun	Not	False	Passed	Model Under Test Equivalent Model
443ca44ac58fac6bc25f093f7c38e8492fe7c495	Apalache	Prime	Not	True	Passed	Model Under Test Equivalent Model
194f8f56fd4fdfedf7e0b4f4a06bfd32c1ad792d	Apalache	Prime	Not	False	Passed	Model Under Test Equivalent Model
951781c18032422457c42dc250fc53a8a85acd60	Apalache	DefFun	Not	True	Passed	Model Under Test Equivalent Model
0c78a63878af135d2ea0894c884f7229ca9885ff	Apalache	DefFun	Not	False	Passed	Model Under Test Equivalent Model
942807f3d88d407f7e9e53ba5e97e194625b23e0	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Not	True	Passed	Model Under Test Equivalent Model
5d581b66b9dbddcad75fb46f823c21101ef11aed	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Not	False	Passed	Model Under Test Equivalent Model
e3b10ba64b0a3b0b1794bd5411a0ba8e330d787c	Apalache	DefFunRecursive	Not	True	Passed	Model Under Test Equivalent Model
db8684c8df227b7669c94220a58eb4114bd6b664	Apalache	DefFunRecursive	Not	False	Passed	Model Under Test Equivalent Model
51f027a43c1eca3ee281727ed363cd522be9103d	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Not	True	Passed	Model Under Test Equivalent Model
b0c0c4251db18faf033e01df75fd521b2ff46c0b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Not	False	Passed	Model Under Test Equivalent Model
e25e3726fa999da58593f4ae2056fa571dc97dda	Apalache	Def0	Not	True	Passed	Model Under Test Equivalent Model
6e8c043ff9c7bc5e701297be2529e26b40389f8b	Apalache	Def0	Not	False	Passed	Model Under Test Equivalent Model
8654e294bc5e5f214c5fc5791ac4734f13474c7f	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Not	True	Passed	Model Under Test Equivalent Model
29bb1d48f2d9da0c87bc3e06ddc2d5198ca984da	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Not	False	Passed	Model Under Test Equivalent Model
b8eb1a420db359a882b2edb725aa38e1d50dbb17	Apalache	Def1	Not	True	Passed	Model Under Test Equivalent Model
9254870bf23a7263621c1dd2527f210512e54673	Apalache	Def1	Not	False	Passed	Model Under Test Equivalent Model
abee8024c5fa8b5411d45c242effe4916475a9f7	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Not	True	Passed	Model Under Test Equivalent Model
326d0298ef24da0b5d7cab35372fb89b2b5e34ea	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Not	False	Passed	Model Under Test Equivalent Model
0d734bbc05c0a98d7d5ddd677f9abce9df24d4bc	Apalache	Def2	Not	True	Passed	Model Under Test Equivalent Model
49d4f3584348c6739018c020548a9287d258958f	Apalache	Def2	Not	False	Passed	Model Under Test Equivalent Model
1723780b0dd96417494df067a13034d4288f0572	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Not	True	Passed	Model Under Test Equivalent Model
ce27716b5a1ed370b28d56684016c92fc61031da	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Not	False	Passed	Model Under Test Equivalent Model
f76acc7f791b910d516d32df3d75eae199426317	Apalache	Def1Recursive	Not	True	Passed	Model Under Test Equivalent Model
c5b5eab4ef1cbe2ac0e61d2a809767679c320b5c	Apalache	Def1Recursive	Not	False	Passed	Model Under Test Equivalent Model
3885c60a8893f4465b40f3560fe20a607078de8c	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Not	True	Passed	Model Under Test Equivalent Model
3ed3a088d637883546414ab9556d0e67cfd9dc47	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Not	False	Passed	Model Under Test Equivalent Model
f01d366758a3b1f9a433129099f1e6856f749ab3	Apalache	Extends	Not	True	Passed	Model Under Test Equivalent Model
f68c8a06103223a2253b68cf4fca5f626efe425d	Apalache	Extends	Not	False	Passed	Model Under Test Equivalent Model
36795d84082b110d2d5ef5e31052c5b015f83001	Apalache	ExtendsInDifferentFolder	Not	True	Passed	Model Under Test Equivalent Model
f8620fd3e104761dca0c388693a4007d03e2ed52	Apalache	ExtendsInDifferentFolder	Not	False	Passed	Model Under Test Equivalent Model
74b0eb20af7a3683f4d419d0ef7e446440f7c00a	Apalache	Variable	Not	True	Passed	Model Under Test Equivalent Model
a3c9baea421b54da7506b64ac43ee5fd608e5f55	Apalache	Variable	Not	False	Passed	Model Under Test Equivalent Model
ba394567a098b0aecf6fb385c730e395639858a2	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Not	True	Passed	Model Under Test Equivalent Model
eefd347c7097b1c84bd57fa86ef17894cc232fec	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Not	False	Passed	Model Under Test Equivalent Model
d53641767d904b3303b9383508e4f61901dec04d	Apalache	Constant	Not	True	Passed	Model Under Test Equivalent Model
ec052f170e4de95f1a12a720bf4be86003dd9a50	Apalache	Constant	Not	False	Passed	Model Under Test Equivalent Model
009c74d7c74476a0c3f5671e997d7916ccd6cccb	Apalache	ConstantRank1	Not	True	Passed	Model Under Test Equivalent Model
9316b4c2b916b37b5c75be6e3c9660c4bf56a12d	Apalache	ConstantRank1	Not	False	Passed	Model Under Test Equivalent Model
95c0ef9a622fc4a90526158599fcbac5e42ddabd	Apalache	Instance	Not	True	Passed	Model Under Test Equivalent Model
7d8a8127df7ce8339ca8648190985cec1314a095	Apalache	Instance	Not	False	Passed	Model Under Test Equivalent Model
b02dac24c226ef3234d1dbece6e40a69ef250b48	Apalache	InstanceWith	Not	True	Passed	Model Under Test Equivalent Model
f204c067f5e8c595943d5945e701b6d3de229f52	Apalache	InstanceWith	Not	False	Passed	Model Under Test Equivalent Model
0a1fefd3cd05cc7a134366f9a35a80072a9e31a5	Apalache	InstanceNamed	Not	True	Passed	Model Under Test Equivalent Model
502bfe6324a9e7d54946434406f2b4e8dc4df716	Apalache	InstanceNamed	Not	False	Passed	Model Under Test Equivalent Model
15cb67f320745cb2e12f265a278c2240075bdaa7	Apalache	InstanceNamedWith	Not	True	Passed	Model Under Test Equivalent Model
c08e9332bad9631a39d7eb597c1009acf6709e4b	Apalache	InstanceNamedWith	Not	False	Passed	Model Under Test Equivalent Model
ef78c6d965452504ac9256dc36d5099507539abb	Apalache	InstanceInFolder	Not	True	Passed	Model Under Test Equivalent Model
3682c3592928e700f3a1c2e9f6a03fb91407fa35	Apalache	InstanceInFolder	Not	False	Passed	Model Under Test Equivalent Model
30e999fc4ac4c361ca9bcd8f9c32ca1ea88f5199	Apalache	InstanceWithInFolder	Not	True	Passed	Model Under Test Equivalent Model
12ca80172623e499ef080e0c847a6b7233c1fcaf	Apalache	InstanceWithInFolder	Not	False	Passed	Model Under Test Equivalent Model
4409246e885448a3d0bea10c0b1b2c1f11e59e75	Apalache	InstanceNamedInFolder	Not	True	Passed	Model Under Test Equivalent Model
9b17098bb39173925b22fced82bc1a7b0e70e59a	Apalache	InstanceNamedInFolder	Not	False	Passed	Model Under Test Equivalent Model
486536447f0e26c3e46442617755cbfbd9a8b9d6	Apalache	InstanceNamedWithInFolder	Not	True	Passed	Model Under Test Equivalent Model
cdf6de2ea742c1bc18917101e09b2703e5fca252	Apalache	InstanceNamedWithInFolder	Not	False	Passed	Model Under Test Equivalent Model
89c236159a0cbea584b1c43cc58659ca793b66d9	Apalache	Enabled	Not	True	Passed	Model Under Test Equivalent Model
37e0a8995dbf39dc7b9d9ebccd61406092d03c0d	Apalache	Enabled	Not	False	Passed	Model Under Test Equivalent Model
c6993462344521884eee0827d1eb34890bac66ea	Apalache	Assume	Not	True	Passed	Model Under Test Equivalent Model
ab1ed1527c6e1d15d04eff06e048d59c2dad1506	Apalache	Assume	Not	False	Passed	Model Under Test Equivalent Model
4de9f86db8ac23f64ca038a596243105e3fb5033	Apalache	AssumeNamed	Not	True	Passed	Model Under Test Equivalent Model
a333320177240021c257d3b3572be5b9fc9ba974	Apalache	AssumeNamed	Not	False	Passed	Model Under Test Equivalent Model
5ad8f1468be36eb0fd6b3108fed35827132cf032	Apalache	Lambda	Not	True	Passed	Model Under Test Equivalent Model
f7b76d27b6954261b997535d72efcbe60aa6d13e	Apalache	Lambda	Not	False	Passed	Model Under Test Equivalent Model
5a0769ca50983e0f0b3002735033c351d6666c8c	Apalache	IfCond	Not	True	Passed	Model Under Test Equivalent Model
d2c6a7f946ab4fc03d90e1e611d902c634f57133	Apalache	IfCond	Not	False	Passed	Model Under Test Equivalent Model
f9120c3685048682711edb5d8b05d141dea0821d	Apalache	IfThen	Not	True	Passed	Model Under Test Equivalent Model
fa32b0575038e4d2a7dabe1e0e98f8da64ac83f8	Apalache	IfThen	Not	False	Passed	Model Under Test Equivalent Model
0d5408fc42709c930937894a009171dab3acef10	Apalache	IfElse	Not	True	Passed	Model Under Test Equivalent Model
db2153d34158d93b4d032ca0af6663184d7f5976	Apalache	IfElse	Not	False	Passed	Model Under Test Equivalent Model
f4a5fc7eca8c1027815dc7867e0364e46b827e2c	Apalache	Unchanged	Not	True	Passed	Model Under Test Equivalent Model
320a7eb5a4eee1bbf9f3ae33ba578b5d563630cb	Apalache	Unchanged	Not	False	Passed	Model Under Test Equivalent Model
93f4e71e3e81f963325458316d0e8a0850225742	Apalache	Equivalence	Not	True	Passed	Model Under Test Equivalent Model
596359e670c0d2603bef29d5347eb42501a282e1	Apalache	Equivalence	Not	False	Passed	Model Under Test Equivalent Model
6f82028fd2765f9d4201a0a215b26ae2d631f43e	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Not	True	Passed	Model Under Test Equivalent Model
28e09122612cf3c3d109441843f8870b4637e443	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Not	False	Passed	Model Under Test Equivalent Model
8379b3b86568127fad0ea572e0d90f0cd2ad1c83	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Not	True	Passed	Model Under Test Equivalent Model
6042d287e7317d62b771df43a2850a9b25f40a98	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Not	False	Passed	Model Under Test Equivalent Model
8ed77716c188ce2af48d077cb084042449538ff5	Apalache	BagBagIn	Not	True	Passed	Model Under Test Equivalent Model
ede531bd35dba1539850a0c8144fc576e45f0900	Apalache	BagBagIn	Not	False	Passed	Model Under Test Equivalent Model
1169e03b27b98bbecdf0c7c942fe590ca1718650	Apalache	BagCopiesIn	Not	True	Passed	Model Under Test Equivalent Model
db90cea1225a3790afd75c30373d263bbd84d21e	Apalache	BagCopiesIn	Not	False	Passed	Model Under Test Equivalent Model
98a41c14095285515cab89e526fc2222d5ed48cb	Apalache	SeqAppend	Not	True	Passed	Model Under Test Equivalent Model
d58248553bd09c8311a795b6dd061ab544f97d8a	Apalache	SeqAppend	Not	False	Passed	Model Under Test Equivalent Model

Index

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