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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
53c6018de4e70e63008e83dccaef467574ab5eb0	Apalache	Eq	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
075d067b3ff4b19d551122a5624cba2e7e91c678	Apalache	Eq	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
f0c4ce82125d8d605c0712fb54b3c94494d2986c	Apalache	Ne	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
b1d419074491962a2889846d34d0b48ad18ac749	Apalache	Ne	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
383b13ec460045744dd5e9262cd7a36cf407c334	Apalache	Let	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
42466a59d054323253cf4cfb1740c9372224837e	Apalache	Let	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
3a91d86f30267c84cae30143105a175df2ade8d0	Apalache	Set0	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
5fa3b7f600ddebce2a1b4c183802f3fb5358aa72	Apalache	Set0	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
b19375e5b6d80977e0610a428257403b971d43e3	Apalache	Set1	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
af462dc38d48397ca3d0b735a98a35751ad25e3b	Apalache	Set1	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
05bdb2c7e72853e52371a506cf0a30cfd019e2fd	Apalache	Set2	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
d2ae253a1e76d6b1f7601a69152cdc37a7eae8d4	Apalache	Set2	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
37bbd082306346f59c07e12154fea614b9ea749b	Apalache	Fun	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
992bc8de300cb1ca95c9fd1913b4b59226d1d996	Apalache	Fun	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
a04494b354ec8ebaa55e95503c0b100f4d97fabe	Apalache	In	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
59c08f3a5d2ac57a7a2febfe56af6f888bd032dc	Apalache	In	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
634365443c82a823b7f3e73eb7fa2d434d57d965	Apalache	NotIn	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
ecc04eadd9f8de0b62ca28f7b9cdcf223fdd6400	Apalache	NotIn	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
5f46ddd84fb283d22b84f0b817428b146ca3cbe8	Apalache	Record	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
c9f1a1929e8c34996d3559aa5c1ea491493c9b92	Apalache	Record	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
4514fabef14e15779b9e522d44cd90c5bc0ba32a	Apalache	Tuple	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
1c53d4d2369968fa351d33aae282a48083ca4c64	Apalache	Tuple	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
402bd9ed798f6e102651ffe0e4932a6b4c573f96	Apalache	FunApp	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
4e22949e02573bba14e667dcdd16b962b52d2c30	Apalache	FunApp	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
a0f9413b76e5ebab3ed3a00f36c89bbf22959b2a	Apalache	Except1Fun	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
52724095821212b3960acee4dccf3744d25584da	Apalache	Except1Fun	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
72412c62a0d3a4bf962059f13cf6c4c6a898d3cd	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
8ef16bd24c1fdf86b4b528fc41581d888d0c8588	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
e22f5b8cc136a251a5021a62b2dd8e9bd985fda5	Apalache	Except1Rec	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
006388eb5ee4a1b5dc20623a9fa5374e137f871f	Apalache	Except1Rec	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
7fc964f730ed30bda3b53af4ee9509796cdfcf2e	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
194838203128d4c990edb2ff3f6c42b29203273d	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
a05e047ea50a14100ea732d5aed64aa96243655a	Apalache	Except2Fun	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
8f6e01c7b76a97c5dd5ce879003faed45b062ef5	Apalache	Except2Fun	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
a17f30013d0b8f3a9e83f839448a6c3e0bdfd967	Apalache	Prime	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
0fb97c3f59ccd7870adef6ceeed319293e754dae	Apalache	Prime	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
4002dee6bcf0ecd2586e39e999c97403b73e6e37	Apalache	NumUnaryMinus	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
1c36181fee87217363077a4b62edd6d7cba726dc	Apalache	NumUnaryMinus	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
2070900cceb25624cb360eb0caf5fad1da8dfdbe	Apalache	NumPlus	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
189897b74b33d4e20126fd93f24a7a9f8351d268	Apalache	NumPlus	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
5daa50534055faa9778b1f1bffd507937cf92f0a	Apalache	NumMinus	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
e45e6cef1fddeb3b779d9ca97ed90dffdfae6868	Apalache	NumMinus	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
3723e0dc12e90caf8205a026afca9db0f6990165	Apalache	NumMul	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
b92542b83d14d5f627c5f02731b29c9aba0f3997	Apalache	NumMul	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
9f14414ef9760a610429042534c5cd449663c53c	Apalache	NumDiv	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
2ba198dca12a9eb5454fc83c196ba485bf657ad4	Apalache	NumDiv	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
7f36d4b5bb574248bc684748862e21dedc89f045	Apalache	NumMod	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
658c0636ab0740f543db24c40814c21b640968db	Apalache	NumMod	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
0f410c3bcfad73a47419a54d9c33057055f574a3	Apalache	NumPow	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
e557682e965b881ab3cb165f9738e933ceb2f3e0	Apalache	NumPow	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
eddffbf62c942fc26567ec0fceabe7059c121f57	Apalache	NumGt	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
85d645d5881a014c457bf625c8087801a4f6c566	Apalache	NumGt	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
d84676a91b2f7b7997022b4ee47ccb8a6e670192	Apalache	NumGe	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
0896ccc490ca6bfcf9e8eb57407aba260a32ff0f	Apalache	NumGe	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
18d3a6c8a2c00fda840884c81d79855d03c612d5	Apalache	NumLt	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
076bb0660a5b9af7731b042b431c01252fc4b1f5	Apalache	NumLt	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
1c018ce6e46fe5e4c6473ec704f38908403e0696	Apalache	NumLe	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
33168aee3e0ea218f84de63d438abe5c1d2ed6d6	Apalache	NumLe	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
8e15d56f85d08c91ef45b2f111c3fba2f54f2910	Apalache	DefFun	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
e56032cc84c984e46b1a0e9b664fd672e3f7dc26	Apalache	DefFun	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
d374c6293a3c5ebd499fb356e7ec996b3e7d7179	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
7f06224aecd9c06e13cf14ef942bd86436732ee1	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
607d7fcb9475a0269022ad549bd86bf4a628f153	Apalache	DefFunRecursive	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
5769a94ac3a404e55d525407c7a47dc51a2f565c	Apalache	DefFunRecursive	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
5aa9a203e75d8f28156bccd0fa6afacef65e161b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
0d3a2ac66447516fce708e7d23b97e05c88c4808	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
1784a87ffc8d1856602654d0d28ed7358745e73e	Apalache	Def0	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
14525ff0150bbaace4553730d39803eac88ce2fd	Apalache	Def0	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
f379f8cb5678f31ff0b592aa6eb2888ece551b66	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
609e63ced72f1459acbf7f2026de59695002757c	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
240c7348f0019fdf6656fdee9f866a7b452fa0a3	Apalache	Def1	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
e46486331f5fae2c76b9d53d38ce7e7c7e775e4b	Apalache	Def1	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
aa8cc88e1781ce0dd54c56be925ed426462ffb48	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
9070b4a56ed6266a4f8d414e768f8462e6772f9f	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
da5c798475b3e07793d8d8c018e3be6777d7c814	Apalache	Def2	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
60962becb77474f5693e8a5d2e3d84495eb58e0f	Apalache	Def2	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
cd853123b8dfc45934271a5e9540db9f70423076	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
da542e1e08361ed6dd3e8acefc3eb209663d9ab5	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
ac2d35e3906084ae60ca10784c5cc6a4dee4516d	Apalache	Def1Recursive	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
af14915c4d4790de1e7d81412fdf3170b6d89bdf	Apalache	Def1Recursive	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
1a69cdd34f5e4ef83370d9e6da0effa0ad8097ca	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
b5fcb2932903ab618ed95f9cde1b32f187eb83a0	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
8a1dad81b0dd59923db726098cdc6adc89f90164	Apalache	Extends	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
52b65a65cd0c260918b6ae4d17fd309c4d26bdbe	Apalache	Extends	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
877e8e6875b9b55827538c1aec8f528b4b0093e1	Apalache	ExtendsInDifferentFolder	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
2607c8c15d303ce322c5b1a30d8f48960ca18bc2	Apalache	ExtendsInDifferentFolder	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
d5ea57379872729137812d14395f1eb361d5e45f	Apalache	Variable	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
7b34fdca8e773148c122856c3aa23d140c949a9a	Apalache	Variable	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
f4e0f35da41e742a26022c97eb55dc5c1062e7aa	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
b394d9afdd7e6eac0134db7784943983d944fde0	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
9614d483f8696f70936ab9147813fd47877da4be	Apalache	Constant	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
2aa8fe8dd097d9b68cf60a209a49ec716b5a5b5d	Apalache	Constant	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
615bac2bb0d75a5ff9e7cefb33d7f369320c71e1	Apalache	ConstantRank1	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
ccd3adfd40455f3c00364f79eb7777f4e8819015	Apalache	ConstantRank1	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
ffa0cc1d7bc355db957b511ca475d2c29839141d	Apalache	Instance	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
e34dd684869a8d539eda62ac9cf6853d08e62d8a	Apalache	Instance	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
2c0742492b9ffb4d0aeb1d23be68399839118552	Apalache	InstanceWith	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
33b140bda260ba0a695adbcb7350ca581e2ef80b	Apalache	InstanceWith	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
10c760946ecef251c803662ab369e7e052f63b67	Apalache	InstanceNamed	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
1f655d992a69061ec0090441b297357625981697	Apalache	InstanceNamed	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
f6694bccf2adea076e06fdfbbec2027087edebf5	Apalache	InstanceNamedWith	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
58ca36553023afe777d0c53806df71f1c6a2d013	Apalache	InstanceNamedWith	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
0989193610cd329dc5f6fdad89a057506adc6cea	Apalache	InstanceInFolder	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
15aab8fae882e0b082d24a5ea25e91c54c03ea64	Apalache	InstanceInFolder	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
f4c813870f7870677625c176b3872a7fb34e3e3e	Apalache	InstanceWithInFolder	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
4d76341c248a9efddaeeba2af07eb06f3ec3c68c	Apalache	InstanceWithInFolder	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
9fa1e99f802547f73dd764555d6e548bb2e458fe	Apalache	InstanceNamedInFolder	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
d50608b2f3dd6e268dfe05db05631c73c782570c	Apalache	InstanceNamedInFolder	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
16a1c277e618320c4f1b0060cadbc559dbc438d4	Apalache	InstanceNamedWithInFolder	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
5fc3400088b38197736e869dd4c0556795d4ba9b	Apalache	InstanceNamedWithInFolder	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
d01bb0ce92d5b7372ebc49eeb17c9074a7bbe1b6	Apalache	Lambda	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
1a617722fb6f59fdf5fc5787726cd30d0dd623a7	Apalache	Lambda	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
daf48378b9d5b578b17e8683a95d781bcaa50a0b	Apalache	IfThen	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
54d0b5e77c7004cd37c10972bc57e6ae64c2129c	Apalache	IfThen	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
60d8ccab4a28ae0009303af5cb2483f3c96bb53d	Apalache	IfElse	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
b2e91e8ab81daf629894f043b76bf0cdfefa6f35	Apalache	IfElse	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
34f216851bafbfa6fd247fad906724ed69ee961c	Apalache	Unchanged	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
26970a6c1d939aeecfa77c00c588e6cb2a31e89d	Apalache	Unchanged	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
50780b1b4f662f20b8e04a43041b58e8c99cb876	Apalache	SeqSubSeq	NumUnaryMinus	True	Failed: TLC requires the second argument of SeqSubSeq to be in domain of the sequence and returns an error otherwise. Apalache always returns some sequence	Model Under Test Equivalent Model
bf75ac824a18bbf6c47d7f496587d59835eca063	Apalache	SeqSubSeq	NumUnaryMinus	False	Failed: TLC requires the second argument of SeqSubSeq to be in domain of the sequence and returns an error otherwise. Apalache always returns some sequence	Model Under Test Equivalent Model
537a6af05b4868faf00d7baa80458fb9dc4fdd3e	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	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
f21d1084ec11990d95de773b402238192841b530	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	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
058eebd2775c16db87bb12d50b273915ee66fdfc	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
5caaf1ecaed78d6937c2a3c7658f8b01cdb5268f	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
c8b00755c1cb55145eb60c1c1a4bafc6666a2bab	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
8417a79c0b5ebf3f8cdefcd24789baadfc2600dc	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
6ef160966158b153bdadfdf589545f841a4f496c	Apalache	BagBagIn	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
469fd873e8772fffef70131ce682ef17473a5af0	Apalache	BagBagIn	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
dc47072e9a5d0c53f7805c827839f5272b3bce78	Apalache	BagCopiesIn	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
7c591b6eb92a29f89e5480e5592d5a19d73ed500	Apalache	BagCopiesIn	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
c5393fd5ac5a308ffa01ccf9f47c405cef08f554	Apalache	SeqAppend	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
a630d7e2d874d0c2ede15f87d2c208ebdba22504	Apalache	SeqAppend	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model

Index

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