A simple implementation of the bisimulation algorithm with verification.

bisim_alg.py

"""A simple implementation of the bisimulation algorithm with verification.

The bisimulation algorithm discovers pairs of states that are bisimilar. This
itself is the bisimulation relation <->.

LICENSE
-------
This is free and unencumbered software released into the public domain.

Anyone is free to copy, modify, publish, use, compile, sell, or
distribute this software, either in source code form or as a compiled
binary, for any purpose, commercial or non-commercial, and by any
means.

In jurisdictions that recognize copyright laws, the author or authors
of this software dedicate any and all copyright interest in the
software to the public domain. We make this dedication for the benefit
of the public at large and to the detriment of our heirs and
successors. We intend this dedication to be an overt act of
relinquishment in perpetuity of all present and future rights to this
software under copyright law.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY CLAIM, DAMAGES OR
OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
OTHER DEALINGS IN THE SOFTWARE.

For more information, please refer to <https://unlicense.org/>
"""

import itertools
from typing import Iterable, NamedTuple, Optional

from itertools import chain, combinations


class Transition(NamedTuple):
    """Encodes a transition from source via label to sink"""

    source: str
    label: str
    sink: str


class LTS:
    """Non-deterministic, finite Labelled Transition System."""

    def __init__(
        self, states: set[str], labels: set[str], transitions: set[Transition]
    ) -> None:
        self._states = states
        self._labels = labels
        self._transitions = transitions

    @property
    def states(self) -> set[str]:
        return self._states

    @property
    def labels(self) -> set[str]:
        return self._labels

    def transition(self, state: str, label: str) -> Iterable[str]:
        """Generator for each sink state reachable from state, via transition."""
        for transition in self._transitions:
            if transition.source == state and transition.label == label:
                yield transition.sink

    def transition_exists(self, source: str, label: str, sink: str) -> bool:
        """Checks if a transition between two points via  given label exists."""
        return Transition(source, label, sink) in self._transitions


class BinaryRelation:
    """Implements a non-symmetric binary relation."""

    def __init__(self, iterable: Iterable[tuple[str, str]]) -> None:
        self._br = set(iterable)

    def __str__(self) -> str:
        return str(self._br)

    def pairs(self) -> Iterable[tuple[str, str]]:
        """Iterates through each tuple in the binary relation."""
        yield from self._br

    def related(self, x, y) -> bool:
        """Checks if a pair exists in the binary relation."""
        return (x, y) in self._br

    def transpose(self) -> "BinaryRelation":
        """Creates a new binary relation with transposed values."""
        return BinaryRelation(transpose(self._br))

    def remove(self, x: str, y: str) -> None:
        self._br.remove((x, y))

    def clone(self) -> "BinaryRelation":
        return BinaryRelation(self._br.copy())

    def __eq__(self, value: object, /) -> bool:
        if isinstance(value, BinaryRelation):
            return set(self.pairs()) == set(value.pairs())
        return False


def formal_qprime_search(
    pprime: str, q: str, lmbda: str, lts: LTS, br: BinaryRelation
) -> bool:
    """Implements the consequent of the following if statement:

    If p {a}{→}  p', then there is q {a}{→} q' such that (p', q') ∈ R
    """
    for qprime in lts.transition(q, lmbda):
        if br.related(pprime, qprime):
            print(f"{q} -{lmbda}> {qprime} && ({pprime}, {qprime}) in R")
            return True
    return False


def formal_pprime_search(
    qprime: str, p: str, lmbda: str, lts: LTS, br: BinaryRelation
) -> bool:
    """Implements the consequent of the following if statement:

    If q {a}{→}  q', then there is p {a}{→} p' such that (p', q') ∈ R
    """

    for pprime in lts.transition(p, lmbda):
        if br.related(pprime, qprime):
            print(f"{p} -{lmbda}> {pprime} && ({pprime}, {qprime}) in R")
            return True
    return False


def formal_definition_one_directional_simulation(lts: LTS, br: BinaryRelation) -> bool:
    """Implements the wikipedia definition of bisimulation in a single direction (simulation).

    R is a simulation if for every pair of states (p, q) ∈ R and all labels a ∈ L:
     - If p {a}{→}  p', then there is q {a}{→} q' such that (p', q') ∈ R
    """

    # for every pair of states (p, q) in R
    for p, q in br.pairs():
        # for all labels lambda in L
        for lmbda in lts.labels:
            # if p lambda trans to p'
            for pprime in lts.transition(p, lmbda):
                if not formal_qprime_search(pprime, q, lmbda, lts, br):
                    return False
    return True


