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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
b62019e401c3a4acfe0f56e6d5e46860ed4250d9 Apalache And NumGt True Passed
  • Model Under Test
  • Equivalent Model
64c8d287ddf77c539e25597dec505cefbf2bb791 Apalache And NumGt False Passed
  • Model Under Test
  • Equivalent Model
0dfb6965b5d2d0df67181f7704503014f451084c TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine NumGt True Passed
  • Model Under Test
  • Equivalent Model
894290d42a62ac554ddba0de015253dffbdea020 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine NumGt False Passed
  • Model Under Test
  • Equivalent Model
107718c668a2bf18f5875eff62821b788f894bb1 Apalache Imply NumGt True Passed
  • Model Under Test
  • Equivalent Model
a1e91f6132e0c04040a85a4c03b144e56d9082b4 Apalache Imply NumGt False Passed
  • Model Under Test
  • Equivalent Model
0430eb8551f91c9f086e750425f93ed65947cca6 Apalache Not NumGt True Passed
  • Model Under Test
  • Equivalent Model
d116421942e60c7d6ea7426803da885eef2cfa3f Apalache Not NumGt False Passed
  • Model Under Test
  • Equivalent Model
bf39a52d93acd7f6ab0d8eac0d0acbcd23e61ec1 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or NumGt True Passed
  • Model Under Test
  • Equivalent Model
bcd988fffa46b8024a89658421983d64ce8e129a TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or NumGt False Passed
  • Model Under Test
  • Equivalent Model
c15af449a8a4bb9320e9d223ce7d07c361af1b06 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine NumGt True Passed
  • Model Under Test
  • Equivalent Model
9cd81e0dfc28f7b4a77e3f5981486c298faab739 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine NumGt False Passed
  • Model Under Test
  • Equivalent Model
6eb754118f45f393d9f1bb14fb1aea8d36f0b200 Apalache AndProp NumGt True Passed
  • Model Under Test
  • Equivalent Model
7efbf058c3aeb0a2ea8e528db271b980dcfbde1a Apalache AndProp NumGt False Passed
  • Model Under Test
  • Equivalent Model
baa1623ee8f3c71d85c4712e288821866f7c3118 Apalache Boxed NumGt True Passed
  • Model Under Test
  • Equivalent Model
fa7f77edc0d52838d16f8c1a2da75917ea018a6d Apalache Boxed NumGt False Passed
  • Model Under Test
  • Equivalent Model
cd7925380674696d526754e58d3aad63a9a04e01 Apalache Eq NumGt True Passed
  • Model Under Test
  • Equivalent Model
07baff831cfda1d5a12573325e958bfc8cffaa76 Apalache Eq NumGt 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
5d3257779203f72b31c9175ccf9ac6b53c48d636 Apalache Let NumGt True Passed
  • Model Under Test
  • Equivalent Model
348d674b1d51b558416b1a5e5e562c760be60eb0 Apalache Let NumGt False Passed
  • Model Under Test
  • Equivalent Model
6641e96b9e42f9edbc9a4f3a95af42aa3914ab5d Apalache Set0 NumGt True Passed
  • Model Under Test
  • Equivalent Model
dfd7c61d97dba61758aeab4f25164ec2fd157393 Apalache Set0 NumGt False Passed
  • Model Under Test
  • Equivalent Model
2b0226bd51f946c5ea1f466ea204b870ab230dd4 Apalache Set1 NumGt True Passed
  • Model Under Test
  • Equivalent Model
3ea4aecb7af1bd66ba5891cc9759a1d245768b78 Apalache Set1 NumGt False Passed
  • Model Under Test
  • Equivalent Model
091c6404135616917e0450296e9803e75b9ac57d Apalache Set2 NumGt True Passed
  • Model Under Test
  • Equivalent Model
2f408964cf3ae51b98cd141f46aba214cd19594f Apalache Set2 NumGt False Passed
  • Model Under Test
  • Equivalent Model
cf84bea4e3da249daddda7e7b57befd7f0bd17df Apalache Fun NumGt True Passed
  • Model Under Test
  • Equivalent Model
c1615a148e9dfdd3ef1aa6916d21cc2c5567864a Apalache Fun NumGt False Passed
  • Model Under Test
  • Equivalent Model
