Module probabilistic_automata.utils

Expand source code
from operator import itemgetter as ig

import funcy as fn
from lenses import bind
from dfa import ProductAlphabet

from probabilistic_automata import pa as PA


def _encode_two_player_game(mapping):
    """Convert transition probabilities from state to two player game
    transition and distribution.

       mapping: State => (Action => (State => Prob))

    where (=>) denotes a Dictionary map.
    """
    e_size = 0  # Environment Alphabet Size.

    def reindex(state2prob):
        """Enumerates states and transforms the mapping:
           State => Prob
        to a mapping:
           Index => (State, Prob)
        """
        nonlocal e_size
        e_size = max(e_size, len(state2prob))

        return {i: (s, p) for i, (s, p) in enumerate(state2prob.items())}

    # State => (Action => (EnvironmentAction => (State, Prob)))
    mapping = bind(mapping).Values().Values().modify(reindex)

    def transition(state, composite_action):
        sys, env = composite_action
        dist = mapping[state][sys]

        if env not in dist:  # Probability 0 event.
            return state
        return dist[env][0]

    def env_dist(state, sys):
        return {e: p for e, (_, p) in mapping[state][sys].items()}

    return {
        "env_inputs": range(e_size),
        "transition": transition,
        "env_dist": env_dist,
    }


def dict2pdfa(mapping, start: PA.State):
    """Convert nested dictionary into a PDFA.

    - mapping is a nested dictionary of the form:

       mapping = {
         <State>:  (<Label>, {
            <Action>: {
                <State>: <Probability>
            }
         }
       }
    """
    label_map = fn.walk_values(ig(0), mapping)
    transition_map = fn.walk_values(ig(1), mapping)

    outputs = set(bind(mapping).Values()[0].collect())
    inputs = set(bind(mapping).Values()[1].Keys().collect())

    return PA.pdfa(
        start=start,
        label=label_map.get,
        inputs=inputs,
        outputs=outputs,
        **_encode_two_player_game(transition_map)
    )


def pdfa2dict(pdfa):
    """Convert PDFA into nested dictionary of the form:

       mapping = {
         <State>:  (<Label>, {
            <Action>: {
                <State>: <Probability>
            }
         }
       }

    Returns: mapping and the start state.
    """
    mapping = {}
    for s in pdfa.states():
        action2state_prob = {
            a: pdfa.transition_probs(s, a) for a in pdfa.inputs
        }

        label = pdfa.dfa._label(s)
        mapping[s] = (label, action2state_prob)
    return mapping, pdfa.start


def prob_pred(dyn, *, pred, horizon) -> float:
    """
    Return the probability that pred will evaluate to true before
    horizon time step assuming system inputs are applied uniformly at
    random.
    """
    prob = {}

    def pevent(state, path_prob, time):
        nonlocal prob
        assert time >= 0

        if state in prob:
            return path_prob * prob[state]
        elif pred(state):
            prob[state] = 0
            return 1
        elif time == 0:
            return 0

        acc = 0
        for action in dyn.inputs:
            for state2, state2_prob in dyn._probs(state, action):
                acc += pevent(state2, path_prob * state2_prob, time - 1)

        return acc / len(dyn.inputs)

    return pevent(dyn.start, path_prob=1, time=horizon)


def tee(left, right):
    """Parallel composition of left and right sharing inputs."""
    if left.inputs <= right.inputs:
        inputs = left.inputs
    elif right.inputs <= left.inputs:
        inputs = right.inputs
    else:
        raise RuntimeError("Inputs need to be compatible")

    def transition(s, composite_input):
        sys_input, (env_l, env_r) = composite_input
        state2_l = left.dfa._transition(s[0], (sys_input, env_l))
        state2_r = right.dfa._transition(s[1], (sys_input, env_r))
        return (state2_l, state2_r)

    def env_dist(composite_state, action):
        state_l, state_r = composite_state

        return PA.ProductDistribution(
            left=left.env_dist(state_l, action),
            right=right.env_dist(state_r, action),
        )

    return PA.pdfa(
        start=(left.start, right.start),
        inputs=inputs,
        transition=transition,
        label=lambda s: (left._label(s[0]), right._label(s[1])),
        outputs=ProductAlphabet(left.outputs, right.outputs),
        env_dist=env_dist,
        env_inputs=ProductAlphabet(left.env_inputs, right.env_inputs),
    )

