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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
e323c8b2a99782aadc7866fe13f16b632fec3612	Apalache	Eq	BoolSet	True	Passed	Model Under Test Equivalent Model
5093886a35ee872a4d4a6f0bb859f764c4a6e5b0	Apalache	Eq	BoolSet	False	Passed	Model Under Test Equivalent Model
774b53be177e11552e3ab31edddaa498e3918a98	Apalache	Ne	BoolSet	True	Passed	Model Under Test Equivalent Model
58314ac19aed9340a960642f65d5d195b0fba64c	Apalache	Ne	BoolSet	False	Passed	Model Under Test Equivalent Model
0f3f1c02e21c33dfb676a9059e4dbd0073a1cb65	Apalache	Let	BoolSet	True	Passed	Model Under Test Equivalent Model
0639a174117014c70222431a97ed3122a43363af	Apalache	Let	BoolSet	False	Passed	Model Under Test Equivalent Model
1b0bf38e95b37505c4b33c424016e692c1148fad	Apalache	Set0	BoolSet	True	Passed	Model Under Test Equivalent Model
c3ff5d5b9a40124679ad6319ecf106f50d4f4aa0	Apalache	Set0	BoolSet	False	Passed	Model Under Test Equivalent Model
a91872790a087e15171a1ff3376fe28caf5bac41	Apalache	Set1	BoolSet	True	Passed	Model Under Test Equivalent Model
0fb6e66527e1faf3810b5ec9af03b71e0c3a3726	Apalache	Set1	BoolSet	False	Passed	Model Under Test Equivalent Model
a55bca863bee2a9caf6dec1803ed94b54b40d802	Apalache	Set2	BoolSet	True	Passed	Model Under Test Equivalent Model
a0f6464645a0f6e27840c127e374734aea18c705	Apalache	Set2	BoolSet	False	Passed	Model Under Test Equivalent Model
74b3f0c9a2533137d554ab5ac95330784442eafc	Apalache	Fun	BoolSet	True	Passed	Model Under Test Equivalent Model
0171767c2eb8de9706f9911832dade5d11b7edbe	Apalache	Fun	BoolSet	False	Passed	Model Under Test Equivalent Model
718799844762de478a5fe4f61c54bcced95525ff	Apalache	In	BoolSet	True	Passed	Model Under Test Equivalent Model
3ee971595d81d5d00fdf97d9d032cb86bc420f28	Apalache	In	BoolSet	False	Passed	Model Under Test Equivalent Model
dbe9c80b94508f9aaeffe8a777f541e04b0da7ca	Apalache	NotIn	BoolSet	True	Passed	Model Under Test Equivalent Model
a3794dc6d2aed7a7244c071a1c140d0f51d7ba8f	Apalache	NotIn	BoolSet	False	Passed	Model Under Test Equivalent Model
870627c805b52251adf6fbc1e6bb14343a5c7549	Apalache	Record	BoolSet	True	Passed	Model Under Test Equivalent Model
e5765c5c65893f7116cc133d5b333c861245d33f	Apalache	Record	BoolSet	False	Passed	Model Under Test Equivalent Model
63b021c22c29fe8c2721b1b2f26d7b2c31eaba31	Apalache	Tuple	BoolSet	True	Passed	Model Under Test Equivalent Model
9197e19d5abc642cb418727aa3e0ffd6f8193fbc	Apalache	Tuple	BoolSet	False	Passed	Model Under Test Equivalent Model
de68dd4c3d45671e717fce375d8da8863a4791ff	Apalache	FunApp	BoolSet	True	Passed	Model Under Test Equivalent Model
a2c68b08e0a96d54277e92023f3e11d0a596c7ef	Apalache	FunApp	BoolSet	False	Passed	Model Under Test Equivalent Model
64cece7efba20fd81ab0d7cf68d0862e9757a483	Apalache	Except1Fun	BoolSet	True	Passed	Model Under Test Equivalent Model
e1db0a04cff159a69af251a29eac76941d0c0917	Apalache	Except1Fun	BoolSet	False	Passed	Model Under Test Equivalent Model
2528ce9fba5ad2e6323c44a60bf60fe4f73a5039	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	BoolSet	True	Passed	Model Under Test Equivalent Model
02a8911e4ba08a1b9229b80f443a15cd92b61aec	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	BoolSet	False	Passed	Model Under Test Equivalent Model
4cc68ea6208c5961cb6575fc3fe932bb8989492b	Apalache	Except1Rec	BoolSet	True	Passed	Model Under Test Equivalent Model
ffae13946bf371a968f56e35ce48c56ac2f4690e	Apalache	Except1Rec	BoolSet	False	Passed	Model Under Test Equivalent Model
184ce5a97fd5a2cfd30834c3cbdd955252c23552	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	BoolSet	True	Passed	Model Under Test Equivalent Model
5d7eb00186f039f19ef8b3bea5e9e575b4e71d88	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	BoolSet	False	Passed	Model Under Test Equivalent Model
54c311e0b468e524727cad058f7a2e433e58dcdf	Apalache	Except2Fun	BoolSet	True	Passed	Model Under Test Equivalent Model
e52a83e7f357cad5c9fc23107a5b30178fa67e87	Apalache	Except2Fun	BoolSet	False	Passed	Model Under Test Equivalent Model
fbb0afedce1f66e31469490c2476c8115dcd853c	Apalache	Prime	BoolSet	True	Passed	Model Under Test Equivalent Model
113457b48f15a472bd3c6b72804bc748fba38cb1	Apalache	Prime	BoolSet	False	Passed	Model Under Test Equivalent Model
7f19de57983f12a3b2675a5217cb68370594209d	Apalache	DefFun	BoolSet	True	Passed	Model Under Test Equivalent Model
8978b915b58fdc2db65d18c0297187c3e6cfce2a	Apalache	DefFun	BoolSet	False	Passed	Model Under Test Equivalent Model
bf1dfd240d08f07914885706133650b3c992322b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	BoolSet	True	Passed	Model Under Test Equivalent Model
4102330f9c19624f3d7750f1285c06597efded9d	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	BoolSet	False	Passed	Model Under Test Equivalent Model
f579fcad41d826073f074e6c75dc33abd464abb7	Apalache	DefFunRecursive	BoolSet	True	Passed	Model Under Test Equivalent Model
9499c9181d57f08b81f9cfb00897db24ee4ca3f2	Apalache	DefFunRecursive	BoolSet	False	Passed	Model Under Test Equivalent Model
fdb3d7687de6fff1fc0d7cf39b00a22e8ad09aa5	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	BoolSet	True	Passed	Model Under Test Equivalent Model
d428c4d152ed04a70ff92b1a6ec5b1695a4277fb	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	BoolSet	False	Passed	Model Under Test Equivalent Model
8367af37389ac6ba6b0fb03bd92bcb6d0adac012	Apalache	Def0	BoolSet	True	Passed	Model Under Test Equivalent Model
129307f960117261ad67950110b2473ffb324003	Apalache	Def0	BoolSet	False	Passed	Model Under Test Equivalent Model
b5387215d34b3a5d00841f81890925e41e4b398a	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	BoolSet	True	Passed	Model Under Test Equivalent Model
4f37077cffb759fbe469bbcb486926c5a624eabc	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	BoolSet	False	Passed	Model Under Test Equivalent Model
59a0860a91e746da4e2ec868962c41c1357f6a64	Apalache	Def1	BoolSet	True	Passed	Model Under Test Equivalent Model
fc49f0cd779e6a0a508a7050566dd4e3183be4fd	Apalache	Def1	BoolSet	False	Passed	Model Under Test Equivalent Model
e1cab0bf2fd879d751b210c9b5002ea271cac2e1	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	BoolSet	True	Passed	Model Under Test Equivalent Model
0429e99ba55f0d256b1479764dc764bdb03beb9a	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	BoolSet	False	Passed	Model Under Test Equivalent Model
9926f24301468c1aaf3d8b0d3b714b62150bde47	Apalache	Def2	BoolSet	True	Passed	Model Under Test Equivalent Model
e14f08753f5bebbbf6650cfa235139fceead595f	Apalache	Def2	BoolSet	False	Passed	Model Under Test Equivalent Model
f6e079a3f069a3f0766b8af6475066910a35cab0	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	BoolSet	True	Passed	Model Under Test Equivalent Model
044bd080c61752c0293edfa061756bde64c7bbe4	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	BoolSet	False	Passed	Model Under Test Equivalent Model
a302768f9f112f9c42bb736771ffba595a8892e7	Apalache	Def1Recursive	BoolSet	True	Passed	Model Under Test Equivalent Model
3461e6c5b2c0e5da5a29a503c815ae60fb68c3d0	Apalache	Def1Recursive	BoolSet	False	Passed	Model Under Test Equivalent Model
21ed6869b8aaacea81087bc77487576a32e4cef0	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	BoolSet	True	Passed	Model Under Test Equivalent Model
fd14f14bddfb11670df89654f93006f4df1db2cb	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	BoolSet	False	Passed	Model Under Test Equivalent Model
0651f6147d0b61acc5545d60399f0fe1b0e52e7c	Apalache	Extends	BoolSet	True	Passed	Model Under Test Equivalent Model
2245364448dbc150e1bc1a915a4f55d02516d4a6	Apalache	Extends	BoolSet	False	Passed	Model Under Test Equivalent Model
a360340b88dfe0c4cf4b388b9484b0acbe60cb03	Apalache	ExtendsInDifferentFolder	BoolSet	True	Passed	Model Under Test Equivalent Model
7a3eead8cc427b032fcc5ca1393790941cf3c1b4	Apalache	ExtendsInDifferentFolder	BoolSet	False	Passed	Model Under Test Equivalent Model
12cb76c5474f5dd0b38c2650bb45f6b32d077858	Apalache	Variable	BoolSet	True	Passed	Model Under Test Equivalent Model
0fb989112132a24ff3dbe124dc16ffb17fecc993	Apalache	Variable	BoolSet	False	Passed	Model Under Test Equivalent Model
d9bda0a12fa573514aaa40fa74b8477cde314d47	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	BoolSet	True	Passed	Model Under Test Equivalent Model
fbb1e5e9a19fefb501803ad84119951f19fb71c6	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	BoolSet	False	Passed	Model Under Test Equivalent Model
7b6e8b00a7b20e5a7709363d409508b1a9d8e88c	Apalache	Constant	BoolSet	True	Passed	Model Under Test Equivalent Model
38e2d989e55ab8e8ac17bd98a7b306faef2ffcea	Apalache	Constant	BoolSet	False	Passed	Model Under Test Equivalent Model
b5af8245bed8213fba673bfa42c9ff39c1bc5f9d	Apalache	ConstantRank1	BoolSet	True	Passed	Model Under Test Equivalent Model
614adbc36211770826f238501f69350aab4bf6a1	Apalache	ConstantRank1	BoolSet	False	Passed	Model Under Test Equivalent Model
9efe56ce06377f558af1e0500ad92c93c96954be	Apalache	Instance	BoolSet	True	Passed	Model Under Test Equivalent Model
902e95763162bf8dfa6c3112f55883e352371c23	Apalache	Instance	BoolSet	False	Passed	Model Under Test Equivalent Model
a7146c2a808828692b81d12d44f1bc4f97cdfaac	Apalache	InstanceWith	BoolSet	True	Passed	Model Under Test Equivalent Model
86e638f87143b703713a228b88a6f5d9b18f56e3	Apalache	InstanceWith	BoolSet	False	Passed	Model Under Test Equivalent Model
432821b9efb7eda8d78b9eee79dd1c64a6511d81	Apalache	InstanceNamed	BoolSet	True	Passed	Model Under Test Equivalent Model
e498ca2febc1670a57cc3f20083964d4b1bfbde2	Apalache	InstanceNamed	BoolSet	False	Passed	Model Under Test Equivalent Model
69f4d4b9299187cd57e553c1460607f91c17279f	Apalache	InstanceNamedWith	BoolSet	True	Passed	Model Under Test Equivalent Model
792d36c57a9d84e09b4a5dbc671c62b155ea9bce	Apalache	InstanceNamedWith	BoolSet	False	Passed	Model Under Test Equivalent Model
cf40daf6ff811808f44e6bd41c0c72ddf6e2796e	Apalache	InstanceInFolder	BoolSet	True	Passed	Model Under Test Equivalent Model
52a5256922babbacfd5582fa8ce5c1f7d093f51d	Apalache	InstanceInFolder	BoolSet	False	Passed	Model Under Test Equivalent Model
e7d5f402292ba09fba077541144dcf0fb4f34366	Apalache	InstanceWithInFolder	BoolSet	True	Passed	Model Under Test Equivalent Model
f806e545bfa468d8aedc77c713d8537fb6ad0d2e	Apalache	InstanceWithInFolder	BoolSet	False	Passed	Model Under Test Equivalent Model
73928828238f2c446c1dab499cf7d86aec2fe5a8	Apalache	InstanceNamedInFolder	BoolSet	True	Passed	Model Under Test Equivalent Model
f97b55bc4fa02d5dd9eef1c3a4056b644f4411fa	Apalache	InstanceNamedInFolder	BoolSet	False	Passed	Model Under Test Equivalent Model
c3db8d986042aa0dbc5d971f16142f8aaa20a514	Apalache	InstanceNamedWithInFolder	BoolSet	True	Passed	Model Under Test Equivalent Model
1c969b0b6b0d01fec6536946da29ec7d987971ab	Apalache	InstanceNamedWithInFolder	BoolSet	False	Passed	Model Under Test Equivalent Model
d2d9b20bc670c5cc255988f0329661b2a6f01d65	Apalache	Lambda	BoolSet	True	Passed	Model Under Test Equivalent Model
9e128778ad2caef95476d398dab68de35eacc864	Apalache	Lambda	BoolSet	False	Passed	Model Under Test Equivalent Model
b2f1014d13224d761556e01cc052c61bb7b808f6	Apalache	Cross2	BoolSet	True	Passed	Model Under Test Equivalent Model
7d287f1edf058ccb38702186f2013536f80c90fd	Apalache	Cross2	BoolSet	False	Passed	Model Under Test Equivalent Model
efc69a34ec7dc84fca7f2901872971a69caa15a7	Apalache	Cross3	BoolSet	True	Passed	Model Under Test Equivalent Model
abb3094badc9605e68048f99f237776b72b5fabc	Apalache	Cross3	BoolSet	False	Passed	Model Under Test Equivalent Model
5a23f7b9e5947ae6e6f664f3338443ca78559020	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	BoolSet	True	Passed	Model Under Test Equivalent Model
2adca37da6cf656c5880c59cca909f6c50815052	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	BoolSet	False	Passed	Model Under Test Equivalent Model
decd59d8efebededf45f4e9a4a4ec93271097580	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	BoolSet	True	Passed	Model Under Test Equivalent Model
a020494904b8039551312479ff9591605f2647a4	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	BoolSet	False	Passed	Model Under Test Equivalent Model
5dc2821b1998ed5abb291892ee6be213571bfd05	Apalache	SetDiff	BoolSet	True	Passed	Model Under Test Equivalent Model
0a5ec998b4a0d19e18bcadef3b778204d0badd0f	Apalache	SetDiff	BoolSet	False	Passed	Model Under Test Equivalent Model
86d1eee35a0a1c184908f4622084b6626f99ec8d	Apalache	SetUnion	BoolSet	True	Passed	Model Under Test Equivalent Model
a4fa22c33c365342be06365bf9debd868d5e4871	Apalache	SetUnion	BoolSet	False	Passed	Model Under Test Equivalent Model
2f175b224190f5b8982b90548770b751adb5b804	Apalache	SetIntersect	BoolSet	True	Passed	Model Under Test Equivalent Model
b176889be3817d86b009c13f02d769d817017b31	Apalache	SetIntersect	BoolSet	False	Passed	Model Under Test Equivalent Model
dae6b4f02db89b960c87b540d9134ea46042949d	Apalache	SubsetEq	BoolSet	True	Passed	Model Under Test Equivalent Model
0871c5aff01d67008d7fa313c650b01aaf53652b	Apalache	SubsetEq	BoolSet	False	Passed	Model Under Test Equivalent Model
f96071e450cb80494058d93a3fe3fa44e5e0b2e9	Apalache	IfThen	BoolSet	True	Passed	Model Under Test Equivalent Model
090afb0b25c94df771fc4076f660160df0b5fb78	Apalache	IfThen	BoolSet	False	Passed	Model Under Test Equivalent Model
604a57d74633a957f55937b98a4c6b3c9fd9302f	Apalache	IfElse	BoolSet	True	Passed	Model Under Test Equivalent Model
c238ceb46ec0c625cf557918760f8895b438c608	Apalache	IfElse	BoolSet	False	Passed	Model Under Test Equivalent Model
86791ea5b266eb262c678a3a0569b698cbab3347	Apalache	Subset	BoolSet	True	Passed	Model Under Test Equivalent Model
cbc6d6c241f77bd9d790769295434148bbe68c12	Apalache	Subset	BoolSet	False	Passed	Model Under Test Equivalent Model
78ce367b918580626c077764c2ebf057c7011353	Apalache	Unchanged	BoolSet	True	Passed	Model Under Test Equivalent Model
3b2fa7f5b2264d42dbd9d31a7800a5b28943e6af	Apalache	Unchanged	BoolSet	False	Passed	Model Under Test Equivalent Model
edddd2465a0eeda20d0c22697985dc9943443302	Apalache	SeqSeq	BoolSet	True	Passed	Model Under Test Equivalent Model
e59ab48d382b59546562ad885622efb5c59bb6d2	Apalache	SeqSeq	BoolSet	False	Passed	Model Under Test Equivalent Model
7d822ae7d8cdbe615314f4eeb5460e3d5754e05e	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	BoolSet	True	Passed	Model Under Test Equivalent Model
db0e77d8cff90452d6818198bb0be6a9dcf87aef	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	BoolSet	False	Passed	Model Under Test Equivalent Model
a7608a583667b7a24badc1a9b961b50e758d00f8	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	BoolSet	True	Passed	Model Under Test Equivalent Model
aaadf43b063a19498afe10922080d6c88d36ab27	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	BoolSet	False	Passed	Model Under Test Equivalent Model
0ad458dc0a660695aebba3af57c4608ccb86e860	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	BoolSet	True	Passed	Model Under Test Equivalent Model
91021823b9eebfce650f3cd9c7480cc77c43bd27	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	BoolSet	False	Passed	Model Under Test Equivalent Model
9e468f8631d813775fa643a8e48bea7db8118850	Apalache	BagSetToBag	BoolSet	True	Passed	Model Under Test Equivalent Model
210375098b924d57bf53b7961a15e93cb3bcf08d	Apalache	BagSetToBag	BoolSet	False	Passed	Model Under Test Equivalent Model
5564e274f9680cbf407956d04361a4f337ea5e19	Apalache	BagBagIn	BoolSet	True	Passed	Model Under Test Equivalent Model
e348d5c844a69bb5dc2ec37dd4cb162319503ca6	Apalache	BagBagIn	BoolSet	False	Passed	Model Under Test Equivalent Model
2d868dbbcacca010a29169005c96834744b142e1	Apalache	BagCopiesIn	BoolSet	True	Passed	Model Under Test Equivalent Model
8cafa06c3632e434672736fce468de4adfb76a98	Apalache	BagCopiesIn	BoolSet	False	Passed	Model Under Test Equivalent Model
fbb5e3b4ec985739ce931382c87baf463b8cbf0a	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	BoolSet	True	Passed	Model Under Test Equivalent Model
2f94b53d1bc4b6752667e40e87ea37490b1eed27	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	BoolSet	False	Passed	Model Under Test Equivalent Model
2dbaad9e2a1728dd50cd9ac7b36ada905dbc0ea5	Apalache	FiniteSetsCardinality	BoolSet	True	Passed	Model Under Test Equivalent Model
0188b51bfdfaa7a8f0dda3bfcb236f42d7276f16	Apalache	FiniteSetsCardinality	BoolSet	False	Passed	Model Under Test Equivalent Model
ffee98d15801fe6ea76b3f397beaf24f0821469a	Apalache	SeqAppend	BoolSet	True	Passed	Model Under Test Equivalent Model
119bc071c28362b7161f726c39c721cde24b9f86	Apalache	SeqAppend	BoolSet	False	Passed	Model Under Test Equivalent Model

Index

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