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 feature combinations: -workers auto
  • SYMMETRY tests: -workers auto

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
e7109ae910dd5b45fc53451a2f45cd0920de61c2 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Ne OneLineComment True Passed
  • Model Under Test
  • Equivalent Model
987e80d40c5b364fe0cabadb0155f397e6a43dfd TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Ne OneLineComment False Passed
  • Model Under Test
  • Equivalent Model
56cdcd0b42d3b7d1ac0612e545540d587dbaa008 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Ne MultiLineComment True Passed
  • Model Under Test
  • Equivalent Model
5aeed97adbf81a3eec7622c45723554ca8fefdfd TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Ne MultiLineComment False Passed
  • Model Under Test
  • Equivalent Model
2f34980954083ab6f7f2276c3799ea4a5c78de73 Apalache Ne BoolTrue True Passed
  • Model Under Test
  • Equivalent Model
865346b17a95db2dda7ca9850eff92eb39018309 Apalache Ne BoolTrue False Passed
  • Model Under Test
  • Equivalent Model
0f9f2a311ddaecf436a57b8e5747d41a0acd832b Apalache Ne BoolFalse True Passed
  • Model Under Test
  • Equivalent Model
6204ea6f74f4e5cc00990985df20f5b74d986fd2 Apalache Ne BoolFalse False Passed
  • Model Under Test
  • Equivalent Model
774b53be177e11552e3ab31edddaa498e3918a98 Apalache Ne BoolSet True Passed
  • Model Under Test
  • Equivalent Model
58314ac19aed9340a960642f65d5d195b0fba64c Apalache Ne BoolSet False Passed
  • Model Under Test
  • Equivalent Model
3e1fc72bf797ae10a67492b2f3be7c68ab292d12 Apalache Ne And True Passed
  • Model Under Test
  • Equivalent Model
717721b88ff823ae158a03239acf2add5c8649a5 Apalache Ne And False Passed
  • Model Under Test
  • Equivalent Model
ea7192d813e7231eed323bfd276d724182e59cde TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Ne AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
00415bb28d3e52a00629a8accfa1a42bf79d8719 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Ne AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
1f60104deb6ce7e40bc2d9c884423fbe864a1e31 Apalache Ne Imply True Passed
  • Model Under Test
  • Equivalent Model
f7cd3466b3c7cea325630804b1feed703ab213f5 Apalache Ne Imply False Passed
  • Model Under Test
  • Equivalent Model
9e66e99317be5d9ae88e96ec4f22696c7b784d3e Apalache Ne Not True Passed
  • Model Under Test
  • Equivalent Model
95f55f66cff664863595b3e3bb3ebd26c499685d Apalache Ne Not False Passed
  • Model Under Test
  • Equivalent Model
fa98a78b209227ba62df4ab92582d8037c58388a TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Ne Or True Passed
  • Model Under Test
  • Equivalent Model
add29db676ad1589af66407a8212016edcbfd555 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Ne Or False Passed
  • Model Under Test
  • Equivalent Model
c23ae89b9ebae83ba6aa3036a30c018f92b30b8f TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Ne OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
8c82e59b35522b2aab1f8eedf5fdbdc3b6ca29d7 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Ne OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
18600d469ce3e8c7129880d504486fb727f243c7 Apalache Ne Eq True Passed
  • Model Under Test
  • Equivalent Model
784dac58080a193be713b0cfa2cc67112e1560c4 Apalache Ne Eq False Passed
  • Model Under Test
  • Equivalent Model
522f16adb8cb89a1ac6db4609c0d26145bc2cd7e Apalache Ne Ne True Passed
  • Model Under Test
  • Equivalent Model
07733a7477313a9cf7a494eb5ded5d270f141290 Apalache Ne Ne False Passed
  • Model Under Test
  • Equivalent Model
743d8048b33be94f69826b2cfe0f5ce0493f1cda Apalache Ne Let True Passed
  • Model Under Test
  • Equivalent Model
7a6847241cdbef258412b0d0eebd661decac634a Apalache Ne Let False Passed
  • Model Under Test
  • Equivalent Model
0b25a15c5d4f00ddd0a243e077963ced452bc88c Apalache Ne SetEmpty True Passed
  • Model Under Test
  • Equivalent Model
