<commit_before>#include <hre/config.h>

#include <limits.h>
#include <stdlib.h>

// Should be first to avoid collision with LTSmin print macros
#include <ltl2ba.h>
#undef Debug

#include <dm/dm.h>
#include <hre/unix.h>
#include <hre/user.h>
#include <ltsmin-lib/ltsmin-tl.h>
#include <ltsmin-lib/ltl2ba-lex.h>
#include <mc-lib/atomics.h>
#include <pins-lib/pins.h>
#include <pins-lib/property-semantics.h>


typedef struct ltl_context {
    model_t         parent;
    int             ltl_idx;
    int             sl_idx_accept;
    int             len;
    int             groups; // for SPIN semantics
    int             edge_labels;
    ltsmin_buchi_t *ba;
} ltl_context_t;

typedef struct cb_context {
    TransitionCB    cb;
    void           *user_context;
    int            *src;
    int             ntbtrans; /* number of textbook transitions */
    ltl_context_t  *ctx;
} cb_context;

static int
ltl_sl_short(model_t model, int label, int *state)
{
    ltl_context_t *ctx = GBgetContext(model);
    if (label == ctx->sl_idx_accept) {
        // state[0] must be the buchi automaton, because it's the only dependency
        return state[0] == -1 || ctx->ba->states[state[0]]->accept;
    } else {
        return GBgetStateLabelShort(GBgetParent(model), label, state);
    }
}

static int
ltl_sl_long(model_t model, int label, int *state)
{
    ltl_context_t *ctx = GBgetContext(model);
    if (label == ctx->sl_idx_accept) {
        HREassert (state[ctx->ltl_idx] < ctx->ba->state_count);
        return state[ctx->ltl_idx] == -1 || ctx->ba->states[state[ctx->ltl_idx]]->accept;
    } else {
        return GBgetStateLabelLong(GBgetParent(model), label, state);
    }
}

static void
ltl_sl_all(model_t model, int *state, int *labels)
{
    ltl_context_t *ctx = GBgetContext(model);
    GBgetStateLabelsAll(GBgetParent(model), state, labels);
    HREassert (state[ctx->ltl_idx] < ctx->ba->state_count);
    labels[ctx->sl_idx_accept] =
        state[ctx->ltl_idx] == -1 || ctx->ba->states[state[ctx->ltl_idx]]->accept;
}

/*
 * TYPE LTSMIN
 */
