Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
8dd211ed95b33fb777d3192790ff0123ca00839d Apalache And IfElse True Passed
f24455401af1829c4895d2e47f20cb08f2dfb3f9 Apalache And IfElse False Passed
50fad3ddd29b66a10714428d021eae8c36a243e0 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine IfElse True Passed
9d404faea7ff867ab7a4436fae1582986b0a13e9 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine IfElse False Passed
b271c898b63029311bc60df88f37ca63e96d71e1 Apalache Imply IfElse True Passed
59773df1edf02b015e646833d78a55d4534bba83 Apalache Imply IfElse False Passed
22dda7daf5a0a323933edff0d63d0ddbc992e037 Apalache Not IfElse True Passed
fa0ad76c47850ccff4b984317b5d543f6f8e11fc Apalache Not IfElse False Passed
7479924f5eab4d53c8be88aa7302416ea78996bd TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or IfElse True Passed
e5b2eb1b52af0e02bc5a50b54be3a9d28705f7c4 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or IfElse False Passed
42bf5572d7972cda65b66c6a240fcf24e6324c28 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine IfElse True Passed
ce4757f17a188727c2aadca8274da1bda247511a TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine IfElse False Passed
8f9b905a2b4a84105af989039350b1a5f0774582 Apalache AndProp IfElse True Passed
fc94218300bb3bad192e14ca28249039837a5bf1 Apalache AndProp IfElse False Passed
0abd39340aa146373597822fbd89237a6303bb6b Apalache Boxed IfElse True Passed
6be131d8c4c20d78d053221b45af214bbfb42610 Apalache Boxed IfElse False Passed
05d5859b9f395a07c1bfe2beb93a7e27e264dd87 Apalache Eq IfElse True Passed
f77e424630070ba41f8cd9fef1f3897375457051 Apalache Eq IfElse False Passed
e51a74bcedb077208dbc9365e646ef06a7730a86 Apalache Ne IfElse True Passed
a84502058a24493d655f7f890af943d3abaa03b5 Apalache Ne IfElse False Passed
1223b4ead3300de738379a33313a969072323bba Apalache Let IfElse True Passed
e0fa5fbd5e6ad70b06ac3810cb290bf9aa5fc75b Apalache Let IfElse False Passed
9e3db955e990c3c3a16e15474a33de4f6c1dabde Apalache Set0 IfElse True Passed
763b4372acded9e33e4bcac91a77f4a4878f52eb Apalache Set0 IfElse False Passed
2de3702389404778df46d22f483d140e943f863c Apalache Set1 IfElse True Passed
ec8192e776751918412238ab85c6e7f6dce13bdc Apalache Set1 IfElse False Passed
ae1e6c184a04b0d373a390173982556f1cb66373 Apalache Set2 IfElse True Passed
814c8ef95d9df274e9ebe54214a9965a519ac146 Apalache Set2 IfElse False Passed
b539e50fbd927dc0553d4c21bacbb2bbd95a3dee Apalache Fun IfElse True Passed
60e406005696176e454052f35f56b6d325d0bc26 Apalache Fun IfElse False Passed
560c908055c2742d05f1257613463efb14c98a40 Apalache In IfElse True Passed
b308e7c12616fa624d6e30ff7abd5daa6eb5f04c Apalache In IfElse False Passed
200d1ab604365b478f9403cd721066337623e859 Apalache NotIn IfElse True Passed
9578d144a4c014cc192c42a4a69635327871084a Apalache NotIn IfElse False Passed
634a11501090b257098922a4349c9f4374f51d5a Apalache Exists IfElse True Passed
a7bbb96492536c009102373e790b5ba31edd3d3b Apalache Exists IfElse False Passed
a79e2fb60ff165cd7da2dfa598cba3fb620ea6c5 Apalache Forall IfElse True Passed
675369d160d254e1fb8b3c7d3838a797d7e97932 Apalache Forall IfElse False Passed
397fcff29abf2ade9f007a53c4331d272a47bc90 Apalache Choose IfElse True Passed
b54dd6a225fb9816eb7e7d27f45f2c502d044175 Apalache Choose IfElse False Passed
cc11710d9acb6c19a2c953050550658eb7a1ff94 Apalache Record IfElse True Passed
c6befcc1e6510ee9139cca5986f8ad68d1a328de Apalache Record IfElse False Passed
65d7d6f1b0a68b10f2af8ffafc803175db1d6572 Apalache Tuple IfElse True Passed
19c50c9180ea68887039bfff20b3b51a7a479d33 Apalache Tuple IfElse False Passed
a5e810207342613d85616a596095555c1ba1951e Apalache FunApp IfElse True Passed
e96762ce5528f1d9946226a9a331c81171dbe094 Apalache FunApp IfElse False Passed
c961f126d86ccc27d06a9420dc2adf01ae8a6185 Apalache Except0 IfElse True Passed
b870ce88c47fdd7aaf98593e91ee44c3faa051e9 Apalache Except0 IfElse False Passed
52e0726f5c91ffa3f25cafe9517a769c22019449 Apalache Except1Fun IfElse True Passed
fbd8f713e3015969ba4fe8ed82947ffe4e986a00 Apalache Except1Fun IfElse False Passed
a1f47176aea0d7a611b2da6a12895bc37387da70 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt IfElse True Passed
a954a21366e67b1065e6c78d92d23e5758870f14 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt IfElse False Passed
7c6e80395fa57a594aeb520ddfbaa922dd729779 Apalache Except1Rec IfElse True Passed
73bf8411a043864de1eb6dc2509d0a20189af56a Apalache Except1Rec IfElse False Passed
4354787c0f3a8485e3afc09f01ae3eef0633a43b TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt IfElse True Passed
64bbaaa276a08da39dc9e7a1b890a2fed3fd3b10 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt IfElse False Passed
7da240f7bfaa1d35ed843a39cdb844ca8f1c5715 Apalache Except2Fun IfElse True Passed
f01edfd0365413092670b1258c991e13f7365d8d Apalache Except2Fun IfElse False Passed
a513c5e98cef97ff25046511b1316aac6390eda5 Apalache Except2FunTuple IfElse True Passed
b677e2f5e272da7a46f1c4016d4b1634d2f5d0cd Apalache Except2FunTuple IfElse False Passed
f8e31894923564781eac7cff215f29c48be324de Apalache Prime IfElse True Passed
f26d65bd5d93fc0ed12b6c408364a0f339e06e3f Apalache Prime IfElse False Passed
0889bb463bb7f355a9ec017e2b0598164ca99628 Apalache NumUnaryMinus IfElse True Passed
10ad2b37370ebdfdeb0459bff05e14679e09ebdd Apalache NumUnaryMinus IfElse False Passed
559446a08400996c6567cca87bc391b578b127b3 Apalache NumPlus IfElse True Passed
9382206fad2c7dfe6ee0a892c2b2055a4f7ce3fa Apalache NumPlus IfElse False Passed
1b2a70bec97d69c58115e0b491b969aaeae8423a Apalache NumMinus IfElse True Passed
5a6db31be5faaf6f34b38530b04476f9c4d4a4fe Apalache NumMinus IfElse False Passed
4ff450a5d41d0bccded5cff05e882ef8358d3cd7 Apalache NumMul IfElse True Passed
5152ff7bee5647a8113f4af7098bd4f6c052f8cf Apalache NumMul IfElse False Passed
05ab36e11ae9398809c5f63aef5a2e38e0441021 Apalache NumDiv IfElse True Passed
50efb77fa7874ac4f79d16d615f02a9f2b48d5b9 Apalache NumDiv IfElse False Passed
c6ed065ff0ee3c2aed5b5c7f30fedcafa16ee0a6 Apalache NumMod IfElse True Passed
2e3665f83ead3dc038c0eec99bf9e2cb1eb461f8 Apalache NumMod IfElse False Passed
b478556e98f0e4cfaf16d538d38f4385990738f3 Apalache NumPow IfElse True Passed
ca576e8a351f7e75437a1e87a27634b0ba87b1ca Apalache NumPow IfElse False Passed
8acf19fd54e327f26dce7cd5451682282af1c0bc Apalache NumGt IfElse True Passed
29a62a6a9aef42e9aac970e9b097d3edfa93279b Apalache NumGt IfElse False Passed
f403ee9c677b3a06534a68d8d7081e4abb6dfad2 Apalache NumGe IfElse True Passed
71142f29b1ac5e8f67a72245c51d855f9abc48f6 Apalache NumGe IfElse False Passed
0fa2257d0393ecf4fdee201d5741acbb255179bc Apalache NumLt IfElse True Passed
2d1f66cbf6907f76bae83a6f8519a45f8487f2cf Apalache NumLt IfElse False Passed
0f6fb2c8b54af2d3b646f9d35a857e6f455965f0 Apalache NumLe IfElse True Passed
07d7d9e7ae2ef385b049e8e5564f31fe76d07609 Apalache NumLe IfElse False Passed
a6de274474e5fa00c1ff721844b68363cf290f2c Apalache DefFun IfElse True Passed
cc482dd0f7ccc9fc28523e56406047593833c67c Apalache DefFun IfElse False Passed
e41107d6f1a8883680d1ed3e2c7042b7ed773aea TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun IfElse True Passed
5dd8f07d8b8bf189190f3ab8b0ef80d7399ae1e5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun IfElse False Passed
c6c15954d31430cc99ffa613399cea23ddde0900 Apalache DefFunRecursive IfElse True Passed
f9c711a98f2837dbbbbbf239c53478dfdf66f2b1 Apalache DefFunRecursive IfElse False Passed
55c80016d2d61051186e857ef9216cadc3e35d03 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive IfElse True Passed
53d20d3a82c2a23f9b76375f9b7bd6a16bd9cf9b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive IfElse False Passed
02635b84ad19d35e7ec416c5353e35185326f304 Apalache Def0 IfElse True Passed
e5c5ed96faca17439fa3b4683d12555de4686898 Apalache Def0 IfElse False Passed
6463bae6262718440facd0b18517a63bb2473f8b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 IfElse True Passed
209e8ce8815bf22161f4519e27065d05669ff3ee TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 IfElse False Passed
7a3370238ec62e28045d3fc59e6002894fb42f65 Apalache Def1 IfElse True Passed
c50eea1fca898d2c2dc4e184f0ad793efae2bb2b Apalache Def1 IfElse False Passed
e17489f1238588d7d331406386bb8ab28c93ea45 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 IfElse True Passed
1a63db77801f1bda6a842210bc4cf2f93c83cbd1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 IfElse False Passed
07b433735b473dadc3920255e79dcd7c355f2fc8 Apalache Def2 IfElse True Passed
66d32294bfca4af863836a156bf522f3d312da75 Apalache Def2 IfElse False Passed
a5f0a01f651922bb2feb2427916ac9497a12a012 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 IfElse True Passed
46fada806ba491f4bc1be0b995ff31bfe189caa3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 IfElse False Passed
3e58506fad9a3813147923c7e65ee095b1775bad Apalache Def1Recursive IfElse True Passed
4cdd296859d7ccfd66597a51a85fd895d226a0c2 Apalache Def1Recursive IfElse False Passed
be208ee4b8e6f45180b862bb9a286d28f1e58679 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive IfElse True Passed
6966821ef3182c34396ce3299470a33b566fc834 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive IfElse False Passed
be234495e4854b5c1e9c78329ce91258ce28030c Apalache Extends IfElse True Passed
443373a8334263bb0de395337cd8189bb970930c Apalache Extends IfElse False Passed
14c47131c84bf507b883fa9ca6014a9cefcb5896 Apalache ExtendsInDifferentFolder IfElse True Passed
8272ff548a05c8fb17ff8ceefc4e213b40c08482 Apalache ExtendsInDifferentFolder IfElse False Passed
0b4db1d6778afedad51d878b8a8a378a1c9bf290 Apalache Variable IfElse True Passed
bdd121054705452a97d00f18f3471c938aafb474 Apalache Variable IfElse False Passed
fb0a6a6efab8bc81dc5dd3f93c82e14727b906e7 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude IfElse True Passed
6e8ad3a5dbaaaf38b7db80c1b78572a66a2b7d1a TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude IfElse False Passed
3d6a9416499716b53cc523d104e6e1f7fc002d09 Apalache Constant IfElse True Passed
e658703c97382dc11887fbcc6b027e87e33d1e02 Apalache Constant IfElse False Passed
8f01478b2e34d58e87e51576b6af3c9774ea48c2 Apalache ConstantRank1 IfElse True Passed
3a42dbb2854211d89533767b2caead93a294088f Apalache ConstantRank1 IfElse False Passed
3432c0f3527f635b06fddb92c7292fb3df74b08a Apalache Instance IfElse True Passed
5d85410a215cb15495beeed97761c3ef4943dfd5 Apalache Instance IfElse False Passed
717f6f187e666540597f37bf82f88d9d13ffb202 Apalache InstanceWith IfElse True Passed
90dd803d3e2d9038b8eee84ba47d7ce1ccf446d2 Apalache InstanceWith IfElse False Passed
cf3454dd4e2ecceacc41a4dbff39ae23677edaea Apalache InstanceNamed IfElse True Passed
08a11c26bbfbbfb96cb4d3b862ec1724d7e1d0f3 Apalache InstanceNamed IfElse False Passed
ee963c1ea7de935ee82dbb85152b0f0dec29c083 Apalache InstanceNamedWith IfElse True Passed
a26c68af20478a2b35f25eb456cb429d1f200360 Apalache InstanceNamedWith IfElse False Passed
a2fa7843c1c6b5e46b833bcf785dcc15c464ddbe Apalache InstanceInFolder IfElse True Passed
a26a3eab388fb1e96b462b45a3439021aaf7da5f Apalache InstanceInFolder IfElse False Passed
21afab4cc531ee16bfbd9f3fe50b4559009f2f8f Apalache InstanceWithInFolder IfElse True Passed
fb7e34c91152709c0731ad4faa3e494a714a7da0 Apalache InstanceWithInFolder IfElse False Passed
99c6f210ea2a663a633e836b8dea098fcb49d071 Apalache InstanceNamedInFolder IfElse True Passed
f2396a9d598f8719c0af61dab73f3d36f0afa4b7 Apalache InstanceNamedInFolder IfElse False Passed
da3e2d09eda69739dda329e8c75b08544576c762 Apalache InstanceNamedWithInFolder IfElse True Passed
fa210d81aa06076419d803d708c2149cfaed1781 Apalache InstanceNamedWithInFolder IfElse False Passed
b611a80fea25749a1df34b20f478cef2ee2a5f65 Apalache Enabled IfElse True Passed
6e56f8ba520133813bbc2b60e178408a95f413a0 Apalache Enabled IfElse False Passed
0a9b6e25f11c5fc08f3215232019a787687598cb Apalache Assume IfElse True Passed
b14104566cfa4a53b860e9a0774c37d9304bc27c Apalache Assume IfElse False Passed
3c0ff3c2eb0a47b74b8a747b5de22d8c95be01d6 Apalache AssumeNamed IfElse True Passed
3d9c763a19ada6c52cc81b4bc458d63927f0dddb Apalache AssumeNamed IfElse False Passed
65f4905de6665fb7023d95f856a64d9e98051ba7 Apalache Lambda IfElse True Passed
86d3ceaf6260ef6a5d1052cb8a536f3531e3d90c Apalache Lambda IfElse False Passed
2a0c4beb3cc93e981c5c70dc7011777bc69377b5 Apalache Cross2 IfElse True Passed
c888d56a4267470039e3f817f108f3b085a0b341 Apalache Cross2 IfElse False Passed
f48f5cc1cf116d8b8dc045288688881b0f4ab8fc Apalache Cross3 IfElse True Passed
6ce3e2479b96e3536232ea55a69c87df93763949 Apalache Cross3 IfElse False Passed
fe801510b58f9f2315115ab70c64501f53f69c3e 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 IfElse True Passed
20454711e42018bf2a435650b148131d3fa94317 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 IfElse False Passed
d111625390e8658d170a1c978d4a776033f7ebac 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 IfElse True Passed
acda925c443a809be2bcaa46059dfa4e8e703e9a 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 IfElse False Passed
d4e4040e34bcf9a4fe7680334482800f9518b465 Apalache SetDiff IfElse True Passed
9bb39eb3a879a71a1c558ef1aa6c2b4585aa434e Apalache SetDiff IfElse False Passed
67adb565327a9837c2cce660bb5185d6b5a782ec Apalache SetUnion IfElse True Passed
324cf0028b094fd185212e6b4104c5d7d7946c0c Apalache SetUnion IfElse False Passed
fba01973e1cddfc092583b015f771d4569c79d90 Apalache SetIntersect IfElse True Passed
a5ce28c5a29e2c2fd53dc128810a752a28291008 Apalache SetIntersect IfElse False Passed
80dcd5cb020229486aa344d05a8a05d2d508318d Apalache SubsetEq IfElse True Passed
7a2336fb371740bb174a5b94a8552eb2e58d3eaa Apalache SubsetEq IfElse False Passed
8bb8bd4b2ee45fa6620e4a5d20979bd68933f01a Apalache IfCond IfElse True Passed
6edba2231e5c2e881c6532531ef40de09f689c81 Apalache IfCond IfElse False Passed
991d54d1c096e42e8f366d998972167744037908 Apalache IfThen IfElse True Passed
98865629ae3c3119cb19c56ec807b101952851bb Apalache IfThen IfElse False Passed
c3bc88179452281350f3e4362aeac941bdc76c98 Apalache IfElse IfElse True Passed
b0cb6f2a1f64dc6ef41af878d2d69ebd4fcb9f7e Apalache IfElse IfElse False Passed
0cccad69ec8f17c1dc42a31eeede4af6451f6af7 Apalache Subset IfElse True Passed
eb07d8f3ab603e4a01105b37bbdcdc362c54a96c Apalache Subset IfElse False Passed
df6bbedd5ce2207e1c31531cceb0934cc179ce6b Apalache Domain IfElse True Passed
3bd901037df53eb0dd4d257304ac12fe71c9cce8 Apalache Domain IfElse False Passed
a3b8ac239013b35f6a895dbbf29d2f63179f39a0 Apalache Union IfElse True Passed
7447037a14e5d148ec09d8bdc4688278098bb47f Apalache Union IfElse False Passed
946d12972bd8ac31711db23e1757673a0bbc46b0 Apalache Unchanged IfElse True Passed
a1fc8a6ca2113ebe6701fad9b5ae3d0ac62da500 Apalache Unchanged IfElse False Passed
e631ea5eac0f2f3d146fafb3936ad54466c8f5e9 Apalache Equivalence IfElse True Passed
f77f354656eab19274ea666dbbbad023b60d9b04 Apalache Equivalence IfElse False Passed
e393674dd64ade67eb55e852ab1d2bb5c4ac4785 Apalache SeqLen IfElse True Passed
2cc06c7c60c375f4c00e348a8e9c62a8cda32171 Apalache SeqLen IfElse False Passed
7aad7647116ca7d159791591d037aff86e570df7 Apalache SeqConcat IfElse True Passed
1d085d70da414563de00407426abfd26fbbda824 Apalache SeqConcat IfElse False Passed
abb13b7fa19a22058ef71cee4dd3c475c240e939 Apalache SeqSeq IfElse True Passed
dd7f4696cb30fd8be8aabc5a4b4eaf0163fddef0 Apalache SeqSeq IfElse False Passed
ac8fdc553ab8da3bde50681e0662285f95cffc36 Apalache SeqSelectSeq IfElse True Passed
08c35002c8632bba7b6f5ace12d26f698fca6592 Apalache SeqSelectSeq IfElse False Passed
04d3b01d339770a79b74fd1653011769d8980e33 Apalache SeqSubSeq IfElse True Passed
3e25695f6f555867be38f6659b512f18c0f56900 Apalache SeqSubSeq IfElse False Passed
46207fc0efa5370993eedff83bc0694d8581aae4 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 IfElse True Passed
a6b153578816f65025bc545a8b33ab1e02cc31c6 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 IfElse False Passed
eae1eef7361ea3bcfa35a7e5c39a7a05a862bd15 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun IfElse True Passed
98b05d8f39a81089b34a761e1061d5611d9ee6ea TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun IfElse False Passed
35f53ce48f7ec26443abb1d960fb2a509f68dcd9 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 IfElse True Passed
2943eada9b3a1e7d3519c3ae6e7a4de99640110e 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 IfElse False Passed
5c977e111d27a8f1011735e34341f3c18b87a1bf TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun IfElse True Passed
b581d694194f95ec2830503759571dfc4b5cb094 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun IfElse False Passed
3e19ab30e16d3b4acb7d568d97c01d75faca2111 TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq IfElse True Passed
4b956b0b22335ba6632cb5071219270b0ded3ff3 TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq IfElse False Passed
c24361afdb68728ccc327ba4c6aa5671de1ffcb3 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval IfElse True Passed
d5e514e0173ea3c90a4449bdb21c81dde1d2b8fb TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval IfElse False Passed
2813e7a1034ed6ebeb83c6a901915a8dd99f0aab Apalache BagBagToSet IfElse True Passed
cd436baa923675a376e9426e8378ff71306ca96a Apalache BagBagToSet IfElse False Passed
885e2e9e1b5a1de4f14f25e83e51dacdb93ae022 Apalache BagSetToBag IfElse True Passed
f9df4dc6e98f35f54616237af4c321042226117d Apalache BagSetToBag IfElse False Passed
39f8495d4c5d882d53ac7c243d4ee955642f7748 Apalache BagBagIn IfElse True Passed
e2a6b1c61c796f167491b086473494dd6b92d531 Apalache BagBagIn IfElse False Passed
ce99fe26825360c30c2793df79447ebe2f4edd5c Apalache BagAddBag IfElse True Passed
0bbaad7d07992eb911b299222e9511a1c8f6d49a Apalache BagAddBag IfElse False Passed
dd0bbb97fbfcf8bf5402f80f9c5c991a87418da8 Apalache BagBagSub IfElse True Passed
e391216f19a354f8eb8fec685623acbb1ec6003d Apalache BagBagSub IfElse False Passed
64b1e63d26fa6f038e9ae54b23e5cd75bf40eb12 Apalache BagCopiesIn IfElse True Passed
3b03be7350b8092c53a7a06e9d71ce6fc15650c8 Apalache BagCopiesIn IfElse False Passed
3fcc5c807a17a7d4997d4582a289627f3db4896e Apalache BagSubsetEqBag IfElse True Passed
c1d5dfede4dbad590e1e0ba31abe71d959271c5a Apalache BagSubsetEqBag IfElse False Passed
01778873471a634f7e33929afac4df7774b385e2 Apalache BagBagUnion IfElse True Passed
cc47003393124f97c44e6cc2e72339f407aea014 Apalache BagBagUnion IfElse False Passed
356cd02f21670ce36e068d18e3f6e51fc6f14275 Apalache BagBagCardinality IfElse True Passed
e0e7d32e1f17ef4277b1ca430fdf8c529fa37e92 Apalache BagBagCardinality IfElse False Passed
c59fd7457d90ebee01c11bc52f08d37eb5aa7309 Apalache BagBagOfAll IfElse True Passed
a5ea73d497adc36833e6719fd7d6b10ba2c039f0 Apalache BagBagOfAll IfElse False Passed
6a06ca8023a45f8935b3b91bb8a4e7031230d627 TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag IfElse True Passed
6b9a869f35387889ddac3510f7d0f1fd7dab6105 TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag IfElse False Passed
59e51540c2c731b249b6c4a2ffcb71d74772a128 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 IfElse True Passed
2c8e5d254e96563245a4cf51a89214158fcfc249 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 IfElse False Passed
4e90a6ac44e47b7923308f135c99831db477d5a7 Apalache FiniteSetsCardinality IfElse True Passed
1199cab74f1718eedc744b83ac102628bf2a0ea5 Apalache FiniteSetsCardinality IfElse False Passed
9513bff3b2ebc396349e0be4657f3be37ddc9cf4 Apalache SeqHead IfElse True Passed
a35915889c5e630896db330c0d11fe53482a27d4 Apalache SeqHead IfElse False Passed
ad67ba558b6741b391b8a93f41ec9325d2437b01 Apalache SeqTail IfElse True Passed
bd6834e9c819edc78ceb1a98521966c9d271f207 Apalache SeqTail IfElse False Passed
7a0c11df98e4375afdf630d3ee9146e71c3e8888 Apalache SeqAppend IfElse True Passed
dc311a8fce0e12827b3c77ec392ad40bd20731e5 Apalache SeqAppend IfElse False Passed