Commit bae4c450 authored by Lars Schieffer's avatar Lars Schieffer
Browse files

update tests

parent f4bb394e
......@@ -24,7 +24,7 @@ def isSupported(model: dict, real2int: bool):
errors.endWithNotSupportedModelType()
if "features" in model:
modelFeatures = {"derived-operators", "functions"}
modelFeatures = {"derived-operators", "functions", "state-exit-rewards"}
for feature in model["features"]:
if not feature in modelFeatures:
errors.endWithNotSupportedFeature()
......
......@@ -13,9 +13,7 @@ NotSupportedModeMessage = "Mode {} is not supported"
WrongVersionNumber = "JANI2PINS supports models of JANI version 1"
NotSupportedModelType = 'JANI2PINS only supports model of type "lts", "dtmc" and "mdp"'
NotSupportedFeature = (
'JANI2PINS only supports "derived-operators" & "functions" as features'
)
NotSupportedFeature = 'JANI2PINS only supports the semantics of "derived-operators" & "functions" as features'
NotSupportedVariable = "JANI2PINS does not support variable: {}"
......
#QCOMP
##DTMC
wget http://qcomp.org/benchmarks/dtmc/brp/brp.jani -O tests/res/dtmc/brp/brp.jani
wget http://qcomp.org/benchmarks/dtmc/coupon/coupon.5-2.jani -O tests/res/dtmc/coupon/coupon.5-2.jani
wget http://qcomp.org/benchmarks/dtmc/leader_sync/leader_sync.3-2.jani -O tests/res/dtmc/leader_sync/leader_sync.3-2.jani
wget http://qcomp.org/benchmarks/dtmc/egl/egl.jani -O tests/res/dtmc/egl/egl.v1.jani
wget -4 http://qcomp.org/benchmarks/dtmc/brp/brp.jani -O tests/res/dtmc/brp/brp.jani
wget -4 http://qcomp.org/benchmarks/dtmc/coupon/coupon.5-2.jani -O tests/res/dtmc/coupon/coupon.5-2.jani
wget -4 http://qcomp.org/benchmarks/dtmc/leader_sync/leader_sync.3-2.jani -O tests/res/dtmc/leader_sync/leader_sync.3-2.jani
wget -4 http://qcomp.org/benchmarks/dtmc/egl/egl.jani -O tests/res/dtmc/egl/egl.v1.jani
##MDP
wget http://qcomp.org/benchmarks/mdp/beb/beb.3-4.jani -O tests/res/mdp/beb/beb.3-4.jani
wget http://qcomp.org/benchmarks/mdp/consensus/consensus.2.jani -O tests/res/mdp/consensus/consensus.2.v1.jani
wget http://qcomp.org/benchmarks/mdp/csma/csma.2-2.jani -O tests/res/mdp/csma/csma.2-2.v1.jani
wget http://qcomp.org/benchmarks/mdp/elevators/elevators.a-3-3.jani -O tests/res/mdp/elevators/elevators.a-3-3.v1.jani
wget http://qcomp.org/benchmarks/mdp/rectangle-tireworld/rectangle-tireworld.5.jani -O tests/res/mdp/rectangle-tireworld/rectangle-tireworld.5.v1.jani
wget http://qcomp.org/benchmarks/mdp/tireworld/tireworld.17.jani -O tests/res/mdp/tireworld/tireworld.17.v1.jani
wget http://qcomp.org/benchmarks/mdp/wlan/wlan.0.jani -O tests/res/mdp/wlan/wlan.0.v1.jani
\ No newline at end of file
wget -4 http://qcomp.org/benchmarks/mdp/beb/beb.3-4.jani -O tests/res/mdp/beb/beb.3-4.jani
wget -4 http://qcomp.org/benchmarks/mdp/consensus/consensus.2.jani -O tests/res/mdp/consensus/consensus.2.v1.jani
wget -4 http://qcomp.org/benchmarks/mdp/echoring/echoring.jani -O tests/res/mdp/echoring/echoring.jani
wget -4 http://qcomp.org/benchmarks/mdp/csma/csma.2-2.jani -O tests/res/mdp/csma/csma.2-2.v1.jani
wget -4 http://qcomp.org/benchmarks/mdp/elevators/elevators.a-3-3.jani -O tests/res/mdp/elevators/elevators.a-3-3.v1.jani
wget -4 http://qcomp.org/benchmarks/mdp/rectangle-tireworld/rectangle-tireworld.5.jani -O tests/res/mdp/rectangle-tireworld/rectangle-tireworld.5.v1.jani
wget -4 http://qcomp.org/benchmarks/mdp/tireworld/tireworld.17.jani -O tests/res/mdp/tireworld/tireworld.17.v1.jani
wget -4 http://qcomp.org/benchmarks/mdp/wlan/wlan.0.jani -O tests/res/mdp/wlan/wlan.0.v1.jani
\ No newline at end of file
#include <jani2pinsPlugin.h>
#ifndef GROUPAMOUNT
#define GROUPAMOUNT 15
#endif
//Create TransitionGroupGuards
guard_t **createTransitionGroupGuardInformation()
{
// Guards of each transition group
int *transitionGuards[GROUPAMOUNT] = {(int[]){0,1},(int[]){2},(int[]){2},(int[]){3},(int[]){4},(int[]){5},(int[]){6},(int[]){7},(int[]){8},(int[]){8},(int[]){9},(int[]){10},(int[]){11},(int[]){12},(int[]){13}};
int transitionGuardsSizes[GROUPAMOUNT] = {2,1,1,1,1,1,1,1,1,1,1,1,1,1,1};
guard_t **guard_info = malloc(GROUPAMOUNT * sizeof(guard_t *));
for (int i = 0; i < GROUPAMOUNT; i++)
{
guard_info[i] = malloc(sizeof(int[transitionGuardsSizes[i] + 1]));
memcpy(guard_info[i]->guard, transitionGuards[i], transitionGuardsSizes[i] * sizeof(int));
guard_info[i]->count = transitionGuardsSizes[i];
}
return guard_info;
}
#include <jani2pinsPlugin.h>
// Name of the PINS plugin
char pins_plugin_name[] = "jani2pins";
// Compute the remainder of Euclidean division
int remEuc(int x, int y){
int remainder = x % y;
if (remainder < 0){
return remainder + abs(y);
}
else{
return remainder;
}
}
// Compute the signum function
int sgn(int x){
if (x>0){
return 1;
}
if (x<0){
return -1;
}
return 0;
}
// Evaluate all state labels or guard
static void stateLabelsGroup(model_t model, sl_group_enum_t group, int *sourceStateVector, int *stateVectorLabels) {
if (group == GB_SL_GUARDS) {
for (int i = 0; i < guardAmount(); i++) {
stateVectorLabels[i] = stateVectorLabelLong(model, i, sourceStateVector);
}
}
if (group == GB_SL_ALL) {
for (int i = 0; i < labelAmount(); i++) {
stateVectorLabels[i] = stateVectorLabelLong(model, i, sourceStateVector);
}
}
}
// Initialise LTSmin Model
void pins_model_init(model_t model) {
// Initialise pins model
initModel(model);
// Set initial state
GBsetInitialState(model, initialStateVector());
//Set pointer to next-state function
GBsetNextStateLong(model, (next_method_grey_t)nextStateLong);
GBsetNextStateShortR2W(model, (next_method_grey_t)nextStateR2W);
GBsetActionsShortR2W(model, (next_method_grey_t)actionsR2W);
//Set pointer to label evaluation function
GBsetStateLabelLong(model, (get_label_method_t)stateVectorLabelLong);
GBsetStateLabelShort(model, (get_label_method_t)stateVectorLabelShort);
// Add new implementation
GBsetStateLabelsGroup(model, stateLabelsGroup);
// Create dependent matrices
matrix_t *rm = malloc(sizeof(matrix_t));
matrix_t *wm = malloc(sizeof(matrix_t));
matrix_t *cm = malloc(sizeof(matrix_t));
matrix_t *lm = malloc(sizeof(matrix_t));
matrix_t *dna = malloc(sizeof(matrix_t));
matrix_t *nes = malloc(sizeof(matrix_t));
matrix_t *nds = malloc(sizeof(matrix_t));
matrix_t *mce = malloc(sizeof(matrix_t));
dm_create(rm, groupAmount(), stateVectorLength());
dm_create(wm, groupAmount(), stateVectorLength());
dm_create(cm, groupAmount(), stateVectorLength());
dm_create(lm, labelAmount(), stateVectorLength());
dm_create(dna, groupAmount(), groupAmount());
dm_create(nes, guardAmount(), groupAmount());
dm_create(nds, guardAmount(), groupAmount());
dm_create(mce, guardAmount(), guardAmount());
// Set read & write dependency matrices
for (int i = 0; i < groupAmount(); i++) {
for (int j = 0; j < stateVectorLength(); j++) {
if (readDependencies(i)[j]) {
dm_set(cm, i, j);
dm_set(rm, i, j);
}
if (writeDependencies(i)[j]) {
dm_set(cm, i, j);
dm_set(wm, i, j);
}
}
}
// Set label dependency matrix
for (int i = 0; i < labelAmount(); i++) {
for (int j = 0; j < stateVectorLength(); j++) {
if (labelDependencies(i)[j]) {
dm_set(lm, i, j);
}
}
}
// Set do-not-accord matrix
for (int i = 0; i < groupAmount(); i++) {
for (int j = 0; j < groupAmount(); j++) {
if (dnaGroup(i)[j]) {
dm_set(dna, i, j);
}
}
}
// Set necessary enabling set and necessary disabling set
for (int i = 0; i < labelAmount(); i++) {
for (int j = 0; j < groupAmount(); j++) {
if (necessaryEnabling(i)[j]) {
dm_set(nes, i, j);
}
if (necessaryDisabling(i)[j]) {
dm_set(nds, i, j);
}
}
}
// Set may-be-co-enabled matrix
for (int i = 0; i < labelAmount(); i++) {
for (int j = 0; j < labelAmount(); j++) {
if (maybeCoEnabled(i)[j]) {
dm_set(mce, i, j);
}
}
}
// Set pointer to dependency matrices
GBsetDMInfoRead(model, rm);
GBsetDMInfoMustWrite(model, wm);
GBsetDMInfo(model, cm);
GBsetStateLabelInfo(model, lm);
GBsetDoNotAccordInfo(model, dna);
GBsetGuardNESInfo(model, nes);
GBsetGuardNDSInfo(model, nds);
GBsetGuardCoEnabledInfo(model, mce);
// Create Label Mapping
sl_group_t *sl_group_all = malloc(labelAmount() * sizeof(sl_group_all));
sl_group_all->count = labelAmount();
for (int i = 0; i < labelAmount(); i++) {
sl_group_all->sl_idx[i] = i;
}
// Create Guard Mapping
sl_group_t *sl_group_guards = malloc(guardAmount() * sizeof(sl_group_guards));
sl_group_guards->count = guardAmount();
for (int i = 0; i < guardAmount(); i++) {
sl_group_guards->sl_idx[i] = i;
}
// Set pointer to label & guard mappings
GBsetStateLabelGroupInfo(model, GB_SL_ALL, sl_group_all);
GBsetStateLabelGroupInfo(model, GB_SL_GUARDS, sl_group_guards);
// Add Action guards
GBsetGuardsInfo(model, createTransitionGroupGuardInformation());
// Printing Guards in stdout
GBprintStateLabelGroupInfo(stdout, model);
}
\ No newline at end of file
#include <ltsmin/dlopen-api.h>
#include <ltsmin/lts-type.h>
#include <ltsmin/ltsmin-standard.h>
#include <ltsmin/pins-util.h>
#include <ltsmin/pins.h>
#include <math.h>
//
// model.c
//
// The amount of all defined groups
int groupAmount();
// The amount of all defined labels
int labelAmount();
// The amount of all defined guards
int guardAmount();
// The length of the whole state vector
int stateVectorLength();
// Initialise the PINS model
void initModel(model_t model);
// Implementation of calculating remainder of Euclidean division
int remEuc(int x, int y);
// Compute the signum function
int sgn(int x);
//
// next-states.c
//
// The initial state vector
int *initialStateVector();
// Successor function for PINS model using a LONG state vector.
int nextStateLong(model_t model, int group, int *state_src, TransitionCB callback, void *context);
// Successor function for PINS model using a R2W state vector.
int nextStateR2W(model_t model, int group, int *state_src, TransitionCB callback, void *context);
// Update function for PINS model using a R2W state vector.
int actionsR2W(model_t model, int group, int *state_src, TransitionCB callback, void *context);
// Label function for LONG state vector:
int stateVectorLabelLong(model_t model, int label, int *state_src);
// Label function for SHORT state vector:
int stateVectorLabelShort(model_t model, int label, int *state_src);
//
// dependencies.c
//
// Read dependencies to state vector
int *readDependencies(int group);
// Write Dependencies
int *writeDependencies(int group);
// Label Dependencies
int *labelDependencies(int label);
// Do not accord
int *dnaGroup(int group);
// Necessary Enabling
int *necessaryEnabling(int guard);
// Necessary Disabling
int *necessaryDisabling(int guard);
// Maybe co-enabled
int *maybeCoEnabled(int guard);
//
// guards.c
//
//Create Action Guards
guard_t **createTransitionGroupGuardInformation();
\ No newline at end of file
#include <jani2pinsPlugin.h>
// Read dependencies to state vector
int readMatrix[15][7] = {{1,1,0,1,1,1,1},{1,0,0,1,1,1,1},{1,0,0,1,1,1,1},{1,0,1,1,1,1,1},{1,0,1,1,1,1,1},{1,0,1,1,1,1,1},{1,0,1,1,1,1,1},{1,0,1,1,1,1,1},{0,1,0,0,0,1,1},{0,1,0,0,0,1,1},{0,1,1,0,0,1,1},{0,1,1,0,0,1,1},{0,1,1,0,0,1,1},{0,1,1,0,0,1,1},{0,1,1,0,0,1,0}};
int *readDependencies(int group){
return readMatrix[group];
}
// Write Dependencies
int writeMatrix[15][7] = {{1,1,0,1,0,1,0},{1,0,0,1,1,0,0},{1,0,0,1,1,0,0},{1,0,1,1,1,0,0},{1,0,1,1,1,0,0},{1,0,0,1,1,0,0},{1,0,0,1,1,0,0},{1,0,0,1,0,0,0},{0,1,0,0,0,1,1},{0,1,0,0,0,1,1},{0,1,1,0,0,1,1},{0,1,1,0,0,1,1},{0,1,0,0,0,1,1},{0,1,0,0,0,1,1},{0,1,0,0,0,1,0}};
int *writeDependencies(int group){
return writeMatrix[group];
}
// Label Dependencies
int labelMatrix[14][7] = {{1,0,0,1,1,1,1},{0,1,0,0,0,1,0},{1,0,0,1,1,1,1},{1,0,1,1,1,1,1},{1,0,1,1,1,1,1},{1,0,1,1,1,1,1},{1,0,1,1,1,1,1},{1,0,1,1,1,1,1},{0,1,0,0,0,1,0},{0,1,1,0,0,1,1},{0,1,1,0,0,1,1},{0,1,1,0,0,1,0},{0,1,1,0,0,1,0},{0,1,1,0,0,1,0}};
int *labelDependencies(int label){
return labelMatrix[label];
}
// Do-not-accord
int DNAMatrix[15][15] = {{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1}};
int *dnaGroup(int group){
return DNAMatrix[group];
}
// Necessary Enabling
int NESMatrix[14][15] = {{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,0,0,0,0,0,0,0,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,0,0,0,0,0,0,0,1,1,1,1,1,1,1},{1,0,0,1,1,0,0,0,1,1,1,1,1,1,1},{1,0,0,1,1,0,0,0,1,1,1,1,1,1,1},{1,0,0,1,1,0,0,0,1,1,1,1,1,1,1},{1,0,0,1,1,0,0,0,1,1,1,1,1,1,1},{1,0,0,1,1,0,0,0,1,1,1,1,1,1,1}};
int *necessaryEnabling(int guard){
return NESMatrix[guard];
}
// Necessary Disabling
int NDSMatrix[14][15] = {{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,0,0,0,0,0,0,0,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,0,0,0,0,0,0,0,1,1,1,1,1,1,1},{1,0,0,1,1,0,0,0,1,1,1,1,1,1,1},{1,0,0,1,1,0,0,0,1,1,1,1,1,1,1},{1,0,0,1,1,0,0,0,1,1,1,1,1,1,1},{1,0,0,1,1,0,0,0,1,1,1,1,1,1,1},{1,0,0,1,1,0,0,0,1,1,1,1,1,1,1}};
int *necessaryDisabling(int guard){
return NDSMatrix[guard];
}
// Maybe co-enabled
int MCEMatrix[14][14] = {{1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1}};
int *maybeCoEnabled(int guard){
return MCEMatrix[guard];
}
\ No newline at end of file
#include <jani2pinsPlugin.h>
// The amount of all defined groups
int groupAmount(){
return 15;
}
// The amount of all defined labels
int labelAmount()
{
return 14;
}
// The amount of all defined guards
int guardAmount()
{
return 14;
}
// The length of the whole state vector
int stateVectorLength()
{
return 7;
}
// Initialise the PINS model
void initModel(model_t model)
{
// Create empty lts datastructure
lts_type_t lts = lts_type_create();
// Create slot types
int intSlot = lts_type_put_type(lts, "int", LTStypeSInt32, NULL);
int actionSlot = lts_type_put_type(lts, "action", LTStypeEnum, NULL);
int guardSlot = lts_type_put_type(lts, "guard", LTStypeBool, NULL);
int boolSlot = lts_type_put_type(lts, "bool", LTStypeBool, NULL);
// Define action edges
lts_type_set_edge_label_count(lts, 1);
lts_type_set_edge_label_name(lts, 0, "action");
lts_type_set_edge_label_type(lts, 0, "action");
lts_type_set_edge_label_typeno(lts, 0, actionSlot);
// Define StateVector
lts_type_set_state_length(lts, stateVectorLength());
lts_type_set_state_name(lts, 0, "process1_instance_0");
lts_type_set_state_typeno(lts, 0, intSlot);
lts_type_set_state_name(lts, 1, "process2_instance_0");
lts_type_set_state_typeno(lts, 1, intSlot);
lts_type_set_state_name(lts, 2, "counter");
lts_type_set_state_typeno(lts, 2, intSlot);
lts_type_set_state_name(lts, 3, "pc1");
lts_type_set_state_typeno(lts, 3, intSlot);
lts_type_set_state_name(lts, 4, "coin1");
lts_type_set_state_typeno(lts, 4, intSlot);
lts_type_set_state_name(lts, 5, "pc2");
lts_type_set_state_typeno(lts, 5, intSlot);
lts_type_set_state_name(lts, 6, "coin2");
lts_type_set_state_typeno(lts, 6, intSlot);
// Define StateLabels
lts_type_set_state_label_count(lts, labelAmount());
lts_type_set_state_label_name(lts, 0, "g_0");
lts_type_set_state_label_typeno(lts, 0, guardSlot);
lts_type_set_state_label_name(lts, 1, "g_1");
lts_type_set_state_label_typeno(lts, 1, guardSlot);
lts_type_set_state_label_name(lts, 2, "g_2");
lts_type_set_state_label_typeno(lts, 2, guardSlot);
lts_type_set_state_label_name(lts, 3, "g_3");
lts_type_set_state_label_typeno(lts, 3, guardSlot);
lts_type_set_state_label_name(lts, 4, "g_4");
lts_type_set_state_label_typeno(lts, 4, guardSlot);
lts_type_set_state_label_name(lts, 5, "g_5");
lts_type_set_state_label_typeno(lts, 5, guardSlot);
lts_type_set_state_label_name(lts, 6, "g_6");
lts_type_set_state_label_typeno(lts, 6, guardSlot);
lts_type_set_state_label_name(lts, 7, "g_7");
lts_type_set_state_label_typeno(lts, 7, guardSlot);
lts_type_set_state_label_name(lts, 8, "g_8");
lts_type_set_state_label_typeno(lts, 8, guardSlot);
lts_type_set_state_label_name(lts, 9, "g_9");
lts_type_set_state_label_typeno(lts, 9, guardSlot);
lts_type_set_state_label_name(lts, 10, "g_10");
lts_type_set_state_label_typeno(lts, 10, guardSlot);
lts_type_set_state_label_name(lts, 11, "g_11");
lts_type_set_state_label_typeno(lts, 11, guardSlot);
lts_type_set_state_label_name(lts, 12, "g_12");
lts_type_set_state_label_typeno(lts, 12, guardSlot);
lts_type_set_state_label_name(lts, 13, "g_13");
lts_type_set_state_label_typeno(lts, 13, guardSlot);
// Validate lts datastructure
lts_type_validate(lts);
// Add lts to pins model
GBsetLTStype(model, lts);
// Add names to action groups
pins_chunk_put(model, actionSlot, chunk_str("done"));
pins_chunk_put(model, actionSlot, chunk_str("tau"));
}
This diff is collapsed.
#include <jani2pinsPlugin.h>
#ifndef GROUPAMOUNT
#define GROUPAMOUNT 501
#endif
//Create TransitionGroupGuards
guard_t **createTransitionGroupGuardInformation()
{
// Guards of each transition group
int *transitionGuards[GROUPAMOUNT] = {(int[]){0},(int[]){1},(int[]){2},(int[]){3},(int[]){4},(int[]){5},(int[]){6},(int[]){7},(int[]){8},(int[]){9},(int[]){10},(int[]){11},(int[]){12},(int[]){13},(int[]){14},(int[]){15,16},(int[]){17,18},(int[]){16,19},(int[]){20,21},(int[]){16,22},(int[]){23,24},(int[]){25,26,27,28,29},(int[]){25,26,28,29,30},(int[]){25,27,28,29,31},(int[]){25,28,29,30,31},(int[]){26,27,28,29,32},(int[]){26,28,29,30,32},(int[]){27,28,29,31,32},(int[]){28,29,30,31,32},(int[]){33,34},(int[]){34,35},(int[]){34,36},(int[]){34,37},(int[]){34,38},(int[]){34,39},(int[]){34,40},(int[]){34,41},(int[]){34,42},(int[]){34,43},(int[]){34,44},(int[]){34,45},(int[]){34,46},(int[]){34,47},(int[]){34,48},(int[]){34,49},(int[]){34,50},(int[]){34,51},(int[]){34,52},(int[]){34,53},(int[]){34,54},(int[]){34,55},(int[]){34,56},(int[]){34,57},(int[]){34,58},(int[]){34,59},(int[]){34,60},(int[]){34,61},(int[]){34,62},(int[]){34,63},(int[]){34,64},(int[]){34,65},(int[]){34,66},(int[]){34,67},(int[]){34,68},(int[]){34,69},(int[]){34,70},(int[]){34,71},(int[]){34,72},(int[]){34,73},(int[]){34,74},(int[]){34,75},(int[]){34,76},(int[]){34,77},(int[]){34,78},(int[]){34,79},(int[]){34,80},(int[]){33,81},(int[]){35,81},(int[]){36,81},(int[]){37,81},(int[]){38,81},(int[]){39,81},(int[]){40,81},(int[]){41,81},(int[]){42,81},(int[]){43,81},(int[]){44,81},(int[]){45,81},(int[]){46,81},(int[]){47,81},(int[]){48,81},(int[]){49,81},(int[]){50,81},(int[]){51,81},(int[]){52,81},(int[]){53,81},(int[]){54,81},(int[]){55,81},(int[]){56,81},(int[]){57,81},(int[]){58,81},(int[]){59,81},(int[]){60,81},(int[]){61,81},(int[]){62,81},(int[]){63,81},(int[]){64,81},(int[]){65,81},(int[]){66,81},(int[]){67,81},(int[]){68,81},(int[]){69,81},(int[]){70,81},(int[]){71,81},(int[]){72,81},(int[]){73,81},(int[]){74,81},(int[]){75,81},(int[]){76,81},(int[]){77,81},(int[]){78,81},(int[]){79,81},(int[]){80,81},(int[]){82,83},(int[]){83,84},(int[]){83,85},(int[]){83,86},(int[]){83,87},(int[]){83,88},(int[]){83,89},(int[]){83,90},(int[]){83,91},(int[]){83,92},(int[]){83,93},(int[]){83,94},(int[]){83,95},(int[]){83,96},(int[]){83,97},(int[]){83,98},(int[]){83,99},(int[]){100,83},(int[]){101,83},(int[]){102,83},(int[]){103,83},(int[]){104,83},(int[]){105,83},(int[]){106,83},(int[]){107,83},(int[]){108,83},(int[]){109,83},(int[]){110,83},(int[]){111,83},(int[]){112,83},(int[]){113,83},(int[]){114,83},(int[]){115,83},(int[]){116,83},(int[]){117,83},(int[]){118,83},(int[]){119,83},(int[]){120,83},(int[]){121,83},(int[]){122,83},(int[]){123,83},(int[]){124,83},(int[]){125,83},(int[]){126,83},(int[]){127,83},(int[]){128,83},(int[]){129,83},(int[]){130,82},(int[]){130,84},(int[]){130,85},(int[]){130,86},(int[]){130,87},(int[]){130,88},(int[]){130,89},(int[]){130,90},(int[]){130,91},(int[]){130,92},(int[]){130,93},(int[]){130,94},(int[]){130,95},(int[]){130,96},(int[]){130,97},(int[]){130,98},(int[]){130,99},(int[]){100,130},(int[]){101,130},(int[]){102,130},(int[]){103,130},(int[]){104,130},(int[]){105,130},(int[]){106,130},(int[]){107,130},(int[]){108,130},(int[]){109,130},(int[]){110,130},(int[]){111,130},(int[]){112,130},(int[]){113,130},(int[]){114,130},(int[]){115,130},(int[]){116,130},(int[]){117,130},(int[]){118,130},(int[]){119,130},(int[]){120,130},(int[]){121,130},(int[]){122,130},(int[]){123,130},(int[]){124,130},(int[]){125,130},(int[]){126,130},(int[]){127,130},(int[]){128,130},(int[]){129,130},(int[]){131,132},(int[]){132,133},(int[]){132,134},(int[]){132,135},(int[]){132,136},(int[]){132,137},(int[]){132,138},(int[]){132,139},(int[]){132,140},(int[]){132,141},(int[]){132,142},(int[]){132,143},(int[]){132,144},(int[]){132,145},(int[]){132,146},(int[]){132,147},(int[]){132,148},(int[]){132,149},(int[]){132,150},(int[]){132,151},(int[]){132,152},(int[]){132,153},(int[]){132,154},(int[]){132,155},(int[]){132,156},(int[]){132,157},(int[]){132,158},(int[]){132,159},(int[]){132,160},(int[]){132,161},(int[]){132,162},(int[]){132,163},(int[]){132,164},(int[]){132,165},(int[]){132,166},(int[]){132,167},(int[]){132,168},(int[]){132,169},(int[]){132,170},(int[]){132,171},(int[]){132,172},(int[]){132,173},(int[]){132,174},(int[]){132,175},(int[]){132,176},(int[]){132,177},(int[]){132,178},(int[]){131,179},(int[]){133,179},(int[]){134,179},(int[]){135,179},(int[]){136,179},(int[]){137,179},(int[]){138,179},(int[]){139,179},(int[]){140,179},(int[]){141,179},(int[]){142,179},(int[]){143,179},(int[]){144,179},(int[]){145,179},(int[]){146,179},(int[]){147,179},(int[]){148,179},(int[]){149,179},(int[]){150,179},(int[]){151,179},(int[]){152,179},(int[]){153,179},(int[]){154,179},(int[]){155,179},(int[]){156,179},(int[]){157,179},(int[]){158,179},(int[]){159,179},(int[]){160,179},(int[]){161,179},(int[]){162,179},(int[]){163,179},(int[]){164,179},(int[]){165,179},(int[]){166,179},(int[]){167,179},(int[]){168,179},(int[]){169,179},(int[]){170,179},(int[]){171,179},(int[]){172,179},(int[]){173,179},(int[]){174,179},(int[]){175,179},(int[]){176,179},(int[]){177,179},(int[]){178,179},(int[]){180,29},(int[]){181,29},(int[]){182,29},(int[]){183,29},(int[]){184,29},(int[]){185,29},(int[]){186,187,188,189,190,191},(int[]){192},(int[]){193},(int[]){194},(int[]){195},(int[]){196},(int[]){197},(int[]){198},(int[]){199},(int[]){200},(int[]){201},(int[]){202},(int[]){203},(int[]){204},(int[]){205},(int[]){206},(int[]){207},(int[]){208},(int[]){209},(int[]){210},(int[]){211},(int[]){212},(int[]){213},(int[]){214},(int[]){215},(int[]){216},(int[]){217},(int[]){218},(int[]){53},(int[]){219},(int[]){220},(int[]){221},(int[]){222},(int[]){223},(int[]){224},(int[]){225},(int[]){226},(int[]){227},(int[]){228},(int[]){229},(int[]){230},(int[]){231},(int[]){232},(int[]){233},(int[]){234},(int[]){235},(int[]){236},(int[]){237},(int[]){238},(int[]){239},(int[]){240},(int[]){241},(int[]){242},(int[]){243},(int[]){244},(int[]){245},(int[]){246},(int[]){247},(int[]){248},(int[]){249},(int[]){250},(int[]){251},(int[]){252},(int[]){253},(int[]){254},(int[]){255},(int[]){256},(int[]){257},(int[]){258},(int[]){259},(int[]){260},(int[]){261},(int[]){262},(int[]){263},(int[]){264},(int[]){265},(int[]){266},(int[]){267},(int[]){268},(int[]){269},(int[]){270},(int[]){271},(int[]){102},(int[]){272},(int[]){273},(int[]){274},(int[]){275},(int[]){276},(int[]){277},(int[]){278},(int[]){279},(int[]){280},(int[]){281},(int[]){282},(int[]){283},(int[]){284},(int[]){285},(int[]){286},(int[]){287},(int[]){288},(int[]){289},(int[]){290},(int[]){291},(int[]){292},(int[]){293},(int[]){294},(int[]){295},(int[]){296},(int[]){297},(int[]){298},(int[]){299},(int[]){300},(int[]){301},(int[]){302},(int[]){303},(int[]){304},(int[]){305},(int[]){306},(int[]){307},(int[]){308},(int[]){309},(int[]){310},(int[]){311},(int[]){312},(int[]){313},(int[]){314},(int[]){315},(int[]){316},(int[]){317},(int[]){318},(int[]){319},(int[]){320},(int[]){321},(int[]){322},(int[]){323},(int[]){324},(int[]){151},(int[]){325},(int[]){326},(int[]){327},(int[]){328},(int[]){329},(int[]){330},(int[]){331},(int[]){332},(int[]){333},(int[]){334},(int[]){335},(int[]){336},(int[]){337},(int[]){338},(int[]){339},(int[]){340},(int[]){341},(int[]){342},(int[]){343},(int[]){344},(int[]){345},(int[]){346},(int[]){347},(int[]){348},(int[]){349},(int[]){350},(int[]){351},(int[]){352},(int[]){353},(int[]){354},(int[]){355},(int[]){356},(int[]){357},(int[]){358},(int[]){359},(int[]){360},(int[]){360},(int[]){361},(int[]){361},(int[]){362},(int[]){362},(int[]){363},(int[]){363},(int[]){364},(int[]){364},(int[]){365},(int[]){365}};
int transitionGuardsSizes[GROUPAMOUNT] = {1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,2,2,2,2,2,5,5,5,5,5,5,5,5,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,6,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1};
guard_t **guard_info = malloc(GROUPAMOUNT * sizeof(guard_t *));
for (int i = 0; i < GROUPAMOUNT; i++)
{
guard_info[i] = malloc(sizeof(int[transitionGuardsSizes[i] + 1]));
memcpy(guard_info[i]->guard, transitionGuards[i], transitionGuardsSizes[i] * sizeof(int));
guard_info[i]->count = transitionGuardsSizes[i];
}
return guard_info;