fdcc565456c0af133599d7cfffd7d6771b3e364d Apalache In NumGt True Passed
  • Model Under Test
  • Equivalent Model
d220a7764a06929f9f69f418d359939ff8d6052d Apalache In NumGt False Passed
  • Model Under Test
  • Equivalent Model
36150a6544484ff12547b69d00751a54a722c990 Apalache NotIn NumGt True Passed
  • Model Under Test
  • Equivalent Model
33d5d85e8c9b7849dee32d7307a9520defd21582 Apalache NotIn NumGt False Passed
  • Model Under Test
  • Equivalent Model
73cae06e4a70be8784fbd804f0053391473bdd70 Apalache Exists NumGt True Passed
  • Model Under Test
  • Equivalent Model
9fd5293680005520e9a6d96baee4bf13b7de63ac Apalache Exists NumGt False Passed
  • Model Under Test
  • Equivalent Model
640150ce9db0c332124168f441dc1c3389ef81b1 Apalache Forall NumGt True Passed
  • Model Under Test
  • Equivalent Model
016d6df55e6c0ccffd7f85141baba36b34fc8fca Apalache Forall NumGt False Passed
  • Model Under Test
  • Equivalent Model
8947cd53ce33c1394731b7fca3beadb8eb6a1167 Apalache Choose NumGt True Passed
  • Model Under Test
  • Equivalent Model
1ad2e06d9a544b0948dd5aa1a8aa5552fd38731f Apalache Choose NumGt False Passed
  • Model Under Test
  • Equivalent Model
dd857f2ba584f8d456e8c7e921eaaedc23280b00 Apalache Record NumGt True Passed
  • Model Under Test
  • Equivalent Model
1edfa34d60f58cb6e13027dcaf1ee58755e0e23f Apalache Record NumGt False Passed
  • Model Under Test
  • Equivalent Model
c6881ac37be1382a4ccb97bbfc8363bddbf529ca Apalache Tuple NumGt True Passed
  • Model Under Test
  • Equivalent Model
45b5b623e2e91946e5f7a33d2f4300ed2d7866d4 Apalache Tuple NumGt False Passed
  • Model Under Test
  • Equivalent Model
48f1ee85219782297459468a382d2fa8c03bd4f2 Apalache FunApp NumGt True Passed
  • Model Under Test
  • Equivalent Model
b2abd64f3625068e53aacc792d74a45b250193fb Apalache FunApp NumGt False Passed
  • Model Under Test
  • Equivalent Model
960a9ca6cb49e5adc61316516980b143b34ef1b5 Apalache Except1Fun NumGt True Passed
  • Model Under Test
  • Equivalent Model
09f76d2b1e9646a8316f858acdbc4c4a5d73686b Apalache Except1Fun NumGt False Passed
  • Model Under Test
  • Equivalent Model
a2ce3fed26648ff18cb6749306af6cec0f198fa9 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt NumGt True Passed
  • Model Under Test
  • Equivalent Model
06725f9526af38141a4ba01babb7f8f6c4fbae26 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt NumGt False Passed
  • Model Under Test
  • Equivalent Model
74fcc675b01469993224b37170c972a67cdab7a8 Apalache Except1Rec NumGt True Passed
  • Model Under Test
  • Equivalent Model
f27c285a39c2999e7bc5d27753885bbb67b9d080 Apalache Except1Rec NumGt False Passed
  • Model Under Test
  • Equivalent Model
32775217f4b523d3ca4c323f16cf38494921e8bd TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumGt True Passed
  • Model Under Test
  • Equivalent Model
95224c623066e5b6d47aca5d09d13fdf3b475829 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumGt False Passed
  • Model Under Test
  • Equivalent Model
909f82b594d6ae1e57406e69773b028eb2d72abf Apalache Except2Fun NumGt True Passed
  • Model Under Test
  • Equivalent Model
df3ff5b6232b52ba46520fb102a25419995f6f13 Apalache Except2Fun NumGt False Passed
  • Model Under Test
  • Equivalent Model
a5c42aa01ddb37d8a589415a4a179afecc24d00b Apalache Prime NumGt True Passed
  • Model Under Test
  • Equivalent Model
56b386439073772df393e3b078d07609ff4ccb96 Apalache Prime NumGt False Passed
  • Model Under Test
  • Equivalent Model
