Index


  • Introduction

  • Skipped feature combinations
  • Failed test cases
  • Tests by feature combinations
  • SYMMETRY tests
  • Tests under anomalous conditions

  • Tests by feature combinations: -workers 2
  • SYMMETRY tests: -workers 2

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
680e368f8d05e2441567195cb4565858c1e9721e TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
SeqHead OneLineComment True Passed
  • Model Under Test
  • Equivalent Model
dc3cf96bcf4fc5809df5357c2191f794585aa8b9 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
SeqHead OneLineComment False Passed
  • Model Under Test
  • Equivalent Model
ff78418f7195197407854d67af1a2a3789a2f117 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
SeqHead MultiLineComment True Passed
  • Model Under Test
  • Equivalent Model
a1bd2cbea53595254ce8bd3020f07c0ecc0e875f TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
SeqHead MultiLineComment False Passed
  • Model Under Test
  • Equivalent Model
e611a1c56dde5c52048bc3bc7c55e4d1b86cb75e Apalache SeqHead Let True Passed
  • Model Under Test
  • Equivalent Model
0b30731273b7a700d1527f6bd227d81ace20d9c2 Apalache SeqHead Let False Passed
  • Model Under Test
  • Equivalent Model
88498a2bfa90da3f9cbcd12b9b65df42d7712319 Apalache SeqHead Choose True Passed
  • Model Under Test
  • Equivalent Model
508795b174bedda8882a81517e700151f67700ab Apalache SeqHead Choose False Passed
  • Model Under Test
  • Equivalent Model
48f88ed399b27318a455b958f20547007a9930c9 Apalache SeqHead Tuple True Passed
  • Model Under Test
  • Equivalent Model
5d4629c4099230ded2337e03c8d809988168b81b Apalache SeqHead Tuple False Passed
  • Model Under Test
  • Equivalent Model
4cf1156e005f4d434d61c44c22b5fa2461c7235e Apalache SeqHead TupleEmpty True Failed: Head of empty sequence results in error in TLC. Apalache is unable to detect such an error and instead returns arbitrary value
  • Model Under Test
  • Equivalent Model
13b8a5df936f0a06bfc14d43a657bcbec061b694 Apalache SeqHead TupleEmpty False Failed: Head of empty sequence results in error in TLC. Apalache is unable to detect such an error and instead returns arbitrary value
  • Model Under Test
  • Equivalent Model
1f99f4330840e72d380adea6072f0bea17dc0e11 Apalache SeqHead FunApp True Passed
  • Model Under Test
  • Equivalent Model
9b4f3daaeec7064f41ceed4bfc3ec388904b431f Apalache SeqHead FunApp False Passed
  • Model Under Test
  • Equivalent Model
727e030fd21e34b95d57925a9191c6015bfe23f2 Apalache SeqHead Prime True Passed
  • Model Under Test
  • Equivalent Model
eadde176d4fe38ecd37226791d63a7a37d78c800 Apalache SeqHead Prime False Passed
  • Model Under Test
  • Equivalent Model
83354d6c048ba4a55c2137c9c348b0f966b1f34b Apalache SeqHead Def0 True Passed
  • Model Under Test
  • Equivalent Model
525ccec070447ae0872a999e8efe78552d207d15 Apalache SeqHead Def0 False Passed
  • Model Under Test
  • Equivalent Model
7a854ce0f13483c6fb8ce84104587d394d65271c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqHead LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
2b83de403fff2e3942b6443bb91acb552771c8d2 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqHead LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
49f2b21ccdfe66889390388dc6090c61395cb5ab Apalache SeqHead Def1 True Passed
  • Model Under Test
  • Equivalent Model
697074930e5b5003ee29f831a054be64e40d2693 Apalache SeqHead Def1 False Passed
  • Model Under Test
  • Equivalent Model
74b82ce3cddb218c0198018cc37defbfaa53edb4 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqHead LetDef1 True Passed
  • Model Under Test
  • Equivalent Model
9f07b5264e97408efc06d250c1223987bab64af0 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqHead LetDef1 False Passed
  • Model Under Test
  • Equivalent Model
