<commit_before>import interfaces.automata
from interfaces.expr import Signal


# TODO: remove non-used


TYPE_MODEL_STATE = 'M'
TYPE_A_STATE = 'A'
TYPE_S_STATE = 'S'

FUNC_MODEL_TRANS = '_tau_'
FUNC_REACH = '_reach_'
FUNC_R = '_r_'

ARG_MODEL_STATE = '_m_'
ARG_A_STATE = '_a_'   # intended to be used for the whole specification (safety and liveness)
ARG_S_STATE = '_s_'   # for the safety automaton


def smt_arg_name_signal(s:Signal):
    return '_%s_' % str(s).lower()


def smt_unname_if_signal(arg_name:str, signals):
    signals = list(signals)  # we need an order
    signal_by_smt_name = dict(zip([smt_arg_name_signal(s)
                                   for s in signals],
                                  signals))

    if arg_name in signal_by_smt_name:
        assert arg_name != ARG_MODEL_STATE,arg_name  # no ambiguities!
        return signal_by_smt_name[arg_name]

    assert arg_name in ARG_MODEL_STATE, arg_name

    return arg_name


def smt_name_spec(spec_state:interfaces.automata.Node, spec_state_type:str):
    return '{0}_{1}'.format(spec_state_type, spec_state.name)


def smt_name_m(m:int):
    return '_m%i_' % m


def smt_unname_m(str_m):
    return int(str_m[2:-1])


def smt_name_free_arg(smt_arg):
    return '?{0}'.format(smt_arg)<commit_msg>changed naming of args to lower probs of collisions<commit_after>import interfaces.automata
from interfaces.expr import Signal


# TODO: remove non-used


TYPE_MODEL_STATE = 'M'
TYPE_A_STATE = 'A'

FUNC_MODEL_TRANS = '__tau'
FUNC_REACH = '__reach'
FUNC_R = '__r'

ARG_MODEL_STATE = '__m'
ARG_A_STATE = '__a'   # intended to be used for the whole specification (safety and liveness)


def smt_arg_name_signal(s:Signal):   # TODO: need better checks of no name collisions
    result = '%s_' % str(s).lower()
    assert result not in (ARG_A_STATE, ARG_MODEL_STATE)
    return result


def smt_unname_if_signal(arg_name:str, signals):
    signals = list(signals)  # we need an order
    signal_by_smt_name = dict(zip([smt_arg_name_signal(s)
                                   for s in signals],
                                  signals))

    if arg_name in signal_by_smt_name:
        assert arg_name != ARG_MODEL_STATE,arg_name  # no ambiguities!
        return signal_by_smt_name[arg_name]

    assert arg_name in ARG_MODEL_STATE, arg_name

    return arg_name


def smt_name_spec(spec_state:interfaces.automata.Node, spec_state_type:str):
    return '{0}_{1}'.format(spec_state_type, spec_state.name)


def smt_name_m(m:int):
    return '__m%i' % m


def smt_unname_m(str_m):
    return int(str_m[3:])


def smt_name_free_arg(smt_arg):
    return '?{0}'.format(smt_arg)
{'fraction_non_alphanumeric': 0.09523809523809523, 'fraction_numerical': 0.003401360544217687, 'mean_word_length': 3.5403087478559176, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6599710', 'n_tokens_mistral': 1012, 'n_tokens_neox': 975, 'n_words': 215}