e1f2440750627bf848a2e5f0755af16848e066db Apalache DefFun NumGt True Passed
  • Model Under Test
  • Equivalent Model
95b6d64e9ce03383b908a27617eda8ac3023ca33 Apalache DefFun NumGt False Passed
  • Model Under Test
  • Equivalent Model
1831559c4169aaf22de0311ee6920e0d833e1150 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumGt True Passed
  • Model Under Test
  • Equivalent Model
de3956a77925e158e43a66b175c82f3ee1c911a0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumGt False Passed
  • Model Under Test
  • Equivalent Model
795b827025ed43555db0289ca883fc1e9d72b718 Apalache DefFunRecursive NumGt True Passed
  • Model Under Test
  • Equivalent Model
849c424cda1714422c3ec57ef4cd2701f7a90643 Apalache DefFunRecursive NumGt False Passed
  • Model Under Test
  • Equivalent Model
a6bcc37cad21138805723c6f3c812fdf0e481504 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumGt True Passed
  • Model Under Test
  • Equivalent Model
f553a591aebec9285c3eba8fab45c523eddf3aab TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumGt False Passed
  • Model Under Test
  • Equivalent Model
3b9d6b19e211810fb360678f3c3a5d995dc246fa Apalache Def0 NumGt True Passed
  • Model Under Test
  • Equivalent Model
f7c2fe6002b4cec3eda5e98e365e6bc6c1e8f71d Apalache Def0 NumGt False Passed
  • Model Under Test
  • Equivalent Model
0f5cf71febb1d5bcf6e25e8b52b98106b3c35ff2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumGt True Passed
  • Model Under Test
  • Equivalent Model
87f5579b3bccf6bfe4b1552ef0bb14cbe4150bd9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumGt False Passed
  • Model Under Test
  • Equivalent Model
0625251670b585605ae9b0fab466ffc184158cc4 Apalache Def1 NumGt True Passed
  • Model Under Test
  • Equivalent Model
b7b5db548e983635811e1a17c80eb430187b990c Apalache Def1 NumGt False Passed
  • Model Under Test
  • Equivalent Model
79c3c79f42a2e6b9369b787479ba71b777859f81 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumGt True Passed
  • Model Under Test
  • Equivalent Model
3b26f0b27877e62ce57c9758891ae254d7b3b471 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumGt False Passed
  • Model Under Test
  • Equivalent Model
a837f052846decb45a5828c2f4aedb331dd3288e Apalache Def2 NumGt True Passed
  • Model Under Test
  • Equivalent Model
ccc48def7f936c126a308c9b1a5fa7e02d5d1c82 Apalache Def2 NumGt False Passed
  • Model Under Test
  • Equivalent Model
8d34e3821bcfe27bd201ac525498a86282759345 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumGt True Passed
  • Model Under Test
  • Equivalent Model
29de02c9898fd7075375688b358ccfe5099115f8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumGt False Passed
  • Model Under Test
  • Equivalent Model
08b1fbdb9f4831d2bdf936532c76302349377b72 Apalache Def1Recursive NumGt True Passed
  • Model Under Test
  • Equivalent Model
3d4426d39f7707c3964d137acf5bd6fb0bf6f8a3 Apalache Def1Recursive NumGt False Passed
  • Model Under Test
  • Equivalent Model
ea0b2a8ad79a74ca8645c57ac65afab14786878a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumGt True Passed
  • Model Under Test
  • Equivalent Model
7f44cc0ea0cdc5ff52a02fbfe04e70195e02eaa3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumGt False Passed
  • Model Under Test
  • Equivalent Model
fad8bcb34f60ba270711e03af58afa600918af7a Apalache Extends NumGt True Passed
  • Model Under Test
  • Equivalent Model
d5a67ff778daa840de90b295964c726d631667b1 Apalache Extends NumGt False Passed
  • Model Under Test
  • Equivalent Model
d85caca565169ea162da4f2a772b46cdf501b965 Apalache ExtendsInDifferentFolder NumGt True Passed
  • Model Under Test
  • Equivalent Model
34c11ea13f87bacdd1a7e43971fa16463f551212 Apalache ExtendsInDifferentFolder NumGt False Passed
  • Model Under Test
  • Equivalent Model
