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

#include <dm/dm.h>
#include <hre/user.h>
#include <hre/stringindex.h>
#include <ltsmin-lib/ltsmin-standard.h>
#include <pins-lib/pins.h>
#include <pins-lib/pins-util.h>
#include <pins-lib/pins2pins-mucalc.h>
#include <util-lib/treedbs.h>

/** \file pins.c */

struct grey_box_model {
	model_t parent;
	lts_type_t ltstype;
	matrix_t *dm_info;
	matrix_t *dm_read_info;
	matrix_t *dm_may_write_info;
	matrix_t *dm_must_write_info;
	int supports_copy;
	matrix_t *sl_info;
    sl_group_t* sl_groups[GB_SL_GROUP_COUNT];
    guard_t** guards;
    matrix_t *commutes_info; // commutes info
    matrix_t *gce_info; // guard co-enabled info
    matrix_t *dna_info; // do not accord info
    matrix_t *gnes_info; // guard necessary enabling set
    matrix_t *gnds_info; // guard necessary disabling set
    int sl_idx_buchi_accept;
    int sl_idx_progress;
    int sl_idx_valid_end;
    int *group_visibility;
    int *label_visibility;
	int *s0;
	int *guard_status;
	void*context;
    next_method_grey_t next_short;
    next_method_grey_t next_short_r2w;
	next_method_grey_t next_long;
    next_method_grey_t actions_short;
    next_method_grey_t actions_long;
	next_method_matching_t next_matching;
	next_method_black_t next_all;
	get_label_method_t state_labels_short;
	get_label_method_t state_labels_long;
	get_label_group_method_t state_labels_group;
	get_label_all_method_t state_labels_all;
	transition_in_group_t transition_in_group;
	covered_by_grey_t covered_by;
    covered_by_grey_t covered_by_short;
	void* newmap_context;
	newmap_t newmap;
	int2chunk_t int2chunk;
	chunk2int_t chunk2int;
    chunkatint_t chunkatint;
	get_count_t get_count;
	void** map;
	string_set_t default_filter;
	
	/** Index of static information matrices. */
	string_index_t static_info_index;
	/** Array of static information matrices. */
	struct static_info_matrix * static_info_matrices;
};

struct static_info_matrix{
    const char* name;
    matrix_t*matrix;
    pins_strictness_t strictness;
    index_class_t row_info;
    index_class_t column_info;
};

int GBsetMatrix(
    model_t model,
    const char*name,
    matrix_t *matrix,
    pins_strictness_t strictness,
    index_class_t row_info,
    index_class_t column_info
){
    int res=SIput(model->static_info_index,name);
    model->static_info_matrices[res].name=name;
    model->static_info_matrices[res].matrix=matrix;
    model->static_info_matrices[res].strictness=strictness;
    model->static_info_matrices[res].row_info=row_info;
    model->static_info_matrices[res].column_info=column_info;
    return res;
}


int GBgetMatrixID(model_t model,char*name){
    return SIlookup(model->static_info_index,name);
}

int GBgetMatrixCount(model_t model){
    return SIgetCount(model->static_info_index);
}

const char* GBgetMatrixName(model_t model,int ID){
    return model->static_info_matrices[ID].name;
}

matrix_t* GBgetMatrix(model_t model,int ID){
    return model->static_info_matrices[ID].matrix;
}

pins_strictness_t GBgetMatrixStrictness(model_t model,int ID){
    return model->static_info_matrices[ID].strictness;
}

index_class_t GBgetMatrixRowInfo(model_t model,int ID){
    return model->static_info_matrices[ID].row_info;
}

index_class_t GBgetMatrixColumnInfo(model_t model,int ID){
    return model->static_info_matrices[ID].column_info;
}

struct nested_cb {
	model_t model;
	int group;
	int *src;
	TransitionCB cb;
	void* user_ctx;
};

