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 IfCond; CLI Option: -workers 1

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
d9ac573f5d9a44bca39dbf671238634a9275c6a7 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
IfCond OneLineComment True Passed
  • Model Under Test
  • Equivalent Model
421fa69db80e35df9cb75465fd19a7248e9b5b6a TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
IfCond OneLineComment False Passed
  • Model Under Test
  • Equivalent Model
fa043dc6a4039ad6009293eb9398485fd26bda9d TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
IfCond MultiLineComment True Passed
  • Model Under Test
  • Equivalent Model
a4276e8b05fb221ddfe5a91c3a60e3e92cfb35ec TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
IfCond MultiLineComment False Passed
  • Model Under Test
  • Equivalent Model
38c89bb8c50b06e2dc2ace0de2da0da9610f6dc0 Apalache IfCond BoolTrue True Passed
  • Model Under Test
  • Equivalent Model
048ac972b41ffb548e179662cd6371991f0ddbd3 Apalache IfCond BoolTrue False Passed
  • Model Under Test
  • Equivalent Model
6a47840bf71e797beb768a736e7419628b9cf53d Apalache IfCond BoolFalse True Passed
  • Model Under Test
  • Equivalent Model
73d3ae1724f1eb279bfb173413e0c232e49707a5 Apalache IfCond BoolFalse False Passed
  • Model Under Test
  • Equivalent Model
2b9eb80e6c5de9d90c59ba35b34fa9d93468288d Apalache IfCond And True Passed
  • Model Under Test
  • Equivalent Model
da7995a2f9a87ad567456f79e8bd5e189911a16a Apalache IfCond And False Passed
  • Model Under Test
  • Equivalent Model
64a3be96f34a9e2a89e3cc63e8e5d0dffe15def7 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
IfCond AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
ac375deb815573158173961773cdfadeed8ae534 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
IfCond AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
2f36c929933b7e3ecc79dc0cee76ea0b6d71c958 Apalache IfCond Imply True Passed
  • Model Under Test
  • Equivalent Model
af53452c806278083050e3f22b5120233a78395f Apalache IfCond Imply False Passed
  • Model Under Test
  • Equivalent Model
5a0769ca50983e0f0b3002735033c351d6666c8c Apalache IfCond Not True Passed
  • Model Under Test
  • Equivalent Model
d2c6a7f946ab4fc03d90e1e611d902c634f57133 Apalache IfCond Not False Passed
  • Model Under Test
  • Equivalent Model
278439f6dbde013cc4a56108adc791b2b4bf5b0e TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
IfCond Or True Passed
  • Model Under Test
  • Equivalent Model
8cd80d8693e5017a0f7f7b4f3a8edb8c7f03068c TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
IfCond Or False Passed
  • Model Under Test
  • Equivalent Model
c6dcea75d114441f44bbfa1544c605efdfaa5db8 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
IfCond OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
75dd5329f688fb10c63fec5bc708a8d534a5a883 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
IfCond OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
6bea2bda286eaa7522212519a2e1dd8e72ef5a3e Apalache IfCond Eq True Passed
  • Model Under Test
  • Equivalent Model
0c7c4accdd0823287642138f038264630ea36e56 Apalache IfCond Eq False Passed
  • Model Under Test
  • Equivalent Model
fdd110c48a6ae0d9d43cf67f8a8238e5e0d8698a Apalache IfCond Ne True Passed
  • Model Under Test
  • Equivalent Model
42204b898547ff8df3db3f4269b7d8994c6aa19b Apalache IfCond Ne False Passed
  • Model Under Test
  • Equivalent Model
275c3394e5f5080547c33724dc884318b7ec3a4c Apalache IfCond Let True Passed
  • Model Under Test
  • Equivalent Model
62636e30487f3992bdbe752070ac45afe1b3910b Apalache IfCond Let False Passed
  • Model Under Test
  • Equivalent Model
184800cab8abc4ece178fd7f14a7c0d0eb651e2e Apalache IfCond In True Passed
  • Model Under Test
  • Equivalent Model
95ee28ba014e76e9a21441249b9d0c5848ae5409 Apalache IfCond In False Passed
  • Model Under Test
  • Equivalent Model
