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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
87d7ad80cc295cd0433ff8c2254f14fbb3c18833	Apalache	Eq	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
7e7bf8ee5cce63f7d36e275ec0a691a818b7fee4	Apalache	Eq	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
3183c6599dbc7abe17c6db76587bb0e2c86fb968	Apalache	Ne	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
c164913254fdb74e54d62a199c8cfdaba1c2edba	Apalache	Ne	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
0ac54ff005396a6396945f0b8f1e561bb3ebc84f	Apalache	Let	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
b9dd7c05be6c428d7a638c480a66eddd6f139848	Apalache	Let	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
d9f734b711e395b8ff2824c36c63621161a95dc2	Apalache	Set0	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
3edf0b5a04801b4de661939cd5c3f485cdd9a080	Apalache	Set0	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
af3f812ddb50fbf4989825a242d030d95fde0ba9	Apalache	Set1	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
c620abfd3c4ef61c30a81ea86c03b3a750a3e764	Apalache	Set1	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
ae095567b714baf3be6a20f3286437bf55eeae15	Apalache	Set2	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
3de6bb1d66e5dcf0d932ddeac7f79bd2d219427c	Apalache	Set2	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
35a54109bdc68b40a802199ada8922db803687a8	Apalache	Fun	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
64aa647114dcbab8e5757ea7d2dff648672d37f3	Apalache	Fun	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
436f51adc70ec59fc3dac47d7b35df954ad27c2c	Apalache	In	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
ea4e578f9160a24cfa986b270bd1f9a720f518aa	Apalache	In	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
747cef4ea71fb8d5a64c8591c27fb0df0d2e8ecd	Apalache	NotIn	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
82635a59dc65222733d1cecf69661b191decb9a4	Apalache	NotIn	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
69cd19b75f57e0c276be9b878175023b684bf7d6	Apalache	Record	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
a00bb5049304921220985fd311669f5489db4d4a	Apalache	Record	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
b87925cc512d9a67b42d9a7e29395493209ce876	Apalache	Tuple	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
082ab9a25322b349bdc78e5af67e2706f544bbf6	Apalache	Tuple	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
4c5e69b49cca62f0d3074f5c71a5606d8fb2d40a	Apalache	FunApp	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
92b9e627c2f3a5e82b9664862cc941738b8fecc0	Apalache	FunApp	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
c852c72f3645a4d5615c7576bb7760768a383526	Apalache	Except0	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
d5350c526969170449d35c56dffef03543b72186	Apalache	Except0	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
4c75caf0f44633c5cf6226b4bc02daa891e8fe62	Apalache	Except1Fun	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
daa1bea8f3bab7c6875a779fe55d769ee13bcfad	Apalache	Except1Fun	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
1f90aa4b4a183da626714c27df5746d8691c9c7f	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
55231465fc6854db5702e29b9b1dafc7c052c4e0	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
e02e385a00d3766d52b5a9165e136dad8f8ac79e	Apalache	Except1Rec	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
0cd39fd2a5a652e6f57b83f6ad543ee2bd260ebd	Apalache	Except1Rec	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
7c01ca0f0b2412a69f636de8997dee9cfe6b2889	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
9a6c671e344e3cb9d211bd1b95bef659aa283230	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
c8bc88df4e8106f9444969bb94e45555bac24d0d	Apalache	Except2Fun	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
79254888cda7e5474b02ab230542b2b6cabf22e6	Apalache	Except2Fun	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
5d9b267b69c1a68994be6369f865739138905b17	Apalache	Prime	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
b21a3a1e3a1b047759c129370191ad755020ad33	Apalache	Prime	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
94d3f31a8aa47a46b3fa005073eab3d08895f6ae	Apalache	DefFun	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
e2daec3167329dc77daa63bc27dfea2a0385c3be	Apalache	DefFun	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
b890259fb43fa60431288528955bade1d38f138a	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
d79ddaf54fabd0470d714c6364ed91e25776df85	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
b76c9a588eaee2366b7f0069e455643d5e40eecb	Apalache	DefFunRecursive	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
63e0df2474f6e3acec940bcabda22b737db037c2	Apalache	DefFunRecursive	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
65fe7eb6aaa96e1bb7382c5b550cf298fed4f9be	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
2074e5159df30e86682d9c224dec923284946ffc	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
0394ee365d19124e11309cf37af1a659c108d34f	Apalache	Def0	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
72ce053bebab3fdfa30662d31f662ee5f12d3a8a	Apalache	Def0	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
d829657be7e0d0e58210f67f632e519fdd6c27ef	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
16fa414dfbe1734c02b6ae1abb6fede6bf9b322e	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
823b4f7fc52c582e47303f7422f9f5fd75d3073f	Apalache	Def1	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
5f5decf7f000f47f15d898a164e5cfa1b2372a11	Apalache	Def1	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
67b4d42c6cad76e6478fa11732cc9dd6d4e7be18	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
e161ce89ff95e7d5a2c047f6f5c633e6e0cba17a	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
4c2bb855f38d9f453cfbc8b4bb32983d3e653859	Apalache	Def2	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
e3cd709498abaff57448d6f5eee062d2bebc3c32	Apalache	Def2	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
f2efa24a641c7cfc87da3ee3639ce20ed60f20ff	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
4692e2f01e2baf174ad7b5399309bf145e5c92f6	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
9dcdb183ff7cdf0e9e80794e442a6c76d608f8eb	Apalache	Def1Recursive	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
74a5a24884b13752a41718f3afc455d7112f1a06	Apalache	Def1Recursive	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
8e03142d2cccf1eb29b9a8d8d26b0d01e68e2c67	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
fa30e12bfdb1b3320b721460d28299c3eed702fc	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
1801562e1dae14dc821747f02e1c749292663733	Apalache	Extends	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
8808bc2a7ef0bd92e0f1fe587c34f23947f364b3	Apalache	Extends	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
2ff025f7cd66580e61e7d1af437010be37cc7c69	Apalache	ExtendsInDifferentFolder	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
95dd7c0fe9718842248ff15c004f2de2f09b1243	Apalache	ExtendsInDifferentFolder	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
c372de507f484807481b36a95b9ca6c4ab519c28	Apalache	Variable	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
290915a55da39a23ee130dfaefecedfeea941fd7	Apalache	Variable	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
71386b669eed8f0b8f1d1aa39c8cee1d93de97f0	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
fe3b1c381251cc3507fc56ab440ca874ca0322c9	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
ab9a5a34eddd92d45db2f57abc19db6070efbb20	Apalache	Constant	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
ce5c4902ebeb36e185e29a3daae8b0203c8ab264	Apalache	Constant	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
8df24c7fde91f3736afb75b64ebca477c370effb	Apalache	ConstantRank1	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
f6854f719118bd5dfaff13cc5052dae476a908bb	Apalache	ConstantRank1	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
6c34c952959fc23b564edc921d28243687372428	Apalache	Instance	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
dcb0d6a218100e86b7d5c6e26fad322d9ee7f011	Apalache	Instance	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
d7826437292f83545f533b6cfacb29cbf41850b2	Apalache	InstanceWith	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
5a5dddd719077a1cb2490162a67a74adf1be97f8	Apalache	InstanceWith	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
ae7a0d02352798cc63d701bf28b153f2f3d888d0	Apalache	InstanceNamed	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
1a209ec2229fa73b71b1fb3bd5c8db315d980ce9	Apalache	InstanceNamed	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
bf3a166e023ed8326d1e35eb1300ae8f44e70e0b	Apalache	InstanceNamedWith	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
c84d6c5031583051a7a1058efdb6bf6d98be36e5	Apalache	InstanceNamedWith	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
9a8f47a5b8261c726d127968542091498ae11eeb	Apalache	InstanceInFolder	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
6b4df7fc82eca27806835e8edca20eab621de31a	Apalache	InstanceInFolder	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
c3ce5eaa8c28fb1ebf929c6efcdb9a111dc09bda	Apalache	InstanceWithInFolder	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
0ce0d71672c2b8a81235d866da19bb2194da4393	Apalache	InstanceWithInFolder	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
cc235f3ce9e6db8e20c5f0975e37493bbc4f0f26	Apalache	InstanceNamedInFolder	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
b60017862d8e641888e73068e46059cd69ee874b	Apalache	InstanceNamedInFolder	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
325e2d98f0ab3d9d6e7c5320e519552c6c0ee77e	Apalache	InstanceNamedWithInFolder	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
5e134335242ba1dc8454db24076bdd94cf6ec02a	Apalache	InstanceNamedWithInFolder	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
ba23acc8a21bd5b779fc279212bce57065f15678	Apalache	Lambda	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
21e4bff41ac722653d677797e949f4b8e1a62479	Apalache	Lambda	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
cf109c3ef7842d82cee1f668a32509399cfcb25f	Apalache	IfThen	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
15face7766c80da2d4e26e74f8438a48099d01c8	Apalache	IfThen	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
db2d10d2cb552f62e2dd96065534939376853322	Apalache	IfElse	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
9f6816afe982193225901ffdfba6fbe0ee03bbc5	Apalache	IfElse	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
b388d862ebade989d278455ea8f9a3d9bd174e94	Apalache	Unchanged	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
8afa93f864ea08d2e4dd71b71989bd5cf6cb98be	Apalache	Unchanged	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
98af65116937abffd370b1e4b8820c32f4a5dc49	Apalache	SeqLen	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
f6b07dba1a9f9960b2fcd162f4d73109b2b72d21	Apalache	SeqLen	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
f9f1941e0dfed321d3dc524ae5e94348ccc9412e	Apalache	SeqConcat	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
9fe221dae1fdd942f00f9aba418f9be09a688dcb	Apalache	SeqConcat	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
475a023f9ad304e5600a7b27f762021e1e13fec9	Apalache	SeqSelectSeq	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
e6600faf4e4dbfd2043c37090f0b27cdcab1e715	Apalache	SeqSelectSeq	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
2aaae43ae019cc97313dc5bb7e11517d5876a96d	Apalache	SeqSubSeq	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
e37b75cee1d86e9444f39b5bdef927b39c326b13	Apalache	SeqSubSeq	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
b8ff613352338ded148a1c27965b83e7a2b4c8c8	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
02d16719a38489158fc87b6ca47196afd34b92b7	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
7c3ad26a5b83ceb61cf71ef2e982bc475896a7be	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
81f3cb87a287749ff7eef8598e3826360eb4cb2f	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
4f96ec3d9ca1d3ad0eace6e50d6ef8a40bf212f3	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
829a5945ff38b96987b943f9115c9bee9b9a7457	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
58b27f2ef6b71eabad0012e3394bb7d4e5341e34	Apalache	BagBagIn	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
fdbcb4f4a5b8f0cf0ac49760e8a204556f0c1e69	Apalache	BagBagIn	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
d97b603d7e6e211464bf024efdbccfae5e3aeb07	Apalache	BagCopiesIn	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
b6dd34ebf54c2ff9c215ba86fa255a1e6eb7f83f	Apalache	BagCopiesIn	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
dac7b210c125b85189ca6cfe5e43745efb83a428	Apalache	SeqHead	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
53af9fa9168fe041c6ef2f91d8a5a72ebf3dc60e	Apalache	SeqHead	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
436c906bb8929a33a1cb833999bac6c941cbc123	Apalache	SeqTail	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
f25716c67c0a6e342b7b7b7aa79de633830cc2f9	Apalache	SeqTail	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
913cc61f0485ec624082be9a225574d40b9de3b0	Apalache	SeqAppend	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
156fe49aa6134a566f949a9fb467ea89f7a0bcf0	Apalache	SeqAppend	SeqSubSeq	False	Passed	Model Under Test Equivalent Model

Index

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