void project_dest(void*context,transition_info_t*ti,int*dst,int*cpy){
#define info ((struct nested_cb*)context)
	int len = dm_ones_in_row(GBgetDMInfo(info->model), info->group);
	int short_dst[len];
	dm_project_vector(GBgetDMInfo(info->model), info->group, dst, short_dst);
    info->cb(info->user_ctx,ti,short_dst,NULL);
#undef info
    return;
    (void)cpy;
}

void project_dest_w(void*context,transition_info_t*ti,int*dst,int*cpy){
#define info ((struct nested_cb*)context)
    int len = dm_ones_in_row(GBgetDMInfoMayWrite(info->model), info->group);
    int short_dst[len];

    dm_project_vector(GBgetDMInfoMayWrite(info->model), info->group, dst, short_dst);
    if (cpy != NULL) {
        int short_cpy[len];
        dm_project_vector(GBgetDMInfoMayWrite(info->model), info->group, cpy, short_cpy);
        info->cb(info->user_ctx,ti,short_dst,short_cpy);
    } else {
        info->cb(info->user_ctx,ti,short_dst,NULL);
    }
#undef info
}

int default_short(model_t self,int group,int*src,TransitionCB cb,void*context){
	struct nested_cb info;
	info.model = self;
	info.group = group;
	info.src=src;
	info.cb=cb;
	info.user_ctx=context;

	int long_src[dm_ncols(GBgetDMInfo(self))];
	dm_expand_vector(GBgetDMInfo(self), group, self->s0, src, long_src);
	return self->next_long(self,group,long_src,project_dest,&info);
}