void ltl_ltsmin_cb (void*context,transition_info_t*ti,int*dst) {
#define infoctx ((cb_context*)context)
    ltl_context_t *ctx = infoctx->ctx;
    // copy dst, append ltl never claim in lockstep
    int dst_buchi[ctx->len];
    int dst_pred[1] = {0}; // assume < 32 predicates..
    memcpy(dst_buchi, dst, (ctx->len - 1) * sizeof(int) );
    // evaluate predicates
    for(int i=0; i < ctx->ba->predicate_count; i++) {
        if (eval_predicate(ctx->ba->predicates[i], ti, infoctx->src)) /* ltsmin: src instead of dst */
            dst_pred[0] |= (1 << i);
    }

    int i = infoctx->src[ctx->ltl_idx];
    HREassert (i < ctx->ba->state_count);
    for(int j=0; j < ctx->ba->states[i]->transition_count; j++) {
        // check predicates
        if ((dst_pred[0] & ctx->ba->states[i]->transitions[j].pos[0]) == ctx->ba->states[i]->transitions[j].pos[0] &&
            (dst_pred[0] & ctx->ba->states[i]->transitions[j].neg[0]) == 0) {
            // perform transition
            dst_buchi[ctx->ltl_idx] = ctx->ba->states[i]->transitions[j].to_state;

            // callback, emit new state, move allowed
            infoctx->cb(infoctx->user_context, ti, dst_buchi);
            ++infoctx->ntbtrans;
            /* debug<commit_msg>Fix initial state in LTL textbook semantics<commit_after>#include <hre/config.h>

#include <limits.h>
#include <stdlib.h>

// Should be first to avoid collision with LTSmin print macros
#include <ltl2ba.h>
#undef Debug

#include <dm/dm.h>
#include <hre/unix.h>
#include <hre/user.h>
#include <ltsmin-lib/ltsmin-tl.h>
#include <ltsmin-lib/ltl2ba-lex.h>
#include <mc-lib/atomics.h>
#include <pins-lib/pins.h>
#include <pins-lib/property-semantics.h>


typedef struct ltl_context {
    model_t         parent;
    int             ltl_idx;
    int             sl_idx_accept;
    int             len;
    int             groups; // for SPIN semantics
    int             edge_labels;
    ltsmin_buchi_t *ba;
} ltl_context_t;

typedef struct cb_context {
    TransitionCB    cb;
    void           *user_context;
    int            *src;
    int             ntbtrans; /* number of textbook transitions */
    ltl_context_t  *ctx;
} cb_context;

static int
ltl_sl_short(model_t model, int label, int *state)
{
    ltl_context_t *ctx = GBgetContext(model);
    if (label == ctx->sl_idx_accept) {
        // state[0] must be the buchi automaton, because it's the only dependency
        return state[0] == -1 || ctx->ba->states[state[0]]->accept;
    } else {
        return GBgetStateLabelShort(GBgetParent(model), label, state);
    }
}

static int
ltl_sl_long(model_t model, int label, int *state)
{
    ltl_context_t *ctx = GBgetContext(model);
    if (label == ctx->sl_idx_accept) {
        HREassert (state[ctx->ltl_idx] < ctx->ba->state_count);
        return ctx->ba->states[state[ctx->ltl_idx]]->accept;
    } else {
        return GBgetStateLabelLong(GBgetParent(model), label, state);
    }
}

static void
ltl_sl_all(model_t model, int *state, int *labels)
{
    ltl_context_t *ctx = GBgetContext(model);
    GBgetStateLabelsAll(GBgetParent(model), state, labels);
    HREassert (state[ctx->ltl_idx] < ctx->ba->state_count);
    labels[ctx->sl_idx_accept] = ctx->ba->states[state[ctx->ltl_idx]]->accept;
}

/*
 * TYPE LTSMIN
 */
void ltl_ltsmin_cb (void*context,transition_info_t*ti,int*dst) {
#define infoctx ((cb_context*)context)
    ltl_context_t *ctx = infoctx->ctx;
    // copy dst, append ltl never claim in lockstep
    int dst_buchi[ctx->len];
    int dst_pred[1] = {0}; // assume < 32 predicates..
    memcpy(dst_buchi, dst, (ctx->len - 1) * sizeof(int) );
    // evaluate predicates
    for(int i=0; i < ctx->ba->predicate_count; i++) {
        if (eval_predicate(ctx->ba->predicates[i], ti, infoctx->src)) /* ltsmin: src instead of dst */
            dst_pred[0] |= (1 << i);
    }

    int i = infoctx->src[ctx->ltl_idx];
    HREassert (i < ctx->ba->state_count);
    for(int j=0; j < ctx->ba->states[i]->transition_count; j++) {
        // check predicates
        if ((dst_pred[0] & ctx->ba->states[i]->transitions[j].pos[0]) == ctx->ba->states[i]->transitions[j].pos[0] &&
            (dst_pred[0] & ctx->ba->states[i]->transitions[j].neg[0]) == 0) {
            // perform transition
            dst_buchi[ctx->ltl_idx] = ctx->ba->states[i]->transitions[j].to_state;

            // callback, emit new state, move allowed
            infoctx->cb(infoctx->user_context, ti, dst_buchi);
            ++infoctx->ntbtrans;
            /* debug
{'fraction_non_alphanumeric': 0.15175572519083969, 'fraction_numerical': 0.006717557251908397, 'mean_word_length': 2.81537565521258, 'pattern_counts': {'":': 0, '<': 43, '<?xml version=': 0, '>': 131, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5498149', 'n_tokens_mistral': 2371, 'n_tokens_neox': 2333, 'n_words': 485}