Index

Tests by plug feature BoolFalse; CLI Option: -workers 1

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
0856bc21023b45ce56b3d3c01cf38abd1851bc59 Apalache And BoolFalse True Passed
52a7f03b0e5f6ae081816856a6bad900ac6a7440 Apalache And BoolFalse False Passed
9fb8920de1e19037d8891e9d7cf4186acfb2ebd2 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine BoolFalse True Passed
0bd45bd0a3e024a6eb9e3671033ea741ed632a7b TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine BoolFalse False Passed
c042df99e6ae6e017ac100060bd2ad5b56e3d3a6 Apalache Imply BoolFalse True Passed
ae992f03b75fbb6d52bb5cc70f256971997599b8 Apalache Imply BoolFalse False Passed
55220aeed17a1df57f7c1252539082684702bb7b Apalache Not BoolFalse True Passed
925f33a35f5b564db7c32d77d5d534663ca819fe Apalache Not BoolFalse False Passed
1e98021b5e0897ca3087f314c0470d7e8f32e721 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or BoolFalse True Passed
bf57281e7131775bc3b08eb9a9ca9123dae625cb TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or BoolFalse False Passed
42e0ca4efe72f99e6afc1b3b9cb699ebd1b90b69 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine BoolFalse True Passed
3ee67d16cccef34bdc4094a040f9391c31f695b6 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine BoolFalse False Passed
ab78aa39fe9beb288acc2b0858d326c89c384394 Apalache AndProp BoolFalse True Failed: TLC reports an error if it sees trivially false property. Whereas Apalache returns violation
5f286ab4bd180ba58d337bae341c7399907d0125 Apalache AndProp BoolFalse False Failed: TLC reports an error if it sees trivially false property. Whereas Apalache returns violation
18ddd500ad3cdf75c329f317c645e11736267539 Apalache Boxed BoolFalse True Passed
400e779330355fb4567b4013e6d1cbb419ef41a8 Apalache Boxed BoolFalse False Passed
1433cf727e0e566bdfdca64b1b72b30a32716461 Apalache Eq BoolFalse True Passed
24f15a44b2df798de8c821d6fe3f677722ac1808 Apalache Eq BoolFalse False Passed
0f9f2a311ddaecf436a57b8e5747d41a0acd832b Apalache Ne BoolFalse True Passed
6204ea6f74f4e5cc00990985df20f5b74d986fd2 Apalache Ne BoolFalse False Passed
3870929418abe4114f36583a9a4d04798480ce4f Apalache Let BoolFalse True Passed
db34a439da0a07814aeb80e65ca4fdb76d980551 Apalache Let BoolFalse False Passed
6a8a731387a90c014efbbc0f72cd0c9dc485d7fb Apalache Set0 BoolFalse True Passed
223582b991e35721bbd09df58c58cfcceebfcfe9 Apalache Set0 BoolFalse False Passed
5b6fd8afd8ff41f2841186afa74698078f137622 Apalache Set1 BoolFalse True Passed
83d8c8fadfeb797a87a848c2be14ed5c32d71a47 Apalache Set1 BoolFalse False Passed
f928a6d04712d14d5ac0ec7296fa98fadf2470af Apalache Set2 BoolFalse True Passed
a3ad33ede5fca116c67b64440e406c4bb98108f3 Apalache Set2 BoolFalse False Passed
735c8312749f6271bf0986f0687d4e709bb64cc7 Apalache Fun BoolFalse True Passed
7e02605666bd9d62deb1f94764a38b8e03f24f0f Apalache Fun BoolFalse False Passed
a4541ea0c0616ffe6efb40a5c2333b461cad22bf Apalache In BoolFalse True Passed
162d432a160919241ae93996ad57d842d149fc1b Apalache In BoolFalse False Passed
15d916aaf4e68f10884f641a1dd54a57758f65e6 Apalache NotIn BoolFalse True Passed
7ba1ea5c3b971cbfe10165867c4ad1c2e92083dd Apalache NotIn BoolFalse False Passed
935d74d83c98c4d11211c89f0203b8ded3cbc310 Apalache Exists BoolFalse True Passed
156c890d66f192fa1b2ec431b1514dba876741b3 Apalache Exists BoolFalse False Passed
07338e830629cab6ed32919cd1672e37dd4a6edd Apalache Forall BoolFalse True Passed
e98a7038eca3f88850f3ad804646ff9616b07dab Apalache Forall BoolFalse False Passed
85de1265e6ddc5777839a5372c6cb145958cec88 Apalache Choose BoolFalse True Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
e9af4b5dda8a82ec1c6e9d135089645fb4fded7d Apalache Choose BoolFalse False Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
234b830e0329c6922930656f0f25e4a5ab4bf4eb Apalache Record BoolFalse True Passed
9f3581360a6c6b0ab7aa585b1ace93b4c9048cb7 Apalache Record BoolFalse False Passed
af71b617f6c925b7b358c75d9f35b54372448725 Apalache Tuple BoolFalse True Passed
74da46e71fd9a4a94b7eb4ed132fdff8b6f15cfb Apalache Tuple BoolFalse False Passed
20e3efa068ddc747802179871a5b3465f1d603c3 Apalache FunApp BoolFalse True Passed
5497444ca2b778f78a382c6cc535638923735dd5 Apalache FunApp BoolFalse False Passed
5fe36f301b5c68b14c5fbfda7868a58680b4cd51 Apalache Except1Fun BoolFalse True Passed
bb38fb00b68364db31a172800c8f3c0c1da52b2c Apalache Except1Fun BoolFalse False Passed
799d5e705c66a81039f95be1030b34f3f47f8465 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt BoolFalse True Passed
2232553e9b587721a51fa0a5c06480ceee0534f1 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt BoolFalse False Passed
0bbb99bff32f0c519f117e8640791ae2c825ca3e Apalache Except1Rec BoolFalse True Passed
06b896fe0c875f43def73ab54c422f6bb5afed94 Apalache Except1Rec BoolFalse False Passed
1e56b9f5deef7fa4aa8e2fbd0b372e38fb5b4172 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BoolFalse True Passed
eca583272a4e933322f1db5e3158b7bdb660cb21 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BoolFalse False Passed
ac8a25242a2b2a19fdcc769aaeb7f056f4fefe3b Apalache Except2Fun BoolFalse True Passed
bca68203bf3dfb077e68ce29b4ba875dbf2c994d Apalache Except2Fun BoolFalse False Passed
3e8d1719329d99212c42e65c339cb41faac80cb4 Apalache Prime BoolFalse True Passed
f9014c53213517944c6e654253c28fc68739ed83 Apalache Prime BoolFalse False Passed
9a5bd8fc221cab88ffc9ff48a3eded87a2a8fca9 Apalache DefFun BoolFalse True Passed
efdca00234252421c0a41f8b6e551b4256371d1d Apalache DefFun BoolFalse False Passed
97f90e2b51b238aa985f21dc4fa02d3cf20d688b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BoolFalse True Passed
1440e6784c506a7f48eabcf6ef623ce24ba43a10 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BoolFalse False Passed
67f24b292f61c0712f740aa1c9d745d59db25f9a Apalache DefFunRecursive BoolFalse True Passed
e497e648eb76675220f5a5ea0b064cf9ff89c663 Apalache DefFunRecursive BoolFalse False Passed
6b34cdab45220875e07bf62d9a5f22ead3d5d389 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BoolFalse True Passed
94e4308a2a9c687d599f45613c9488db7eafaccf TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BoolFalse False Passed
0769cf6df8b0111e3ea68cf5680cf6570de1a25c Apalache Def0 BoolFalse True Passed
e550c24cf4ee42bf1a2be7e68d7870b9415f4118 Apalache Def0 BoolFalse False Passed
8e77fd0535e1ec0fea9ab609eb8da2a7f87ecd57 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BoolFalse True Passed
db28d00d3f8bff9e2891591f2b6efe6541c2aa17 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BoolFalse False Passed
63a6965e320c77c34094ca144b902cf9d07b79c8 Apalache Def1 BoolFalse True Passed
8e3dceac7856ac3f42895d2f3963744da2e50bc8 Apalache Def1 BoolFalse False Passed
55df86dbf80ada2ceb8cdda249fa224600299ed8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BoolFalse True Passed
1ca0794a32c0edb2a94d52e8580e9bb2afd10993 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BoolFalse False Passed
8862f9830bbacf04a9866d0aee72915d3629e29b Apalache Def2 BoolFalse True Passed
70e04f1e4295738e4346770d9c775cba57e2da9e Apalache Def2 BoolFalse False Passed
f3b142e80a5ee54cb33258112ac50dab2b1c11f3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BoolFalse True Passed
f55c7c5a92a024f2f9a38c42f495a9603953e012 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BoolFalse False Passed
210328ac8de01513df49f2342922519fca997c0f Apalache Def1Recursive BoolFalse True Passed
02aa6d744ba3aaeb7a441ba5574862e940ad3a38 Apalache Def1Recursive BoolFalse False Passed
4013ae863ca032ece376e70359a4f4f592230971 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BoolFalse True Passed
2ca4ed7d3caa9dd3d123a41c83156d9b21cf1ca3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BoolFalse False Passed
88c476bb25fc0ef88528f3ca2d1310e62ba4f0f8 Apalache Extends BoolFalse True Passed
cb5fb8a47995de121669249b25eff0f08b7d00bd Apalache Extends BoolFalse False Passed
04bb17a875692fcd1a81dab68a2b7c3fc7e4c2ee Apalache ExtendsInDifferentFolder BoolFalse True Passed
7465240dacf24a456795ca5262eafc86fbe1b6a8 Apalache ExtendsInDifferentFolder BoolFalse False Passed
d416b36d1af6ab925e99be5bed44bb70b599d3c8 Apalache Variable BoolFalse True Passed
06efdd4e789cee241b922d2887db0fa0ad345c07 Apalache Variable BoolFalse False Passed
700339b84caac4340ef12f9bed643dd6c5fe3440 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude BoolFalse True Passed
7aae012214aff6d739dffcedfb2e2316b962692c TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude BoolFalse False Passed
90a31cfe2351c3877a9c990aff476bd6f9d98ede Apalache Constant BoolFalse True Passed
290925cb1855d34e656eb10e0a817d00c36969fc Apalache Constant BoolFalse False Passed
8a53be181bfc52e45d54259ff9e32ef1259ab05a Apalache ConstantRank1 BoolFalse True Passed
abe6cbd06db1ab6bfbe4f223540ef66cee7158a6 Apalache ConstantRank1 BoolFalse False Passed
48c407c33c7a677b163bf0ef174bdc28bb9ce3d3 Apalache Instance BoolFalse True Passed
a81a54f4d3e2beeccf35eb66dbe2b0bc65f28788 Apalache Instance BoolFalse False Passed
74ec2655b480b66ef073c48a7950e597d23124bc Apalache InstanceWith BoolFalse True Passed
bf3c0aa3e4701be2f31f90b41d79dd49b69626da Apalache InstanceWith BoolFalse False Passed
5c47f156eb22b069fce473dcb0946489449d542f Apalache InstanceNamed BoolFalse True Passed
c77d109e2737d71cf9091f6b96cd8cab9085ec16 Apalache InstanceNamed BoolFalse False Passed
90fd9daab81221afee6ce88c42448621ec9afb45 Apalache InstanceNamedWith BoolFalse True Passed
4e97856939057fc81a11c6e4e811523e016df94c Apalache InstanceNamedWith BoolFalse False Passed
abb641246dd96583ee4b1b8e1554acb8b4e0a0f7 Apalache InstanceInFolder BoolFalse True Passed
79bb0f956be1aa700db7cb4f6ff93d4f6e7c2d85 Apalache InstanceInFolder BoolFalse False Passed
b405e4fc2afdeb43f3b73a58f8439400df47cc0c Apalache InstanceWithInFolder BoolFalse True Passed
28136f720547b9d50e55f88ab6e08277eac30df9 Apalache InstanceWithInFolder BoolFalse False Passed
c5275974220bdc4e9752377c68d5c565f5cf1bec Apalache InstanceNamedInFolder BoolFalse True Passed
89d5f6f355d2b1c180affbc2c8f8c07f0bc7ef6f Apalache InstanceNamedInFolder BoolFalse False Passed
768a805373df47d68afffb1905a8f83961cc83c7 Apalache InstanceNamedWithInFolder BoolFalse True Passed
5bbdce123db6963611d6e0741f7ae4ba06a7e871 Apalache InstanceNamedWithInFolder BoolFalse False Passed
5d9425415c79d7fd9b6407f9eb3d100716e6bc2a Apalache Enabled BoolFalse True Passed
e5d7e351f1d2a4c04a6827d0297b2a90db5011ce Apalache Enabled BoolFalse False Passed
2a4eddf14b8b28638c031964f594239d9d39d869 Apalache Assume BoolFalse True Passed
be4148cfbd9a57f8456c1235c223377ee61b5f4a Apalache Assume BoolFalse False Passed
d8a4c533cccde5070c0ee43590a0990325794eff Apalache AssumeNamed BoolFalse True Passed
15e7076be3334e2508f6d0540a8d13fe40f8b1bf Apalache AssumeNamed BoolFalse False Passed
98f6a57bd6736530c61a3d28468e53305c2e1ba7 Apalache Lambda BoolFalse True Passed
50ea1e9f54ff3874c4e28ef3cab6e925a226ea5e Apalache Lambda BoolFalse False Passed
6a47840bf71e797beb768a736e7419628b9cf53d Apalache IfCond BoolFalse True Passed
73d3ae1724f1eb279bfb173413e0c232e49707a5 Apalache IfCond BoolFalse False Passed
73338903b4f9f82e4164e6677dc2613dac15fcdc Apalache IfThen BoolFalse True Passed
5426724b9437cca0127cbf17ec7894c21df5478f Apalache IfThen BoolFalse False Passed
370f155ee014637f19b3c076cb107552383bb529 Apalache IfElse BoolFalse True Passed
2bff9282cc35e24ddc669d722433b29895731252 Apalache IfElse BoolFalse False Passed
7137701d9d4f237c49e230393f1cf631a97e3acf Apalache Unchanged BoolFalse True Passed
275975f93f366be21edb0ec793efb487a51cf8d1 Apalache Unchanged BoolFalse False Passed
557626860ef46ec7a7076a354d09b25fabecfe30 Apalache Equivalence BoolFalse True Passed
90cbc98d1426fdab82d2a8ba594d4a7255344e83 Apalache Equivalence BoolFalse False Passed
0d8c501100d53ad9df6fbc5ad9c7ef4634a05b39 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BoolFalse True Passed
b5061aed8bdaa77bb01b4c0ffa9dd645bc196f4e TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BoolFalse False Passed
99859ccbe0a85f6b0a1e403e702c83aee3335151 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BoolFalse True Passed
ef5dc9f851b9ded0c21e3403eb6cca3e64baa69e TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BoolFalse False Passed
7091f83aebd93858fba2eccbf6b11ae10dbaa6b7 Apalache BagBagIn BoolFalse True Passed
7018a9a746b635fdcf0fa69bfabbca22c08c8e1d Apalache BagBagIn BoolFalse False Passed
8d7bcb754c0e6494f62b59dfa1b42b451268d5de Apalache BagCopiesIn BoolFalse True Passed
8d03ceffb86f40cfcac4d718acd3a80e5a00e92b Apalache BagCopiesIn BoolFalse False Passed
a1ae4630261a6a4493e3f00e6516c7c56333ebc2 Apalache SeqAppend BoolFalse True Passed
efc523748bdf037cb5f3d4c2de2a0fb0112dd716 Apalache SeqAppend BoolFalse False Passed