int default_short_r2w(model_t self,int group,int*src,TransitionCB cb,void*context){
    struct nested_cb info;
    info.model = self;
    info.group = group;
    info.src=src;
    info.cb=cb;
    info.user_ctx=context;<commit_msg>Fixed a bug in PINS with automatic projecting and expanding vectors. The group information was not copied correctly.<commit_after>#include <hre/config.h>
#include <stdlib.h>

#include <dm/dm.h>
#include <hre/user.h>
#include <hre/stringindex.h>
#include <ltsmin-lib/ltsmin-standard.h>
#include <pins-lib/pins.h>
#include <pins-lib/pins-util.h>
#include <pins-lib/pins2pins-mucalc.h>
#include <util-lib/treedbs.h>

/** \file pins.c */

struct grey_box_model {
	model_t parent;
	lts_type_t ltstype;
	matrix_t *dm_info;
	matrix_t *dm_read_info;
	matrix_t *dm_may_write_info;
	matrix_t *dm_must_write_info;
	int supports_copy;
	matrix_t *sl_info;
    sl_group_t* sl_groups[GB_SL_GROUP_COUNT];
    guard_t** guards;
    matrix_t *commutes_info; // commutes info
    matrix_t *gce_info; // guard co-enabled info
    matrix_t *dna_info; // do not accord info
    matrix_t *gnes_info; // guard necessary enabling set
    matrix_t *gnds_info; // guard necessary disabling set
    int sl_idx_buchi_accept;
    int sl_idx_progress;
    int sl_idx_valid_end;
    int *group_visibility;
    int *label_visibility;
	int *s0;
	int *guard_status;
	void*context;
    next_method_grey_t next_short;
    next_method_grey_t next_short_r2w;
	next_method_grey_t next_long;
    next_method_grey_t actions_short;
    next_method_grey_t actions_long;
	next_method_matching_t next_matching;
	next_method_black_t next_all;
	get_label_method_t state_labels_short;
	get_label_method_t state_labels_long;
	get_label_group_method_t state_labels_group;
	get_label_all_method_t state_labels_all;
	transition_in_group_t transition_in_group;
	covered_by_grey_t covered_by;
    covered_by_grey_t covered_by_short;
	void* newmap_context;
	newmap_t newmap;
	int2chunk_t int2chunk;
	chunk2int_t chunk2int;
    chunkatint_t chunkatint;
	get_count_t get_count;
	void** map;
	string_set_t default_filter;
	
	/** Index of static information matrices. */
	string_index_t static_info_index;
	/** Array of static information matrices. */
	struct static_info_matrix * static_info_matrices;
};

struct static_info_matrix{
    const char* name;
    matrix_t*matrix;
    pins_strictness_t strictness;
    index_class_t row_info;
    index_class_t column_info;
};

int GBsetMatrix(
    model_t model,
    const char*name,
    matrix_t *matrix,
    pins_strictness_t strictness,
    index_class_t row_info,
    index_class_t column_info
){
    int res=SIput(model->static_info_index,name);
    model->static_info_matrices[res].name=name;
    model->static_info_matrices[res].matrix=matrix;
    model->static_info_matrices[res].strictness=strictness;
    model->static_info_matrices[res].row_info=row_info;
    model->static_info_matrices[res].column_info=column_info;
    return res;
}


int GBgetMatrixID(model_t model,char*name){
    return SIlookup(model->static_info_index,name);
}

int GBgetMatrixCount(model_t model){
    return SIgetCount(model->static_info_index);
}

const char* GBgetMatrixName(model_t model,int ID){
    return model->static_info_matrices[ID].name;
}

matrix_t* GBgetMatrix(model_t model,int ID){
    return model->static_info_matrices[ID].matrix;
}

pins_strictness_t GBgetMatrixStrictness(model_t model,int ID){
    return model->static_info_matrices[ID].strictness;
}

index_class_t GBgetMatrixRowInfo(model_t model,int ID){
    return model->static_info_matrices[ID].row_info;
}

index_class_t GBgetMatrixColumnInfo(model_t model,int ID){
    return model->static_info_matrices[ID].column_info;
}

struct nested_cb {
	model_t model;
	int group;
	int *src;
	TransitionCB cb;
	void* user_ctx;
};

void project_dest(void*context,transition_info_t*ti,int*dst,int*cpy){
#define info ((struct nested_cb*)context)
	int len = dm_ones_in_row(GBgetDMInfo(info->model), info->group);
	int short_dst[len];
	dm_project_vector(GBgetDMInfo(info->model), info->group, dst, short_dst);
    ti->group = info->group;
    info->cb(info->user_ctx,ti,short_dst,NULL);
#undef info
    return;
    (void)cpy;
}

void project_dest_w(void*context,transition_info_t*ti,int*dst,int*cpy){
#define info ((struct nested_cb*)context)
    int len = dm_ones_in_row(GBgetDMInfoMayWrite(info->model), info->group);
    int short_dst[len];

    dm_project_vector(GBgetDMInfoMayWrite(info->model), info->group, dst, short_dst);
    ti->group = info->group;
    if (cpy != NULL) {
        int short_cpy[len];
        dm_project_vector(GBgetDMInfoMayWrite(info->model), info->group, cpy, short_cpy);
        info->cb(info->user_ctx,ti,short_dst,short_cpy);
    } else {
        info->cb(info->user_ctx,ti,short_dst,NULL);
    }
#undef info
}

int default_short(model_t self,int group,int*src,TransitionCB cb,void*context){
	struct nested_cb info;
	info.model = self;
	info.group = group;
	info.src=src;
	info.cb=cb;
	info.user_ctx=context;

	int long_src[dm_ncols(GBgetDMInfo(self))];
	dm_expand_vector(GBgetDMInfo(self), group, self->s0, src, long_src);
	return self->next_long(self,group,long_src,project_dest,&info);
}

int default_short_r2w(model_t self,int group,int*src,TransitionCB cb,void*context){
    struct nested_cb info;
    info.model = self;
    info.group = group;
    info.src=src;
    info.cb=cb;
    info.user_ctx=context;
{'fraction_non_alphanumeric': 0.10726541817825277, 'fraction_numerical': 0.0017648789096970292, 'mean_word_length': 5.2653562653562656, 'pattern_counts': {'":': 0, '<': 23, '<?xml version=': 0, '>': 89, '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': '6158701', 'n_tokens_mistral': 3849, 'n_tokens_neox': 3782, 'n_words': 666}