Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
9a5e3863bdbc237c337f081c9e7fe4cf4453725c Apalache And Let True Passed
f14fb5ed8ba02349ac0fca1e49adf786525979b0 Apalache And Let False Passed
a4d77a5af8d20fb01dffcf8fa65392cd878c7b1c TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Let True Passed
b2bbd1e4fbda3c2c934b85696806f2d305691470 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Let False Passed
05e2c017f740cb149aa1057fc5b8f398d6ce79d8 Apalache Imply Let True Passed
2aa02ab8be2109af112cc0a60557af2ad6dacd17 Apalache Imply Let False Passed
ad93bda5d89e18cc26be89f61f46fe743c8ead35 Apalache Not Let True Passed
4ab8f0a1fc5c254a61f4c0dbafbe84061a538c0c Apalache Not Let False Passed
43f8e8fee3a9d0eba39d7efa59eab937e8347c1f TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or Let True Passed
9ec75f2964635eebf21ac5269a9342f9a541953b TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or Let False Passed
df3addd7cdc79524e8ca9cce9e37527cff50992a TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine Let True Passed
489a67473641e0fe4f8646440bea8f7807c05d69 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine Let False Passed
613a91f14d6eabe8cf3a763e136e60f0bc92405d Apalache AndProp Let True Passed
3861a5a09c85f55a899b4408f782cb089fb7fff9 Apalache AndProp Let False Passed
1d44351a2f715b9df8ef545eb2a4e1061383d592 Apalache Boxed Let True Passed
c377f00ef97672465349b8c2b33ac1e66445e903 Apalache Boxed Let False Passed
3ccc55201f881efba3b0efbf2eabc5a203bc82e9 Apalache Eq Let True Passed
1c0eefaa83f5c7769f47f02f7bd607c7b9fc574d Apalache Eq Let False Passed
743d8048b33be94f69826b2cfe0f5ce0493f1cda Apalache Ne Let True Passed
7a6847241cdbef258412b0d0eebd661decac634a Apalache Ne Let False Passed
fd5bba37f7dcb973d109eba71e90d9b374214ac7 Apalache Let Let True Passed
3824cad01a99a912935462b68af6984838e52835 Apalache Let Let False Passed
c907133d532a08027e4dc85c6c48f3517fc3ffe2 Apalache Set0 Let True Passed
2091701479cfc47fe9b2800590fdbb98471ac477 Apalache Set0 Let False Passed
6e1968f3cf534514ac788385842d982143468ba6 Apalache Set1 Let True Passed
d5819d5ece9a56e371d887c4b3609ac8b5227cae Apalache Set1 Let False Passed
df1a355a5b933cb9ebdec21e06ed2388d2506016 Apalache Set2 Let True Passed
98bed916b5e1461502faeabe0e956910365b21ae Apalache Set2 Let False Passed
b8f577b3232cc73120b16055a0346a0adfcb4553 Apalache Fun Let True Passed
4079b34156db6041851127a06191d59f921b9671 Apalache Fun Let False Passed
cd830bd0efff8b79ab250cc90bcad631f1426adb Apalache In Let True Passed
8a65292e6e4ee5c1635cb407486d9a75a2139102 Apalache In Let False Passed
3426f7fc4e089e42ef5ac53bb75d34dc99385a48 Apalache NotIn Let True Passed
07470b03a2f545da2b2ec663005294e2d5eecb71 Apalache NotIn Let False Passed
5b2a3533162dff034d56036fffed406db9ba9967 Apalache Exists Let True Passed
3fa5ab0ba7bbc76f27a0607426319584f48b628a Apalache Exists Let False Passed
a651e1abbc3430395266b5e3a2c4605c6ef5cec3 Apalache Forall Let True Passed
fff3f5ed4e49ab0af8ad436d7121595b49ec7a39 Apalache Forall Let False Passed
2d63ed11de84a4bb94e3e7e63191b8b87fda08d3 Apalache Choose Let True Passed
aea48a836519e3ccfb96e5908e99e4248712ff27 Apalache Choose Let False Passed
272c9e9e5af40291e866b6dffe5a0819e4cd9e46 Apalache Record Let True Passed
babbd6b3336d63bef568069764a3b128fbfa76d3 Apalache Record Let False Passed
5f44d699383209dae983f7021b9d4e9963284ba7 Apalache Tuple Let True Passed
b06f363f7a7df14c778575e9b1c57d4f2d718755 Apalache Tuple Let False Passed
e779f6477b2718781087209699e7a8f06e2e9725 Apalache FunApp Let True Passed
c46c5e066b167212d1c83fd47a3eae78c29c2435 Apalache FunApp Let False Passed
af41682ebf577ba8fd4dd0e68cde6e4bf301d694 Apalache Except0 Let True Passed
043c0823202ce3fcc30d7c0e05f2ff16491e49f9 Apalache Except0 Let False Passed
ed1f4d51e70139e7a1e8d6b995d382b31a789141 Apalache Except1Fun Let True Passed
d27eb606dec72c536fbe157f7bc6c6edb74f4382 Apalache Except1Fun Let False Passed
0f2c443ecaeb4703f9715a3812ca07edf93a47e2 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Let True Passed
974b8bf2551d2e630ca32057e9fad618973debc1 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Let False Passed
f4c34b524c5937e1ce6d31808e013d4399f163aa Apalache Except1Rec Let True Passed
005a21fe1055b214e222e4a3794696bc3e9eaac7 Apalache Except1Rec Let False Passed
4490481a7ac1162638de351eb1607061ad444c9f TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Let True Passed
aed804059ecab539d00c557bfbe43541aa42ebc4 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Let False Passed
84a11bfe508d3c2ca7c51e27a2b9c35e06f2538e Apalache Except2Fun Let True Passed
65a8d83958a6d3571b44ef57bd99ef9ddee9e770 Apalache Except2Fun Let False Passed
1e8d54bcf155f547d761362c875b9d0bb8d7b3d1 Apalache Except2FunTuple Let True Passed
1fd66f8c8fac27c3c719b8e7f2ae6e1926e0ec69 Apalache Except2FunTuple Let False Passed
e15d6f9aad481d7076374e1715b0eb963e7616ea Apalache Prime Let True Passed
543027166735956225ab7db0092cc27956557499 Apalache Prime Let False Passed
ec94240ed58010540c10a268a8b0816194a05360 Apalache NumUnaryMinus Let True Passed
df9664948fa7f41769b08216273b5874e620fc1f Apalache NumUnaryMinus Let False Passed
2ac3b32246d0f7e9bfd696583655714cab2a4113 Apalache NumPlus Let True Passed
fa2e9e21dd88c7c82bea74631767088d44d7bfd3 Apalache NumPlus Let False Passed
8fb7553c246bf8e3e70985e5ff5d29d597f29a7d Apalache NumMinus Let True Passed
4568555ca676e3e284e84ea2da28f0ef28006ae5 Apalache NumMinus Let False Passed
f5470e1a530041826c29e3186120570341b207d5 Apalache NumMul Let True Passed
d88ffd09d1fafb680f11eafbd7107bd9e478b340 Apalache NumMul Let False Passed
141d24dfd5b99d9b08e5fe9604e9180d8b83506a Apalache NumDiv Let True Passed
13ff87a457b221e778ea2d0694f866c48c0192e5 Apalache NumDiv Let False Passed
095b74a3d98759a6e523a55b4bb63bae6641cd39 Apalache NumMod Let True Passed
4db00a8e7af1fc25c7bb7b77ccb47a722d63b1da Apalache NumMod Let False Passed
69b49d4d371f9bf9634c4f4a1423973066c2c13b Apalache NumPow Let True Passed
50ead2819b482124b1dabfbe42b4dc1b62cc42aa Apalache NumPow Let False Passed
f0f62d2d2d81395411356eea3e6d6a580f6068c3 Apalache NumGt Let True Passed
7a79dcb52f2ae259c974a01f2ed792500ef15fba Apalache NumGt Let False Passed
da0ccbe6641dd8bc140c734802e5de10d2fd7674 Apalache NumGe Let True Passed
2ea9651af29a03db9fdb78acaa4e3b4d27c17ad8 Apalache NumGe Let False Passed
cda03521c89623ee5d34458478a4213fd26712e5 Apalache NumLt Let True Passed
15989815a9c311a8545b8fe9d1cbe2711341e693 Apalache NumLt Let False Passed
9a5706208a925594f16ef35936b1a221cd874c91 Apalache NumLe Let True Passed
69e939ac771a43c97e23c02d070cd12b5b027ddc Apalache NumLe Let False Passed
06bc6ffae460b4d0d8accc6bee84bcbccca69672 Apalache DefFun Let True Passed
acb67a134c0892c45dab739fc6ef2af05557ab5b Apalache DefFun Let False Passed
5772072deefc46afb7de8f46a9cbbf9c4246fe84 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Let True Passed
97d6915d61a85403a3cb0ed9d591d125afe51db8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Let False Passed
280da4d3753ead18c4ab4c27092b117cd0e37e09 Apalache DefFunRecursive Let True Passed
84e03a501d20f691179b6d468a915fded5dac89e Apalache DefFunRecursive Let False Passed
3e41e38a2a44d1c6db6f94536e3a76c052d05ca5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Let True Passed
51721c754db142855ffb06af3045d45e94a8ecd5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Let False Passed
6eaf62cb073d4b836e47eb3a0548c5f1fe80ba4e Apalache Def0 Let True Passed
32298417b45e969e21bfcdefbe4b99a5ea2ea4bb Apalache Def0 Let False Passed
d0364d21e6c99192f891cdbb2ccdc78841b442ac TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Let True Passed
c363b39269a9de4b14b0c43aaa7906f1a2c982ad TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Let False Passed
275dd483d9ef6cd4cf8e87ebd6945eddd892dc19 Apalache Def1 Let True Passed
bc4423d71190f984db3cfa49207e68ecb1ca86e6 Apalache Def1 Let False Passed
22f80d73c46a9a5f757a1fa39e5bb5245e48c6bf TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Let True Passed
fc3d0bab8f467b824a34552f075b7f9a70d7bcb8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Let False Passed
22911c9ab54123c87c28cb2c0e726af2885ac4d2 Apalache Def2 Let True Passed
ada3394cc53eb7f77a09e64bcbf2a38cd07124af Apalache Def2 Let False Passed
0e9a1291e0008fb0293669e2a50d9cd8b63226f2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Let True Passed
b36b1d8365fd3534ad587e3a9087ec93dd25fcc9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Let False Passed
334adb6f6e8778fd470d27705d44a646703eb57d Apalache Def1Recursive Let True Passed
eca83004c2c921750bb94f3825d125c8bf0f37ec Apalache Def1Recursive Let False Passed
035a2d72df1331553632c0ca7d14552e53e69756 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Let True Passed
a68be952a827fa04ba1a3d193a98d52477ba0eef TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Let False Passed
5f55331a470819da7a81cc4250fd750a3b32f053 Apalache Extends Let True Passed
43fc56cc479dabaaa2eaae8e832ecea11f759d1f Apalache Extends Let False Passed
7e61d152b6fc0e37026289a8e1f4a518d43ad142 Apalache ExtendsInDifferentFolder Let True Passed
984b0f6d191de4a21f7323d9a234c135898550b8 Apalache ExtendsInDifferentFolder Let False Passed
0321e7454ac0d76f700030c5d5eb9187602e5738 Apalache Variable Let True Passed
d536ca2e41328507fd41c16a5a3ac078f78f7fd7 Apalache Variable Let False Passed
888b06200df026ec436fe1702af52d7f65abdb31 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Let True Passed
e6380b2efc6f39746fd90a8b8e36bec0f0862a8d TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Let False Passed
d9d4b1e57236056d92b1acaadfcd2add76dee40c Apalache Constant Let True Passed
6eae32dcaedf5e37e8cb819cd038ff7e5012cf5e Apalache Constant Let False Passed
c7f2c8b838e8bd65dbb241ccc3a851cb1da6d05c Apalache ConstantRank1 Let True Passed
b93a6b2cb6a78bc76c92929da81bbb4de682e8aa Apalache ConstantRank1 Let False Passed
451436f1b15cd72ed0b3e9289ed9f50d461d6d87 Apalache Instance Let True Passed
c029294473543fddb2bebd271ac89db54f19620f Apalache Instance Let False Passed
137f03d7edf87a4484629b677dccbe7c8de8a4d0 Apalache InstanceWith Let True Passed
ab6ae72640a6054ef6a01160b4ba0a776a3be156 Apalache InstanceWith Let False Passed
7dee05f550335a0ee150d822c65640aaa5c98393 Apalache InstanceNamed Let True Passed
bace87aa8574ed65787578c92c5692ddb16842c5 Apalache InstanceNamed Let False Passed
d0f76ae1d20a09d2a6bdbba9128d812f4ea1e8cb Apalache InstanceNamedWith Let True Passed
7f86b88c3eca00bea8715e457cf70a5605afecd3 Apalache InstanceNamedWith Let False Passed
008cdf52840f46610f01114867f4cccd95264b8d Apalache InstanceInFolder Let True Passed
079aee035a9296706d36672e7a1ab75bf43a336a Apalache InstanceInFolder Let False Passed
d88ffea98598a259623984522f03f9f146a35405 Apalache InstanceWithInFolder Let True Passed
a9f258632468250efdfa4e66bf49e8a208760fa3 Apalache InstanceWithInFolder Let False Passed
2b31750cef4bedc0b94576fe946e1589ba207f6a Apalache InstanceNamedInFolder Let True Passed
65acd75f266bb09f1a1760325de5c78792015cf5 Apalache InstanceNamedInFolder Let False Passed
c125e747229df03dddbe9b01ee29749d00ad5a8c Apalache InstanceNamedWithInFolder Let True Passed
be1d28ee067b873c5408588687ac221778818cf2 Apalache InstanceNamedWithInFolder Let False Passed
e787fd1072947590c5fa8f048cc526f29ab1d7cc Apalache Enabled Let True Passed
14a8952437c5e540aa9538e75cb386d372b4bf5e Apalache Enabled Let False Passed
af51207f3a842721866d61e8c130eb309e4df84b Apalache Assume Let True Passed
cb19c183b03f8f7c5283c5d353351815e5a1a71a Apalache Assume Let False Passed
15df0ece8aa5e70715521bfb6615a515a4672124 Apalache AssumeNamed Let True Passed
982a328909dc2c857bc9825a7106acbdffc44459 Apalache AssumeNamed Let False Passed
e5b044149ebbc21ca8f7114d6f8631bb447f2f5f Apalache Lambda Let True Passed
3494b027929168b299115d7adeb0f3df138f5b90 Apalache Lambda Let False Passed
412cde423e6452b037febc099a89486a02c2ae80 Apalache Cross2 Let True Passed
fc8319732e1b214b93a705de1fa72ea0c35e3a99 Apalache Cross2 Let False Passed
15d70c98a8b4185feb58ce064a4fc50cec433833 Apalache Cross3 Let True Passed
34135523d889da35542717d90cfb37c9741d3865 Apalache Cross3 Let False Passed
441b3b2ec04c56421dafe9b5c0013dbee959845d 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 Let True Passed
2589bab88fe29ad3f473d735e17f97bbe75b433e 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 Let False Passed
e78903a76a7a7714eeb5cb1d3128439d1ba45a0f 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 Let True Passed
2de7fc7fb0dc0ef3938357c71d5c2564bea7a918 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 Let False Passed
5cd0d00aac8c6c3eb78379bcb50caf862b3d4aae Apalache SetDiff Let True Passed
29673f1eae00123d768df6b4c88bd2d70aadf487 Apalache SetDiff Let False Passed
0962e39f811d6e7be63b811a097d682703251d66 Apalache SetUnion Let True Passed
c5e5e1b73a40a39c4d69e39fd9222ce7d82bc3bf Apalache SetUnion Let False Passed
328e0e80c5363c0b9684e4814d9473a25198e773 Apalache SetIntersect Let True Passed
e44d0756dbcefca492e02356f9761a3f0c3f02de Apalache SetIntersect Let False Passed
106fac0428ee39a3732484eae971d1411ca71c65 Apalache SubsetEq Let True Passed
ba5f33ccd9a3533bbe44695553afea02a8fd99bd Apalache SubsetEq Let False Passed
275c3394e5f5080547c33724dc884318b7ec3a4c Apalache IfCond Let True Passed
62636e30487f3992bdbe752070ac45afe1b3910b Apalache IfCond Let False Passed
20fadf5a0766645024a836236aefba00f78b4b34 Apalache IfThen Let True Passed
a714a6965268547ee2ab13402d3d66afe28b0957 Apalache IfThen Let False Passed
64e3117a356acbbd19cd880531983f6ca2149b78 Apalache IfElse Let True Passed
fc4fd3b12dcef2d9113f5687b35ca0dea6a0e150 Apalache IfElse Let False Passed
167dc31d64d9a8550b33ef3b7a819426f911fdab Apalache Subset Let True Passed
597a84f873b795ecf4fada528d03a668f1080ba8 Apalache Subset Let False Passed
498b34db27febf443af0bdea731f6108d761ecd0 Apalache Domain Let True Passed
499bf05fae91fda8b6ce3516aa85c42abfc865ea Apalache Domain Let False Passed
60318e733a0f70bd5b748c7d8080d1bfc1b35cb5 Apalache Union Let True Passed
69545560cbfe8547d92c5dbededed5e061110ed9 Apalache Union Let False Passed
003334938af7ce3cb5790a15f71e4dfcb968ff40 Apalache Unchanged Let True Passed
507babf81908513f9989538f2522016d589591c3 Apalache Unchanged Let False Passed
2dd4ecba7b3867ec81f264736f64d9ba7c4e5186 Apalache Equivalence Let True Passed
b44ad948a1eff03467f37cb2206239be8dd08e02 Apalache Equivalence Let False Passed
1af1afe1855356e42bda1c8563dd09295d8a7c31 Apalache SeqLen Let True Passed
473547cb759a719860d5b458441169c51969b48d Apalache SeqLen Let False Passed
73d187d88a9c06e2d62d8e0728e593eb220d32db Apalache SeqConcat Let True Passed
3e5002fb791b1dd8331256ce1a0bb6a237175162 Apalache SeqConcat Let False Passed
9eff50885eceeef15b93ad460aa5ef124822d9e9 Apalache SeqSeq Let True Passed
4c6773c89039a78b51cdf9e6fad4b459272e4c43 Apalache SeqSeq Let False Passed
2d8b5849cb8ce685b1f02b84b4b9547428e6eb23 Apalache SeqSelectSeq Let True Passed
da4bf95736c5ae79e4cc1ed402e29ee1091efe2b Apalache SeqSelectSeq Let False Passed
d1e747ec3c7a5c9d6fb06c3ac566da6d57992a74 Apalache SeqSubSeq Let True Passed
766b5df459c36e496a923d08dc7b11ceb603ef40 Apalache SeqSubSeq Let False Passed
0b6c107e48cb51ccaee178196743993ac1cf158e 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 Let True Passed
1347a9f6b97f13aa30aa49c86bf7ea975ba511d3 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 Let False Passed
4cbea1160b877bbc64e2e5be77cb65fb62df0986 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Let True Passed
de41710e9a98d3da215cd24b9da210fa04a80926 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Let False Passed
4829cf6f55f2d93b3ed8ee6839c2f3cc364c7834 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 Let True Passed
89cc825fafb7209ff8a99513f1e9f1ccc4689faa 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 Let False Passed
086f17286213ac6e00b1419519273b6e0a6cc32b TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Let True Passed
b75d5b5863d79fb8a5620f5fe8b4689886b33f26 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Let False Passed
59e8c31d818df659e5bf9d974bd5d446f941884e TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq Let True Passed
9d2385f55b65d5b54c7c15cc1824cc7d012115f9 TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq Let False Passed
0066fe48f7c9cd549262ea1487353628101b7a95 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Let True Passed
2fc25103b839389d551bf788ff7abf1a9f44d221 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Let False Passed
4505d27297a66e25cd2a21317f10186ac3d514a8 Apalache BagBagToSet Let True Passed
2f2d2e7e8e6f2e76b5b3e2c9500f881c699b6a70 Apalache BagBagToSet Let False Passed
abd4666373642111302c4cc85ce8884f0bd62d24 Apalache BagSetToBag Let True Passed
f07f9177511d7b556c04917ff0cc46ec232c3363 Apalache BagSetToBag Let False Passed
07978bbb3a0b68031b1daf99196ba661154c1880 Apalache BagBagIn Let True Passed
7cbfe20373528a5717db2be7ae2a890e183a8390 Apalache BagBagIn Let False Passed
574126e4e2810b5c87a82387a7666ae51cc339d9 Apalache BagAddBag Let True Passed
0990fcdb9c1918dbbddfa488d5e99949abbffd98 Apalache BagAddBag Let False Passed
7bbc1c1cb749b8b46b8ab0711dca2b01c01ec229 Apalache BagBagSub Let True Passed
3bacd82867af22fc43961e134eafe30ba8b24d12 Apalache BagBagSub Let False Passed
dd06f89571a7bb26781a18012e2424f27186e50d Apalache BagCopiesIn Let True Passed
608e429a39c4c056f5423e21c114cc88b5f90a79 Apalache BagCopiesIn Let False Passed
b6a76a0c7e664e4a323ff03708e59232d7a86429 Apalache BagSubsetEqBag Let True Passed
d6b7a982b2f1e30555010acf6d89c2c30d870c5e Apalache BagSubsetEqBag Let False Passed
e85d3595e16e59946d334285c08ea468fde49d20 Apalache BagBagUnion Let True Passed
228a22caa0e202497206363ae2dacfcc897051f0 Apalache BagBagUnion Let False Passed
d23d2977f426782ddfb9489011a25917f320f813 Apalache BagBagCardinality Let True Passed
2d79429c6a6626f97796f5590a63a3a0ea2fb990 Apalache BagBagCardinality Let False Passed
e21bc4f151079f2416c9e557a1e68a91244a38aa Apalache BagBagOfAll Let True Passed
fb243582415daad8316da15870e51b5a6be7c48b Apalache BagBagOfAll Let False Passed
9b86abbe47542a7a2eebbf31eb6eb2e43e49c289 TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag Let True Passed
9104c0ca2640ce20760feb026aafbab9dca024df TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag Let False Passed
ca2a3a0a77287beace6f7217e51b189a667aa07d 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 Let True Passed
9df8cb4da00452f5d006dd65b8f593bab1ab0521 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 Let False Passed
9f0af8c71778d9933edad9c6b2d360b151c7794d Apalache FiniteSetsCardinality Let True Passed
39db5ee4ee4789cd932b08e4292f5fdd9ce0313e Apalache FiniteSetsCardinality Let False Passed
e611a1c56dde5c52048bc3bc7c55e4d1b86cb75e Apalache SeqHead Let True Passed
0b30731273b7a700d1527f6bd227d81ace20d9c2 Apalache SeqHead Let False Passed
32da7a832813b1cdf53d9b2e2e576c30e6048c5f Apalache SeqTail Let True Passed
7b26be91c74e03878217185d34a8402215f0e760 Apalache SeqTail Let False Passed
4c638b305246399b6685937096a2daf0356b7e3c Apalache SeqAppend Let True Passed
14b7ca60954ee2909acea0460c85053364025fe3 Apalache SeqAppend Let False Passed