Tests by case feature AndProp; CLI Option: -workers 1

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
3f9fb5d0da2f9305efff3284add9d20773d326b0	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	AndProp	OneLineComment	True	Passed	Model Under Test Equivalent Model
2610b3064bca2691c7dea94ea3a8f76240bd868f	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	AndProp	OneLineComment	False	Passed	Model Under Test Equivalent Model
0c582ab9acdc4de231a29e690ff98aa5888ab7ba	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	AndProp	MultiLineComment	True	Passed	Model Under Test Equivalent Model
c95f8cdcd5e31a0f3fe816a905cc3c3a60bd6dd3	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	AndProp	MultiLineComment	False	Passed	Model Under Test Equivalent Model
0af0f1af6a006e5d0abe2379d777b3bbf82b1669	Apalache	AndProp	BoolTrue	True	Passed	Model Under Test Equivalent Model
8ae3d519172735485924620e62e79e416f78cd0d	Apalache	AndProp	BoolTrue	False	Passed	Model Under Test Equivalent Model
ab78aa39fe9beb288acc2b0858d326c89c384394	Apalache	AndProp	BoolFalse	True	Failed: TLC reports an error if it sees trivially false property. Whereas Apalache returns violation	Model Under Test Equivalent Model
5f286ab4bd180ba58d337bae341c7399907d0125	Apalache	AndProp	BoolFalse	False	Failed: TLC reports an error if it sees trivially false property. Whereas Apalache returns violation	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
a52e9b0e02ded6194b832ef9d4320e1e03dd0a8d	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	AndProp	AndMultiLine	True	Passed	Model Under Test Equivalent Model
21c2dd05a176ba21cc8733a7d3668a20b760c57d	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	AndProp	AndMultiLine	False	Passed	Model Under Test Equivalent Model
bfe86f3b86de574f9783c168f86f7804d968095c	Apalache	AndProp	Imply	True	Passed	Model Under Test Equivalent Model
6d4c19883182cbbc38e886fb8915bdbbcc71f255	Apalache	AndProp	Imply	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
ca709d829ec9aaf0774b40cc529da1db909af590	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	AndProp	Or	True	Passed	Model Under Test Equivalent Model
f607553d63c1ea0f1e587a116d20df259fff4ce2	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	AndProp	Or	False	Passed	Model Under Test Equivalent Model
05934505c1cc36769e9f4c7c5b0fee6a91a3f48b	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	AndProp	OrMultiLine	True	Passed	Model Under Test Equivalent Model
2b1c58ecf61421fac9946f6895b7c7ccf763caf2	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	AndProp	OrMultiLine	False	Passed	Model Under Test Equivalent Model
0df3204ded413ea2ee3bf5417bfd3b6e40b35bd3	Apalache	AndProp	AndProp	True	Passed	Model Under Test Equivalent Model
593076a7d11b76266a33b4487ee671f887e3ddee	Apalache	AndProp	AndProp	False	Passed	Model Under Test Equivalent Model
c61675e65b6356999dfb1ed4ef3d92c14b5711e2	Apalache	AndProp	Boxed	True	Passed	Model Under Test Equivalent Model
745765a375a9b1c3ef0767ddaa55d26ef88e45df	Apalache	AndProp	Boxed	False	Passed	Model Under Test Equivalent Model
323026ced96d63cff02b753025d9f1968b87b428	Apalache	AndProp	Eq	True	Passed	Model Under Test Equivalent Model
cd81efff89c4cabe70c5c47736558b0259bfe4ba	Apalache	AndProp	Eq	False	Passed	Model Under Test Equivalent Model
5e86c02fd4dfc4cae8a6985c3c3b6142d181097e	Apalache	AndProp	Ne	True	Passed	Model Under Test Equivalent Model
88a063e88524449d6e7fc0643b3e1f963119839c	Apalache	AndProp	Ne	False	Passed	Model Under Test Equivalent Model
613a91f14d6eabe8cf3a763e136e60f0bc92405d	Apalache	AndProp	Let	True	Passed	Model Under Test Equivalent Model
3861a5a09c85f55a899b4408f782cb089fb7fff9	Apalache	AndProp	Let	False	Passed	Model Under Test Equivalent Model
166b6ede1ae86eef81f9f35ac56d3c4b222aaafc	Apalache	AndProp	In	True	Passed	Model Under Test Equivalent Model
f99568c29398ee9cfed0f395341f1d81bac50f5d	Apalache	AndProp	In	False	Passed	Model Under Test Equivalent Model
69a37baed46e3ce18ad3152091c24c53856363a7	Apalache	AndProp	NotIn	True	Passed	Model Under Test Equivalent Model
c7bbf9ea4589559f7ab8acfb5a8a91d35d3dc471	Apalache	AndProp	NotIn	False	Passed	Model Under Test Equivalent Model
997fbf116338fe4ee0c0bde809d5452e725bd4b7	Apalache	AndProp	Exists	True	Passed	Model Under Test Equivalent Model
5e2cdd9f589ab0902ba6332a5925f904f23f77d3	Apalache	AndProp	Exists	False	Passed	Model Under Test Equivalent Model
1c7dc89a9f17204c86023fbb896a77971a8af744	Apalache	AndProp	Forall	True	Passed	Model Under Test Equivalent Model
f2f7190fe3cdc39de4535d491276f6a1dd110b54	Apalache	AndProp	Forall	False	Passed	Model Under Test Equivalent Model
c683c6c470beaf9083f4f62e25b12a5aeb8ecf06	Apalache	AndProp	Choose	True	Passed	Model Under Test Equivalent Model
a89e835f832cdd7ae08b9f1b7af9f5c0c4be239f	Apalache	AndProp	Choose	False	Passed	Model Under Test Equivalent Model
68d4ba16ed078ae915d8d650479f2ceb714347d4	Apalache	AndProp	FunApp	True	Passed	Model Under Test Equivalent Model
ba74835a1a078068183ddb5291d259d942ad302a	Apalache	AndProp	FunApp	False	Passed	Model Under Test Equivalent Model
6eb754118f45f393d9f1bb14fb1aea8d36f0b200	Apalache	AndProp	NumGt	True	Passed	Model Under Test Equivalent Model
7efbf058c3aeb0a2ea8e528db271b980dcfbde1a	Apalache	AndProp	NumGt	False	Passed	Model Under Test Equivalent Model
6a48cd57005372eb9e30fc63ebe738fa7630ebb5	Apalache	AndProp	NumGe	True	Passed	Model Under Test Equivalent Model
74957808889d63c06a8f86b937ff524d54662bab	Apalache	AndProp	NumGe	False	Passed	Model Under Test Equivalent Model
5d4f779840f28eb36f7fcafc972beb9f9576b813	Apalache	AndProp	NumLt	True	Passed	Model Under Test Equivalent Model
d3aea441146d286bfb3aee5b706aed22abc9b7fd	Apalache	AndProp	NumLt	False	Passed	Model Under Test Equivalent Model
90d13ec06873d0e8a14d614fb3b07fb6e94cc2c1	Apalache	AndProp	NumLe	True	Passed	Model Under Test Equivalent Model
add309c8a1d3c633abe946483dc0aaa8f87f1810	Apalache	AndProp	NumLe	False	Passed	Model Under Test Equivalent Model
2d6ac45cc30ae7476814e5f9ef6a6f1b84caf5e2	Apalache	AndProp	Def0	True	Passed	Model Under Test Equivalent Model
df31bb030d93cc86a3cc906df71830578aa97dd4	Apalache	AndProp	Def0	False	Passed	Model Under Test Equivalent Model
db5fbca5be5882372ce55486a83babf0442d8cea	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	AndProp	LetDef0	True	Passed	Model Under Test Equivalent Model
5df6e902f80826156290c8fbd89564f75749cad2	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	AndProp	LetDef0	False	Passed	Model Under Test Equivalent Model
6431e3c5f37ff1007b53056a8d01a74c585a627c	Apalache	AndProp	Def1	True	Passed	Model Under Test Equivalent Model
e9860959e99970a8ae5d663bfcd257ec4cbdb439	Apalache	AndProp	Def1	False	Passed	Model Under Test Equivalent Model
45a2300b40f4774b742e40c685700bb0d2fea8a4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	AndProp	LetDef1	True	Passed	Model Under Test Equivalent Model
317d0044ca8e181f8e1b6061779196b6925f36a1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	AndProp	LetDef1	False	Passed	Model Under Test Equivalent Model
fe50757c5a64d680855efceec1cc66b052f4bd3e	Apalache	AndProp	Def2	True	Passed	Model Under Test Equivalent Model
41a965e576e91e672aab096c5d3fa53792f70072	Apalache	AndProp	Def2	False	Passed	Model Under Test Equivalent Model
3fe72060f00e3f069bed10f3daa188c02685338d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	AndProp	LetDef2	True	Passed	Model Under Test Equivalent Model
568a9c26d30ec72656538b9e52d4ad5856be9743	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	AndProp	LetDef2	False	Passed	Model Under Test Equivalent Model
ea45a092f35a1079dabb16dfceddf8a8a40b3265	Apalache	AndProp	Def1Recursive	True	Passed	Model Under Test Equivalent Model
d1af571805ff92212c8cae7f7e41a258eb769763	Apalache	AndProp	Def1Recursive	False	Passed	Model Under Test Equivalent Model
8dc6a03fc55c1fc13b8c75071f810adca1dd3047	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	AndProp	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
6604a14425f5a38b5d9f992e0922cfc5dd2e1458	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	AndProp	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
ca524d2c72adbd53ba435ad7c894daa475f35f48	Apalache	AndProp	Extends	True	Passed	Model Under Test Equivalent Model
b2aa7456548e79d7e10aedb6321c9dfa13608412	Apalache	AndProp	Extends	False	Passed	Model Under Test Equivalent Model
0563ff61911cc38c75bab2e04621187ae262883c	Apalache	AndProp	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
a42900be5d087bba1b7df212a3bc570eb93b6c4b	Apalache	AndProp	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
205d11b0e7b19a91be2f0bddaac15059503b7464	Apalache	AndProp	Instance	True	Passed	Model Under Test Equivalent Model
2929190149a47e69775abb6b58b8f0efc9424f74	Apalache	AndProp	Instance	False	Passed	Model Under Test Equivalent Model
6086f9374923815a3b4aa1ccfba57899449959d0	Apalache	AndProp	InstanceWith	True	Passed	Model Under Test Equivalent Model
799c396acdcc598dd574105edab49a47786894e8	Apalache	AndProp	InstanceWith	False	Passed	Model Under Test Equivalent Model
1af85443a83fb30974777a94a834e8b22115516e	Apalache	AndProp	InstanceNamed	True	Passed	Model Under Test Equivalent Model
3a0c6aa97c18d2fd3138391e749762e698d2ba39	Apalache	AndProp	InstanceNamed	False	Passed	Model Under Test Equivalent Model
f0a8f8e4487b2e503a1bff1e09a82e1736d7e47d	Apalache	AndProp	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
c1cc2ea517ef45745c0c0699032bf0d0aa9f4597	Apalache	AndProp	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
a6db2baee279bbc6735321e405156a44a023e912	Apalache	AndProp	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
fb69af4cac7248b86bd94bf1996df1df7d130048	Apalache	AndProp	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
fda3749a994388025e40c8d85132db08014bc463	Apalache	AndProp	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
8c730279fd511c38e03a55e6ba1887e9b29378d2	Apalache	AndProp	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
933c42af2dc621554379f77a7ac1c1e92e441c0a	Apalache	AndProp	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
f3a8e354daa8c8f86ca4bd519c10c79a134c01fc	Apalache	AndProp	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
891f099613a1a38ee50bfb305a1c131da5d7800a	Apalache	AndProp	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
2d30e5c5c6fdb339bd9169f5f981d6f708aa2ae9	Apalache	AndProp	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
580698336ac0a8026381f2b7bc97659b85a2dbaa	Apalache	AndProp	Enabled	True	Passed	Model Under Test Equivalent Model
e0fc93f5e208785dadcc8067e7b3e009f93abe2c	Apalache	AndProp	Enabled	False	Passed	Model Under Test Equivalent Model
68e9809ad348a1c53c2a4241d5d50fd02443056e	Apalache	AndProp	SubsetEq	True	Passed	Model Under Test Equivalent Model
5321abd1d5835a94dc5a7a0950b9fdd710c0c91e	Apalache	AndProp	SubsetEq	False	Passed	Model Under Test Equivalent Model
ef2c4b6b4fdcc995aaae89d1a9b97b6d3f9e3ffc	Apalache	AndProp	IfCond	True	Passed	Model Under Test Equivalent Model
774afc9ea23f3d36a6277dfe4bcbb57b3cb67e93	Apalache	AndProp	IfCond	False	Passed	Model Under Test Equivalent Model
60e8b720bb3784fbcb38ca8d654a783650a191cc	Apalache	AndProp	IfThen	True	Passed	Model Under Test Equivalent Model
2dc2cdc264ae197184b710a500749116f8121ac4	Apalache	AndProp	IfThen	False	Passed	Model Under Test Equivalent Model
8f9b905a2b4a84105af989039350b1a5f0774582	Apalache	AndProp	IfElse	True	Passed	Model Under Test Equivalent Model
fc94218300bb3bad192e14ca28249039837a5bf1	Apalache	AndProp	IfElse	False	Passed	Model Under Test Equivalent Model
424b7a3952ff96e18fde23e5d8ce025992d62cfd	Apalache	AndProp	Equivalence	True	Passed	Model Under Test Equivalent Model
86e60331786db986bf6a2f43387b354566614115	Apalache	AndProp	Equivalence	False	Passed	Model Under Test Equivalent Model
61feeb6995a5b8d7387ffd90993cec462b64ad0f	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	AndProp	TlcEval	True	Passed	Model Under Test Equivalent Model
bce6ce128893dc3b64c3fc4b17d2e32212f8cd98	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	AndProp	TlcEval	False	Passed	Model Under Test Equivalent Model
fc0bb98f6e30d8c6accd8bb7d31395016e4af5ac	Apalache	AndProp	BagBagIn	True	Passed	Model Under Test Equivalent Model
49899a521d4b95a86c211e3edd559c88005dafab	Apalache	AndProp	BagBagIn	False	Passed	Model Under Test Equivalent Model
68ced92e52c5a24210e5ce4c21c10df088f5fdf2	Apalache	AndProp	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
2ee3d93b5695153d5be0ea929d841addb7cd4ac2	Apalache	AndProp	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
4b6d6a7632f2556940ece6afa51de11a8301a3c0	TLC with reduction strategy: Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)	AndProp	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
d20582d8916c07079aa51562031049e8d4d12512	TLC with reduction strategy: Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)	AndProp	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
8adab3f487246dfcdf04a0086b7ceea323dc012e	Apalache	AndProp	SeqHead	True	Passed	Model Under Test Equivalent Model
087c0008503ea6185f828c98cf5ffecfed4dd9a5	Apalache	AndProp	SeqHead	False	Passed	Model Under Test Equivalent Model

Index

Tests by case feature AndProp; CLI Option: -workers 1