7edd74719335669221de709ba8771163e84794d5 Apalache Ne SetEmpty False Passed
  • Model Under Test
  • Equivalent Model
2356ed16cbed5e34073e7ccd31557c01ced73a35 Apalache Ne Set0 True Passed
  • Model Under Test
  • Equivalent Model
7e0fa81d489891f1fa557177a7c636f6aef09987 Apalache Ne Set0 False Passed
  • Model Under Test
  • Equivalent Model
a8b8ce929472dce1b538a01ab78ccc83e19bef60 Apalache Ne Set1 True Passed
  • Model Under Test
  • Equivalent Model
af74f6ed35a011d700cfccc8bfb1d02a497163f7 Apalache Ne Set1 False Passed
  • Model Under Test
  • Equivalent Model
5538b6f0beb7d412ab09db158597fb2aa56a16ae Apalache Ne Set2 True Passed
  • Model Under Test
  • Equivalent Model
9807923866f6ffeb28a8a724d6e1d4d703656488 Apalache Ne Set2 False Passed
  • Model Under Test
  • Equivalent Model
77d35058e256d3e856b2d4ed9cfeb38a260a1976 Apalache Ne Fun True Passed
  • Model Under Test
  • Equivalent Model
520569c45e2fa865eb07fd484140954db87896eb Apalache Ne Fun False Passed
  • Model Under Test
  • Equivalent Model
a4a4c5af03db6cbc0492d253fd866d453b77f3a6 Apalache Ne In True Passed
  • Model Under Test
  • Equivalent Model
30650ace5d22e82c512662f715bed398512d4adc Apalache Ne In False Passed
  • Model Under Test
  • Equivalent Model
c96fb7146c64a51e3921f4efc81a7ed30aea3c31 Apalache Ne NotIn True Passed
  • Model Under Test
  • Equivalent Model
340e7e9cb60e3556cb0bb3591232ef6d20397eac Apalache Ne NotIn False Passed
  • Model Under Test
  • Equivalent Model
42ff11476ac9ee3ac267f1ec0b3d2edbf3ec7a70 Apalache Ne Exists True Passed
  • Model Under Test
  • Equivalent Model
15f809673c284044c5022d6470af3c14198da8ec Apalache Ne Exists False Passed
  • Model Under Test
  • Equivalent Model
f081c6f2f05b1365cdd382122f779c2ee1d25a61 Apalache Ne Forall True Passed
  • Model Under Test
  • Equivalent Model
fb1cf6abd5375323a1459ea01ac8ddf158ddffc4 Apalache Ne Forall False Passed
  • Model Under Test
  • Equivalent Model
d27c02796e8d0ca1c31bf26452c8282ab2a44a70 Apalache Ne Choose True Passed
  • Model Under Test
  • Equivalent Model
879757d98aeb03c8cb7b2e0e1d29971bbdd637f9 Apalache Ne Choose False Passed
  • Model Under Test
  • Equivalent Model
9422f04df46f9e735cbebcddecafbe96fdab0fee Apalache Ne Record True Passed
  • Model Under Test
  • Equivalent Model
eebe51dcd3973e5afb0734aa3ef09f298ea395db Apalache Ne Record False Passed
  • Model Under Test
  • Equivalent Model
69dc4ac7185f6150e4ef0bb80fda02478e812518 Apalache Ne Tuple True Passed
  • Model Under Test
  • Equivalent Model
08bac4e0d928dc8ba052d443794ac4fd9968f354 Apalache Ne Tuple False Passed
  • Model Under Test
  • Equivalent Model
ff8264c8788b987d8ceeae5c9fe674c2b0eadcee Apalache Ne TupleEmpty True Passed
  • Model Under Test
  • Equivalent Model
98ce93f6470fcd30f6e3884132d097d5db2d22bc Apalache Ne TupleEmpty False Passed
  • Model Under Test
  • Equivalent Model
9de6f6043e944227ec5db202ef34e6ef06f2c4d8 Apalache Ne FunApp True Passed
  • Model Under Test
  • Equivalent Model
1cfd4cf6aee16fb39c2a4c12f41ae225820a4d8c Apalache Ne FunApp False Passed
  • Model Under Test
  • Equivalent Model
129f150b3232c70b700710f8a12f4aa64d0bfcb6 Apalache Ne Prime True Passed
  • Model Under Test
  • Equivalent Model