4b2f0ea10e9f41536bde2e9cd98fb0605c9e8aaf Apalache SeqHead Def2 True Passed
  • Model Under Test
  • Equivalent Model
8f56feff41c9a75902a9d4be10fa81b55ee1049b Apalache SeqHead Def2 False Passed
  • Model Under Test
  • Equivalent Model
765b138e3e3c4916b83488dc02cf77a04b9933d7 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqHead LetDef2 True Passed
  • Model Under Test
  • Equivalent Model
b58b3731180b2b69c057df914494e6dab0fafa63 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqHead LetDef2 False Passed
  • Model Under Test
  • Equivalent Model
996cfee789dae6223a2bf80dae528f7863cbbabe Apalache SeqHead Def1Recursive True Passed
  • Model Under Test
  • Equivalent Model
ea39f4ce603c323cc57a6fdb115e0f6524e0921c Apalache SeqHead Def1Recursive False Passed
  • Model Under Test
  • Equivalent Model
ebcd6b01706339a12ab6195af019b4514790af51 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqHead LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
d5a722b2b26932052d549473744fd418e97e5d70 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqHead LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
932542e0e7f2ee86c458f2cc2708d19ebecba9bd Apalache SeqHead Extends True Passed
  • Model Under Test
  • Equivalent Model
e08c4b0481469d9695d89d7d2645e0097213659e Apalache SeqHead Extends False Passed
  • Model Under Test
  • Equivalent Model
540c70102c02fced15063a38792610eb72cc7236 Apalache SeqHead ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
7b7b5c85def59c39758f34edf22e6ed4e19faef9 Apalache SeqHead ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
571649dfe7518a8814620fc4aeb4b1f38f3dcf11 Apalache SeqHead Variable True Passed
  • Model Under Test
  • Equivalent Model
4346779e0f7256277fd01ebab9c347cb6654023d Apalache SeqHead Variable False Passed
  • Model Under Test
  • Equivalent Model
a2bde81f0e9128308fa2ac4c2d613a1abdbb7d92 Apalache SeqHead Constant True Passed
  • Model Under Test
  • Equivalent Model
1f9e677357eeeb9b220d95727d72bbc204be1b82 Apalache SeqHead Constant False Passed
  • Model Under Test
  • Equivalent Model
ddce54f39124250621b1b6e6cebb35b47d0b8c5b Apalache SeqHead ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
26dd5f9817be25dbde29d358ef2c2fd48491217d Apalache SeqHead ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
929797852d5e84fb407024351f488da39f563a4a Apalache SeqHead Instance True Passed
  • Model Under Test
  • Equivalent Model
b2098465432ddfcaa8c34c60031958dcdfd3dfcc Apalache SeqHead Instance False Passed
  • Model Under Test
  • Equivalent Model
feee2fd85054ea9876a78c90b9fe7b508c4b9424 Apalache SeqHead InstanceWith True Passed
  • Model Under Test
  • Equivalent Model
501483323f290b605e4652d82fcedf3281011e3f Apalache SeqHead InstanceWith False Passed
  • Model Under Test
  • Equivalent Model
d351edc78f92c502d5981814add8226026bc67f9 Apalache SeqHead InstanceNamed True Passed
  • Model Under Test
  • Equivalent Model
e03dbe352254cb31a39f8b9d5125a8014d5e4105 Apalache SeqHead InstanceNamed False Passed
  • Model Under Test
  • Equivalent Model
10ef17cf0d45ba39248c49339e98474caf9d4cdf Apalache SeqHead InstanceNamedWith True Passed
  • Model Under Test
  • Equivalent Model
e98885d78b2ba4c7843e7b34708b0ee2b6bd15b9 Apalache SeqHead InstanceNamedWith False Passed
  • Model Under Test
  • Equivalent Model
