Commit 4935d687 authored by Lars Schieffer's avatar Lars Schieffer
Browse files

update grouping strategy

parent 0175bb7c
......@@ -2,11 +2,13 @@ import asyncio
import sys
import websockets
from jsonschema.exceptions import ValidationError
import src.utilities.io.filesystem as filesystem
import src.utilities.parser.commandline as commandline
from src.pins.plugin import PINS
from src.server.server import handleMessages
from src.utilities.io.communication.errors import JANI2PINSError, errorFormat
if commandline.requestServer():
# Start WebSocket Server
......@@ -24,14 +26,17 @@ if commandline.requestServer():
else:
path = commandline.getJANIPath()
syntax = not commandline.getDisableCheck()
jani = filesystem.loadJANI(path, syntax)
r2i = commandline.getR2IFlag()
experiment = commandline.getExperimentValues()
try:
pinsPlugin = PINS(jani, r2i, experiment)
except Exception as error:
jani = filesystem.loadJANI(path, syntax)
pinsPlugin = PINS(jani, experiment, r2i)
except ValidationError as error:
print(error)
sys.exit(1)
except JANI2PINSError as error:
print(errorFormat.format(type="Error:", message=error.message))
sys.exit(1)
# Write Plugin to File
filesystem.writePlugin(pinsPlugin, commandline.getPINSPath())
# Compile Plugin
......
......@@ -53,25 +53,22 @@ def instancesOf(model: dict, functions: dict) -> list:
for synchronisation in system["syncs"]:
result = synchronisation["result"] if "result" in synchronisation else "tau"
syncVector = synchronisation["synchronise"]
if isLocal(syncVector) or ndProblem(syncVector, ndLabels):
edges = []
for index, label in enumerate(syncVector):
if label:
edges.append(instances[index][label])
removeLabel[index].add(label)
edges = flattenOf(edges)
for uniqueIndex, edge in enumerate(edges):
updatedLabel = "{}_flatten_{}".format(result, uniqueIndex)
updatedVector = []
for index, entry in enumerate(syncVector):
if entry:
instances[index][updatedLabel] = [edge.pop(0)]
updatedVector.append(updatedLabel)
else:
updatedVector.append(None)
synchronisation = {"result": result, "synchronise": updatedVector}
updatedSyncs.append(synchronisation)
else:
edges = []
for index, label in enumerate(syncVector):
if label:
edges.append(instances[index][label])
removeLabel[index].add(label)
edges = flattenOf(edges)
for uniqueIndex, edge in enumerate(edges):
updatedLabel = "{}_flatten_{}".format(result, uniqueIndex)
updatedVector = []
for index, entry in enumerate(syncVector):
if entry:
instances[index][updatedLabel] = [edge.pop(0)]
updatedVector.append(updatedLabel)
else:
updatedVector.append(None)
synchronisation = {"result": result, "synchronise": updatedVector}
updatedSyncs.append(synchronisation)
model["system"]["syncs"] = updatedSyncs
for index, labels in enumerate(removeLabel):
......
import sys
from jsonschema.exceptions import ValidationError
# Error communication
errorFormat = "{type:<8} {message}"
......@@ -14,8 +10,6 @@ NotSupportedTypeMessage = 'Not supported {} type: "{}" is of type "{}".'
NotSupportedModeMessage = "Mode {} is not supported"
IncorrectJANIModel1 = "The JANI model is not correct, because:\n"
WrongVersionNumber = "JANI2PINS supports models of JANI version 1"
NotSupportedModelType = 'JANI2PINS only supports model of type "lts", "dtmc" and "mdp"'
......@@ -34,62 +28,68 @@ NotSupportedWindowsFeature = (
)
class JANI2PINSError(Exception):
"""Exception raised for errors in JANI2PINS.
Attributes:
message: str
JANI2PINS Error Message
"""
def __init__(self, message: str):
super().__init__(message)
def notSupportedOperator(operator) -> None:
message = OperatorNotSupportedMessage.format(repr(operator))
raise Exception(errorFormat.format(type="Error:", message=message))
raise JANI2PINSError(message)
def notSupportedExpression(expression) -> None:
message = ExpressionNotSupportedMessage.format(repr(expression))
raise Exception(errorFormat.format(type="Error:", message=message))
raise JANI2PINSError(message)
def endWithConstantsHaveToBeSpecifiedError(parameter: str):
message = ConstantsHaveToBeSpecifiedMessage.format(parameter)
raise Exception(errorFormat.format(type="Error:", message=message))
raise JANI2PINSError(message)
def endWithWrongConstantTypeError(constantName: str, constantType: str):
message = NotSupportedTypeMessage.format("constant", constantName, constantType)
raise Exception(errorFormat.format(type="Error:", message=message))
raise JANI2PINSError(message)
def endWithWrongModeError(mode: str):
message = NotSupportedModeMessage.format(mode)
raise Exception(errorFormat.format(type="Error:", message=message))
def endWithWrongJANIInput(error: ValidationError):
message = IncorrectJANIModel1
raise Exception(errorFormat.format(type="Error:", message=message))
raise Exception(errorFormat.format(type="", message=error.message))
raise JANI2PINSError(message)
def endWithWrongJANIVersion():
message = WrongVersionNumber
raise Exception(errorFormat.format(type="Error:", message=message))
raise JANI2PINSError(message)
def endWithNotSupportedModelType():
message = NotSupportedModelType
raise Exception(errorFormat.format(type="Error:", message=message))
raise JANI2PINSError(message)
def endWithNotSupportedFeature():
message = NotSupportedFeature
raise Exception(errorFormat.format(type="Error:", message=message))
raise JANI2PINSError(message)
def endWithNotSupportedVariable(variableName: str):
message = NotSupportedVariable.format(variableName)
raise Exception(errorFormat.format(type="Error:", message=message))
raise JANI2PINSError(message)
def endWithNotSupportedWindowsFeature():
message = NotSupportedWindowsFeature
raise Exception(errorFormat.format(type="Error:", message=message))
raise JANI2PINSError(message)
def endWithNotSupportedFunction(functionName: str):
message = NotSupportedFunction.format(functionName)
raise Exception(errorFormat.format(type="Error:", message=message))
raise JANI2PINSError(message)
......@@ -8,10 +8,7 @@ from jsonschema import Draft7Validator
from jsonschema.exceptions import ValidationError
from src.pins.plugin import PINS
from src.utilities.io.communication.errors import (
endWithNotSupportedWindowsFeature,
endWithWrongJANIInput,
)
from src.utilities.io.communication.errors import endWithNotSupportedWindowsFeature
from src.utilities.io.schema.janiModel import JANIjsonSchema
......@@ -30,11 +27,8 @@ def loadJANI(path: str, check: bool) -> dict:
with open(path, "r", encoding="utf-8-sig") as janiFile:
janiModel = load(janiFile)
if check:
try:
JANIValidator = Draft7Validator(JANIjsonSchema)
JANIValidator.validate(janiModel)
except ValidationError as error:
endWithWrongJANIInput(error)
JANIValidator = Draft7Validator(JANIjsonSchema)
JANIValidator.validate(janiModel)
return janiModel
......
#include <jani2pinsPlugin.h>
#ifndef GROUPAMOUNT
#define GROUPAMOUNT 2
#define GROUPAMOUNT 5
#endif
//Create TransitionGroupGuards
guard_t **createTransitionGroupGuardInformation()
{
// Guards of each transition group
int *transitionGuards[GROUPAMOUNT] = {(int[]){0,1},(int[]){2,3}};
int transitionGuardsSizes[GROUPAMOUNT] = {2,2};
int *transitionGuards[GROUPAMOUNT] = {(int[]){0,1},(int[]){1,2},(int[]){0,3},(int[]){2,3},(int[]){1,4}};
int transitionGuardsSizes[GROUPAMOUNT] = {2,2,2,2,2};
guard_t **guard_info = malloc(GROUPAMOUNT * sizeof(guard_t *));
for (int i = 0; i < GROUPAMOUNT; i++)
......
#include <jani2pinsPlugin.h>
// Read dependencies to state vector
int readMatrix[2][3] = {{1,1,1},{1,1,0}};
int readMatrix[5][3] = {{1,1,0},{1,1,0},{1,1,1},{1,1,1},{1,1,0}};
int *readDependencies(int group){
return readMatrix[group];
}
// Write Dependencies
int writeMatrix[2][3] = {{1,1,1},{1,1,0}};
int writeMatrix[5][3] = {{1,1,0},{1,1,0},{1,1,1},{1,1,1},{1,1,0}};
int *writeDependencies(int group){
return writeMatrix[group];
}
// Label Dependencies
int labelMatrix[4][3] = {{1,0,0},{0,1,0},{1,0,0},{0,1,0}};
int labelMatrix[5][3] = {{1,0,0},{0,1,0},{1,0,0},{0,1,0},{1,0,0}};
int *labelDependencies(int label){
return labelMatrix[label];
}
// Do-not-accord
int DNAMatrix[2][2] = {{1,1},{1,1}};
int DNAMatrix[5][5] = {{1,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[4][2] = {{1,1},{1,1},{1,1},{1,1}};
int NESMatrix[5][5] = {{1,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 *necessaryEnabling(int guard){
return NESMatrix[guard];
}
// Necessary Disabling
int NDSMatrix[4][2] = {{1,1},{1,1},{1,1},{1,1}};
int NDSMatrix[5][5] = {{1,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 *necessaryDisabling(int guard){
return NDSMatrix[guard];
}
// Maybe co-enabled
int MCEMatrix[4][4] = {{1,1,0,1},{1,1,1,1},{0,1,1,1},{1,1,1,1}};
int MCEMatrix[5][5] = {{1,1,0,1,0},{1,1,1,0,1},{0,1,1,1,0},{1,0,1,1,1},{0,1,0,1,1}};
int *maybeCoEnabled(int guard){
return MCEMatrix[guard];
}
\ No newline at end of file
......@@ -2,19 +2,19 @@
// The amount of all defined groups
int groupAmount(){
return 2;
return 5;
}
// The amount of all defined labels
int labelAmount()
{
return 4;
return 5;
}
// The amount of all defined guards
int guardAmount()
{
return 4;
return 5;
}
// The length of the whole state vector
......@@ -60,6 +60,8 @@ void initModel(model_t model)
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);
// Validate lts datastructure
lts_type_validate(lts);
......
......@@ -21,25 +21,59 @@ int nextStateLong(model_t model, int group, int *sourceStateVector, TransitionCB
{
int actionLabel[1];
transition_info_t transitionInformation = {actionLabel, group};
if (group == 0 && (((sourceStateVector[0] == 0) || (sourceStateVector[0] == 2)) && ((sourceStateVector[1] == 0) || (sourceStateVector[1] == 1)))){
if (group == 0 && ((sourceStateVector[0] == 0) && (sourceStateVector[1] == 0))){
actionLabel[0] = 0;
int targetStateVector[STATEVECTORLENGTH];
memcpy(targetStateVector, sourceStateVector, STATEVECTORLENGTH * sizeof(int));
int One_instance_00 = sourceStateVector[0];
int Two_instance_00 = sourceStateVector[1];
int term0 = sourceStateVector[2];
int One_instance_01 = One_instance_00;
int Two_instance_01 = Two_instance_00;
int term1 = term0;
if (sourceStateVector[0] == 0){
One_instance_01 = 1;
}
if (sourceStateVector[1] == 0){
Two_instance_01 = 0;
}
targetStateVector[0] = One_instance_01;
targetStateVector[1] = Two_instance_01;
int copy[STATEVECTORLENGTH] = {0,0,1};
callback(context, &transitionInformation, targetStateVector, copy);
return 1;
}
if (group == 1 && ((sourceStateVector[0] == 2) && (sourceStateVector[1] == 0))){
actionLabel[0] = 0;
int targetStateVector[STATEVECTORLENGTH];
memcpy(targetStateVector, sourceStateVector, STATEVECTORLENGTH * sizeof(int));
int One_instance_00 = sourceStateVector[0];
int Two_instance_00 = sourceStateVector[1];
int One_instance_01 = One_instance_00;
int Two_instance_01 = Two_instance_00;
if (sourceStateVector[0] == 2){
One_instance_01 = 3;
}
if (sourceStateVector[1] == 0){
Two_instance_01 = 0;
}
targetStateVector[0] = One_instance_01;
targetStateVector[1] = Two_instance_01;
int copy[STATEVECTORLENGTH] = {0,0,1};
callback(context, &transitionInformation, targetStateVector, copy);
return 1;
}
if (group == 2 && ((sourceStateVector[0] == 0) && (sourceStateVector[1] == 1))){
actionLabel[0] = 0;
int targetStateVector[STATEVECTORLENGTH];
memcpy(targetStateVector, sourceStateVector, STATEVECTORLENGTH * sizeof(int));
int One_instance_00 = sourceStateVector[0];
int Two_instance_00 = sourceStateVector[1];
int term0 = sourceStateVector[2];
int One_instance_01 = One_instance_00;
int Two_instance_01 = Two_instance_00;
int term1 = term0;
if (sourceStateVector[0] == 0){
One_instance_01 = 1;
}
if (sourceStateVector[1] == 1){
Two_instance_01 = 3;
}
......@@ -53,7 +87,33 @@ int nextStateLong(model_t model, int group, int *sourceStateVector, TransitionCB
callback(context, &transitionInformation, targetStateVector, copy);
return 1;
}
if (group == 1 && ((sourceStateVector[0] == 1) && (sourceStateVector[1] == 0))){
if (group == 3 && ((sourceStateVector[0] == 2) && (sourceStateVector[1] == 1))){
actionLabel[0] = 0;
int targetStateVector[STATEVECTORLENGTH];
memcpy(targetStateVector, sourceStateVector, STATEVECTORLENGTH * sizeof(int));
int One_instance_00 = sourceStateVector[0];
int Two_instance_00 = sourceStateVector[1];
int term0 = sourceStateVector[2];
int One_instance_01 = One_instance_00;
int Two_instance_01 = Two_instance_00;
int term1 = term0;
if (sourceStateVector[0] == 2){
One_instance_01 = 3;
}
if (sourceStateVector[1] == 1){
Two_instance_01 = 3;
}
if (sourceStateVector[1] == 1){
term1 = 1;
}
targetStateVector[0] = One_instance_01;
targetStateVector[1] = Two_instance_01;
targetStateVector[2] = term1;
int copy[STATEVECTORLENGTH] = {0,0,0};
callback(context, &transitionInformation, targetStateVector, copy);
return 1;
}
if (group == 4 && ((sourceStateVector[0] == 1) && (sourceStateVector[1] == 0))){
actionLabel[0] = 1;
int targetStateVector[STATEVECTORLENGTH];
memcpy(targetStateVector, sourceStateVector, STATEVECTORLENGTH * sizeof(int));
......@@ -81,24 +141,54 @@ int nextStateR2W(model_t model, int group, int *sourceStateVector, TransitionCB
{
int actionLabel[1];
transition_info_t transitionInformation = {actionLabel, group};
if (group == 0 && (((sourceStateVector[0] == 0) || (sourceStateVector[0] == 2)) && ((sourceStateVector[1] == 0) || (sourceStateVector[1] == 1)))){
if (group == 0 && ((sourceStateVector[0] == 0) && (sourceStateVector[1] == 0))){
actionLabel[0] = 0;
int targetStateVector[dm_ones_in_row(GBgetDMInfoMustWrite(model), group)];
int One_instance_00 = sourceStateVector[0];
int Two_instance_00 = sourceStateVector[1];
int term0 = sourceStateVector[2];
int One_instance_01 = One_instance_00;
int Two_instance_01 = Two_instance_00;
int term1 = term0;
if (sourceStateVector[0] == 0){
One_instance_01 = 1;
}
if (sourceStateVector[1] == 0){
Two_instance_01 = 0;
}
targetStateVector[0] = One_instance_01;
targetStateVector[1] = Two_instance_01;
callback(context, &transitionInformation, targetStateVector, NULL);
return 1;
}
if (group == 1 && ((sourceStateVector[0] == 2) && (sourceStateVector[1] == 0))){
actionLabel[0] = 0;
int targetStateVector[dm_ones_in_row(GBgetDMInfoMustWrite(model), group)];
int One_instance_00 = sourceStateVector[0];
int Two_instance_00 = sourceStateVector[1];
int One_instance_01 = One_instance_00;
int Two_instance_01 = Two_instance_00;
if (sourceStateVector[0] == 2){
One_instance_01 = 3;
}
if (sourceStateVector[1] == 0){
Two_instance_01 = 0;
}
targetStateVector[0] = One_instance_01;
targetStateVector[1] = Two_instance_01;
callback(context, &transitionInformation, targetStateVector, NULL);
return 1;
}
if (group == 2 && ((sourceStateVector[0] == 0) && (sourceStateVector[1] == 1))){
actionLabel[0] = 0;
int targetStateVector[dm_ones_in_row(GBgetDMInfoMustWrite(model), group)];
int One_instance_00 = sourceStateVector[0];
int Two_instance_00 = sourceStateVector[1];
int term0 = sourceStateVector[2];
int One_instance_01 = One_instance_00;
int Two_instance_01 = Two_instance_00;
int term1 = term0;
if (sourceStateVector[0] == 0){
One_instance_01 = 1;
}
if (sourceStateVector[1] == 1){
Two_instance_01 = 3;
}
......@@ -111,7 +201,31 @@ int nextStateR2W(model_t model, int group, int *sourceStateVector, TransitionCB
callback(context, &transitionInformation, targetStateVector, NULL);
return 1;
}
if (group == 1 && ((sourceStateVector[0] == 1) && (sourceStateVector[1] == 0))){
if (group == 3 && ((sourceStateVector[0] == 2) && (sourceStateVector[1] == 1))){
actionLabel[0] = 0;
int targetStateVector[dm_ones_in_row(GBgetDMInfoMustWrite(model), group)];
int One_instance_00 = sourceStateVector[0];
int Two_instance_00 = sourceStateVector[1];
int term0 = sourceStateVector[2];
int One_instance_01 = One_instance_00;
int Two_instance_01 = Two_instance_00;
int term1 = term0;
if (sourceStateVector[0] == 2){
One_instance_01 = 3;
}
if (sourceStateVector[1] == 1){
Two_instance_01 = 3;
}
if (sourceStateVector[1] == 1){
term1 = 1;
}
targetStateVector[0] = One_instance_01;
targetStateVector[1] = Two_instance_01;
targetStateVector[2] = term1;
callback(context, &transitionInformation, targetStateVector, NULL);
return 1;
}
if (group == 4 && ((sourceStateVector[0] == 1) && (sourceStateVector[1] == 0))){
actionLabel[0] = 1;
int targetStateVector[dm_ones_in_row(GBgetDMInfoMustWrite(model), group)];
int One_instance_00 = sourceStateVector[0];
......@@ -142,19 +256,49 @@ int actionsR2W(model_t model, int group, int *sourceStateVector, TransitionCB ca
int targetStateVector[dm_ones_in_row(GBgetDMInfoMustWrite(model), group)];
int One_instance_00 = sourceStateVector[0];
int Two_instance_00 = sourceStateVector[1];
int term0 = sourceStateVector[2];
int One_instance_01 = One_instance_00;
int Two_instance_01 = Two_instance_00;
int term1 = term0;
if (sourceStateVector[0] == 0){
One_instance_01 = 1;
}
if (sourceStateVector[1] == 0){
Two_instance_01 = 0;
}
targetStateVector[0] = One_instance_01;
targetStateVector[1] = Two_instance_01;
callback(context, &transitionInformation, targetStateVector, NULL);
return 1;
}
if (group == 1){
actionLabel[0] = 0;
int targetStateVector[dm_ones_in_row(GBgetDMInfoMustWrite(model), group)];
int One_instance_00 = sourceStateVector[0];
int Two_instance_00 = sourceStateVector[1];
int One_instance_01 = One_instance_00;
int Two_instance_01 = Two_instance_00;
if (sourceStateVector[0] == 2){
One_instance_01 = 3;
}
if (sourceStateVector[1] == 0){
Two_instance_01 = 0;
}
targetStateVector[0] = One_instance_01;
targetStateVector[1] = Two_instance_01;
callback(context, &transitionInformation, targetStateVector, NULL);
return 1;
}
if (group == 2){
actionLabel[0] = 0;
int targetStateVector[dm_ones_in_row(GBgetDMInfoMustWrite(model), group)];
int One_instance_00 = sourceStateVector[0];
int Two_instance_00 = sourceStateVector[1];
int term0 = sourceStateVector[2];
int One_instance_01 = One_instance_00;
int Two_instance_01 = Two_instance_00;
int term1 = term0;
if (sourceStateVector[0] == 0){
One_instance_01 = 1;
}
if (sourceStateVector[1] == 1){
Two_instance_01 = 3;
}
......@@ -167,7 +311,31 @@ int actionsR2W(model_t model, int group, int *sourceStateVector, TransitionCB ca
callback(context, &transitionInformation, targetStateVector, NULL);
return 1;
}
if (group == 1){
if (group == 3){
actionLabel[0] = 0;
int targetStateVector[dm_ones_in_row(GBgetDMInfoMustWrite(model), group)];
int One_instance_00 = sourceStateVector[0];
int Two_instance_00 = sourceStateVector[1];
int term0 = sourceStateVector[2];
int One_instance_01 = One_instance_00;
int Two_instance_01 = Two_instance_00;
int term1 = term0;
if (sourceStateVector[0] == 2){
One_instance_01 = 3;
}
if (sourceStateVector[1] == 1){
Two_instance_01 = 3;