e785733c086bc4c483c8a13ca948ae52884f7a90 Apalache Ne Prime False Passed
  • Model Under Test
  • Equivalent Model
d1ef23301e83bd53ae53c4591d291d70f10b82fc Apalache Ne NumZero True Passed
  • Model Under Test
  • Equivalent Model
56c5b03431c61c72e70866fb2bbf44dd50d371ae Apalache Ne NumZero False Passed
  • Model Under Test
  • Equivalent Model
70be87046f62b5bb579d0aed86a9b65c61dee184 Apalache Ne NumOne True Passed
  • Model Under Test
  • Equivalent Model
10cd5885b6466532f49391f34694816bcb6fcb57 Apalache Ne NumOne False Passed
  • Model Under Test
  • Equivalent Model
741d0f2e3c9d7e05825860dd8a0fe33f1c53d1bb Apalache Ne NumMaxInt True Passed
  • Model Under Test
  • Equivalent Model
816bc804dd0e397594e7f182b3421e814096461a Apalache Ne NumMaxInt False Passed
  • Model Under Test
  • Equivalent Model
f0c4ce82125d8d605c0712fb54b3c94494d2986c Apalache Ne NumUnaryMinus True Passed
  • Model Under Test
  • Equivalent Model
b1d419074491962a2889846d34d0b48ad18ac749 Apalache Ne NumUnaryMinus False Passed
  • Model Under Test
  • Equivalent Model
90a3081d76a1621090056895be27bbf7269b9f6c Apalache Ne NumPlus True Passed
  • Model Under Test
  • Equivalent Model
e1e6188ef72cf1aac1079ee71674d2eada1dda21 Apalache Ne NumPlus False Passed
  • Model Under Test
  • Equivalent Model
5dd1d0f59bc967d91f488b8a3f68cb209093fccb Apalache Ne NumMinus True Passed
  • Model Under Test
  • Equivalent Model
fb4adf120868f0a35f614fe61e4168b1f3410b58 Apalache Ne NumMinus False Passed
  • Model Under Test
  • Equivalent Model
7230aa6ec042fcb7e92a657cbf80ddace667a8a8 Apalache Ne NumMul True Passed
  • Model Under Test
  • Equivalent Model
ad32eab86e32c73eee09d46852e4ea3138bf046d Apalache Ne NumMul False Passed
  • Model Under Test
  • Equivalent Model
b45c1928355b7f99ea37cc5d41ab63ae4136927d Apalache Ne NumDiv True Passed
  • Model Under Test
  • Equivalent Model
014e86c7f6be3c33491e971ff4f1c2a7df601277 Apalache Ne NumDiv False Passed
  • Model Under Test
  • Equivalent Model
84eef8ad07ebbd4491f9e19e72f6bfa8736a4fc0 Apalache Ne NumMod True Passed
  • Model Under Test
  • Equivalent Model
f85228084018c3b2f0395252cc5d1c9d6ab64479 Apalache Ne NumMod False Passed
  • Model Under Test
  • Equivalent Model
4998af75adfc149d4b36f5c877546c703fbc3ed6 Apalache Ne NumPow True Passed
  • Model Under Test
  • Equivalent Model
d74bc4ef096215098faa12c9c8a7777df6fe2cd2 Apalache Ne NumPow False Passed
  • Model Under Test
  • Equivalent Model
61aa5898380bf1666e47dd2ecb9ae2f6ddd31da9 Apalache Ne NumGt True Passed
  • Model Under Test
  • Equivalent Model
939738a13531b27d8227ca6df04e15c10506b249 Apalache Ne NumGt False Passed
  • Model Under Test
  • Equivalent Model
07c085dec75e167d78318ddfe1b7bb285fd35c24 Apalache Ne NumGe True Passed
  • Model Under Test
  • Equivalent Model
904ae4355b6538d880d7ce75817b13036f2da01f Apalache Ne NumGe False Passed
  • Model Under Test
  • Equivalent Model
a8026af34acd8bb277677227918be077e2469e33 Apalache Ne NumLt True Passed
  • Model Under Test
  • Equivalent Model
0f2f5e0fcf89024e193b5f6367dbf2c490ebc016 Apalache Ne NumLt False Passed
  • Model Under Test
  • Equivalent Model
