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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
e977357801c613c33c2260c0031104e82231b0ee Apalache And InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
44d422cbcaf42adb91217e4f833b46222170a9dd Apalache And InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
9cc93938d7081cc2082dac686df77f085b994aac TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
c534a7ee17103a32e34567f5c499abb8109abecd TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
2a689859877ab0fd831df9747d21e28f6daaae64 Apalache Imply InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
a1d1b3b7cd308c04fa5c425005bacc6fbcb51580 Apalache Imply InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
cf3ef4446dd5c109a363795824bb22d2d07434de Apalache Not InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
1b36f09e34b21a8a37ac19bff458b899994f52c5 Apalache Not InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
fbfa4b730c2937ddfe0fab827aa288ba8cd3d376 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
cc8312789ee2057b3393eb9d108797382cb7c49d TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
e697e9ebe7c8ae356abdba9edb6eb05ff8a09d4c TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
5a45f0039ce4bf479e7e6a14d142bada9b8a6ab8 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
fda3749a994388025e40c8d85132db08014bc463 Apalache AndProp InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
8c730279fd511c38e03a55e6ba1887e9b29378d2 Apalache AndProp InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
ecad16289a759e3e804ed52c411bd6b752c1b74d Apalache Boxed InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
64c8543668825330d61e3bff76523ca33385dce3 Apalache Boxed InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
16b25bb72035b1e06c089134d54e9edbc97e91de Apalache Eq InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
deb683b4c4656d12c109dde2131a34593d6daf2e Apalache Eq InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
30ecb7ad78c4d2d29122122398405b7e01ed5618 Apalache Ne InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
23f39a2896fadc8ca48d546c12b9bdbf20d1bcae Apalache Ne InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
01fa4943cf5bb59279b536035a68ae1ed92466ce Apalache Let InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
2b4007bc0f6632bb0940d49914ed52670b08c087 Apalache Let InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
01dd27251c59b83acec672934fc3fca73c34b43d Apalache Set0 InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
8a31607dfaa337e8f006a16d4da88f2b4a9372ea Apalache Set0 InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
f98ff0ffef581423112d19d0ea171c8bb7483ab0 Apalache Set1 InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
36dd8c847e8b8a6f51fc614b4340d6e88cfc323d Apalache Set1 InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
22f936e441d86b9ba0466a01d65023de46d1de61 Apalache Set2 InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
ff3d83591206124570435bd44685880edcad5a54 Apalache Set2 InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
ae24fce5a454a78e1d3fab9fa9724bcc36a803ae Apalache Fun InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
ffd9fa00d92e701b4272cde8e1724de0d3ffa14c Apalache Fun InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
40459e2b6529623897d4f2f0befa7c432ccff5bc Apalache In InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
e0ffa75878b980d75ed36dd172bf23708642e64b Apalache In InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
f0576f68bdd4847297887ee569f6ef7f1f0870bb Apalache NotIn InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
c4841828e9ad98ff87f171aa3a6570b5a97f6d4b Apalache NotIn InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
61df5851a5b61ef31271390b72c750d182f491e9 Apalache Exists InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
684a2ff71e741d2d04dd5d091b74a49800e7c03d Apalache Exists InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
c506f5de1f0033293541b771159d143347e079fa Apalache Forall InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
5995266c1bb718f6ffe2ab95183f24b256984ad6 Apalache Forall InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
a02b3fec904d9f47911944605feda9b83795cf45 Apalache Choose InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
ee1ca11fc6fede3870c5076fe0f1ab9a0a662416 Apalache Choose InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
8b38d8f087a39543a4fb8727fdf00517a74ef7c7 Apalache Record InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
ba7692f92ed91831b42627b8530f0b0b67244aae Apalache Record InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
a2079af3156cce231276a263ebc687f78940913e Apalache Tuple InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
93d80ba6959dca2c998868bb7b3be4dba72d9fc7 Apalache Tuple InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
faaf35f248dcd55c4c0d86557e0f95c8cbaa7e4b Apalache FunApp InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
9e2c204ba779075ab76b068363735b5e6e571a8b Apalache FunApp InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
734bc806926ca9766c4f0c8452a7a1f3e0dddb38 Apalache Except0 InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
eef5213ac414e9fe85aacb86b28355df69aa5fe3 Apalache Except0 InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
d9270d5f45079c7adc9e47b3365cf785e0c556ef Apalache Except1Fun InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
a1788f13815e6062faebb1105d0c0a907b5143b0 Apalache Except1Fun InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
5e0d75c3ded7abc507d6e23493328d88d523d132 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
f9384ccb43a4d6b54b0e63497fe4a21c7cb56bdf TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
f7caff23f7453843e6f0eb0ca35cbd06d232bf61 Apalache Except1Rec InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
6b0d6e228bdb590460d54fd5519e21c8aeb3c194 Apalache Except1Rec InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
26dd69598d6e004973c8d0046e1f9f7323b3cd34 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
a3544100b80feae1bd122b9a2286c9d5f4712304 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
910c09175c41efa3499b2d304455c7616921bbbb Apalache Except2Fun InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
e9238eb624f92c2d94cd06bdc5a0b21f3fa1004f Apalache Except2Fun InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
f076a8664bbeb3fa5566bda76da4ea80e7c535e0 Apalache Except2FunTuple InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
cae71406d028e1bb73458ff4a673eae0299ca0d4 Apalache Except2FunTuple InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
4f37a665fb71b6842c18a59fc05d418af06c1fc2 Apalache Prime InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
ef6d3baa65322e5d633caa22cf3f6268c57f4ce3 Apalache Prime InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
58dbfc9c36fdb96d82c76c4b58663f25d610effd Apalache NumUnaryMinus InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
be57d51c436701e2797c3e2b4dbf68261bbca77c Apalache NumUnaryMinus InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
53e0a9a500c8d1613ee0767d1c55deb29e36c68c Apalache NumPlus InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
7e900bb0fc70705a296b08ba4da3f6384ddcd435 Apalache NumPlus InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
415816eaf7f7f01edc535a98ac57121c44513f08 Apalache NumMinus InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
2f5d5fb03cbf3ddad8f9451598a629b35a37326f Apalache NumMinus InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
ae862ed9367251d9258b7993dd3e2d34a76940a2 Apalache NumMul InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
e11de3d86108d3a752f3b35135e57de64d2005f1 Apalache NumMul InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
e9c0fcc40c53d275e9c6639d86703009b6713021 Apalache NumDiv InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
06a1473bb6f06243b10b64f4654a89f8086936e9 Apalache NumDiv InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
c574b03d2a219b92d5002cc21b32f3b697a37ca7 Apalache NumMod InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
754afe765d4303163b6b77c9ee14d90e63ac6b2c Apalache NumMod InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
9419cf663657d65dd1fc45085d392bd8ae468796 Apalache NumPow InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
337fe26e5ec30e48bd902d7d7cb96565e30ba763 Apalache NumPow InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
f002fc31445ad84efa4c7bb49f1ec86b05bf39f9 Apalache NumGt InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
6496cf6aaeb925ae3917feb0a60630a153fcd4e8 Apalache NumGt InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
e346654b1d45d4fb5d59cbf9213ff9d78911f6bf Apalache NumGe InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
8f4ac659a260eace8bac0370490b6ef7d8815fd7 Apalache NumGe InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
1b7e0cd5e6f9a76475949d3e4f44a55cfc1754f0 Apalache NumLt InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
16b0bab31426dff539316925a90809bd2858680f Apalache NumLt InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
2d3e6a1055afda6d137b62f15a1631747d6ef4a0 Apalache NumLe InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
e75ac19fb1a29d7dc28a4ffbac22d6261f530ace Apalache NumLe InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
b87c574d65e83e44af95f8c95d5721cfe97f8ae3 Apalache DefFun InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
587f7041a43d9190807dbf49dfe4ac27c0299280 Apalache DefFun InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
e67bc14b32f7385e36b769cc544ca325a0fe10e2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
fe440ebf5df653ec39f4dad6026ee7e4bb550372 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
2059d94c0308d9ad8fe8a1db5a9b3c7c2d9dba20 Apalache DefFunRecursive InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
8ea42d1ae6ff6c9e75f56b027a5d9bddc80cf760 Apalache DefFunRecursive InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
4a3164409ca62ab8f808638588657fb6e1020069 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
6cdbaf32bd9c26581801e22c54aee1653c0859ed TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
9d89f629b61db9b82f407aed3dd28a42e0a7d7fd Apalache Def0 InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
f3c21630b7a93001b69997fc8349e644b4b7cd75 Apalache Def0 InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
dd06d85041c0663442ff0ee8eb07733c60bdb2c6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
35b8e949bdafb041d5238c6c112ffcd83184f202 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
4808f4ea12b31c5c8406be74e8abb60d6a19a5fa Apalache Def1 InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
447fdfd9ff74c384d0aa678fa9746dcf57ca50b7 Apalache Def1 InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
50985dec2d392bdb8f91d4c7cba4f157aeefe929 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
97b4f801b90e46df5977ab3f599ba3b2eb2dd142 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
00ac9e72d4e134034bb8abe36fe5ff980bd43248 Apalache Def2 InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
226c89d57443f61c6f5fca59812e2962356e5b13 Apalache Def2 InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
2ca777b2f28e5249cd0eddb16a16570c3f0f8d11 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
4fe7ee846b59470b7b0772e246c761d01bc8df78 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
29017165b926c1a20efb7edc01b8f495a02e4d62 Apalache Def1Recursive InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
e2f93ca905ec16d9a7bed7dc4dd7b96792ee0973 Apalache Def1Recursive InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
bb6646bc7f16c052e8e115fcbf7c16d495065543 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
7731e6382f59e572332f4dc4d82448491b43b5d1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
ff85237e6132478d33246ccd9e6abbbd04f8b73f Apalache Extends InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
bf142383dfd348681b7c68e3188ed2035502663d Apalache Extends InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
318288b9bc398066e1db56e1456cf9561decdb3e Apalache ExtendsInDifferentFolder InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
e5021e7aef29a59cf71dc8621f310eaf4429c617 Apalache ExtendsInDifferentFolder InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
02e5c25f6244480783782a537c4e89c2d7ed99af Apalache Variable InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
03454f5b5e4b0eb833f2a163dfe23420a92294ab Apalache Variable InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
698295e145c433905ec1430f8c3983490ece513f TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
7ca7e5df998a70a45d5b57b0b102beb8d9f9305e TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
166dcebeb15b2196c06555173741cb461ca9f437 Apalache Constant InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
dc16ebc19b928f20b82c2704a0574417d4661526 Apalache Constant InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
a7405257f50f166279bb6239e3671a9391ee265f Apalache ConstantRank1 InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
3882c51886831ccb717106aa28340f267628354c Apalache ConstantRank1 InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
727c5ff8be3bd2cf826df4ac88e80fe61d5cf7d6 Apalache Instance InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
7109912cfe5535619d55d15ad6b7695ef7ef227b Apalache Instance InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
3d17ac8f5dced8b699470719136562d8e6b6f074 Apalache InstanceWith InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
699ab5ff088135aff7746a29a1c14d270e15156e Apalache InstanceWith InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
c3d002fb5a149cc9fc101ae6a3bbb9560309d655 Apalache InstanceNamed InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
890601e708eda2bfdd530dc136033c52fdf1afcf Apalache InstanceNamed InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
0e45582814ca713b9ed427bd131aa7f4afe634c3 Apalache InstanceNamedWith InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
fa8c6637c788553627ea11fa08aae501aa36f3e9 Apalache InstanceNamedWith InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
21a0a93ff52c252946bf72152ee10551a372805c Apalache InstanceInFolder InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
c976046066de3e84b06a7b9e38d0ceeb459f99b1 Apalache InstanceInFolder InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
9ea95d34c83753cbd9af3a15e3ffa36370ab3f50 Apalache InstanceWithInFolder InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
c246b4a32611b5d2f8d1330cbc48fe7ce55af0d1 Apalache InstanceWithInFolder InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
b15824fa95cbd4157bdf46a8b2d2e2085bd40a65 Apalache InstanceNamedInFolder InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
61d463c2a246bbd9af2cbf0810452f0d9db2d15a Apalache InstanceNamedInFolder InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
5dfec5edeb753f82edebf673c2c0941ae063da07 Apalache InstanceNamedWithInFolder InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
e0892b18cf2fa1c2ed74d2ab1180cb02ad753f71 Apalache InstanceNamedWithInFolder InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
86a1fcd98f630ec5d19f7e23cd0e63285efa7b7a Apalache Enabled InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
fae4a06b8c61705587dd2b599012209ed64ec9c7 Apalache Enabled InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
2bc8c9e1117ba8c5ab9af14973e0d7c3ec9b3da8 Apalache Assume InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
52b956f83ec60fad9ebf1544aa6fe88c92287bc9 Apalache Assume InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
71f522c07acfa14608d3eb8960589f17be86bc8f Apalache AssumeNamed InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
33b6f1fd1d929d4a4f2888cae4d20dcf3320318a Apalache AssumeNamed InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
0390fd122a523087ba03338d7dbe1facf4162da9 Apalache Lambda InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
5b68d2bc2d3c37e4619667aa75d4395b15ea0076 Apalache Lambda InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
cb9090679fec0719d3d7946bc39d6255c629a6e1 Apalache Cross2 InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
03eeae84adeef13b0cbb6f0db99105a6f7ff3294 Apalache Cross2 InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
d38b538a7018cfa2c4bd9eeb59aa7bfab9bd9442 Apalache Cross3 InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
5a828a1b1807831054d9077f9948dc8308b2145b Apalache Cross3 InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
b8ff8388586434c2ba1b58dbd6092cd289435ad0 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 InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
292a89d4a3b95169a709e4d128d30c3829c39dd0 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 InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
42896e44808f007b863fdf56171b5d6112994c02 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 InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
4cff20dfc3dbaf603adce3a7bcf5cf799af2121c 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 InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
cc24f1c3a81fc9cf5b87de5fb1e08c993c1b5ac9 Apalache SetDiff InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
e38ac06842eb01b1dd0ba32879b4fa1c1b73cbfc Apalache SetDiff InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
8bd1c89a49d2ab517545b8c6d547b23c83acf919 Apalache SetUnion InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
e3ab56bd16764b49bff222eb7904fc8f7197f0b7 Apalache SetUnion InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
9509b98931df088ddc208adb8b301428f41d36b3 Apalache SetIntersect InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
8a21acc8e5ea4f1598de292928eb98c1d68cb50e Apalache SetIntersect InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
c2e57f3894f2817eac3d0edf1d5fd4f3c3863338 Apalache SubsetEq InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
4c03b2c23eef94c4c79a00c1d400a38b97cc9894 Apalache SubsetEq InstanceWithInFolder 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
0b56b008a168d2711996c45557d3a02008ea9769 Apalache IfThen InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
f170aab80ac985216d5138f979f98cfc3b2e4ce9 Apalache IfThen InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
e2477718868a4c48752e9d634575ea50eae04c6f Apalache IfElse InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
9ceba54d463c445987a318d4f61a2afce6c6267f Apalache IfElse InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
196802741f3598efc4c5d9e39a65b971ab87d4e9 Apalache Subset InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
4270016eb7a753d8996380d9d129386ef84185ba Apalache Subset InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
4836934049d7441262d004ec7f441612f8524ac2 Apalache Domain InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
3deff240ba8712fdac205609bd3d98369f6b1f88 Apalache Domain InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
54871aa4f89e16c1d5a4728db95e150e25fc8365 Apalache Union InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
3e8098909d4ae53935fa1b2fe3cf18a780e9739d Apalache Union InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
4ce61b79cc6c2c979a4bca8dfec08ee82c4761c7 Apalache Unchanged InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
c2f3dc394d837e6bb268251f0958e5c75dac0416 Apalache Unchanged InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
e3644546586c5f7d0d9748546b516e95afcb9418 Apalache Equivalence InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
3a636935ab2dc4295b37399e1cdc9aa02f2188bc Apalache Equivalence InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
094c3542a66826c1fd7562156d94267e7521f87d Apalache SeqLen InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
6131115e7eee92fd7ebd82339372d0ba2a1d4fc3 Apalache SeqLen InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
1bc15cfc9585256dff8eedb174debd8ece4b0bb4 Apalache SeqConcat InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
cd150a21acc4f1a48f4b64ae4a87be7e55b0f16e Apalache SeqConcat InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
80af51657109e782610aeffd49c8b9e3768f1230 Apalache SeqSeq InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
5ed7db65dcf1e1ee94770bd3797533c359305034 Apalache SeqSeq InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
47a2c7f45e8f2b398f24056508f7ec656cf04462 Apalache SeqSelectSeq InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
a7028570c51bdd16d27c92c193cfc85f884a443d Apalache SeqSelectSeq InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
c050113ad09d5c03ef19ca624f5664608a8c0535 Apalache SeqSubSeq InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
3d5999c7c490edf147106557a7072c9c08a41f83 Apalache SeqSubSeq InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
ba97fa5caf801873aa1cfe4016ee345a5f7d0df6 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 InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
67580b379368653d2be3e1f2a4c4e6696787992d 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 InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
437e189654a7692f8ac1abb97c52c1a9c9f251e9 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
7f9f0a53834a36d5f93256569eb588e5464d2acc TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
09c18a7a7a7276fafd28dd63e5f1083370ab208a 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 InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
b719191bc63d70970bd5a82dea85678dec2f0077 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 InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
9e7bb06fe8924d4f66bac71da122551adaa14e24 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
bc554efff5e0b79ab22290f8890a19275d93a689 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
b008436b0e101364d050c94bf436822dccef3510 TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
5d4402ccc513f0931d408efe2ee74ac59890e540 TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
7744d63b203404b1b6510d930d5789b36bb95f52 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
b09dae27529cf84e17a23639ceea1d6d862ca1a4 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
fadd4fabfc78c5974e2a4862a40c620e848d21f0 Apalache BagBagToSet InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
c161b75cbb28035de43487935d7f6ff69c8f7807 Apalache BagBagToSet InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
e9813d95444dcf2cb4f86ab6c48624b4380877da Apalache BagSetToBag InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
a00c6821d6ab9e095d9a691c13169700035ca703 Apalache BagSetToBag InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
8098fcb706ffce8ed778b04c65db8dcf302286b1 Apalache BagBagIn InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
ad48493f829a921eeb70c4c0de515aa6e8c5e997 Apalache BagBagIn InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
2ddb0f3f47f3920a1c9e5fe84d2d0f3247d65d39 Apalache BagAddBag InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
c18fd335487440db32ba9e47d38c6ba89278c11f Apalache BagAddBag InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
1c2c5562a0c3dc17efb63bf8785dba6dade18744 Apalache BagBagSub InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
6c77cdd9e7163cfdefe71786f8a1a77324f42a29 Apalache BagBagSub InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
9dd337971dcd2e24043eb8d57715bd780f8d0cb4 Apalache BagCopiesIn InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
a8c38a330cff997f16d79ccce2df5b29824a3d23 Apalache BagCopiesIn InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
f6c6cceae9ed2fad66620169a15c42c2581c4c6e Apalache BagSubsetEqBag InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
253815d94aee6b127e2af11480acde4988b0bdf4 Apalache BagSubsetEqBag InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
8ab7b2458b5f0d6589118494ef2fd160afab5cd2 Apalache BagBagUnion InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
34e4dada5c6b93edf0665db251fcb9af0953ab1a Apalache BagBagUnion InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
eefbccda5373e642f96224ad4603004be60a8d83 Apalache BagBagCardinality InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
d7f716469c39d76c0f535eeabe0f152cb1f688ac Apalache BagBagCardinality InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
8d00fffdd6072eb5ed4aac11caaba3c7c447eb10 Apalache BagBagOfAll InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
f7e82bb57503757c209ea3bc43d77b98c953251c Apalache BagBagOfAll InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
6cb0188531b1a7bcb2ef9d82ee7a49df003bc12a TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
6d5fda2471532ec7ed7828bdfa5b7ba06bb90572 TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
ff090ec5e8ec5770500c6fc411e51ddbca0af658 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 InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
24a217095e031b41aa8efb625d81040c5d0031e4 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 InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
ed28556fa3138cbe3f86ffe1662cc3a5ca58e85e Apalache FiniteSetsCardinality InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
b6e611c6eb46a973de3ae7974e54d8c585ec987f Apalache FiniteSetsCardinality InstanceWithInFolder 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
39177e1f1084afcbf1e1051cae7e45e4fc9233fe Apalache SeqTail InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
57c735d367a6973d9de267c6693d179dc4df4e58 Apalache SeqTail InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
67856c0703e0ab2fc641adada5880154e0b9b1a3 Apalache SeqAppend InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
fee0a51119e964f102714e99dc59959b7242eb5d Apalache SeqAppend InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model