%run FixedPoint.ipynb

def arb(M):
    for x in M:
        return x
    assert False, 'Error: arb called with empty set!'

"""
Explanation: Minimizing a <span style="font-variant:small-caps;">Fsm</span>
End of explanation
"""


def cart_prod(A, B):
    return { (x, y) for x in A for y in B }

"""
Explanation: The function cart_prod(A, B) computes the Cartesian product $A \times B$ of the sets $A$ and $B$ where
$$ A \times B := { (x, y) \mid x \in A \wedge y \in B }. $$
End of explanation
"""


def separate(Pairs, States, Σ, 𝛿):
    Result = { (q1, q2) for q1 in States
                        for q2 in States
                        for c  in Σ 
                        if (𝛿[q1, c], 𝛿[q2, c]) in Pairs
             }
    return Result

"""
Explanation: This function takes three arguments:
- Pairs  a set Pairs of pairs of states from some <span style="font-variant:small-caps;">Fsm</span> $F$.
   If $(p_1, p_2) \in \texttt{Pairs}$, then $p_1$ and $p_2$ are known to be separable,
- States is the set of states of the <span style="font-variant:small-caps;">Fsm</span> $F$,
- Sigma  is the alphabet of the underlying <span style="font-variant:small-caps;">Fsm</span> $F$.
The function separate(Pairs) computes the set of pairs of states $(q_1, q_2)$ that are separable because there is some
$c \in \Sigma$ such that 
$$\delta(q_1,c) = p_1, \quad \delta(q_2,c) = p_2. $$
End of explanation
"""


def find_equivalence_class(p, eqClasses):
    return arb({ C for C in eqClasses if p in C })

"""
Explanation: Given a state $p$, find the equivalence class of $p$.  Here, eqClasses is a set of sets of states.
End of explanation
"""


def minimize(F):
    States, Σ, 𝛿, q0, Accepting = F
    States       = fixpoint({q0}, lambda q: { 𝛿[q, c] for c in Σ })
    Separable    = cart_prod(States - Accepting, Accepting) | \
                   cart_prod(Accepting, States - Accepting)
    AllSeparable = fixpoint2(Separable, lambda Pairs: separate(Pairs, States, Σ, 𝛿))
    Equivalent   = cart_prod(States, States) - AllSeparable
    EquivClasses = { frozenset({ p for p in States if (p, q) in Equivalent })
                     for q in States 
                   }
    newQ0        = arb({ M for M in EquivClasses if q0 in M })
    newAccept    = { M for M in EquivClasses if arb(M) in Accepting }   
    newDelta         = {}
    for q in States:
        for c in Σ:
            p = 𝛿.get((q, c))
            if p != None:
                classOfP = find_equivalence_class(p, EquivClasses)
                classOfQ = find_equivalence_class(q, EquivClasses)
                newDelta[(classOfQ, c)] = classOfP
            else:
                newDelta[(classOfQ, c)] = frozenset()
    return EquivClasses, Σ, newDelta, newQ0, newAccept

"""
Explanation: The function minimize(A) takes a deterministic 
<span style="font-variant:small-caps;">Fsm</span> F as its input.
Here F is a 5-tuple of the form
$$ F = (Q, \Sigma, \delta, q_0, A) $$
The algorithm performs the following steps:
1. All unreachable states are eliminated.
2. All accepting states are separated form all non-accepting states.
3. States are separated as long as possible.
   Two states $p_1$ and $p_2$ are separable if there is a character 
   $c \in \Sigma$ such that 
   $$\delta(p_1,c) = q_1, \quad \delta(p_2,c) = q_2, \quad \textrm{and} \quad
     \mbox{$q_1$ and $q_2$ are separable.}
   $$
4. States that are not separable are equivalent and are therefore identified and grouped
   in equivalence classes.
End of explanation
"""