1fa7044fd3adcaf3ee0241b98b196b762522c5a2 Apalache Ne NumLe True Passed
  • Model Under Test
  • Equivalent Model
8502029eebcbe44c6a2271557e4440f347d5bd89 Apalache Ne NumLe False Passed
  • Model Under Test
  • Equivalent Model
4a7602354d41d5a85ef6eb572ae639fae72fbf9e Apalache Ne DefFun True Passed
  • Model Under Test
  • Equivalent Model
44c6f0f0a79fff1b9c5ecbe12962769b6be6ca2a Apalache Ne DefFun False Passed
  • Model Under Test
  • Equivalent Model
b7d834a1bd892a11ec595b00a23776da646ca1cb TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Ne LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
e5f5812b01b4a846a31f70742e677fc0e102b0a5 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Ne LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
da924680287b9fc2c32facea7af237a13d8e50b3 Apalache Ne DefFunRecursive True Passed
  • Model Under Test
  • Equivalent Model
816242a6736d065a696bc1c1c5e47d539e96e231 Apalache Ne DefFunRecursive False Passed
  • Model Under Test
  • Equivalent Model
4e78dd603edc89145d68a25999a3068d9c914ce8 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Ne LetDefFunRecursive True Passed
  • Model Under Test
  • Equivalent Model
94ae07e892d66ea5432a0d31a88c7c67c6506088 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Ne LetDefFunRecursive False Passed
  • Model Under Test
  • Equivalent Model
146a7b4ee5372d79f81b28f1897cb9ba9599f8fb Apalache Ne Def0 True Passed
  • Model Under Test
  • Equivalent Model
ad5d1eaa4f335cf4ad69ab2dbfb676120a4d89f4 Apalache Ne Def0 False Passed
  • Model Under Test
  • Equivalent Model
b3af95c5f4bf104b4224a7d9206a0dbdb5a03c1e TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Ne LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
a9295de3697348fa931581b5463eaad11f18c07b TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Ne LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
f79c6e77fa86fb2f1b8d1bcb88fd260d559982ad Apalache Ne Def1 True Passed
  • Model Under Test
  • Equivalent Model
c2767441bad3fce0366e175f3b9911dd76ab680f Apalache Ne Def1 False Passed
  • Model Under Test
  • Equivalent Model
335490b55fb82f65ab888185140b6850ca420f26 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Ne LetDef1 True Passed
  • Model Under Test
  • Equivalent Model
e8d3c816c2b64ee2f9b24de4c9847c46af0646d9 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Ne LetDef1 False Passed
  • Model Under Test
  • Equivalent Model
9534e30ec7a02a3fbde7f99dbf0a1067ce6b5e25 Apalache Ne Def2 True Passed
  • Model Under Test
  • Equivalent Model
b281c41573a8d0adcd5bc6ebbefdc446da9bb115 Apalache Ne Def2 False Passed
  • Model Under Test
  • Equivalent Model
770b03dbfe0ed67350aeee741d4338cb26d8c4bf TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Ne LetDef2 True Passed
  • Model Under Test
  • Equivalent Model
fa56f796c91e6895dd8a78195717da8c5557b43f TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Ne LetDef2 False Passed
  • Model Under Test
  • Equivalent Model
16a8bfa7e1621a5fc5a9a507f03ee27f078794c7 Apalache Ne Def1Recursive True Passed
  • Model Under Test
  • Equivalent Model
13f5b9197fcb5bf9d208a5e403fc066335cab6c9 Apalache Ne Def1Recursive False Passed
  • Model Under Test
  • Equivalent Model
406f41b240332193ddb459768c5eb89c5efccf78 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Ne LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
dac5ec4d570530e28a667030e0a4b1836a2d0d87 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Ne LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
41b59394b1bbefc87323a82c13443df944dc61ee Apalache Ne Extends True Passed
  • Model Under Test
  • Equivalent Model
b1c10ad9b7214a12f265c2d1c149d274e1bdf826 Apalache Ne Extends 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
bd029079b616d835b0f1c71e62cd56d3ce6d3ad8 Apalache Ne Variable True Passed
  • Model Under Test
  • Equivalent Model
48007f4402aa3e822f0257cc909bfd3bba8687a6 Apalache Ne Variable False Passed
  • Model Under Test
  • Equivalent Model