2554d3e18971170866f1b656dd9ab9af86b9b025 Apalache IfCond NotIn True Passed
  • Model Under Test
  • Equivalent Model
e029e60af36a3e8da8d3383c42b186bdeaef9ad2 Apalache IfCond NotIn False Passed
  • Model Under Test
  • Equivalent Model
dd8f0121f919336b8810c2d5c721f3e0c142892f Apalache IfCond Exists True Passed
  • Model Under Test
  • Equivalent Model
ec93584919db49c5ac98183fdad4eb257f1b1a45 Apalache IfCond Exists False Passed
  • Model Under Test
  • Equivalent Model
0823bbcf75e298e094320566ea3aa438c7706f5d Apalache IfCond Forall True Passed
  • Model Under Test
  • Equivalent Model
18cb9692e220e43b59cb21ace6e24afd00935a34 Apalache IfCond Forall False Passed
  • Model Under Test
  • Equivalent Model
03077444965e6a3027cc41b453d6975a076f8ba0 Apalache IfCond Choose True Passed
  • Model Under Test
  • Equivalent Model
fd89f1938f68a88f2d0b3d9e823a887ac5fbdef1 Apalache IfCond Choose False Passed
  • Model Under Test
  • Equivalent Model
acdeb4dfe1a94d7e9585a83fb87273222bfa1e5d Apalache IfCond FunApp True Passed
  • Model Under Test
  • Equivalent Model
f783886a101a14537297d7230d04c8395d296be7 Apalache IfCond FunApp False Passed
  • Model Under Test
  • Equivalent Model
5541bd1232289c8241b615955bffa5eb5dbbf027 Apalache IfCond Prime True Passed
  • Model Under Test
  • Equivalent Model
ef76214524a4af1a6be5dbdb8d0b00c52f753162 Apalache IfCond Prime False Passed
  • Model Under Test
  • Equivalent Model
b2be74a7987214c4f0ed2c2dd164f12bfee4cf3a Apalache IfCond NumGt True Passed
  • Model Under Test
  • Equivalent Model
f7f1c3474d2702651be9864fc2efb1396cdf7536 Apalache IfCond NumGt False Passed
  • Model Under Test
  • Equivalent Model
e6a0d0fc7ea21159cf93d8ca565ae35cc353bb3e Apalache IfCond NumGe True Passed
  • Model Under Test
  • Equivalent Model
39131f23645a6f03bd0f84c4c9739fac7f1d797a Apalache IfCond NumGe False Passed
  • Model Under Test
  • Equivalent Model
79c4aa367ea2b001ea353bc84140bd1b7ce72d06 Apalache IfCond NumLt True Passed
  • Model Under Test
  • Equivalent Model
9cb887065553762efa6a124815bb7453e4098bf2 Apalache IfCond NumLt False Passed
  • Model Under Test
  • Equivalent Model
9ad1563a063b18adb1d10828357e86b4451c2115 Apalache IfCond NumLe True Passed
  • Model Under Test
  • Equivalent Model
a3dbbaebd852e576a94ba1910d90f791aa6c311a Apalache IfCond NumLe False Passed
  • Model Under Test
  • Equivalent Model
7fd09bdc0322eb87796f12ea483378773329f828 Apalache IfCond Def0 True Passed
  • Model Under Test
  • Equivalent Model
45dbb2dc01582d20d5371b5caad3af19a295cf9b Apalache IfCond Def0 False Passed
  • Model Under Test
  • Equivalent Model
76d04b2905fb69b65d9bc491c462cb1829cc0876 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
IfCond LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
3226cb4e0bca038c2bb8ac5ef3045b70ce34ae32 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
IfCond LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
d6780d2405d7439c84658ee0d6be966b65c0e77b Apalache IfCond Def1 True Passed
  • Model Under Test
  • Equivalent Model
bd0673462a66bf728daa823208967446d97461e9 Apalache IfCond Def1 False Passed
  • Model Under Test
  • Equivalent Model
57361f7898b45560a542c126f986692d4ff3c521 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
IfCond LetDef1 True Passed
  • Model Under Test
  • Equivalent Model
c1b01c24dec250fe4b57601f9e913ca758942327 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
IfCond LetDef1 False Passed
  • Model Under Test
  • Equivalent Model