9f2a9b61306ca7bc9194125bf280252456d7b416 Apalache SeqHead InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
e1a11a631a30d15d50c8f1c2ddae1eced115a428 Apalache SeqHead InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
21d950b59386720692b58a3a95360ee3dca5e208 Apalache SeqHead InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
f9213f39147ad00428563029ce70224fb6175466 Apalache SeqHead InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
528e470b3c1d9f899adb0673e8cf8b210ca7d204 Apalache SeqHead InstanceNamedInFolder True Passed
  • Model Under Test
  • Equivalent Model
54674a26ff449d1c9691455e638936bc805858f4 Apalache SeqHead InstanceNamedInFolder False Passed
  • Model Under Test
  • Equivalent Model
c377e5fd0bba5832050d9fb2f4d7dd96067c0142 Apalache SeqHead InstanceNamedWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
2f78f9fb012063d40651b6007430071f9cff58e6 Apalache SeqHead InstanceNamedWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
d8c254303e582b434be2ffdefc2b9b05ea373624 Apalache SeqHead IfCond True Passed
  • Model Under Test
  • Equivalent Model
0c8155ade0fb3fdd54f7d43232bbd9a7fee46c20 Apalache SeqHead IfCond False Passed
  • Model Under Test
  • Equivalent Model
9f9b731f650db07265624b9e8ec439fbb9faee6c Apalache SeqHead IfThen True Passed
  • Model Under Test
  • Equivalent Model
019e651872cbc49131e370e7cea1b77bfb60cb1c Apalache SeqHead IfThen False Passed
  • Model Under Test
  • Equivalent Model
9513bff3b2ebc396349e0be4657f3be37ddc9cf4 Apalache SeqHead IfElse True Passed
  • Model Under Test
  • Equivalent Model
a35915889c5e630896db330c0d11fe53482a27d4 Apalache SeqHead IfElse False Passed
  • Model Under Test
  • Equivalent Model
a2b7062f084c5147ce3e7cd355f1899fb6ae2499 Apalache SeqHead SeqConcat True Passed
  • Model Under Test
  • Equivalent Model
6a241d0f4cb85632b268e9c9d24182b12f99738e Apalache SeqHead SeqConcat False Passed
  • Model Under Test
  • Equivalent Model
448c6384156cfeb120ee68712030a30fd861d6f0 Apalache SeqHead SeqSelectSeq True Passed
  • Model Under Test
  • Equivalent Model
88bed97c90c5b355e28a1cc478ed2e1e850d9b29 Apalache SeqHead SeqSelectSeq 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
a217bfa10d359412d0476f9434e769664af4b762 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
SeqHead TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
9e334b8e4735d1822a5393bc7bcd17669d4791e6 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
SeqHead TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
fe5bd15db5b3457a65bcddaddf801f3ce0461027 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SeqHead TlcEval True Passed
  • Model Under Test
  • Equivalent Model
3cd99092241890859b893cf73e65d0a7469f74f4 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SeqHead TlcEval False Passed
  • Model Under Test
  • Equivalent Model
206eee6c7b08a142bf18b646a826dc4951390797 Apalache SeqHead SeqHead True Passed
  • Model Under Test
  • Equivalent Model
d226ed08096d6836d0d24cb312db935961d33c17 Apalache SeqHead SeqHead False Passed
  • Model Under Test
  • Equivalent Model
40a2cd5141b4338d90ceb2a6ef7eb7dc3bf39f4b Apalache SeqHead SeqTail True Failed: Head of empty sequence results in error in TLC. Apalache is unable to detect such an error and instead returns arbitrary value
  • Model Under Test
  • Equivalent Model
b40b7b84fd06cc86dbc07d7161924a9dc068e129 Apalache SeqHead SeqTail False Failed: Head of empty sequence results in error in TLC. Apalache is unable to detect such an error and instead returns arbitrary value
  • Model Under Test
  • Equivalent Model
244c4638e656c8b6c6ece14c2b98f3004584c793 Apalache SeqHead SeqAppend True Passed
  • Model Under Test
  • Equivalent Model
a634e75f6b0453ce3247869dcdf71708e835a2c0 Apalache SeqHead SeqAppend False Passed
  • Model Under Test
  • Equivalent Model