28a85dd592c8b54bdc74c66253b94c44404795bf Apalache Variable NumGt True Passed
  • Model Under Test
  • Equivalent Model
6e324428af5599ea509533a485a2b33d44f56278 Apalache Variable NumGt False Passed
  • Model Under Test
  • Equivalent Model
df385c4d66adb4305e25417879e9a784f3cd35fd TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude NumGt True Passed
  • Model Under Test
  • Equivalent Model
fecd08c7872dec502c3d5ca380cecd57e83423de TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude NumGt False Passed
  • Model Under Test
  • Equivalent Model
f98a177f83b2f346eab178e67dbe5650bdca91bd Apalache Constant NumGt True Passed
  • Model Under Test
  • Equivalent Model
c4c4711c5e94766d85f6c5f4fffdbeafcaf0e247 Apalache Constant NumGt False Passed
  • Model Under Test
  • Equivalent Model
74db11316a265f0cae095a7d1f006e4ea025d7c6 Apalache ConstantRank1 NumGt True Passed
  • Model Under Test
  • Equivalent Model
41dec343144b55e3ddddecfd5ce4477c4453c62b Apalache ConstantRank1 NumGt False Passed
  • Model Under Test
  • Equivalent Model
61102584fc18f8e867b194a997ee19452fd76781 Apalache Instance NumGt True Passed
  • Model Under Test
  • Equivalent Model
f62ca666fc515f37c47a2f40224fb17599ad66ca Apalache Instance NumGt False Passed
  • Model Under Test
  • Equivalent Model
9734babf0826c1aa41b6a9916a409ccc72226e77 Apalache InstanceWith NumGt True Passed
  • Model Under Test
  • Equivalent Model
e4fd3173721e878d84995139d47ecc0d9dcc060b Apalache InstanceWith NumGt False Passed
  • Model Under Test
  • Equivalent Model
351a6b3a56cc4754a0bf3b1b1e107df69cfc1853 Apalache InstanceNamed NumGt True Passed
  • Model Under Test
  • Equivalent Model
ae036da370ff1857d3dcf0d8c9a18249631292b3 Apalache InstanceNamed NumGt False Passed
  • Model Under Test
  • Equivalent Model
f8e07817f138dd7e15e9a396e137f2c46802ece3 Apalache InstanceNamedWith NumGt True Passed
  • Model Under Test
  • Equivalent Model
538e1f3bc3cdbf18404182bda0576f0f2f29a3f9 Apalache InstanceNamedWith NumGt False Passed
  • Model Under Test
  • Equivalent Model
a3e0369e340fb41961cd343b9f1e8e90d4fec0af Apalache InstanceInFolder NumGt True Passed
  • Model Under Test
  • Equivalent Model
f1c3811ae172aea8f25889f50f6912a482ca2f65 Apalache InstanceInFolder NumGt False Passed
  • Model Under Test
  • Equivalent Model
56118527e8b2727cc5c24ea1a11170d79709ecf3 Apalache InstanceWithInFolder NumGt True Passed
  • Model Under Test
  • Equivalent Model
1b9eeda02e9cb4ad4d90b09ce3471094736852b4 Apalache InstanceWithInFolder NumGt False Passed
  • Model Under Test
  • Equivalent Model
c8959ac9cc9bf3066cc4a2a91ab5a714a6240f28 Apalache InstanceNamedInFolder NumGt True Passed
  • Model Under Test
  • Equivalent Model
d71cc75c297d57cc171d8225feb860e0bf76bc6c Apalache InstanceNamedInFolder NumGt False Passed
  • Model Under Test
  • Equivalent Model
3a44ea0d5b6b75bf3c04669b467dd6cd7ff99152 Apalache InstanceNamedWithInFolder NumGt True Passed
  • Model Under Test
  • Equivalent Model
5b383a19340ffdff4d562e7928afc9b3f0188f17 Apalache InstanceNamedWithInFolder NumGt False Passed
  • Model Under Test
  • Equivalent Model
a6f4c5d899312a2fb972977f640c984c1e1c82d9 Apalache Enabled NumGt True Passed
  • Model Under Test
  • Equivalent Model
