Commit 092685aa authored by Lars Schieffer's avatar Lars Schieffer
Browse files

update server settings to command line settings

parent 39a9f3e5
import asyncio
import sys
import websockets
......@@ -21,14 +22,16 @@ if commandline.requestServer():
finally:
eventLoop.close()
else:
pinsPlugin = PINS(
janiModel=filesystem.loadJANI(
commandline.getJANIPath(), not commandline.getDisableCheck()
),
real2int=commandline.getR2IFlag(),
experiment=commandline.getExperimentValues(),
)
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:
print(error)
sys.exit(1)
# Write Plugin to File
filesystem.writePlugin(pinsPlugin, commandline.getPINSPath())
# Compile Plugin
......
......@@ -23,6 +23,12 @@ def isSupported(model: dict, real2int: bool):
if not model["type"] in modelTypes:
errors.endWithNotSupportedModelType()
if "features" in model:
modelFeatures = {"derived-operators", "functions"}
for feature in model["features"]:
if not feature in modelFeatures:
errors.endWithNotSupportedFeature()
# Restrict-Initial are not evaluated for transformation
if "restrict-initial" in model:
warnings.displyRestrictInitial()
......
......@@ -8,7 +8,7 @@ def server() -> dict:
"""
metadata = {
"name": "JANI - Server LTSmin",
"version": version.create(0, 1, 2),
"version": version.create(1, 0, 0),
"author": "Lars Schieffer",
"description": "Implementation of the JANI interaction-protocol with LTSmin support",
}
......@@ -22,7 +22,7 @@ def analysisEngine() -> dict:
"""
metadata = {
"name": "JANI2PINS - Analysis Engine",
"version": version.create(0, 1, 2),
"version": version.create(1, 0, 0),
"author": "Lars Schieffer",
"description": "Engine for performing model checking of JANI models with LTSmin",
}
......@@ -36,7 +36,7 @@ def modelTransformer() -> dict:
"""
metadata = {
"name": "JANI2PINS - Model Transformer",
"version": version.create(0, 1, 2),
"version": version.create(1, 0, 0),
"author": "Lars Schieffer",
"description": "Model transformer for JANI models to produce PINS models",
}
......
......@@ -3,4 +3,4 @@ def supported() -> list:
Function Description:
Supported model types by JANI2PINS server
"""
return ["lts", "mdp"]
return ["lts", "mdp", "dtmc"]
def syncMode() -> dict:
"""
Function Description:
Create syncMode parameter
"""
mode = {
"id": "syncMode",
"name": "JANI2PINS Syncmode",
"description": "Set mode of synchronized edges",
"category": "JANI2PINS",
"is-global": False,
"type": ["FLATTEN", "POSTPONE"],
"default-value": "FLATTEN",
}
return mode
def real2int() -> dict:
"""
Function Description:
......@@ -32,23 +15,6 @@ def real2int() -> dict:
return r2i
def recursionJANI2PINS() -> dict:
"""
Function Description:
Create recursion limit of JANI2PINS parameter
"""
limit = {
"id": "limitJ2P",
"name": "Recursion Limit (JANI2PINS)",
"description": "Set the python recursion limit",
"category": "JANI2PINS",
"is-global": False,
"type": "int",
"default-value": 1000,
}
return limit
def backend() -> dict:
"""
Function Description:
......@@ -105,5 +71,5 @@ def create() -> list:
Function Description:
Create all parameters for ltsmin analysis engine
"""
parameters = [syncMode(), real2int(), recursionJANI2PINS(), backend(), command(), trace()]
parameters = [real2int(), backend(), command(), trace()]
return parameters
def syncMode() -> dict:
"""
Function Description:
Create syncMode parameter
"""
mode = {
"id": "syncMode",
"name": "JANI2PINS Syncmode",
"description": "Set mode of synchronized edges",
"category": "JANI2PINS",
"is-global": False,
"type": ["FLATTEN", "POSTPONE"],
"default-value": "FLATTEN",
}
return mode
def real2int() -> dict:
"""
Function Description:
......@@ -32,23 +15,6 @@ def real2int() -> dict:
return r2i
def recursionJANI2PINS() -> dict:
"""
Function Description:
Create recursion limit of JANI2PINS parameter
"""
limit = {
"id": "limitJ2P",
"name": "Recursion Limit (JANI2PINS)",
"description": "Set the python recursion limit",
"category": "JANI2PINS",
"is-global": False,
"type": "int",
"default-value": 1000,
}
return limit
def experiment() -> dict:
"""
Function Description:
......@@ -71,5 +37,5 @@ def create() -> list:
Function Description:
Create all parameters for ltsmin model transformers
"""
parameters = [syncMode(), real2int(), recursionJANI2PINS(), experiment()]
parameters = [real2int(), experiment()]
return parameters
......@@ -7,13 +7,13 @@ def fail(taskID: int) -> dict:
taskID: int
Unique task id
"""
paramters = {
"type": "server-paramters",
parameters = {
"type": "server-parameters",
"id": taskID,
"success": False,
"error": "Server has no parameters to adjust",
}
return paramters
return parameters
def success(taskID: int) -> dict:
......@@ -25,5 +25,5 @@ def success(taskID: int) -> dict:
taskID: int
Unique task id
"""
parameters = {"type": "server-paramters", "id": taskID, "success": True}
parameters = {"type": "server-parameters", "id": taskID, "success": True}
return parameters
......@@ -178,13 +178,16 @@ async def handleModelTransformation(
)
await websocket.send(json.dumps(tasks.error(model.getID(), j2pErrors)))
await websocket.send(json.dumps(tasks.ended(model.getID())))
await websocket.send(json.dumps(tasks.status(model.getID(), "Complete Task")))
await websocket.send(
json.dumps(
transform.provideTransformationResults(model.getID(), model.getLocation())
else:
await websocket.send(json.dumps(tasks.status(model.getID(), "Complete Task")))
await websocket.send(
json.dumps(
transform.provideTransformationResults(
model.getID(), model.getLocation()
)
)
)
)
await websocket.send(json.dumps(tasks.ended(model.getID())))
await websocket.send(json.dumps(tasks.ended(model.getID())))
async def handlePINSChecking(
......
......@@ -49,10 +49,8 @@ class Model:
self.__backend = backend.BACKEND.SEQUENTIAL
self.__command = ""
self.__trace = False
self.__syncMode = "FLATTEN"
self.__experimentValues = ""
self.__real2int = False
self.__limitJ2P = 1000
self.__handleParameters(parameters)
self.__saveModel(model)
......@@ -65,13 +63,7 @@ class Model:
experiment: str
Values of not initialized constants in JANI model
"""
errors = jani2pins.execute(
self.__location,
self.__syncMode,
experiment,
self.__real2int,
self.__limitJ2P,
)
errors = jani2pins.execute(self.__location, experiment, self.__real2int)
return errors
def executeLTSmin(self) -> str:
......@@ -129,15 +121,11 @@ class Model:
self.__command = parameter["value"]
elif parameter["id"] == "trace":
self.__trace = parameter["value"]
elif parameter["id"] == "syncMode":
self.__syncMode = parameter["value"]
elif parameter["id"] == "experiment":
if parameter["value"]:
self.__experimentValues = parameter["value"]
elif parameter["id"] == "real2int":
self.__real2int = parameter["value"]
elif parameter["id"] == "limitJ2P":
self.__limitJ2P = parameter["value"]
else:
print(repr(parameter))
......
......@@ -6,9 +6,7 @@ import src.utilities.parser.expression.toExpression as expression
from src.pins.plugin import PINS
def execute(
location: str, mode: str, experiment: str, real2int: bool, recursionLimit: int
) -> str:
def execute(location: str, experiment: str, real2int: bool) -> str:
"""
Function Description:
Create PINS model in filesystem by executing jani2pins parser and return occurring
......@@ -17,23 +15,17 @@ def execute(
Function Parameters:
location: str
Directory of jani model
mode: str
Mode for performing synchronization of non deterministic edges
experiment: str
Values of not initialized constants in JANI model
real2int: bool
Should real values cast to integer?
"""
errors = ""
try:
pinsPlugin = PINS(
janiModel=filesystem.loadJANI(path.join(location, "model.jani"), False),
real2int=real2int,
experiment=expression.createExperiments(experiment),
)
except e:
return "Error"
model = filesystem.loadJANI(path.join(location, "model.jani"), False)
pinsPlugin = PINS(model, real2int, expression.createExperiments(experiment))
except Exception as error:
return str(error)
# Write Plugin to File
filesystem.writePlugin(pinsPlugin, location)
return errors
return ""
......@@ -18,7 +18,10 @@ IncorrectJANIModel1 = "The JANI model is not correct, because:\n"
WrongVersionNumber = "JANI2PINS supports models of JANI version 1"
NotSupportedModelType = 'JANI2PINS supports only model of type "lts", "dtmc" and "mdp"'
NotSupportedModelType = 'JANI2PINS only supports model of type "lts", "dtmc" and "mdp"'
NotSupportedFeature = (
'JANI2PINS only supports "derived-operators" & "functions" as features'
)
NotSupportedVariable = "JANI2PINS does not support variable: {}"
......@@ -33,66 +36,60 @@ NotSupportedWindowsFeature = (
def notSupportedOperator(operator) -> None:
message = OperatorNotSupportedMessage.format(repr(operator))
print(errorFormat.format(type="Error:", message=message))
sys.exit(1)
raise Exception(errorFormat.format(type="Error:", message=message))
def notSupportedExpression(expression) -> None:
message = ExpressionNotSupportedMessage.format(repr(expression))
print(errorFormat.format(type="Error:", message=message))
sys.exit(1)
raise Exception(errorFormat.format(type="Error:", message=message))
def endWithConstantsHaveToBeSpecifiedError(parameter: str):
message = ConstantsHaveToBeSpecifiedMessage.format(parameter)
print(errorFormat.format(type="Error:", message=message))
sys.exit(1)
raise Exception(errorFormat.format(type="Error:", message=message))
def endWithWrongConstantTypeError(constantName: str, constantType: str):
message = NotSupportedTypeMessage.format("constant", constantName, constantType)
print(errorFormat.format(type="Error:", message=message))
sys.exit(1)
raise Exception(errorFormat.format(type="Error:", message=message))
def endWithWrongModeError(mode: str):
message = NotSupportedModeMessage.format(mode)
print(errorFormat.format(type="Error:", message=message))
sys.exit(1)
raise Exception(errorFormat.format(type="Error:", message=message))
def endWithWrongJANIInput(error: ValidationError):
message = IncorrectJANIModel1
print(errorFormat.format(type="Error:", message=message))
print(errorFormat.format(type="", message=error.message))
sys.exit(1)
raise Exception(errorFormat.format(type="Error:", message=message))
raise Exception(errorFormat.format(type="", message=error.message))
def endWithWrongJANIVersion():
message = WrongVersionNumber
print(errorFormat.format(type="Error:", message=message))
sys.exit(1)
raise Exception(errorFormat.format(type="Error:", message=message))
def endWithNotSupportedModelType():
message = NotSupportedModelType
print(errorFormat.format(type="Error:", message=message))
sys.exit(1)
raise Exception(errorFormat.format(type="Error:", message=message))
def endWithNotSupportedFeature():
message = NotSupportedFeature
raise Exception(errorFormat.format(type="Error:", message=message))
def endWithNotSupportedVariable(variableName: str):
message = NotSupportedVariable.format(variableName)
print(errorFormat.format(type="Error:", message=message))
sys.exit(1)
raise Exception(errorFormat.format(type="Error:", message=message))
def endWithNotSupportedWindowsFeature():
message = NotSupportedWindowsFeature
print(errorFormat.format(type="Error:", message=message))
sys.exit(1)
raise Exception(errorFormat.format(type="Error:", message=message))
def endWithNotSupportedFunction(functionName: str):
message = NotSupportedFunction.format(functionName)
print(errorFormat.format(type="Error:", message=message))
sys.exit(1)
raise Exception(errorFormat.format(type="Error:", message=message))
......@@ -8,7 +8,10 @@ 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,
endWithWrongJANIInput,
)
from src.utilities.io.schema.janiModel import JANIjsonSchema
......@@ -93,7 +96,8 @@ def compilePlugin(pluginPath: str, pluginName: str, LTSminPath: str) -> None:
chdir("..")
if platform == "darwin":
run(
f"gcc -shared -o {pluginName}.so -undefined dynamic_lookup implementation/*.o", shell=True,
f"gcc -shared -o {pluginName}.so -undefined dynamic_lookup implementation/*.o",
shell=True,
)
elif platform == "linux":
run(
......
This diff is collapsed.
......@@ -543,7 +543,7 @@ JANIjsonSchema = {
"type": "object",
"additionalProperties": False,
"properties": {
"name": {"type": "string"},
"name": {"type": "string", "pattern": "[^#].*$"},
"time-progress": {
"type": "object",
"additionalProperties": False,
......@@ -571,15 +571,18 @@ JANIjsonSchema = {
"required": ["name"],
},
},
"initial-locations": {"type": "array", "items": {"type": "string"},},
"initial-locations": {
"type": "array",
"items": {"type": "string", "pattern": "[^#].*$"},
},
"edges": {
"type": "array",
"items": {
"type": "object",
"additionalProperties": False,
"properties": {
"location": {"type": "string"},
"action": {"type": "string"},
"location": {"type": "string", "pattern": "[^#].*$"},
"action": {"type": "string", "pattern": "[^#].*$"},
"rate": {
"type": "object",
"additionalProperties": False,
......@@ -602,7 +605,10 @@ JANIjsonSchema = {
"type": "array",
"additionalProperties": False,
"properties": {
"location": {"type": "string"},
"location": {
"type": "string",
"pattern": "[^#].*$",
},
"probability": {
"type": "object",
"additionalProperties": False,
......@@ -1250,7 +1256,7 @@ JANIjsonSchema = {
"additionalProperties": False,
"properties": {
"jani-version": {"type": "integer", "minimum": 1},
"name": {"type": "string"},
"name": {"type": "string", "pattern": "[^#].*$"},
"metadata": {"$ref": "#/definitions/Metadata"},
"type": {"$ref": "#/definitions/ModelType"},
"features": {"type": "array", "items": {"$ref": "#/definitions/ModelFeature"}},
......@@ -1260,7 +1266,7 @@ JANIjsonSchema = {
"type": "object",
"additionalProperties": False,
"properties": {
"name": {"type": "string"},
"name": {"type": "string", "pattern": "[^#].*$"},
"comment": {"type": "string"},
},
"required": ["name"],
......
#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());