cfe05173e1c28aa2d4106e3a90f7655aa2bc1501 Apalache Ne Constant True Passed
  • Model Under Test
  • Equivalent Model
565344f638b10b3116a5ee46996782fe417c1dee Apalache Ne Constant False Passed
  • Model Under Test
  • Equivalent Model
4d076d88a5568aef6ca438066528223143e9e095 Apalache Ne ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
f4afe220544b0798990491de87a3564424b38775 Apalache Ne ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
157d637f923b54b41d9d4bc6bcf45103543e9ba2 Apalache Ne ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
b561b1b899128f490611c0a465bc9e82e28d0751 Apalache Ne ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
55457c5179008703a484d91a90fd6b981887aa6d Apalache Ne Instance True Passed
  • Model Under Test
  • Equivalent Model
878142087a2fc4bc439de2f1aa19d5d5d3e7b57e Apalache Ne Instance False Passed
  • Model Under Test
  • Equivalent Model
c60a34305204ba7ee114f462d339d588d0552ec8 Apalache Ne InstanceWith True Passed
  • Model Under Test
  • Equivalent Model
8a8c40cd549eead0042eec7eff79128e20c43e37 Apalache Ne InstanceWith False Passed
  • Model Under Test
  • Equivalent Model
5b4abb480f416acd725ef7729a0759f02574bf93 Apalache Ne InstanceNamed True Passed
  • Model Under Test
  • Equivalent Model
5c70992d3932e4fb3e4d213f042eae8e56087185 Apalache Ne InstanceNamed False Passed
  • Model Under Test
  • Equivalent Model
16f051cd173249423e0c499246f7b3c1548b7efe Apalache Ne InstanceNamedWith True Passed
  • Model Under Test
  • Equivalent Model
d4c52604fa0abccfc4d9eaf438fa40831791f564 Apalache Ne InstanceNamedWith False Passed
  • Model Under Test
  • Equivalent Model
74285f84fdc14b1443e2c0a34c1b8efb9d596617 Apalache Ne InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
dbad4313c09fe43686b025183abd3f8ac5d07910 Apalache Ne InstanceInFolder 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
a060d1dd17e75dce9907238fcbf19cad9cb7d035 Apalache Ne InstanceNamedInFolder True Passed
  • Model Under Test
  • Equivalent Model
00f2f76b2f79e00d85bdf557fc53fb3d24a14cc7 Apalache Ne InstanceNamedInFolder False Passed
  • Model Under Test
  • Equivalent Model
1403658220fa0e3357a36856ae858a8690c328c4 Apalache Ne InstanceNamedWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
d7bc0df3e50c3eee70fff86f942e888c9806876d Apalache Ne InstanceNamedWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
1828875686fae94065b7c3eeffa988840a3625ef Apalache Ne Enabled True Passed
  • Model Under Test
  • Equivalent Model
460a22adecdac8bb1a587fdf25b368ea0b541b87 Apalache Ne Enabled False Passed
  • Model Under Test
  • Equivalent Model
a03365fad35c5f5b5c40410d4558b5a857a28148 Apalache Ne Cross2 True Passed
  • Model Under Test
  • Equivalent Model
dc14621abde83c60e566d133244c02e622b69929 Apalache Ne Cross2 False Passed
  • Model Under Test
  • Equivalent Model
5472850c65ad56cf657679202e2f5fd3b3a93343 Apalache Ne Cross3 True Passed
  • Model Under Test
  • Equivalent Model
a2d0f29caa476d975b3468fef940ddcbe5c0bbc6 Apalache Ne Cross3 False Passed
  • Model Under Test
  • Equivalent Model
cefa890a55d3fee3e60d3fbcb8e042ce143b4c74 TLC with reduction strategy:
  • Plug 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))
Ne FunSet True Passed
  • Model Under Test
  • Equivalent Model
8bda5ebb55f172928848509dcf0c51a7b7112e5f TLC with reduction strategy:
  • Plug 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))
Ne FunSet False Passed
  • Model Under Test
  • Equivalent Model
9ef76e38748c9bfa7e14addbcbbc153bc3d96f46 TLC with reduction strategy:
  • Plug 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)
Ne RecordSet True Passed
  • Model Under Test
  • Equivalent Model