def formal_definition_trans_directional_simulation(
    lts: LTS, br: BinaryRelation
) -> bool:
    """Implements the wikipedia definition of bisimulation in a single direction (simulation).

    R is a simulation if for every pair of states (p, q) ∈ R and all labels a ∈ L:
     - If q {a}{→}  q', then there is p {a}{→} p' such that (p', q') ∈ R
    """
    # for every pair of states (p, q) in R
    for p, q in br.pairs():
        # for all labels lambda in L
        for lmbda in lts.labels:
            # if q lambda trans to q'
            for qprime in lts.transition(q, lmbda):
                if not formal_pprime_search(qprime, p, lmbda, lts, br):
                    return False
    return True


def formal_definition_bisimulation(lts: LTS, br: BinaryRelation) -> bool:
    """Implements the wikipedia definition of bisimulation in a single direction (simulation).

    R is a bisimulation if and only if for every pair of states (p, q) ∈ R and all labels a ∈ L:
     - If p {a}{→}  p', then there is q {a}{→} q' such that (p', q') ∈ R
     - If q {a}{→}  q', then there is p {a}{→} p' such that (p', q') ∈ R
    """
    return formal_definition_one_directional_simulation(
        lts, br
    ) and formal_definition_trans_directional_simulation(lts, br)


def transpose(iterable: Iterable[tuple[str, str]]) -> Iterable[tuple[str, str]]:
    return ((y, x) for x, y in iterable)


def test_binary_relation(lts: LTS, br: BinaryRelation):
    if formal_definition_one_directional_simulation(lts, br):
        print("works in the p -> p' direction")
    if formal_definition_trans_directional_simulation(lts, br):
        print("works in the q -> q' direction")
    if formal_definition_one_directional_simulation(lts, br.transpose()):
        print("works in the q -> q' direction (via transpose)")
    if formal_definition_trans_directional_simulation(lts, br.transpose()):
        print("works in the p -> p' direction (via transpose)")
    if formal_definition_bisimulation(lts, br):
        print(f"{br} is a bisimulation (via wikipedia def.)")
    if formal_definition_bisimulation(lts, br.transpose()):
        print(f"{br} is a bisimulation (via transp. wikipedia def.)")


def tilde_0(
    iterable: Iterable[str],
) -> set[tuple[str, str]]:
    """Produces the binary relation elements for the most coarse equivalence relation."""
    return set(itertools.product(iterable, iterable))


def check_x_y_valid(lts: LTS, tn: BinaryRelation, x: str, y: str) -> bool:
    for a in lts.labels:
        for xprime in lts.transition(x, a):
            if not formal_pprime_search(xprime, y, a, lts, tn):
                print("  Failed pprime search")
                return False
        for yprime in lts.transition(y, a):
            if not formal_qprime_search(yprime, x, a, lts, tn):
                print("  Failed qprime search")
                return False
    return True


def bisimulation_algorithm_step(lts: LTS, tn: BinaryRelation) -> BinaryRelation:
    tn_inc = tn.clone()
    for x, y in tn.pairs():
        print(x, y)
        if not check_x_y_valid(lts, tn, x, y):
            print(f"    Removing: {x, y}")
            tn_inc.remove(x, y)

    return tn_inc


def bisimulation_algorithm(lts: LTS) -> BinaryRelation:
    tn = BinaryRelation(tilde_0(lts.states))
    tn_inc = bisimulation_algorithm_step(lts, tn)
    i = 1
    while tn != tn_inc:
        i += 1
        print(f"Step: {i}")
        tn = tn_inc
        tn_inc = bisimulation_algorithm_step(lts, tn)
    return tn


def test_bisimulation_algorithm(lts: LTS) -> None:
    bisim_result = bisimulation_algorithm(lts)
    print(bisim_result)
    print(formal_definition_bisimulation(lts, bisim_result))


def main() -> None:
    # LTS with a bisimulation on any of the nodes.
    lts = LTS(
        {"x", "x1", "x2", "x3"},
        {"a"},
        {
            Transition("x", "a", "x1"),
            Transition("x1", "a", "x2"),
            Transition("x2", "a", "x3"),
        },
    )
    test_bisimulation_algorithm(lts)

    # LTS with a bisimulation x <-> y

    lts2 = LTS(
        {"x", "x1", "x3", "y", "y1", "y2"},
        {"a", "b"},
        {
            Transition("x", "a", "x1"),
            # Transition("x", "a", "x2"),
            Transition("x1", "b", "x3"),
            Transition("y", "a", "y1"),
            Transition("y1", "b", "y2"),
        },
    )
    test_bisimulation_algorithm(lts2)

    # LTS without a bisimulation x <-> y
    lts3 = LTS(
        {"x", "x1", "x2", "x3", "y", "y1", "y2"},
        {"a", "b"},
        {
            Transition("x", "a", "x1"),
            Transition("x", "a", "x2"),
            Transition("x1", "b", "x3"),
            Transition("y", "a", "y1"),
            Transition("y1", "b", "y2"),
        },
    )

    test_bisimulation_algorithm(lts3)


if __name__ == "__main__":
    main()