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 plug feature ExtendsInDifferentFolder; CLI Option: -workers 1

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
c712508f80fd7bbde4c149a73cc801c0f49886a2 Apalache And ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
ae1e597ab9e05a25f6c5921003fcbc64f0d4d23c Apalache And ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
ed7eddc202a1d13b38da92954dedfa6b8596454b TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
5322f05050c15a8edcd0a2be5ddc264b41274974 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
2ea2e1d46d5f423b8c41185058bc0f2334369274 Apalache Imply ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
cd2a7cb60eb11839e2955f0cb9b2c4a5c3d781ea Apalache Imply ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
bad3a091b771009c00f8453d89f825be7cbabcb7 Apalache Not ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
500dd0207a3ecd5c86821bc0db4d8da40b3c1b53 Apalache Not ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
373608255dc986cebd2f7b6b8170e136668ff559 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
796ae86c0ecf2b055fa1c3214a94af4d36efe6e2 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
d4530816878a30861c4be905c79ab2c2f74d15ab TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
52760e1a4974917aeca12755bc25d08f35236254 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine ExtendsInDifferentFolder 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
a56666a78cb3b65a43751bd2570746834ab66550 Apalache Boxed ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
f999a1d92d5c3ad10729358e479c16de96a81e34 Apalache Boxed ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
5058a7b4a3048a285aef1d2dc754fb08278ac5e3 Apalache Eq ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
a89ada9742ac3b2d3ce40aa0422d347d94bba951 Apalache Eq ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
aa6d3456fb2e926d676e58788d6673d64a752c11 Apalache Ne ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
833b43e4b0b94c790342cb524ae8d3bd649230a1 Apalache Ne ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
eb1b51e99a3fc91dba9474edaf4d54c88ac90995 Apalache Let ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
7e34b889b060a50d868207eaefa9b93798d26ccb Apalache Let ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
130b7a796f1e9f53d87400ee86391494ed7614ed Apalache Set0 ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
9dc559b6da601079dd0abdce7435a1eb7e2d6d40 Apalache Set0 ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
ab69bd28edcad20fff700dcec2afd2db1660d3b1 Apalache Set1 ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
f95adeb42c343cef4c08489e84f3ec0293d1c078 Apalache Set1 ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
d3e1c1f67dd93dfb2ca8236605f7aaf1956edc57 Apalache Set2 ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
ebe1bf22b3a5e1a0a7a02b26fb6a1f56af549797 Apalache Set2 ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
efc2b113789bd830b5c41c6688c0893befa71585 Apalache Fun ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
2a736c0686c20e54af7f2ee384b38ba186315fae Apalache Fun ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
7e8be95b3877b337bbab3eed401bf0280c1f055c Apalache In ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
3c74573af1ee266e7b79c93e75c0fed1d0026269 Apalache In ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
3403ce865333a0aae6f12c0e851d9ce6c67f64f5 Apalache NotIn ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
01bf261dd0d931f052eb816d550c744cebdf9b49 Apalache NotIn ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
29d4c7a72b2eaec1910705593709d1c34120a386 Apalache Exists ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
34c0d758fd2905abf0f5b39916e375ab81b93766 Apalache Exists ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
894affc054d89eff1d6d4441501946e0bca4ad41 Apalache Forall ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
aa4a1e85a78ffc427e0f4c2da5968d43648558a9 Apalache Forall ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
e4f7a6a6da51ff112e928b4fc15613f2bdeb9c77 Apalache Choose ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
61a71c9c2f82c46a873ab4287f944324c0de6e56 Apalache Choose ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
129e2bb4ec6d15c928b3f03af2beccb78a2c0cc1 Apalache Record ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
cc81282f75f4b03ed296af89968182414daf83bc Apalache Record ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
1e48acb5e1c7ba05b0474457873824bc750bb9fc Apalache Tuple ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
06fdaf2864b195d36f2fc90d3804c23de6d90467 Apalache Tuple ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
6dbc7ffe8b19246e434dacdbc46f3ce97e818f65 Apalache FunApp ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
3e484aa0bc2cbdbc0f64e286b3b0bebc957b9568 Apalache FunApp ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
f48a4a660318a4da5e00b1666873714f595df495 Apalache Except0 ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
c1d84275c740998f4cac39a714e3a5f821382b21 Apalache Except0 ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
26c848e80b0b28c7b5c4108f55558fbf2740af47 Apalache Except1Fun ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
e2cf2250abbcaf4c9b5991a4ff8dc74baee23c73 Apalache Except1Fun ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
3348b4d077cf49c8dc749aec7b4bf663fc97a207 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
8d48289d3f7004e35dc4ac8893db27b6cb54de1f TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
05c4dbd74b64ff1832dc3fb258b60745d66a187f Apalache Except1Rec ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
95ac3881cba6867a6d18f84dfe97b2692169bda0 Apalache Except1Rec ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
f9ef88489cce1f774fc929105e8c876981aa58c8 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
68182d60ee2b4affa11815d7d0c0ca1c5dac47ac TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
6a5c3bbaf983eea82df35ec78678d533c35acb2a Apalache Except2Fun ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
dad693f6ef56a2c844baf18eb2ed2a50ab817fe9 Apalache Except2Fun ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
f63ee4983c69b7fbfb5431041a546652306d52b2 Apalache Except2FunTuple ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
a02fc15dccaa13b39a793a3a7b18b20457dbb0d7 Apalache Except2FunTuple ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
6763f6cc045f879ea2c2985b16512e9e7603972b Apalache Prime ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
fc6e78629143ea9f39ae71edcdc18eefe88cc0ae Apalache Prime ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
2c05f92c57d661f19290549468147a6e0a7e3c20 Apalache NumUnaryMinus ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
84359fd319757869718653905707491ca3ea7e8a Apalache NumUnaryMinus ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
a28f17ecf89a38d9810d174f3f5860cfa4a9a137 Apalache NumPlus ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
699a477570699172b020d10efcf95abb66b7fabb Apalache NumPlus ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
5f48d5fe59ccb1215a7a95d814649fb9169a86ef Apalache NumMinus ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
94684a7b8b9a84a4d6f93f7910c63d16ca13780e Apalache NumMinus ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
7e1bbbeafb3d1e47afea45742ebfc689b9d2e830 Apalache NumMul ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
0c9df7f7f422e922239c30c9b1a7ede0a5e10c14 Apalache NumMul ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
2e664c18c948468cb6c86d67b9e1764900b5b45f Apalache NumDiv ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
edac7cd50f6a00d7f8347d8ded173ca489edf1f7 Apalache NumDiv ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
8f43db7b973dec0a1b390256de919509fe6c1a52 Apalache NumMod ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
3d1078419bb1ce0e193b80f4ae6eece020fd4d35 Apalache NumMod ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
fc9889b81d7370417725bf2028ce264383c0d273 Apalache NumPow ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
970b9a637f799f5923e4fecba3534dbb2466dacd Apalache NumPow ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
4f8f56d43410c3c2215960d8f8df2b6107bc32cc Apalache NumGt ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
543c027a7b7352ceb5df118952a86d760a3b916f Apalache NumGt ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
189c3974ba78e33a2feaf03a6eac3788881381b2 Apalache NumGe ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
106a5326e19eb9d1a9defe21f5f835019e6f1e03 Apalache NumGe ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
0fc0aad956d9b639e1a2b9e66008b2f8746f84c0 Apalache NumLt ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
f7b1b91db33e8619eff0039e37d7ca48f34f8aa8 Apalache NumLt ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
161a9a54ff3543d4733f44770b820c8f4c77178a Apalache NumLe ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
fcfe13609ceb80d9ec082f6e701180a94e9c3b70 Apalache NumLe ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
ca168b7fa9a29d2252f71d9abbb1d6f8c1170258 Apalache DefFun ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
bfaeea8b474f88dfde6e45759de48957f16f06ad Apalache DefFun ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
fd3b7993a5b4ab23531ec367ab4eb17b2afdc3fb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
ec087ea719204a14758012e0a06d8583944639dc TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
dcbd0aec5d8c69ac72c9e7a8836632bdc1ba0a3f Apalache DefFunRecursive ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
9e0d91338377215e965c47e71d1ed68c13f94819 Apalache DefFunRecursive ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
e650e41b81d7993a2e5ac8e037cb39510b04147a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
28bbae232a43987c6541b6d8b545665e68fc9329 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
453be6c29ae8c86087cfd825c5a9736206a6ed00 Apalache Def0 ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
768e0884354b61bb099fe14f5d6d48995c325247 Apalache Def0 ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
12440f22e89e0c781ed35b60e043ffb610b53f96 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
7ba96ea5ef29219a0dc884a15e10c7b5c1a1439d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
d2f9bf4069a06ab7599c42618565e61ff0300a2c Apalache Def1 ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
d10e88aa9e3930f69cd9fed3750cef1a3ea60713 Apalache Def1 ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
5e98496d1efbe61a5a6dae86d43c9b7526e94f16 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
9102822bdb030181b16acf3651497bd2cc52e8c3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
05de0a4c79932e4f13843eb3871d275c94dbd6a2 Apalache Def2 ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
78ad3449460deaa076101c9a2104cf9c5b9682df Apalache Def2 ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
256cabf620529995f54179484556406f8f6fbcbc TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
e6d639186ff048b5929b8a69ff060e8f7fd0cb6f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
a925b5b0d4a0f1777f593ad2823ee5609e5d6fc5 Apalache Def1Recursive ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
9c78881a16eb14bb597af129fce47b879c98532e Apalache Def1Recursive ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
ca310d746170e3d2b481a32d0f59d34cc780c3d0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
d9cfd396e5e1cc08d09bf7ba5c0ca03903ace31e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
b89ff633d3ae7344138b5d61159fb0c5e1899535 Apalache Extends ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
d30d358844ff68492aa1ba105e9990097f7cff6a Apalache Extends ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
5dbece7f377569549670ec6e0d1f0f4a7b603cd9 Apalache ExtendsInDifferentFolder ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
def0325d17a79f29fe6e7292332056bcaa5ea973 Apalache ExtendsInDifferentFolder ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
a931cf86d4f815759b8b8f9aebca97004a219e29 Apalache Variable ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
732cc3e1de3ded5def2cbac2dd9384e4d7da4b98 Apalache Variable ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
b59fd381bcd187f5c669238cb741b10173f64f18 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
01cf218157060d39487dfde135e7f04d19b3cc5d TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
ddc96dbc4b64e1786491945d72d2eafbac81f861 Apalache Constant ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
5b049dc45cad8234e07830bb079efff1e7e54274 Apalache Constant ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
74079cfcba562e2584c42d266515efdaea8103d8 Apalache ConstantRank1 ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
cb6df7cf849135be9bece27430ad826b5faf8dc9 Apalache ConstantRank1 ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
3ae41fd48228b11701815c5e56d9cde4fe92841d Apalache Instance ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
19318ed6d761357925fa71ee49c79852fe3f620b Apalache Instance ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
472cc747a42c1e1ff02d4fedbc8650a4d73183f7 Apalache InstanceWith ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
5967b5d6d1e91094f8fbf28a2d2ac5b8b761077e Apalache InstanceWith ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
320e17e4718865fd4736e42238b7d0b200834f33 Apalache InstanceNamed ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
37836383ea231b0245f61d422d8adcdb4077cf70 Apalache InstanceNamed ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
dc33d7145b59dcfc6c93574a3afc556430641adb Apalache InstanceNamedWith ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
35f78df623bc91adcc34286f09e7743b4f6d2233 Apalache InstanceNamedWith ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
b7434ece150ab5dc59fc60b40523e76854b45e43 Apalache InstanceInFolder ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
2f27e2211558e879424313bd8d91cbeb36f76a23 Apalache InstanceInFolder ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
6c075976b71296e9e17a460197f53b5169056400 Apalache InstanceWithInFolder ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
63b2a3ec5572443d2c434dc04f2886333319db18 Apalache InstanceWithInFolder ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
77a963609164d33cc6feb6f4861c9a7de6e6bf3c Apalache InstanceNamedInFolder ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
8c466313cfca2573ab2b7087d6599c1a31dab499 Apalache InstanceNamedInFolder ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
519618c515c707e00c5b13b42d904d8db1ed7d06 Apalache InstanceNamedWithInFolder ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
f9d6baaf3624909fb5194df123101b8014a2ef6b Apalache InstanceNamedWithInFolder ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
721ee7e0fa82ccbb59aea133fa50d9519273db4f Apalache Enabled ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
d35b8d97489727c7b8438fa34880dcecaa923f64 Apalache Enabled ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
db4e826185da6fc08da66905a8ce3d3a42d0417c Apalache Assume ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
454deffac84956b1aa11cc632a6a641a9d4b7938 Apalache Assume ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
f126a3111eba96cc1e332f7bb140a4938f399f10 Apalache AssumeNamed ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
e81d38fdb8abb1892e3886e5ec883263bd453c39 Apalache AssumeNamed ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
2a0b1ac91a696089c245734815869dd6cedb75a6 Apalache Lambda ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
adf18be2adea5151f3bfce5ddffea290864ad917 Apalache Lambda ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
126e88d97ff134a6d690dc322077cf9f962f9295 Apalache Cross2 ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
0f42dda5077937c4845fb56f52171fa9e702ade2 Apalache Cross2 ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
a1fe249d5237be21c5d6523a90b9c43f58d5e679 Apalache Cross3 ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
bf3d2cf42b8ffea9f6d9c08b3534f73ae8109b57 Apalache Cross3 ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
1d490854121bc2a145bee60955f6fdc640f015ca 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 ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
eeb794f42f682e0cd8dd6c6cc3cb03af7552df01 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 ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
09cadd2f8e9fe2c7022c1bff373a9bf4645a2852 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 ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
f7c44a43d8dcd2dca09790b3a2af924ee70c2030 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 ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
24ad79168b452dccae01828be6bbaeb7726be68d Apalache SetDiff ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
a19147603a6f206580727b7097e7ae1dc56886c5 Apalache SetDiff ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
5f84a934bed590feb7abcf7c107bbd68dc441331 Apalache SetUnion ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
6487e112981e63641bec4442a1a1597cbf8248a7 Apalache SetUnion ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
acf14392760aa2970aab49bd6508745cf6440c5d Apalache SetIntersect ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
c1057488506fcd049ae3938236e184702b763f31 Apalache SetIntersect ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
7042ff6acd610e57e331f0f560bcaca736343693 Apalache SubsetEq ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
960e44c959d91f712361864bfd689237946693f5 Apalache SubsetEq ExtendsInDifferentFolder 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
883341efb1897b496cc42548b6c913359b9e2694 Apalache IfThen ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
66ee3db8754d38e9e5d7bc17213dd241a3da90e4 Apalache IfThen ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
c1f6bf5eaf050f74e0f861e868b84496b4a33b2d Apalache IfElse ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
e960f0c14c07f3cd95879999052a27776c27ee61 Apalache IfElse ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
9e0b13a25727b17cffe645b3d016f809d460c82c Apalache Subset ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
08dda511771232186eaa23b09a687d17bc212888 Apalache Subset ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
ad7c2467320c488cf16d3102dab4a8a9d1ca4534 Apalache Domain ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
ea9ccd789d977857703fba49e6385478e98ce6b9 Apalache Domain ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
0c79bac8f6f350c9f5d5c210110524a876b726ef Apalache Union ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
3a22d22c44f5bcef89262df00035bfe6f1fb08e1 Apalache Union ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
2bdc1c3a5e9fb3a6d39ae171ee02974335336e25 Apalache Unchanged ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
93c1ad208958c9a446029aaacff502ebb6b5f9b0 Apalache Unchanged ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
62a9383f3421d160f60ad0d1ccfa18fb8d281ab6 Apalache Equivalence ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
b9bb94f1536d293a3cede2a503bb4462fc7d44d9 Apalache Equivalence ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
11ad7ac5bb32c561393f99cecc70f21390bbd3d9 Apalache SeqLen ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
09f09fda467ab498012935b514c9c6ab7c4147b4 Apalache SeqLen ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
926f6e263d44d0fcc17a4cccfc566f7505784cc0 Apalache SeqConcat ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
e55703ebf55b049563fcc5d5112713a9d0ec48df Apalache SeqConcat ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
e7a70ef1cfe672ad5f29a2e9c2ae4776f125d7e6 Apalache SeqSeq ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
1791c8201139b04ee033b05eb8f2bfac8b054990 Apalache SeqSeq ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
7f32d468b4a8aea5b0dfd45b055bebe174830f5b Apalache SeqSelectSeq ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
84b363ce78260f70335ad5a12138f9722086cc17 Apalache SeqSelectSeq ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
f7df2e85e8dcbd0cc5733f10d7fda0a36c1ad488 Apalache SeqSubSeq ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
5e8b88254b69709b07d8adf22e8713125773929c Apalache SeqSubSeq ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
f4ac08ae9b55cd65d9e49b7fb8536813f5eed057 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
08c0a51b8f4c536e89250cb443a25a549548b5da TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
88520bc3b22ba4fabb49986b6eb9e2559865d252 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
04b36442037435e774f0fa3a274507f73dcedaf4 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
cdabdd3fd41c774bd8006cede96001736c4cc2a4 TLC with reduction strategy:
  • Case Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g |-> IF u \in DomF THEN f[u] ELSE g[x]]