1cf3fa1314dcd04c1c86b87d6e8f6726632cb516 TLC with reduction strategy:
  • Plug 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)
Ne RecordSet False Passed
  • Model Under Test
  • Equivalent Model
47036164b1d24f0f9764f9b8efd58d3a6e024b79 Apalache Ne SetDiff True Passed
  • Model Under Test
  • Equivalent Model
6283ec40a18f4c9de21d19051a620a4b856067fc Apalache Ne SetDiff False Passed
  • Model Under Test
  • Equivalent Model
ee09d48e5de1b297f562b3ebfbbb128a0ee19ed2 Apalache Ne SetUnion True Passed
  • Model Under Test
  • Equivalent Model
6a15b294eb2bb996b663848ec5611a5c57957827 Apalache Ne SetUnion False Passed
  • Model Under Test
  • Equivalent Model
6407c399e2d57c2c1826017b9ed33f3b66218f14 Apalache Ne SetIntersect True Passed
  • Model Under Test
  • Equivalent Model
9b53b0840843b2f716f2e69031b9e7b9c8ab91f9 Apalache Ne SetIntersect False Passed
  • Model Under Test
  • Equivalent Model
dda4409df0bf2decda25bf5a61a58775bdba7244 Apalache Ne SubsetEq True Passed
  • Model Under Test
  • Equivalent Model
b0eea226c8a0913ec79b96949f1328c3df4676a7 Apalache Ne SubsetEq False Passed
  • Model Under Test
  • Equivalent Model
d60086af239f09e67aa46d1c05002bc4e8fb3e1d Apalache Ne IfCond True Passed
  • Model Under Test
  • Equivalent Model
67e7329f7e8666ee9684bd2c1bd95da460f95805 Apalache Ne IfCond False Passed
  • Model Under Test
  • Equivalent Model
0aab24710c83dea386f8674c65e19d58da0a4a5d Apalache Ne IfThen True Passed
  • Model Under Test
  • Equivalent Model
5026626e769b782cd25649c42aa898d728f5093b Apalache Ne IfThen False Passed
  • Model Under Test
  • Equivalent Model
e51a74bcedb077208dbc9365e646ef06a7730a86 Apalache Ne IfElse True Passed
  • Model Under Test
  • Equivalent Model
a84502058a24493d655f7f890af943d3abaa03b5 Apalache Ne IfElse False Passed
  • Model Under Test
  • Equivalent Model
6b03695874c807d91684fce7267cddbae62685be Apalache Ne Subset True Passed
  • Model Under Test
  • Equivalent Model
0b54be0a6940661e25e8e2be9fbed21e446dfdb3 Apalache Ne Subset False Passed
  • Model Under Test
  • Equivalent Model
1ce922ec88d72adba97132ffecbfb8bffb61e76a Apalache Ne Domain True Passed
  • Model Under Test
  • Equivalent Model
dc391e0cafbfb78050edbed54b1f187e388ded3c Apalache Ne Domain False Passed
  • Model Under Test
  • Equivalent Model
a2c8fa0534ce2544197d2de826db4add839da93f Apalache Ne Union True Passed
  • Model Under Test
  • Equivalent Model
04433599e0611cb5f74c3a8b212c401d467e9071 Apalache Ne Union False Passed
  • Model Under Test
  • Equivalent Model
7a64b03db95c0d311fed1c46fead9166f6f83c68 Apalache Ne Unchanged True Passed
  • Model Under Test
  • Equivalent Model
ac3890d72c2fd1f02ffddff581e70028e32be358 Apalache Ne Unchanged False Passed
  • Model Under Test
  • Equivalent Model
461c4d6c3903d0910a751d6aab3c023dd124f22d Apalache Ne Equivalence True Passed
  • Model Under Test
  • Equivalent Model
a36aa00347bf387e3ad0ba0c61b07008e0dec6f2 Apalache Ne Equivalence False Passed
  • Model Under Test
  • Equivalent Model
73fdb4d59ada0b83c3ab6d909b6efa782ee46164 Apalache Ne StringEmpty True Passed
  • Model Under Test
  • Equivalent Model
f1533ea5f8ceef2fa3f73d85383a8c83aef5b773 Apalache Ne StringEmpty False Passed
  • Model Under Test
  • Equivalent Model
312db331a90eb456063c9af3482c9868a176dff2 Apalache Ne String True Passed
  • Model Under Test
  • Equivalent Model