50c6db42ceded617768f7ba3f91247e4eefc5a68 Apalache Enabled NumGt False Passed
  • Model Under Test
  • Equivalent Model
402af71f13b2e538c15ac6a217e4f57e74be0881 Apalache Assume NumGt True Passed
  • Model Under Test
  • Equivalent Model
1f0e1169d050c0ffaf0ef642144657085fc77198 Apalache Assume NumGt False Passed
  • Model Under Test
  • Equivalent Model
7df3936fb29adf96e712d54b106e9e858cbe292d Apalache AssumeNamed NumGt True Passed
  • Model Under Test
  • Equivalent Model
969ddd3e173ac14968ece4147e93d9d727c8a858 Apalache AssumeNamed NumGt False Passed
  • Model Under Test
  • Equivalent Model
2a10bd4e62da01fe7ca9c77c8d782f9d005238c7 Apalache Lambda NumGt True Passed
  • Model Under Test
  • Equivalent Model
683afa699c6e77b736a23a5041608c2b8d12ecf7 Apalache Lambda NumGt False Passed
  • Model Under Test
  • Equivalent Model
b2be74a7987214c4f0ed2c2dd164f12bfee4cf3a Apalache IfCond NumGt True Passed
  • Model Under Test
  • Equivalent Model
f7f1c3474d2702651be9864fc2efb1396cdf7536 Apalache IfCond NumGt False Passed
  • Model Under Test
  • Equivalent Model
be410545a8ab684683211e5d4c0fa9b79da4604c Apalache IfThen NumGt True Passed
  • Model Under Test
  • Equivalent Model
73476054bf9f1aeabcce6a6cee8b3f8245d98ace Apalache IfThen NumGt False Passed
  • Model Under Test
  • Equivalent Model
1f92c0d24cfa98d50816ea83ce3a85cb841ed636 Apalache IfElse NumGt True Passed
  • Model Under Test
  • Equivalent Model
7bfcaa8fdfe14347ffd72deb086f2a7c0cb4e5a3 Apalache IfElse NumGt False Passed
  • Model Under Test
  • Equivalent Model
3a4b9b9842ff4c5bb2ce29ebac3777d50b7d42d2 Apalache Unchanged NumGt True Passed
  • Model Under Test
  • Equivalent Model
f7e9f7b49f5039a4c1e02725f5dc0820abbef066 Apalache Unchanged NumGt False Passed
  • Model Under Test
  • Equivalent Model
af91226b10e26f202dbb6008990aafd9bbf7f020 Apalache Equivalence NumGt True Passed
  • Model Under Test
  • Equivalent Model
0dbe900ee8f4c69666815f371896fc62a78abca0 Apalache Equivalence NumGt False Passed
  • Model Under Test
  • Equivalent Model
7080e4b55722a627c0bdf09497eed7690e719fdb TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumGt True Passed
  • Model Under Test
  • Equivalent Model
4bb1fd5f4eee8a40629ea601b172e5d613be74a6 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumGt False Passed
  • Model Under Test
  • Equivalent Model
69d3eff51e8ef6011369a8cd6d3b479069bc8ed0 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumGt True Passed
  • Model Under Test
  • Equivalent Model
3fabf8b50ae6731a4925a8c9cb626892915515af TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumGt False Passed
  • Model Under Test
  • Equivalent Model
2c0fd16b66001d37dcaa8a1b4f11684e39f4d935 Apalache BagBagIn NumGt True Passed
  • Model Under Test
  • Equivalent Model
d7ce9358fe885c919bdfbcc4d06e50cbf7a2b73d Apalache BagBagIn NumGt False Passed
  • Model Under Test
  • Equivalent Model
7a2f5696ca1a250fada82d4e5c83392bb153e283 Apalache BagCopiesIn NumGt True Passed
  • Model Under Test
  • Equivalent Model
c34230f4b3a682f02f9d8150331c9f494ab873cf Apalache BagCopiesIn NumGt False Passed
  • Model Under Test
  • Equivalent Model
617dd5622eb8e7f88095b02ca9ef0cbac3fc15e3 Apalache SeqAppend NumGt True Passed
  • Model Under Test
  • Equivalent Model
2a8699f50e64a8f0184de68e1f34e265fd03e030 Apalache SeqAppend NumGt False Passed
  • Model Under Test
  • Equivalent Model