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

update supported models

parent 4b03324f
......@@ -27,7 +27,6 @@ JANI2PINS/client
tmp/
#QCOMP jani-models
tests/res/dtmc/**/*.jani
tests/res/mdp/**/*.jani
#Pytest Coverage
......
......@@ -78,6 +78,12 @@ Provide the path to the input file containing the jani-model
Provide the path to PINS model implementation
### --strategy {FLATTEN,MIXED,SYMBOLIC}
(default: SYMBOLIC)
The grouping strategy for synchronising automaton instances
### --ltsmin PATH
(default: "/usr/local/include/ltsmin/")
......
......@@ -19,7 +19,7 @@ def isSupported(model: dict, real2int: bool):
errors.endWithWrongJANIVersion()
# Supporting only not timed automata
modelTypes = {"lts", "mdp", "dtmc"}
modelTypes = {"lts", "mdp"}
if not model["type"] in modelTypes:
errors.endWithNotSupportedModelType()
......
......@@ -3,4 +3,4 @@ def supported() -> list:
Function Description:
Supported JANI model features by JANI2PINS server
"""
return ["derived-operators", "functions"]
return ["derived-operators", "functions", "state-exit-rewards"]
......@@ -3,4 +3,4 @@ def supported() -> list:
Function Description:
Supported model types by JANI2PINS server
"""
return ["lts", "mdp", "dtmc"]
return ["lts", "mdp"]
......@@ -9,7 +9,7 @@ def specification() -> dict:
Create specification of LTSmin model transformer
"""
ltsmin = {
"id": "ltsmin",
"id": "jani2pins",
"metadata": metadata.modelTransformer(),
"parameters": parameters.create(),
"model-features": modelFeatures.supported(),
......
......@@ -114,7 +114,7 @@ async def handleMessages(websocket: WebSocketServerProtocol, path: str):
protocolTasks[str(taskID)] = task
elif (
messageType == "transformation-start"
and message["transformer"] == "ltsmin"
and message["transformer"] == "jani2pins"
):
anyModel = message["model"]
parameters = message["parameters"]
......@@ -149,7 +149,7 @@ async def handleMessages(websocket: WebSocketServerProtocol, path: str):
await stopTasks(websocket, protocolTasks, "Message does not fit schema.")
break
print("Clean Up Session ({}):".format(id(websocket)))
print("Clean Up Session ({})".format(id(websocket)))
path = os.path.abspath("/".join(["tmp", str(id(websocket))]))
if os.path.exists(path):
shutil.rmtree(path)
......
......@@ -22,7 +22,6 @@ def execute(location: str, experiment: str, real2int: bool, mode: str) -> str:
mode: str
Grouping strategy mode
"""
print(mode)
try:
model = filesystem.loadJANI(path.join(location, "model.jani"), False)
......
......@@ -12,7 +12,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"'
NotSupportedModelType = 'JANI2PINS only supports model of type "lts" and "mdp"'
NotSupportedFeature = 'JANI2PINS only supports the semantics of "derived-operators" & "functions" as features'
NotSupportedVariable = "JANI2PINS does not support variable: {}"
......
#QCOMP
##DTMC
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 -4 http://qcomp.org/benchmarks/mdp/beb/beb.3-4.jani -O tests/res/mdp/beb/beb.3-4.jani
......
#include <jani2pinsPlugin.h>
#ifndef GROUPAMOUNT
#define GROUPAMOUNT 30
#endif
//Create TransitionGroupGuards
guard_t **createTransitionGroupGuardInformation()
{
// Guards of each transition group
int *transitionGuards[GROUPAMOUNT] = {(int[]){0,1},(int[]){2,3},(int[]){3,4},(int[]){2,5},(int[]){4,5},(int[]){2,6},(int[]){4,6},(int[]){2,7},(int[]){4,7},(int[]){8,9},(int[]){10,8},(int[]){11,12},(int[]){12,13},(int[]){11,12},(int[]){12,13},(int[]){14,8},(int[]){15,16},(int[]){16,17},(int[]){15,16},(int[]){16,17},(int[]){18,3},(int[]){18,19},(int[]){20},(int[]){21},(int[]){22},(int[]){23},(int[]){24},(int[]){25},(int[]){26},(int[]){27}};
int transitionGuardsSizes[GROUPAMOUNT] = {2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,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[30][23] = {{1,0,1,0,0,1,1,0,1,0,0,0,0,0,0,0,0,0,0,0,1,0,1},{1,1,0,0,0,1,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,1},{1,1,0,0,0,1,0,0,0,0,1,0,0,1,0,0,0,0,0,0,0,0,1},{1,1,0,0,0,1,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0,0,1},{1,1,0,0,0,1,0,0,0,0,1,0,1,1,0,0,0,0,0,0,0,0,1},{1,1,0,0,0,1,0,0,0,0,0,0,1,1,1,0,0,0,0,0,0,0,1},{1,1,0,0,0,1,0,0,0,0,1,0,1,1,1,0,0,0,0,0,0,0,1},{1,1,0,0,0,1,0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0,1},{1,1,0,0,0,1,0,0,0,0,1,0,0,1,1,0,0,0,0,0,0,0,1},{1,0,0,0,1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1},{1,0,0,1,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,1},{0,1,0,0,1,0,0,0,0,0,0,0,0,1,0,0,0,0,1,0,0,0,1},{0,1,0,0,1,0,0,0,0,0,0,0,0,1,0,0,0,1,1,0,0,0,1},{0,1,0,0,1,0,0,0,0,0,0,0,0,1,0,0,0,0,1,0,0,0,1},{0,1,0,0,1,0,0,0,0,0,0,0,0,1,0,0,0,1,1,0,0,0,1},{1,0,0,0,1,1,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,1},{1,0,0,1,0,1,0,1,1,1,1,1,1,0,0,0,0,0,0,0,0,1,1},{1,0,0,1,0,1,0,1,1,1,1,1,1,0,0,0,0,0,0,0,0,1,1},{1,0,0,1,0,1,0,1,1,1,1,1,1,0,0,0,0,0,0,0,0,1,1},{1,0,0,1,0,1,0,1,1,1,1,1,1,0,0,0,0,0,0,0,0,1,1},{0,1,0,1,0,0,0,0,0,1,0,1,1,1,0,1,1,1,0,1,1,1,1},{0,1,0,1,0,0,0,0,0,1,0,1,1,1,0,1,1,1,0,1,1,1,1},{1,0,0,0,0,1,1,1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,1},{1,0,0,0,0,1,1,1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,1},{1,0,0,0,0,1,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,1},{1,0,0,0,0,1,1,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,1},{0,1,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,1,1,0,0,0,1},{0,1,0,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,1,0,0,0,1},{0,1,0,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,1,0,0,0,1},{0,1,0,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,1,0,0,0,1}};
int *readDependencies(int group){
return readMatrix[group];
}
// Write Dependencies
int writeMatrix[30][23] = {{1,0,1,0,0,1,1,0,1,0,0,0,0,0,0,0,0,0,0,0,1,0,0},{1,1,0,0,0,1,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0},{1,1,0,0,0,1,0,0,0,0,1,0,0,1,0,0,0,0,0,0,0,0,0},{1,1,0,0,0,1,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0},{1,1,0,0,0,1,0,0,0,0,1,0,0,1,0,0,0,0,0,0,0,0,0},{1,1,0,0,0,1,0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0,0},{1,1,0,0,0,1,0,0,0,0,1,0,0,1,1,0,0,0,0,0,0,0,0},{1,1,0,0,0,1,0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0,0},{1,1,0,0,0,1,0,0,0,0,1,0,0,1,1,0,0,0,0,0,0,0,0},{1,0,0,0,1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1},{1,0,0,1,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0},{0,1,0,0,1,0,0,0,0,0,0,0,0,1,0,0,0,0,1,0,0,0,1},{0,1,0,0,1,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,1},{0,1,0,0,1,0,0,0,0,0,0,0,0,1,0,0,0,0,1,0,0,0,1},{0,1,0,0,1,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,1},{1,0,0,0,1,1,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,1},{1,0,0,1,0,1,0,1,0,1,0,1,1,0,0,0,0,0,0,0,0,1,0},{1,0,0,1,0,1,0,1,0,1,0,1,1,0,0,0,0,0,0,0,0,1,0},{1,0,0,1,0,1,0,1,0,1,0,1,1,0,0,0,0,0,0,0,0,1,0},{1,0,0,1,0,1,0,1,0,1,0,1,1,0,0,0,0,0,0,0,0,1,0},{0,1,0,1,0,0,0,0,0,0,0,0,0,1,0,1,1,1,0,1,0,1,0},{0,1,0,1,0,0,0,0,0,0,0,0,0,1,0,1,1,1,0,1,0,1,0},{1,0,0,0,0,1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},{1,0,0,0,0,1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},{1,0,0,0,0,1,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0},{1,0,0,0,0,1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},{0,1,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,1,0,0,0,0},{0,1,0,0,0,0,0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0,0},{0,1,0,0,0,0,0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0,0},{0,1,0,0,0,0,0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0,0}};
int *writeDependencies(int group){
return writeMatrix[group];
}
// Label Dependencies
int labelMatrix[28][23] = {{1,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},{0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0},{1,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},{0,1,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0},{1,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},{0,1,0,0,0,0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0,0,0},{0,1,0,0,0,0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0,0,0},{0,1,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0},{1,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},{0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1},{0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0},{0,1,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0},{0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1},{0,1,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,1,1,0,0,0,0},{0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1},{1,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},{0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0},{1,0,0,0,0,1,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},{0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0},{0,1,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0},{1,0,0,0,0,1,0,1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0},{1,0,0,0,0,1,0,1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0},{1,0,0,0,0,1,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0},{1,0,0,0,0,1,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0},{0,1,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0},{0,1,0,0,0,0,0,0,0,0,0,0,0,1,0,1,1,1,1,0,0,0,0},{0,1,0,0,0,0,0,0,0,0,0,0,0,1,0,1,1,1,1,0,0,0,0},{0,1,0,0,0,0,0,0,0,0,0,0,0,1,0,1,1,1,1,0,0,0,0}};
int *labelDependencies(int label){
return labelMatrix[label];
}
// Do-not-accord
int DNAMatrix[30][30] = {{1,1,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},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,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},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,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},{1,1,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},{1,1,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},{1,1,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},{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,1,1,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,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,1,1,1,1,0,0,0,0},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0},{0,1,1,1,1,1,1,1,1,1,0,1,1,1,1,1,0,0,0,0,1,1,0,0,0,0,1,1,1,1},{0,1,1,1,1,1,1,1,1,1,0,1,1,1,1,1,0,0,0,0,1,1,0,0,0,0,1,1,1,1},{0,1,1,1,1,1,1,1,1,1,0,1,1,1,1,1,0,0,0,0,1,1,0,0,0,0,1,1,1,1},{0,1,1,1,1,1,1,1,1,1,0,1,1,1,1,1,0,0,0,0,1,1,0,0,0,0,1,1,1,1}};
int *dnaGroup(int group){
return DNAMatrix[group];
}
// Necessary Enabling
int NESMatrix[28][30] = {{1,1,1,1,1,1,1,1,1,1,1,0,0,0,0,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0},{1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},{1,1,1,1,1,1,1,1,1,1,1,0,0,0,0,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0},{0,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0,0,1,1,0,0,0,0,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,0,0,0,0,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0},{0,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,1,1,1,1,1,1,0,0,0,0,1,1,1,1},{0,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,1,1,1,1,1,1,0,0,0,0,1,1,1,1},{0,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0,0,1,1,0,0,0,0,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,0,0,0,0,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0},{0,0,0,0,0,0,0,0,0,1,0,1,1,1,1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0},{0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,1,1,1,1,1,1,0,0,0,0,0,0,0,0},{0,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0,0,1,1,0,0,0,0,1,1,1,1},{0,0,0,0,0,0,0,0,0,1,0,1,1,1,1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0},{0,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0,0,1,1,0,0,0,0,1,1,1,1},{0,0,0,0,0,0,0,0,0,1,0,1,1,1,1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0},{1,1,1,1,1,1,1,1,1,1,1,0,0,0,0,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0},{0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,1,1,1,1,1,1,0,0,0,0,0,0,0,0},{1,1,1,1,1,1,1,1,1,1,1,0,0,0,0,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0},{0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,1,1,1,1,1,1,0,0,0,0,0,0,0,0},{0,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0,0,1,1,0,0,0,0,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,0,0,0,0,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0},{1,1,1,1,1,1,1,1,1,1,1,0,0,0,0,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0},{1,1,1,1,1,1,1,1,1,1,1,0,0,0,0,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0},{1,1,1,1,1,1,1,1,1,1,1,0,0,0,0,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0},{0,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0,0,1,1,0,0,0,0,1,1,1,1},{0,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0,0,1,1,0,0,0,0,1,1,1,1},{0,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0,0,1,1,0,0,0,0,1,1,1,1},{0,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0,0,1,1,0,0,0,0,1,1,1,1}};
int *necessaryEnabling(int guard){
return NESMatrix[guard];
}
// Necessary Disabling
int NDSMatrix[28][30] = {{1,1,1,1,1,1,1,1,1,1,1,0,0,0,0,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0},{1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},{1,1,1,1,1,1,1,1,1,1,1,0,0,0,0,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0},{0,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0,0,1,1,0,0,0,0,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,0,0,0,0,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0},{0,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,1,1,1,1,1,1,0,0,0,0,1,1,1,1},{0,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,1,1,1,1,1,1,0,0,0,0,1,1,1,1},{0,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0,0,1,1,0,0,0,0,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,0,0,0,0,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0},{0,0,0,0,0,0,0,0,0,1,0,1,1,1,1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0},{0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,1,1,1,1,1,1,0,0,0,0,0,0,0,0},{0,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0,0,1,1,0,0,0,0,1,1,1,1},{0,0,0,0,0,0,0,0,0,1,0,1,1,1,1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0},{0,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0,0,1,1,0,0,0,0,1,1,1,1},{0,0,0,0,0,0,0,0,0,1,0,1,1,1,1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0},{1,1,1,1,1,1,1,1,1,1,1,0,0,0,0,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0},{0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,1,1,1,1,1,1,0,0,0,0,0,0,0,0},{1,1,1,1,1,1,1,1,1,1,1,0,0,0,0,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0},{0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,1,1,1,1,1,1,0,0,0,0,0,0,0,0},{0,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0,0,1,1,0,0,0,0,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,0,0,0,0,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0},{1,1,1,1,1,1,1,1,1,1,1,0,0,0,0,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0},{1,1,1,1,1,1,1,1,1,1,1,0,0,0,0,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0},{1,1,1,1,1,1,1,1,1,1,1,0,0,0,0,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0},{0,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0,0,1,1,0,0,0,0,1,1,1,1},{0,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0,0,1,1,0,0,0,0,1,1,1,1},{0,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0,0,1,1,0,0,0,0,1,1,1,1},{0,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,0,0,0,0,1,1,0,0,0,0,1,1,1,1}};
int *necessaryDisabling(int guard){
return NDSMatrix[guard];
}
// Maybe co-enabled
int MCEMatrix[28][28] = {{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1},{1,1,1,