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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
23025fbcd8936222f9ecd5d962e96c1c6a2e0bdb	Apalache	And	And	True	Passed	Model Under Test Equivalent Model
2e0b8a91610c08545b3c504344ed8b6804140875	Apalache	And	And	False	Passed	Model Under Test Equivalent Model
3b0f9b30dcd7fa9aec1bbcce8af69dd5954757c9	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	And	True	Passed	Model Under Test Equivalent Model
30db4bf014b0d23e9e18b2d1c8f864e28128c697	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	And	False	Passed	Model Under Test Equivalent Model
30e0bc9cd7d72c14a253f8fef6e3a72dbdeb356d	Apalache	Imply	And	True	Passed	Model Under Test Equivalent Model
8a10eda0546c96ae209d1b2788f8f2c7b927d29e	Apalache	Imply	And	False	Passed	Model Under Test Equivalent Model
1eef4085ef3dd9dd4764d72bc092b06258cfc0fb	Apalache	Not	And	True	Passed	Model Under Test Equivalent Model
b3ad7d811b6ceeb78da8ca69dc5ce436397bca7e	Apalache	Not	And	False	Passed	Model Under Test Equivalent Model
76a649ed1a43817fff112b17a5739a6477fbdb80	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	And	True	Passed	Model Under Test Equivalent Model
1be54779a56284ed80b1a7e7cad9e6e00b6b2393	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	And	False	Passed	Model Under Test Equivalent Model
86d67e4ee5d86734c079c958addcb25e7f989e95	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	And	True	Passed	Model Under Test Equivalent Model
eeca228f1f6ad9e5ffc9af1fd9392729dbcbe5b7	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	And	False	Passed	Model Under Test Equivalent Model
1ce4f5773f7d8b622856a335cc7485327c83fbe5	Apalache	AndProp	And	True	Passed	Model Under Test Equivalent Model
5ea6d3c2a8d49f60d55d0b43270e110658013890	Apalache	AndProp	And	False	Passed	Model Under Test Equivalent Model
957bd8e1bbc932665fd6eb9b16b500a8c904418c	Apalache	Boxed	And	True	Passed	Model Under Test Equivalent Model
f726da81f621df9985a4e1da54729db8a35b6d3e	Apalache	Boxed	And	False	Passed	Model Under Test Equivalent Model
0ec84299f7fddfabfcee8fb2acc5c06f30c38b91	Apalache	Eq	And	True	Passed	Model Under Test Equivalent Model
3e7a0c3ee40e61d8477341b5d3bf29fd13b00d90	Apalache	Eq	And	False	Passed	Model Under Test Equivalent Model
3e1fc72bf797ae10a67492b2f3be7c68ab292d12	Apalache	Ne	And	True	Passed	Model Under Test Equivalent Model
717721b88ff823ae158a03239acf2add5c8649a5	Apalache	Ne	And	False	Passed	Model Under Test Equivalent Model
4590c0d29ca74d0f554a4612ae59ec9b70b8ac90	Apalache	Let	And	True	Passed	Model Under Test Equivalent Model
3452634f7ed56b53b96306eeb7f5b4d876187680	Apalache	Let	And	False	Passed	Model Under Test Equivalent Model
5aaa4a3ade9f8b2d4907cfa9161f3239fb5976fd	Apalache	Set0	And	True	Passed	Model Under Test Equivalent Model
03d542f84f353571b4a37ece8753addc933b9c3c	Apalache	Set0	And	False	Passed	Model Under Test Equivalent Model
f96f1aa9f578d0280220cde9543966c7c9f58b32	Apalache	Set1	And	True	Passed	Model Under Test Equivalent Model
ae57f7023e0c1d7339c73b5e7115963f5eb111cf	Apalache	Set1	And	False	Passed	Model Under Test Equivalent Model
53580c96fca888df598dbe2a03a5c786e123711c	Apalache	Set2	And	True	Passed	Model Under Test Equivalent Model
2bdff88b939a033ccc0b39545c45d86a78290f18	Apalache	Set2	And	False	Passed	Model Under Test Equivalent Model
aa8432aa959ddfb76b7b396dc023623c81d3527e	Apalache	Fun	And	True	Passed	Model Under Test Equivalent Model
07668dd4fa7ff418b39146f18d1e975748e591c6	Apalache	Fun	And	False	Passed	Model Under Test Equivalent Model
65ce41b483a2636da7a0606285d1e68e4127396e	Apalache	In	And	True	Passed	Model Under Test Equivalent Model
ffa6524a8879828fc800d7315f5fa46b2c1a23a1	Apalache	In	And	False	Passed	Model Under Test Equivalent Model
6fca85d169975c0a58204d27b45bbdded8b1cb35	Apalache	NotIn	And	True	Passed	Model Under Test Equivalent Model
76d5a28a8b57e12fb2086b11782a97c29ecc2414	Apalache	NotIn	And	False	Passed	Model Under Test Equivalent Model
5332141224a2d3fc948c1be832a3c6aa96666574	Apalache	Exists	And	True	Passed	Model Under Test Equivalent Model
56f02cf1d0802de9f601dacb7b5ebab4a6ad3fd5	Apalache	Exists	And	False	Passed	Model Under Test Equivalent Model
9da46ad15f99ba3a7af1ee2065369ae3e8d84a53	Apalache	Forall	And	True	Passed	Model Under Test Equivalent Model
880b7defc6fe642b0a2206180cdf7f3085af8d5e	Apalache	Forall	And	False	Passed	Model Under Test Equivalent Model
cc558a2e9f56efa6d0c6a991647611410173c8f4	Apalache	Choose	And	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
c530df788f11eab722295a74084444a71942868f	Apalache	Choose	And	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
9f4499a6de4cca8631a60a9037cde4c839baaf17	Apalache	Record	And	True	Passed	Model Under Test Equivalent Model
428e21c7e9ac79e2db5d59ea94aa42e9017e6454	Apalache	Record	And	False	Passed	Model Under Test Equivalent Model
7d0cc700a1b5de035a1c59394704c3e3dc86a4bb	Apalache	Tuple	And	True	Passed	Model Under Test Equivalent Model
c8c1457d8f7191d7f00434be8972935fc2c52cfd	Apalache	Tuple	And	False	Passed	Model Under Test Equivalent Model
7888fe3891a88c2ebc2d8b2456728ae30e2b8476	Apalache	FunApp	And	True	Passed	Model Under Test Equivalent Model
1a51acb4d4ecfb8ffb4d9b0f002269d19817e300	Apalache	FunApp	And	False	Passed	Model Under Test Equivalent Model
ba2ca2d336de0ddaa7fdebd3e79eb3fad39238cf	Apalache	Except1Fun	And	True	Passed	Model Under Test Equivalent Model
4d2cff560c49e8c03609f708200bdd8cd05bc9ff	Apalache	Except1Fun	And	False	Passed	Model Under Test Equivalent Model
98bd44355466ec6519fbb27da4961e6ba7741c4f	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	And	True	Passed	Model Under Test Equivalent Model
12ac8d87c66c3d09079cf73613e8bdaef39c635d	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	And	False	Passed	Model Under Test Equivalent Model
32bb17411ffa2a39a7239fc859758d867c95e33f	Apalache	Except1Rec	And	True	Passed	Model Under Test Equivalent Model
f4af101b90c31328e6bbf22688d76b875e9fd592	Apalache	Except1Rec	And	False	Passed	Model Under Test Equivalent Model
83ed5fff341f881bcc5225bd8f2e2d15ebd3d9e1	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	And	True	Passed	Model Under Test Equivalent Model
f1d7f915673731a4c3939651b7b3731ae7ae46c9	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	And	False	Passed	Model Under Test Equivalent Model
5c3e045cde5492750a5a4461c83e2f79919ff9d9	Apalache	Except2Fun	And	True	Passed	Model Under Test Equivalent Model
c3f539a6598d9bbe63c92237372958b5a6ba2d97	Apalache	Except2Fun	And	False	Passed	Model Under Test Equivalent Model
c991ad52bae67ecf7024102ac2d7d746d4589c10	Apalache	Prime	And	True	Passed	Model Under Test Equivalent Model
cf9893eb0ea13a1b22ac855ea1f85cc482735a53	Apalache	Prime	And	False	Passed	Model Under Test Equivalent Model
e79b7f1c6900dd5c3ab1eb0f4b3bcb13ef0a4965	Apalache	DefFun	And	True	Passed	Model Under Test Equivalent Model
3d1713cb7a6f01f834e9cece80accb72fe90406d	Apalache	DefFun	And	False	Passed	Model Under Test Equivalent Model
ec9581169ad99de87afbda406716d11e68d07472	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	And	True	Passed	Model Under Test Equivalent Model
85da523b1e71e66d170c5021f07c233210ab5d9e	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	And	False	Passed	Model Under Test Equivalent Model
91d87ad69372bef0983472d6a2bc85ca778b08ae	Apalache	DefFunRecursive	And	True	Passed	Model Under Test Equivalent Model
7f23713268ca0e1f460397ffebe0b0bfb5e3243e	Apalache	DefFunRecursive	And	False	Passed	Model Under Test Equivalent Model
3e9299e95b50ddc8078cc2415fa85954141cd524	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	And	True	Passed	Model Under Test Equivalent Model
4830ccb35ade38886203c58ffe3123317d1934f3	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	And	False	Passed	Model Under Test Equivalent Model
89545d8e531014711ac3b6cc7b27994dbc862f2b	Apalache	Def0	And	True	Passed	Model Under Test Equivalent Model
3a043a81bbc9421da16778de13e80ca6d2ae8f57	Apalache	Def0	And	False	Passed	Model Under Test Equivalent Model
ef8be8c8737efecd864f41b346f4144be2b70b1e	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	And	True	Passed	Model Under Test Equivalent Model
ba1a817abec98c3c08fb7b75bfe3055adf2f5216	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	And	False	Passed	Model Under Test Equivalent Model
7f776639b1b78fab1036f26266fc998f1d0e15b8	Apalache	Def1	And	True	Passed	Model Under Test Equivalent Model
9c3f454a94001ee9c3c812479073ea9cc71eb561	Apalache	Def1	And	False	Passed	Model Under Test Equivalent Model
fb5059d04468edd8c277ade1c82eafb29596d536	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	And	True	Passed	Model Under Test Equivalent Model
dda05781d09e2f0aaae766bfeb2181f79fac6b3d	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	And	False	Passed	Model Under Test Equivalent Model
03137c8cb78812556d84ba314d1c7acaabccf920	Apalache	Def2	And	True	Passed	Model Under Test Equivalent Model
38b43ab0ea035342d321fde55d19d3229496efad	Apalache	Def2	And	False	Passed	Model Under Test Equivalent Model
94a2ad2f82228a6691a04a9120003d65b10cd9e0	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	And	True	Passed	Model Under Test Equivalent Model
f0c3af74ba4e643f2ed61a6e66a0b021f65fbced	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	And	False	Passed	Model Under Test Equivalent Model
968dd79c8b3bc18ac153e19aaf82cd7d8e67c1a3	Apalache	Def1Recursive	And	True	Passed	Model Under Test Equivalent Model
194416f2f0d5974dd004c3538a58bb3bd1eaadc4	Apalache	Def1Recursive	And	False	Passed	Model Under Test Equivalent Model
1221c2a5ea9dbed26287934a55d72bc107e6dad4	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	And	True	Passed	Model Under Test Equivalent Model
87b1def3d0f481aa94e324083e9b15ba227064ba	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	And	False	Passed	Model Under Test Equivalent Model
406190758dcc7efdb123a6a5c64254e29e6fe9fb	Apalache	Extends	And	True	Passed	Model Under Test Equivalent Model
46c37ea8efb181c2c05f4c212d90a656af29f541	Apalache	Extends	And	False	Passed	Model Under Test Equivalent Model
d3b3f79f167b08a644f4b1b16c39eddb32a2aca9	Apalache	ExtendsInDifferentFolder	And	True	Passed	Model Under Test Equivalent Model
dea2e4768614d078018e8c99e54ec8b62c492509	Apalache	ExtendsInDifferentFolder	And	False	Passed	Model Under Test Equivalent Model
6003c9daf0ae7e2c6a5d623936f30de25e28af91	Apalache	Variable	And	True	Passed	Model Under Test Equivalent Model
81cde0ae2de17771118f160f5f4652eb7b5239cf	Apalache	Variable	And	False	Passed	Model Under Test Equivalent Model
91376e55ef8de569816453b20bb8e87f67553ea0	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	And	True	Passed	Model Under Test Equivalent Model
644b1924fa45ef6e8b65813fb01f2264d2166292	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	And	False	Passed	Model Under Test Equivalent Model
105c1f186698b729cabdb22674f62d6b5027f2ed	Apalache	Constant	And	True	Passed	Model Under Test Equivalent Model
b7cc29ac7b7d0ddd65a99b5d6c02cff8fbffb09e	Apalache	Constant	And	False	Passed	Model Under Test Equivalent Model
2a93d2d25c35132bd4d82ee9be0983ba1b9af77d	Apalache	ConstantRank1	And	True	Passed	Model Under Test Equivalent Model
59114fc8bcd249335780b10db41f681165fe42c6	Apalache	ConstantRank1	And	False	Passed	Model Under Test Equivalent Model
9364f95ea8bfee7b6711cd36e08f395465ae2f15	Apalache	Instance	And	True	Passed	Model Under Test Equivalent Model
27ee7659e2015386230a9d05b2a3325e9b11dc51	Apalache	Instance	And	False	Passed	Model Under Test Equivalent Model
cfd95aa67162c5d452e566d2c29aefae12bdd619	Apalache	InstanceWith	And	True	Passed	Model Under Test Equivalent Model
e0892d77dea96e24755bcea349b54fa4afe270ce	Apalache	InstanceWith	And	False	Passed	Model Under Test Equivalent Model
e4c64880c69009d250d0dc7721c7f61b06d66314	Apalache	InstanceNamed	And	True	Passed	Model Under Test Equivalent Model
45a607d7e7fd33331fcedc5a623c22fdcd09af37	Apalache	InstanceNamed	And	False	Passed	Model Under Test Equivalent Model
3dcf9d70aa78a456cbb182efd7f781ab96e66a16	Apalache	InstanceNamedWith	And	True	Passed	Model Under Test Equivalent Model
e3668795bee711dbb38f57c3ed4dada9423a4f0b	Apalache	InstanceNamedWith	And	False	Passed	Model Under Test Equivalent Model
f7dfbaf641e34d157093728b952278226e1bc7c6	Apalache	InstanceInFolder	And	True	Passed	Model Under Test Equivalent Model
a9592b8ae8a7d432ae69bfb5587f9e67bdad6de1	Apalache	InstanceInFolder	And	False	Passed	Model Under Test Equivalent Model
4594ecc1f579613a486dfeb6c8c6c4fd884214b7	Apalache	InstanceWithInFolder	And	True	Passed	Model Under Test Equivalent Model
168fadddb450a713a51ffb8709837ce895de5e18	Apalache	InstanceWithInFolder	And	False	Passed	Model Under Test Equivalent Model
9cec2692155bc92dc57da58e9d3f49c8bc7459c4	Apalache	InstanceNamedInFolder	And	True	Passed	Model Under Test Equivalent Model
c44f0b0e5e559f62c77043bb66057541414b2727	Apalache	InstanceNamedInFolder	And	False	Passed	Model Under Test Equivalent Model
8d73f79d81ed5d930eab4554ce212b014bdda45f	Apalache	InstanceNamedWithInFolder	And	True	Passed	Model Under Test Equivalent Model
5a97138821d3ea8faa62893100d0586c61c7ba0a	Apalache	InstanceNamedWithInFolder	And	False	Passed	Model Under Test Equivalent Model
0e0801a307b1c0a412c0f4c8046aa0eeeb3004de	Apalache	Enabled	And	True	Passed	Model Under Test Equivalent Model
c326c874e88d400492ee29585f7efd473e0ccccd	Apalache	Enabled	And	False	Passed	Model Under Test Equivalent Model
b889191a8d3e9f6beafeff003f75d2caa0c392ee	Apalache	Assume	And	True	Passed	Model Under Test Equivalent Model
42fed1a230c67500cd5a0dbc6d9667e43f95eb62	Apalache	Assume	And	False	Passed	Model Under Test Equivalent Model
bbb8ca5b61901edeee2635ca519f3a16276795b7	Apalache	AssumeNamed	And	True	Passed	Model Under Test Equivalent Model
678a2e09e397c51571943f20f977af5b5013de67	Apalache	AssumeNamed	And	False	Passed	Model Under Test Equivalent Model
fb0ea992400043826e0e2dd293af5a5a42d7b976	Apalache	Lambda	And	True	Passed	Model Under Test Equivalent Model
b1acdc641bd2ed8f01824b87a2c588f9ba3c2b3c	Apalache	Lambda	And	False	Passed	Model Under Test Equivalent Model
2b9eb80e6c5de9d90c59ba35b34fa9d93468288d	Apalache	IfCond	And	True	Passed	Model Under Test Equivalent Model
da7995a2f9a87ad567456f79e8bd5e189911a16a	Apalache	IfCond	And	False	Passed	Model Under Test Equivalent Model
a2af0a53b1686b16361152d46dc57d34fd718c4a	Apalache	IfThen	And	True	Passed	Model Under Test Equivalent Model
9ae75749d9dd835090a4d3018142b86ed4800993	Apalache	IfThen	And	False	Passed	Model Under Test Equivalent Model
6454ad35d2548e657e0cd22b9ec5cd3c69180948	Apalache	IfElse	And	True	Passed	Model Under Test Equivalent Model
fdf36695c44cbc1b3d4170cc07a2698dff2d5494	Apalache	IfElse	And	False	Passed	Model Under Test Equivalent Model
e3d147f6643207195e76e489d5165145e20d2675	Apalache	Unchanged	And	True	Passed	Model Under Test Equivalent Model
8060a873668e669c3194bc616182b7d8640ca796	Apalache	Unchanged	And	False	Passed	Model Under Test Equivalent Model
e02c41c9b3790c43c1dc5df07e2294a23544e9c4	Apalache	Equivalence	And	True	Passed	Model Under Test Equivalent Model
1d9be6eb480fd48a6a73846168beda9708886609	Apalache	Equivalence	And	False	Passed	Model Under Test Equivalent Model
e1df42b4dbd1eadb9657d2d532111e0686fe93b1	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	And	True	Passed	Model Under Test Equivalent Model
755874a1745bcc47247bfb5ffb1be40c3eceaf0d	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	And	False	Passed	Model Under Test Equivalent Model
238357c05cdd1baddac0c2203a237f43c0f47353	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	And	True	Passed	Model Under Test Equivalent Model
c64ca0ce7dbfd6ada086bd0cb1b517e04b607cae	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	And	False	Passed	Model Under Test Equivalent Model
833b79106b22f7525f1733886e2e92ddbc9e496b	Apalache	BagBagIn	And	True	Passed	Model Under Test Equivalent Model
518179c800b20eee9aca88bd490459fd0cbc8ac4	Apalache	BagBagIn	And	False	Passed	Model Under Test Equivalent Model
3a82d9cfdf5accabf28a6c47fb850f032c4602d7	Apalache	BagCopiesIn	And	True	Passed	Model Under Test Equivalent Model
2e1a96ab326afdb8b63f3edec07f221e89ec6da8	Apalache	BagCopiesIn	And	False	Passed	Model Under Test Equivalent Model
db560338d0005461bfe8bfd07306c75891a3eff5	Apalache	SeqAppend	And	True	Passed	Model Under Test Equivalent Model
b9c273c9df503d549bf1bbad11a0fe122a358cd1	Apalache	SeqAppend	And	False	Passed	Model Under Test Equivalent Model

Index

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