b25b2be78fe7f3c719ba582f62f152aaaa04eba5 Apalache Ne String False Passed
  • Model Under Test
  • Equivalent Model
f5d1f50294de386ac5d81b005a324cfb0930855e Apalache Ne SeqLen True Passed
  • Model Under Test
  • Equivalent Model
03b5dff48afe0f225291add700d56ab72931a442 Apalache Ne SeqLen False Passed
  • Model Under Test
  • Equivalent Model
4adccc9c7805cd6e8e77541383350e45a5864b40 Apalache Ne SeqConcat True Passed
  • Model Under Test
  • Equivalent Model
16162eaa2a626965710680854e58ae16d24cafad Apalache Ne SeqConcat False Passed
  • Model Under Test
  • Equivalent Model
57ddae4faa7688e1a829612639c5683ebf9ade0f Apalache Ne SeqSelectSeq True Passed
  • Model Under Test
  • Equivalent Model
e135ae16d86d8cc19139e240b9371027431119ca Apalache Ne SeqSelectSeq False Passed
  • Model Under Test
  • Equivalent Model
3183c6599dbc7abe17c6db76587bb0e2c86fb968 Apalache Ne SeqSubSeq True Passed
  • Model Under Test
  • Equivalent Model
c164913254fdb74e54d62a199c8cfdaba1c2edba Apalache Ne SeqSubSeq False Passed
  • Model Under Test
  • Equivalent Model
a3e4e3ead32c226be04ebe5365d3e59fad47c84b TLC with reduction strategy:
  • Plug 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
Ne NumRange True Passed
  • Model Under Test
  • Equivalent Model
58f234ccff9da66e8d4c87db879d4b9624d03f36 TLC with reduction strategy:
  • Plug 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
Ne NumRange False Passed
  • Model Under Test
  • Equivalent Model
0d5f24a7696c6a76dac9e24224cb0eace5c2b64c TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Ne TlcSingletonFun True Passed
  • Model Under Test
  • Equivalent Model
26ca409032849263abd7baa9703c331dd0ce09f7 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Ne TlcSingletonFun False Passed
  • Model Under Test
  • Equivalent Model
9c8f67871de9493e9b6cce23de4f064c095c00df TLC with reduction strategy:
  • Plug 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]]
Ne TlcExtendFun True Passed
  • Model Under Test
  • Equivalent Model
c86e01c8f1eefc311740544b92d76d61c620692c TLC with reduction strategy:
  • Plug 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]]
Ne TlcExtendFun False Passed
  • Model Under Test
  • Equivalent Model
9c0a88505bdda8429f0b8946f72a1bad0c9799cb TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Ne TlcPermuteFun True Passed
  • Model Under Test
  • Equivalent Model
bd23d9035aa342378d2eac6af7d598670f812b1d TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Ne TlcPermuteFun False Passed
  • Model Under Test
  • Equivalent Model
e7b69af17e79e0ed105101f719572e48b631fe3d TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Ne TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
ccab69710a5b23ce3b55bf7c7cf9f05d489693a5 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Ne TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
fae71c0a7dcd3cbe831901c8e352ed8df4cd60b2 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Ne TlcEval True Passed
  • Model Under Test
  • Equivalent Model
e24f56bead7ce71843eca2bd30729778833545b5 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Ne TlcEval False Passed
  • Model Under Test
  • Equivalent Model
2fbb65837527657ba04b04c5a1cd533cfbe50608 Apalache Ne BagBagToSet True Passed
  • Model Under Test
  • Equivalent Model
08c3f5fc93cb972c598ba84a93a2fd5423ad456a Apalache Ne BagBagToSet False Passed
  • Model Under Test
  • Equivalent Model
f141f94c26326a852378d03e20ad716571825437 Apalache Ne BagSetToBag True Passed
  • Model Under Test
  • Equivalent Model
d150b881ce8ea4b184897cc458db3d7e2bc55679 Apalache Ne BagSetToBag False Passed
  • Model Under Test
  • Equivalent Model
7cbf04e9c81d467a2b3a33b87d13f5e51f4c7427 Apalache Ne BagBagIn True Passed
  • Model Under Test
  • Equivalent Model