bf2637f44401f43e81f1e97617e00766ce7fc698 Apalache IfCond Def2 True Passed
  • Model Under Test
  • Equivalent Model
2c5174f3111f74f00b760ca3958876b7f562e5b3 Apalache IfCond Def2 False Passed
  • Model Under Test
  • Equivalent Model
d0452484b226966eacfa104ffd8aa570a77cc90f TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
IfCond LetDef2 True Passed
  • Model Under Test
  • Equivalent Model
3571a3460b1528763744db4b45a8034057d2979c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
IfCond LetDef2 False Passed
  • Model Under Test
  • Equivalent Model
597b99e074a7879314bcc8912303e825919e837e Apalache IfCond Def1Recursive True Passed
  • Model Under Test
  • Equivalent Model
3a6dc3789bf1716f461b6a211c383de7e07aa1fe Apalache IfCond Def1Recursive False Passed
  • Model Under Test
  • Equivalent Model
6811f35555c4faf8b10155e4f81c2f69d72588bd TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
IfCond LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
d30bc4c007047ce4954392f724653a19b9988995 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
IfCond LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
0d62280f29ee3a503876586887d3f02e57352ee6 Apalache IfCond Extends True Passed
  • Model Under Test
  • Equivalent Model
cf516f5eba9730933f4948746e426aa3ec76ee0c Apalache IfCond Extends False Passed
  • Model Under Test
  • Equivalent Model
5ba671f37ac003fb2ab82ac9f62e4d5f6d0ba74b Apalache IfCond ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
841db179bab17314e999fe6ce22117abe4915102 Apalache IfCond ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
5af841eda6c3a0024873232b923913770c0e054d Apalache IfCond Variable True Passed
  • Model Under Test
  • Equivalent Model
27ef54909e5bc0298d60a9425da84991220165bc Apalache IfCond Variable False Passed
  • Model Under Test
  • Equivalent Model
1bf43839d8dea50fa0b51353cd8fd4906d9f35c8 Apalache IfCond Constant True Passed
  • Model Under Test
  • Equivalent Model
a3cec76ed273153491897a1b80c14153329fa8c4 Apalache IfCond Constant False Passed
  • Model Under Test
  • Equivalent Model
2f77d4be7050474cbc95791d0cd0d8e4f2765b5b Apalache IfCond ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
7075187047528f63e9d37ba870763791fa20fbbf Apalache IfCond ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
3cba2c78587524ea7b32e1dfdb66fcc1d15d6344 Apalache IfCond Instance True Passed
  • Model Under Test
  • Equivalent Model
793f5a38f2d4583508a42c03a03ff28e4d770848 Apalache IfCond Instance False Passed
  • Model Under Test
  • Equivalent Model
aa29eca9a60ce2e3be555fbc325ccf95b066ae8b Apalache IfCond InstanceWith True Passed
  • Model Under Test
  • Equivalent Model
59a2fbfea9703a597fdf8c8966d45069aac41556 Apalache IfCond InstanceWith False Passed
  • Model Under Test
  • Equivalent Model
b5f2807f98617ef708f1685152d4b4128b506fcc Apalache IfCond InstanceNamed True Passed
  • Model Under Test
  • Equivalent Model
8403bbbc17fd17ef25f1ac3ca8a6c63c55c2c077 Apalache IfCond InstanceNamed False Passed
  • Model Under Test
  • Equivalent Model
6e1f2b564d41d04db6c8cf48c54a1bc52cc5d8a4 Apalache IfCond InstanceNamedWith True Passed
  • Model Under Test
  • Equivalent Model
10bf34aecdc82347ec9a2dc7969ee8fdddf14316 Apalache IfCond InstanceNamedWith False Passed
  • Model Under Test
  • Equivalent Model
1dd42248093731f4b75ff98e18ce70cd3e8fe824 Apalache IfCond InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
6d7505c965d9e0a6bf8e79b3f3b92b3135280bcd Apalache IfCond InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
ab8f5dde1ee689f01f640676677a935fdcef9a96 Apalache IfCond InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
3c4ecf8c63db97fd583f48d52ee14373898175c6 Apalache IfCond InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
d80ffe5112e747ecfdd570249fcf4e911f66cc0c Apalache IfCond InstanceNamedInFolder True Passed
  • Model Under Test
  • Equivalent Model