TlcExtendFun ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
614e9b114c2dd52a65a570b2edec8d65e24f9ecb TLC with reduction strategy:
  • Case Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g |-> IF u \in DomF THEN f[u] ELSE g[x]]
TlcExtendFun ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
4166d9da1f79e61172b87cade705a95f2c21c6f5 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
1da6a479f8c5a174b5a6a613c9a63dad7d68292a TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
4a631fa5a73cd3ba1456cc1f535901d17696877f TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
d3adce64fc9514ce47508f9a8dcee427abf141d1 TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
e66b64c8f2196f0b5dbe98e1eaaa025d74364599 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
fbaafc57f4df0a0da8a5b056497a90d2b2666448 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
94583a8ab139f4becc1bb757ffe0bc51ec3e73eb Apalache BagBagToSet ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
f10debbe66326cfb9a3d5fb7e4c58b633f4c7ef7 Apalache BagBagToSet ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
9c6f443d6cb79ef06cd8c47d2a03371be7c73e63 Apalache BagSetToBag ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
00e448d81ad905dffe8bff97ac5b2dbc39316d66 Apalache BagSetToBag ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
e8928c3fa4d85f04b8775d444077f1f8e0040cfe Apalache BagBagIn ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
7042902fd03458950a9f4b70bc29244197f8ca08 Apalache BagBagIn ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
12690bace7dcad0c9254767b18aac321ba6ff142 Apalache BagAddBag ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
cac992684725f58594fd74a33865f8728ff00fa6 Apalache BagAddBag ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
6d0dbf0ca3fc6349a71420af7686729a39b6c2f2 Apalache BagBagSub ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
cdffbe9ae0b14a121a45cd7f75cb1562dc455b6f Apalache BagBagSub ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
c5f2766d6ffade35db3f399956d9c90ed2d906f2 Apalache BagCopiesIn ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
9ced19d1af49eb6dac4cbeea75afe0dbb0d0e2b6 Apalache BagCopiesIn ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
e18374da31f81be08073e52771cbdea7721639af Apalache BagSubsetEqBag ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
cbbafed0ec550cbb75f76684b5d7b0761021e09e Apalache BagSubsetEqBag ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
08c9902b96862b8713b8d1a6cc805d8b2bdf290c Apalache BagBagUnion ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
a43d5fa565d5ebba0976a01301ce812a96d54232 Apalache BagBagUnion ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
ee0ffe868cfe85b5183971cc6dce5f78b3524f11 Apalache BagBagCardinality ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
27a6daedde229a1e2df220d2bac8902708b422d6 Apalache BagBagCardinality ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
8a1576d2ad586796e36a3f54c48fed12de726091 Apalache BagBagOfAll ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
41f1d57a5827aafa450a5316058885ecc87e1ce7 Apalache BagBagOfAll ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
bedefa37ff788e5340843499adcac42d5855487b TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
22bfc44805bdc1643f833e22677744232a6acaca TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
a832f2b03177926c5c5d04292843661b9269eff0 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 ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
4c45b01dfeec021c6a0995d85b8259dd930a0e0b 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 ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
e0aa14704aba3628dbf6282dbabe96d9729819aa Apalache FiniteSetsCardinality ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
883963eab7d9814a35569c6ed8844362221ae03c Apalache FiniteSetsCardinality ExtendsInDifferentFolder 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
1e9448cb14e0f3b3470840d4bbff45bd7642a65d Apalache SeqTail ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
a89e7e9bacb6cb05eaec674bef17d45c0f3f55c1 Apalache SeqTail ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
dfa116825a5529a249f53b7e5234376a6b2cc138 Apalache SeqAppend ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
47e2fa9978cfa07ddd0acf701e18e8bc0d457c74 Apalache SeqAppend ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model