Functions

def dict2pdfa(mapping, start)

Convert nested dictionary into a PDFA.

  • mapping is a nested dictionary of the form:

mapping = { : (

Expand source code
def dict2pdfa(mapping, start: PA.State):
    """Convert nested dictionary into a PDFA.

    - mapping is a nested dictionary of the form:

       mapping = {
         <State>:  (<Label>, {
            <Action>: {
                <State>: <Probability>
            }
         }
       }
    """
    label_map = fn.walk_values(ig(0), mapping)
    transition_map = fn.walk_values(ig(1), mapping)

    outputs = set(bind(mapping).Values()[0].collect())
    inputs = set(bind(mapping).Values()[1].Keys().collect())

    return PA.pdfa(
        start=start,
        label=label_map.get,
        inputs=inputs,
        outputs=outputs,
        **_encode_two_player_game(transition_map)
    )
def pdfa2dict(pdfa)

Convert PDFA into nested dictionary of the form:

mapping = { : (

Returns: mapping and the start state.

Expand source code
def pdfa2dict(pdfa):
    """Convert PDFA into nested dictionary of the form:

       mapping = {
         <State>:  (<Label>, {
            <Action>: {
                <State>: <Probability>
            }
         }
       }

    Returns: mapping and the start state.
    """
    mapping = {}
    for s in pdfa.states():
        action2state_prob = {
            a: pdfa.transition_probs(s, a) for a in pdfa.inputs
        }

        label = pdfa.dfa._label(s)
        mapping[s] = (label, action2state_prob)
    return mapping, pdfa.start
def prob_pred(dyn, *, pred, horizon)

Return the probability that pred will evaluate to true before horizon time step assuming system inputs are applied uniformly at random.

Expand source code
def prob_pred(dyn, *, pred, horizon) -> float:
    """
    Return the probability that pred will evaluate to true before
    horizon time step assuming system inputs are applied uniformly at
    random.
    """
    prob = {}

    def pevent(state, path_prob, time):
        nonlocal prob
        assert time >= 0

        if state in prob:
            return path_prob * prob[state]
        elif pred(state):
            prob[state] = 0
            return 1
        elif time == 0:
            return 0

        acc = 0
        for action in dyn.inputs:
            for state2, state2_prob in dyn._probs(state, action):
                acc += pevent(state2, path_prob * state2_prob, time - 1)

        return acc / len(dyn.inputs)

    return pevent(dyn.start, path_prob=1, time=horizon)
def tee(left, right)

Parallel composition of left and right sharing inputs.

Expand source code
def tee(left, right):
    """Parallel composition of left and right sharing inputs."""
    if left.inputs <= right.inputs:
        inputs = left.inputs
    elif right.inputs <= left.inputs:
        inputs = right.inputs
    else:
        raise RuntimeError("Inputs need to be compatible")

    def transition(s, composite_input):
        sys_input, (env_l, env_r) = composite_input
        state2_l = left.dfa._transition(s[0], (sys_input, env_l))
        state2_r = right.dfa._transition(s[1], (sys_input, env_r))
        return (state2_l, state2_r)

    def env_dist(composite_state, action):
        state_l, state_r = composite_state

        return PA.ProductDistribution(
            left=left.env_dist(state_l, action),
            right=right.env_dist(state_r, action),
        )

    return PA.pdfa(
        start=(left.start, right.start),
        inputs=inputs,
        transition=transition,
        label=lambda s: (left._label(s[0]), right._label(s[1])),
        outputs=ProductAlphabet(left.outputs, right.outputs),
        env_dist=env_dist,
        env_inputs=ProductAlphabet(left.env_inputs, right.env_inputs),
    )