# Merging Functions

In addition to general debugging tools, extending TLC adds two function operators:

• a :> b is the function [x \in {a} |-> b], or the function that maps a to b.
• f1 @@ f2 merges both functions into a new one with the same domain and values. If some element is in both domains, it uses f1.

@@ in particular is a great tool for simplifying PlusCal specs. As a toy example, imagine we have a sequence of digits and want to count the number of occurrences of each digit. Here’s one way to write that:

EXTENDS TLC, Integers, Sequences, FiniteSets

Digits == 0..9
Count(seq) ==
[x \in Digits |-> Cardinality({y \in DOMAIN seq: seq[y] = x})]

(* --algorithm counter

variables seq \in [1..5 -> Digits],
counter = [x \in Digits |-> 0],
pos = 1;

begin
while pos <= Len(seq) do
counter[seq[pos]] := counter[seq[pos]] + 1;
pos := pos + 1;
end while;
assert counter = Count(seq);
end algorithm; *)


That works, but what if instead of a sequence of digits, it was a sequence of sets of digits? The solution gets a little messy (and the state space is much larger):

Digits == 0..2
Count(seq) ==
[x \in Digits |-> Cardinality({y \in DOMAIN seq: x \in seq[y]})]

(* --algorithm counter

variables seq \in [1..5 -> SUBSET Digits],
counter = [x \in Digits |-> 0],
pos = 1;

begin
while pos <= Len(seq) do
counter := [
x \in Digits |->
IF x \in seq[pos]
THEN counter[x] + 1
ELSE counter[x]
];
pos := pos + 1;
end while;
assert counter = Count(seq);
end algorithm; *)


With @@, we can make the assignment much cleaner:

counter := [x \in seq[pos] |-> counter[x] + 1] @@ counter;