a250f7117529bbc6f7828d2263714473c15a55c7 Apalache IfCond InstanceNamedInFolder False Passed
  • Model Under Test
  • Equivalent Model
06cd57a3317051c2512b32e2e1d76d56f22a5049 Apalache IfCond InstanceNamedWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
22f935635593fa986123a1bea902fe74981c510d Apalache IfCond InstanceNamedWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
46d7c292d7de076086222e21e41c546daf03debc Apalache IfCond Enabled True Passed
  • Model Under Test
  • Equivalent Model
4e4f428f084ad7455ae0224415ac4de35d2104a8 Apalache IfCond Enabled False Passed
  • Model Under Test
  • Equivalent Model
4b46a6a4c366a14e731937fc7e75f5ee89a66b9a Apalache IfCond SubsetEq True Passed
  • Model Under Test
  • Equivalent Model
a8709300b4c78327c0485e55ea5d44e034a66926 Apalache IfCond SubsetEq False Passed
  • Model Under Test
  • Equivalent Model
dca1025cecf5e00f39c12fc75ea69bcf493cc413 Apalache IfCond IfCond True Passed
  • Model Under Test
  • Equivalent Model
4f3ac5ad0bb3717cfc337677eead9f0e921a183e Apalache IfCond IfCond False Passed
  • Model Under Test
  • Equivalent Model
988145162afce7e238c0a4cb76cd9e1b93c6e013 Apalache IfCond IfThen True Passed
  • Model Under Test
  • Equivalent Model
125dd2aa2ca5c90774e9f522d49cbe720006730b Apalache IfCond IfThen False Passed
  • Model Under Test
  • Equivalent Model
8bb8bd4b2ee45fa6620e4a5d20979bd68933f01a Apalache IfCond IfElse True Passed
  • Model Under Test
  • Equivalent Model
6edba2231e5c2e881c6532531ef40de09f689c81 Apalache IfCond IfElse False Passed
  • Model Under Test
  • Equivalent Model
4d68141e5a6286708280324f28db661109017583 Apalache IfCond Unchanged True Passed
  • Model Under Test
  • Equivalent Model
00ace853e47ecd5d3a4127554de916a1d0999a17 Apalache IfCond Unchanged False Passed
  • Model Under Test
  • Equivalent Model
28993c91864402d39ca59927806a0916368b0d09 Apalache IfCond Equivalence True Passed
  • Model Under Test
  • Equivalent Model
7994d25ea99f7ad562319c0c3cf6d7ab2fe12b95 Apalache IfCond Equivalence False Passed
  • Model Under Test
  • Equivalent Model
9379488003dae16839bb725de1106efba2634933 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
IfCond TlcEval True Passed
  • Model Under Test
  • Equivalent Model
6016ce3244b9a12836c763d55dd064faa636661c TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
IfCond TlcEval False Passed
  • Model Under Test
  • Equivalent Model
cf14e12a301d77145778c0fd16493c17f7616c3f Apalache IfCond BagBagIn True Passed
  • Model Under Test
  • Equivalent Model
5a729e2610df85f8d98e303ec693709f68d34fce Apalache IfCond BagBagIn False Passed
  • Model Under Test
  • Equivalent Model
8355b23b2536721f0bd07d7755b169897b60f22c Apalache IfCond BagSubsetEqBag True Passed
  • Model Under Test
  • Equivalent Model
bb33b539005ba23c2545156e7c9288636992315b Apalache IfCond BagSubsetEqBag False Passed
  • Model Under Test
  • Equivalent Model
416ca4e8910fcb9275aed2e6281938b96f56b82f 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)
IfCond FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
261f3d400205d6c01ae8491b9e6d567dd9e07064 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)
IfCond FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
236b0746bb07bf3f934961dcc1ee78e88d4e4709 Apalache IfCond SeqHead True Passed
  • Model Under Test
  • Equivalent Model
6dc18df976302ab2d94ca6c030d93384105d2f61 Apalache IfCond SeqHead False Passed
  • Model Under Test
  • Equivalent Model