Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
627894965dcd7d112a807812d64c2450c428b18d Apalache And Instance True Passed
fd359cc68b9b9e58a27a13b77a6b35b9408ddaaa Apalache And Instance False Passed
c027ff59d61d9120e19d2d64f84b07eedd67cd0e TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Instance True Passed
b1664b39579a59d030c02d89b7426dbaeb2cf07d TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Instance False Passed
ad8c5567dbde28787a8ef844df33d69a279b7e60 Apalache Imply Instance True Passed
a233b38594cd8d9e0f82828edba69a60fe3fc244 Apalache Imply Instance False Passed
a50a0fb3927b7705b99ea64e7a96b465742973d5 Apalache Not Instance True Passed
5e8d90f2b8c51027409410f72aca978444ea30c3 Apalache Not Instance False Passed
ee288f344f568b39c574de611680a4bd29d19580 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or Instance True Passed
2c1325b77794080dc3c3d2df48f019e3209d0bed TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or Instance False Passed
edf1bb1fdb634e6f5dd2dc7fb4e1d0fbd712773c TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine Instance True Passed
c7deeed7bc9a96f86eb9833f60dccc7ae3153bdc TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine Instance False Passed
205d11b0e7b19a91be2f0bddaac15059503b7464 Apalache AndProp Instance True Passed
2929190149a47e69775abb6b58b8f0efc9424f74 Apalache AndProp Instance False Passed
9c01d0a7d100027c262e290cac89c56fa958c36e Apalache Boxed Instance True Passed
d6c66f1ff4f072fea78d3da207e6036ae123db90 Apalache Boxed Instance False Passed
467714980793b40bf83689774ee1c11078c90648 Apalache Eq Instance True Passed
100a19eb630ccc0b302a2f9131030bfb1244bbd4 Apalache Eq Instance False Passed
55457c5179008703a484d91a90fd6b981887aa6d Apalache Ne Instance True Passed
878142087a2fc4bc439de2f1aa19d5d5d3e7b57e Apalache Ne Instance False Passed
a78f33bfb1881e1b55f1647c98cb22a50cdba44b Apalache Let Instance True Passed
3cc797661d38f6af98d846ea6ac65dd01b8516a4 Apalache Let Instance False Passed
9f290ce27cc9f8bc89369e3838d6dd6755a61340 Apalache Set0 Instance True Passed
72abfee38998ef9175c2d4f4a87ac1bd6c300647 Apalache Set0 Instance False Passed
062458b53230ad56d4061c20366f880e84e6d58b Apalache Set1 Instance True Passed
f0afd17a99088a6c28fbffadad64280844f5cf13 Apalache Set1 Instance False Passed
7e6f881dc51ef9a26e52990cbee0a4fbd8638175 Apalache Set2 Instance True Passed
8a841cd71b6d44a581a21bda996b814b1b0e8abe Apalache Set2 Instance False Passed
7cbf91165007ac2e2ebe58b0d55051cd54e60569 Apalache Fun Instance True Passed
9ea6bb39c868f6798f4bfd1e2596356c1fd8c304 Apalache Fun Instance False Passed
70802044075a32bd8511516444386ec3d3f20f87 Apalache In Instance True Passed
af0d4cf96778442a712d27fff9057ec9e0039465 Apalache In Instance False Passed
1c45d9b783e9e919997680a402852ac390e32bfd Apalache NotIn Instance True Passed
34e3fe54718dfe7ddf3b6add0b54f768f5dccbc0 Apalache NotIn Instance False Passed
a7cc1d5f22b31ef71af6b28db1d78a18badd5407 Apalache Exists Instance True Passed
4770a8762008f7c0024dfc0bbd1743b94cd688c9 Apalache Exists Instance False Passed
2c2fd2de9d6fa9dff20ab4c075a7c7349751a04b Apalache Forall Instance True Passed
2b3ec5e176324aa9f29fb03e16c92b2491390af8 Apalache Forall Instance False Passed
a99a0fa1b8071e14dcd14723677c3a7d020de893 Apalache Choose Instance True Passed
1d11228e1a0b03116b3844873b7e03d274c5e2d5 Apalache Choose Instance False Passed
a59c41a960b634cdf0b6c21f8a4dd64aaa7d7263 Apalache Record Instance True Passed
84550f2af0a9dd6e1a0aa46ef5c2f77175b189bc Apalache Record Instance False Passed
bbda4c7f9cbbf81173a1dc21ca7e69b643124798 Apalache Tuple Instance True Passed
a1ea917ae03ea051d23a5e2a8b8280102b8092d7 Apalache Tuple Instance False Passed
1879578d93f35f9bbb7c9d61a00c76e04cbdb84c Apalache FunApp Instance True Passed
4607d9f05e3eb39f2aedcfeaf49b684f58b22542 Apalache FunApp Instance False Passed
01cb6eb6502233b15282efe11abe05577deec2d4 Apalache Except0 Instance True Passed
e82a1794c8c58652d736bc56f226cebe52132161 Apalache Except0 Instance False Passed
38ca7ddd5de1b18131368bad914538c6230636d0 Apalache Except1Fun Instance True Passed
c5ea3173a315dc4802fcf7eb5ebe8110774eb6c5 Apalache Except1Fun Instance False Passed
1d1e96e1953e5f9a3e0e00b991c0fcc01a79e36b TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Instance True Passed
316a49634b0d70b7ee494062dbd5725dc73e56e5 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Instance False Passed
f40c9f6a4b2fcafa609f96b67dc63841cdbc86f4 Apalache Except1Rec Instance True Passed
55b453c9f6eee0d7880e39a77fca51fcb6a20930 Apalache Except1Rec Instance False Passed
00e264526dcea1f815c908a7dfd3244627145f98 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Instance True Passed
a4d8d2d4fa4fc6d909f2684b48aaafa61a0b5d1d TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Instance False Passed
148ef11a29134cec07df22a40759c364b5ab4ddd Apalache Except2Fun Instance True Passed
0f5171b2e78138a1e71f6b7f8f23917e7b80a1fa Apalache Except2Fun Instance False Passed
31b55887531d8a8ad759078b686b9091171573e6 Apalache Except2FunTuple Instance True Passed
0ffbdae103febfe25ce1230adae67beae27b2cc2 Apalache Except2FunTuple Instance False Passed
6d09a2920b94a2596442de117218e88f15f473ad Apalache Prime Instance True Passed
c53e6bd0469a7e75c9e0eb1aebb9d8a538a01178 Apalache Prime Instance False Passed
3cddf3782623717349cdb7886cf1d8f0950f2bf2 Apalache NumUnaryMinus Instance True Passed
511bf07fc2cdbce1a6480c98fcea08d99bf281ad Apalache NumUnaryMinus Instance False Passed
a91760fef364e633cd241b914271a3a3072f4e88 Apalache NumPlus Instance True Passed
f474f2c79254904de4959f0750393e28c473ef56 Apalache NumPlus Instance False Passed
4c21c2f73dc563fccd074b481443517694ef1272 Apalache NumMinus Instance True Passed
ea26ec47c962991ef605aacb995cfb785bfe9194 Apalache NumMinus Instance False Passed
cfca201f8c99d9b5d4d515cd78894e86a883f90f Apalache NumMul Instance True Passed
6d1dd14a80b6b975c8344fb7a19af150eda0b642 Apalache NumMul Instance False Passed
818c9219523d03e2b3b2261e2a8edd54508fe020 Apalache NumDiv Instance True Passed
8150f69a422783a58e3d51c7e6a7b8b47229731a Apalache NumDiv Instance False Passed
c95c750f6274d48645ae68b8552cc42a84eddffb Apalache NumMod Instance True Passed
d885139a2b09298c9ff872c5e021ef0916beeeaa Apalache NumMod Instance False Passed
51ac529914a793a06575c8da4b025f0e6b515339 Apalache NumPow Instance True Passed
a9cc1b367a4278eb9f8d7e0f182ccc5edfde17b9 Apalache NumPow Instance False Passed
28326f3dc8adb4e1d982a2f2f9f6df20328da5b8 Apalache NumGt Instance True Passed
1024fbeb7cca7caaff0ffcd88feb33701c01c538 Apalache NumGt Instance False Passed
42e2486d026e6c0f2ced856637156b73c506b0c4 Apalache NumGe Instance True Passed
121537c2da01f8b6a0e7413da9c08de67fe89493 Apalache NumGe Instance False Passed
9366484f15322d340362a3d95f32b83875072471 Apalache NumLt Instance True Passed
35d2a41274ec0cd585e1e413714a80411e229902 Apalache NumLt Instance False Passed
11230e245c233006f69b8a242809cc48664d68ed Apalache NumLe Instance True Passed
0f9b8b02a329f8c312e4c871caa94f1d5b0977d0 Apalache NumLe Instance False Passed
350a11aa4d0c7543ff88c7d4b68748d9e66c0bd1 Apalache DefFun Instance True Passed
2698c8ebeefa4aa08fbd4a461d7e5184ec613fa8 Apalache DefFun Instance False Passed
f66e8b878b12c2cdac9468137f334bd2f1c2bf66 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Instance True Passed
c591d97770b4dd3244e84a79c6643014269362ef TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Instance False Passed
27b03bb3e4f6cfae0277566bb603982cb809d0d4 Apalache DefFunRecursive Instance True Passed
d47795e82a40c3798ff34d9dc42e51cdb169efd3 Apalache DefFunRecursive Instance False Passed
b9e81cf83e40b61d6a3b92e5a17e5f9b61c3b93b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Instance True Passed
bb072ef5b0ab160445192137b1031443d876764e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Instance False Passed
731b4a1731f84584495e3abe329e7a0803912019 Apalache Def0 Instance True Passed
4fba4efc0ec310221d01961e545b8492d3948b49 Apalache Def0 Instance False Passed
c37f0443a813a3e0974a7f3c34abf10e19f6fcf8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Instance True Passed
52a83398bb8e39c1e0c17f0e2f43e72c9410b86d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Instance False Passed
263e0c7ae4764930461e32749ac3304f1e68422d Apalache Def1 Instance True Passed
41760e766de13787ef8612843abee133227e1fe0 Apalache Def1 Instance False Passed
d10a9ffd011441149590bd08fc7bc7d61ecd776e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Instance True Passed
dcd1e43fb715204df212e6846b7653b74ba120d3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Instance False Passed
f0e6da1d8c2a37117863e1f5da5c56f80719831f Apalache Def2 Instance True Passed
5fd18f7379a02b0b52bda563781da23c7b04cb36 Apalache Def2 Instance False Passed
dd0b83f5962ef9b05f596575b6adaa416a8f41d3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Instance True Passed
b77ca9f45ea8daf30fcdff4239c022cc9ac81f43 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Instance False Passed
3bd38e4f72fe251a26c24d53950da794a3a57d95 Apalache Def1Recursive Instance True Passed
a10821031f0adc0c8b8d7f8c2e896d3a07bd9db3 Apalache Def1Recursive Instance False Passed
4661403ca15c277778ff54722a7fe82819c3243a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Instance True Passed
ed7c8a37f5df9dd1afa8a409cf6b07e2db40bc8d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Instance False Passed
7373bb312482ca573cf40ca19e6a9b38d698b2e3 Apalache Extends Instance True Passed
3aaccce3b42ea3cb479d96fe61ae3879bb451a67 Apalache Extends Instance False Passed
9fd2fce31cd622f87f3176d1dafbe58b8adab8ae Apalache ExtendsInDifferentFolder Instance True Passed
e21aacf36284603a1752da3942a6eb3a9ad240a0 Apalache ExtendsInDifferentFolder Instance False Passed
642d376051f55bc6122f93a15ba3eac816dcc3cd Apalache Variable Instance True Passed
cc9c79db36016fa557cc6f446bfe5049695a940b Apalache Variable Instance False Passed
68090eb1e14726641c5dd687e3661368537025b7 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Instance True Passed
ee77c3ae1e806e6f9c89dbb56390d7a38bf251a3 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Instance False Passed
8d32a5977f0f96d0ecbf9f8c246f9e3a1d9a3fce Apalache Constant Instance True Passed
1e82095b3ff76f538578b9aa87b85fb92c540fc5 Apalache Constant Instance False Passed
578c37a18eef6cab28410acbeb174d5ec210de92 Apalache ConstantRank1 Instance True Passed
062a7c407be297f887864bf880253c98335c4a7c Apalache ConstantRank1 Instance False Passed
af3cbb9c1babc120f62f9ba85b07ba7730cb2065 Apalache Instance Instance True Passed
cf9ed8d703c7d6ee8b11329a21c697470974ee81 Apalache Instance Instance False Passed
bc72b566a0d5363485d7e1448b1d80504eaa6934 Apalache InstanceWith Instance True Passed
cb8f5ac2dfb934c4664afb0698071771f6b28c98 Apalache InstanceWith Instance False Passed
1cf929fcaeb163d4fc4e5109e8931b8d01a968ff Apalache InstanceNamed Instance True Passed
dac482d0b722deeebc40a5d48e527d3ab4549683 Apalache InstanceNamed Instance False Passed
75db12168d94726300874039a78c7f3996a1cc60 Apalache InstanceNamedWith Instance True Passed
e4ec17df66efa06414ec85ff0642b19552c848ff Apalache InstanceNamedWith Instance False Passed
8a2973644adbc4e56aa29a8c8de99b3e2c280836 Apalache InstanceInFolder Instance True Passed
6df75af6d8ddb5c03fee0e956cb13d8911ba1999 Apalache InstanceInFolder Instance False Passed
ba0342cd028ff192a64acce5976a5a546cd2cc76 Apalache InstanceWithInFolder Instance True Passed
1719de79ba40c6ca09f0a5cf276f4621442b47a5 Apalache InstanceWithInFolder Instance False Passed
b50810e86b02a53875df9ff6a29b647b3db795cd Apalache InstanceNamedInFolder Instance True Passed
722ddb6ba5223e2bfb9b7a200825b2d1091aaf71 Apalache InstanceNamedInFolder Instance False Passed
3d3c11c6f0cc8e0444c28bff875abde55e7510f7 Apalache InstanceNamedWithInFolder Instance True Passed
c520f5e1466eadf6cf117a8299ffa1045c96c421 Apalache InstanceNamedWithInFolder Instance False Passed
8321f38d089b76e015b0762e12ea4392f48345d7 Apalache Enabled Instance True Passed
4bed2a44e4314e55702acb3707833ba31c4b46b5 Apalache Enabled Instance False Passed
d0201764396b58ecda07652722848410bda73431 Apalache Assume Instance True Passed
3859307b43c261d675a23426a3e7ec888d49dc50 Apalache Assume Instance False Passed
2c6d9acf1262022246f71565b06cabda4d011ce8 Apalache AssumeNamed Instance True Passed
572dfd78aada27959000ec2beae3fd1433b20bc9 Apalache AssumeNamed Instance False Passed
ae1b44cf1437005b3f2599e35059851ad9883f5c Apalache Lambda Instance True Passed
f2b94d36c82925faa00720c2ea8aafce3233474d Apalache Lambda Instance False Passed
381418dcc0bc8420a1a8f319a501a3ab2f1dcf4d Apalache Cross2 Instance True Passed
0b4e55f1abe533473d90ab4d774a99c643089c72 Apalache Cross2 Instance False Passed
850233e2f1d61dbfba7d58978b5b1347dd68969c Apalache Cross3 Instance True Passed
98d930489ff717a5cea0195aeeb953826ffa46fb Apalache Cross3 Instance False Passed
5035fad20445cc379f96726a69c45e0bbc1f9cf1 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 Instance True Passed
7c08cc9e1c184048f0efd7326bd250ba53647e4f 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 Instance False Passed
4cb0eb594b18fe95a76716878749db9d5e747731 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 Instance True Passed
cdf71f9067cba4e381affd6843ed228b02080d05 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 Instance False Passed
678edab2cc009b1341a58654148eda06f795e9cb Apalache SetDiff Instance True Passed
1371de522c5bd3b80d018b026539587e5dd53f42 Apalache SetDiff Instance False Passed
991aeb9f3e43f5f1f7ab0807e143b0ee49f0eb75 Apalache SetUnion Instance True Passed
923fcac56b49ce935847350911b6158fbc610c3e Apalache SetUnion Instance False Passed
7f1f9f1d8ef4d88f4481cc908adfb7c7ca6e295f Apalache SetIntersect Instance True Passed
38dba3932fe344763345116e6a25860eca2f37f6 Apalache SetIntersect Instance False Passed
9e6b95f0ba1ad74a4eaf40ce7093489b1ad8d07e Apalache SubsetEq Instance True Passed
6cd6614060d3b99f07758e065bec47306793849b Apalache SubsetEq Instance False Passed
3cba2c78587524ea7b32e1dfdb66fcc1d15d6344 Apalache IfCond Instance True Passed
793f5a38f2d4583508a42c03a03ff28e4d770848 Apalache IfCond Instance False Passed
6dd2e6e75c573cfd915a885fda1b208286662d35 Apalache IfThen Instance True Passed
ceeff3cc5ce89751581092596b3b52cd0b209f99 Apalache IfThen Instance False Passed
56784229d6a87a89ae0478f8adcbeb962972f765 Apalache IfElse Instance True Passed
fe9b7bcad16212c83f0e17e1991fde8dba2f3beb Apalache IfElse Instance False Passed
09ea4063ec9c96d4a6625e8f4cf4024c6787bfa7 Apalache Subset Instance True Passed
56834f672aa888e4c060235a4215fd03dd2628a2 Apalache Subset Instance False Passed
842bd011cb878dac2b3d85d1a84c9dcf3e6eb55f Apalache Domain Instance True Passed
16bf96ae0fa0e8e85b2628dd36c67866e5a805f2 Apalache Domain Instance False Passed
64bff6315c47c00b73ed22774dec5958660019b6 Apalache Union Instance True Passed
84a75c71139536ce202d818112b8af98cf1aa7c1 Apalache Union Instance False Passed
b9fc716dc414c457bda393f396c72352a64ed398 Apalache Unchanged Instance True Passed
5c166d960f03709d8f54d6d02cc810bfeaf0fe91 Apalache Unchanged Instance False Passed
aba8f541a3d3fc73e54e091260b4403384d45b41 Apalache Equivalence Instance True Passed
ac8d8d3f0012a42a09d79f3a7f95f87c99c299fd Apalache Equivalence Instance False Passed
e688083bdca55ee16c92d1ca47078f984e50b104 Apalache SeqLen Instance True Passed
882eaa083a1042ce13cd72084b752f028a135c7c Apalache SeqLen Instance False Passed
1b890bacce3461f47b6ee4b4c3b47dd1ea347975 Apalache SeqConcat Instance True Passed
37398181ffb5accb598f9d1cbd46735834387522 Apalache SeqConcat Instance False Passed
5b1df1b1d0002ac86125807fb93a9d8fa884f2e4 Apalache SeqSeq Instance True Passed
fbc9e978faf15254706914ca25ff8a27c2df36db Apalache SeqSeq Instance False Passed
7ec257962e9b8bfb5e0aaa2d43c8abc8ef51a213 Apalache SeqSelectSeq Instance True Passed
6bcecbcf7e8c1225955e401f841dfd46583953e4 Apalache SeqSelectSeq Instance False Passed
04ec840541e29cbef2d15303d4f2c6530eebde14 Apalache SeqSubSeq Instance True Passed
88800836821f5fbf37aa9fdf72c15c355da03eaa Apalache SeqSubSeq Instance False Passed
b466bddc1d94d859e6299bf0e0c9aae125454981 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 Instance True Passed
4e7f5222ecb4a5b2fad1a02bc98109717dd769a5 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 Instance False Passed
a99ad677ea429d2f52993cef235759709d1cca40 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Instance True Passed
bbf32d0ad0506f64468357edf57aef64d9af74bb TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Instance False Passed
f49e049c64ff1bc4977c6fc765ef065fcdb02375 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 Instance True Passed
8c2668c029f53b341acd561dffb2b378acaa5364 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 Instance False Passed
b77881c29cf1f8a5cf66e43cea74de6de739041e TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Instance True Passed
a3faf681ff6bbdb47ce0c82761c309a2de2c35ab TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Instance False Passed
1137178f93e3932d6950d57e22dd3e65421744f1 TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq Instance True Passed
157c38d7c72c438dd110b6468e3dceb996d158ed TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq Instance False Passed
20d538933249ae49f9ff28729f7596ddcfedb742 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Instance True Passed
99f68b306227034f0a8785821808c6475c4fb5cc TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Instance False Passed
a76cd90a28014e49a5333562daa1cc1711f58a50 Apalache BagBagToSet Instance True Passed
842f5f10fa72f8573aada3f4a7f1b5e6c3ac22d1 Apalache BagBagToSet Instance False Passed
c48634b29961cbe6ea9b2658968ab03d9b2a7b6d Apalache BagSetToBag Instance True Passed
182efc506991d5b316d44363dc624e6bc8985dcb Apalache BagSetToBag Instance False Passed
ca5278e8f6d46c2d7216612302a65e9087758846 Apalache BagBagIn Instance True Passed
04557dc236d315023dcb3d101deecdfe225dcaa8 Apalache BagBagIn Instance False Passed
342d68194f8fa9aae51a096c262d92db60de8296 Apalache BagAddBag Instance True Passed
8f2ad57f296cbc5c083753d91b94a054358573d9 Apalache BagAddBag Instance False Passed
4b2652308aa452a32c64387fa724b02a4cbcbd86 Apalache BagBagSub Instance True Passed
b13e40f53a1ab356128d15148ff3b6c6b045260a Apalache BagBagSub Instance False Passed
4d7c0da52dd94b8d62bcea236c4077f91b1fd8f8 Apalache BagCopiesIn Instance True Passed
cfd2bf1155b84558b00e06885609b82b80464813 Apalache BagCopiesIn Instance False Passed
07060edac6904072402f221abbe60f5708f23c18 Apalache BagSubsetEqBag Instance True Passed
906fd8986a6558f41abba745ff31d102c7dcd25e Apalache BagSubsetEqBag Instance False Passed
24a3735c772bff443d3dcdb358c1a1cdae9b4f60 Apalache BagBagUnion Instance True Passed
29242e7e49647aada95f559ee656845dab464cc9 Apalache BagBagUnion Instance False Passed
23d1805364a358e9cb7cdcc4b71926e30f6a78b7 Apalache BagBagCardinality Instance True Passed
be7bfac41fcbaf875711f3210301540e6de3725c Apalache BagBagCardinality Instance False Passed
1ba2e2227e110ef1197792d1104f5df3feedc012 Apalache BagBagOfAll Instance True Passed
e348d864703c9861eb663190725262de56c4cdf8 Apalache BagBagOfAll Instance False Passed
cff815b56dee512244a5f6c4348239ba39e679b8 TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag Instance True Passed
85b8830d048eb3a18f353ebbea18ea46d5c79cb5 TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag Instance False Passed
28f4c073ee8e1a65a3daa11c2bba3ad8b66aa23d 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 Instance True Passed
c0075ebbf456cf270f49408a2646b503e9ab33f9 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 Instance False Passed
cd1d036d8cc6b3c83938f1102cd3879b71fa0ea1 Apalache FiniteSetsCardinality Instance True Passed
b4f9dece36ed057abf61962ab022ea2cb5bb5127 Apalache FiniteSetsCardinality Instance False Passed
929797852d5e84fb407024351f488da39f563a4a Apalache SeqHead Instance True Passed
b2098465432ddfcaa8c34c60031958dcdfd3dfcc Apalache SeqHead Instance False Passed
4c6b9059ffa94ded3c40f1fcbef6359ca1de214a Apalache SeqTail Instance True Passed
d64718ece31acac88b00e4f5820f2a4edff2235b Apalache SeqTail Instance False Passed
59df4c6287e4ab003d7ede2ae47a4b62a7ddd0c8 Apalache SeqAppend Instance True Passed
e68e7a509fdcae23c23cfa45463486c116d05f02 Apalache SeqAppend Instance False Passed