c8378c0ced14a7ea7e33aeee962b978f7fbaecf7 Apalache Ne BagBagIn False Passed
  • Model Under Test
  • Equivalent Model
4f7f27479aca9bb174b5ab042815d0c743960f3a Apalache Ne BagEmptyBag True Passed
  • Model Under Test
  • Equivalent Model
fd1dedf49f4f6ccd3c8af6f0a485510073f8b1e4 Apalache Ne BagEmptyBag False Passed
  • Model Under Test
  • Equivalent Model
62c0e5ba9bce4283db93f9d169688d0f0ff2b2c6 Apalache Ne BagAddBag True Passed
  • Model Under Test
  • Equivalent Model
0c18bffa619bdf9f60cf84c6cbc614219ed6cd41 Apalache Ne BagAddBag False Passed
  • Model Under Test
  • Equivalent Model
138d79cb92388c21dc707ea5ae32bca561dc0567 Apalache Ne BagBagSub True Passed
  • Model Under Test
  • Equivalent Model
69807393accd9834879812bd31f211c45cb701ba Apalache Ne BagBagSub False Passed
  • Model Under Test
  • Equivalent Model
61a58b2c8f689e1e9c6b8e435b49b9942d128c55 Apalache Ne BagCopiesIn True Passed
  • Model Under Test
  • Equivalent Model
1c69fae13596082628109db1e0b8344f5c27ad4c Apalache Ne BagCopiesIn False Passed
  • Model Under Test
  • Equivalent Model
f142a75557363ea0b11774cbe7a570e7bbe0a193 Apalache Ne BagSubsetEqBag True Passed
  • Model Under Test
  • Equivalent Model
217aba63029199e99e83d56f975a987d2643bb5d Apalache Ne BagSubsetEqBag False Passed
  • Model Under Test
  • Equivalent Model
9698220d5f1fb99526ed81a6d38acc5e3281e517 Apalache Ne BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
811ea012e96dc6b73e2fb1fbccf4067aeacc96fd Apalache Ne BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
5f2ffc75c0c81fbe341f97f908bccd38576c80ee Apalache Ne BagBagCardinality True Passed
  • Model Under Test
  • Equivalent Model
7919ec292e1542b2c3657ea7885598413717fc9d Apalache Ne BagBagCardinality False Passed
  • Model Under Test
  • Equivalent Model
86e0bc6c861e258e4d4db41e7d0875a29b1d1333 Apalache Ne BagBagOfAll True Passed
  • Model Under Test
  • Equivalent Model
809d69e7f172934a7183ded1e8f41af3be23c8ad Apalache Ne BagBagOfAll False Passed
  • Model Under Test
  • Equivalent Model
5aed793a75d4f5942fd389f5c3b610b4d6e4e5b8 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Ne BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
a5ed8fdbbbff8caab02a3fcd0aba11ecaa104c81 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Ne BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
087284367b66f64fe7bb5bdc7a88505c22f5dfeb 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)
Ne FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
98a88225ad0ce6b5918f06346ef2110d9c919e9e 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)
Ne FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
55fe4835eec6adb8f2813319d9c990565e429a1b Apalache Ne FiniteSetsCardinality True Passed
  • Model Under Test
  • Equivalent Model
a3136feb237d2f58e9e0b1e71a87ec76c8a71fbf Apalache Ne FiniteSetsCardinality False Passed
  • Model Under Test
  • Equivalent Model
5c38aaf986a043a08ee899c5d0c058027b700596 Apalache Ne SeqHead True Passed
  • Model Under Test
  • Equivalent Model
c6e741e9cc4561c6dc858daa2cac4ed8417ab6bd Apalache Ne SeqHead False Passed
  • Model Under Test
  • Equivalent Model
6b38137e037f191c01e94bb0353cb660a087f3c3 Apalache Ne SeqTail True Passed
  • Model Under Test
  • Equivalent Model
c0e136056f1c47be5898be42602c2eadf497ac84 Apalache Ne SeqTail False Passed
  • Model Under Test
  • Equivalent Model
992de4f57e3be98439b3be549e8190ac0cd5d32c Apalache Ne SeqAppend True Passed
  • Model Under Test
  • Equivalent Model
1595422c375a25a8e81217db0936bfbfdc2b30cb Apalache Ne SeqAppend False Passed
  • Model Under Test
  • Equivalent Model