Commit 5e95b3a7 authored by Lars Schieffer's avatar Lars Schieffer
Browse files

initialise tests

parent 57d9c50e
......@@ -53,7 +53,7 @@ def edgesByAutomatonOf(model: dict, functions: dict) -> dict:
oldLabels[automaton].add(label)
edges = flattenOf(edges)
for uniqueIndex, edge in enumerate(edges):
updatedLabel = result + str(uniqueIndex)
updatedLabel = "{}_flatten_{}".format(result, uniqueIndex)
updatedVector = []
for index, entry in enumerate(syncVector):
if entry:
......@@ -66,11 +66,11 @@ def edgesByAutomatonOf(model: dict, functions: dict) -> dict:
flattenSyncs.append(synchronisation)
else:
flattenSyncs.append(synchronisation)
model["system"]["syncs"] = flattenSyncs
for automaton in oldLabels:
labels = oldLabels[automaton]
for label in sorted(list(labels)):
edgesByAutomaton[automaton].pop(label, None)
model["system"]["syncs"] = flattenSyncs
for automaton in oldLabels:
labels = oldLabels[automaton]
for label in sorted(list(labels)):
edgesByAutomaton[automaton].pop(label, None)
return edgesByAutomaton
......
def functionsOf(model: dict) -> dict:
import src.utilities.io.communication.errors as errors
import src.utilities.parser.expression.toDependency as dependency
import src.utilities.parser.expression.toRename as rename
from src.pins.modules.stateVector import StateVector
def functionsOf(model: dict, stateVector: StateVector) -> dict:
"""
Function Description:
Update jani-model function identifier
......@@ -13,15 +19,26 @@ def functionsOf(model: dict) -> dict:
functionByIdentifier = {}
if "functions" in model:
for function in model["functions"]:
identifier = function["name"]
function["name"] = f"function_{identifier}"
functionByIdentifier[identifier] = function
if not dependency.perform(function["body"], stateVector):
identifier = function["name"]
function["name"] = f"function_{identifier}"
functionByIdentifier[identifier] = function
else:
errors.endWithNotSupportedFunction(function["name"])
for automaton in model["automata"]:
if "functions" in automaton:
name = automaton["name"]
variables = set()
if "variables" in automaton:
variables = set(variable["name"] for variable in automaton["variables"])
for function in automaton["functions"]:
identifier = function["name"]
function["name"] = f"{name}_function_{identifier}"
functionByIdentifier[identifier] = function
body = function["body"]
body = rename.localVariablesTo(body, variables, name, dict())
if not dependency.perform(body, stateVector):
identifier = function["name"]
function["name"] = f"{name}_function_{identifier}"
functionByIdentifier[identifier] = function
else:
errors.endWithNotSupportedFunction(function["name"])
return functionByIdentifier
......@@ -51,7 +51,7 @@ class Model:
isSupported(janiModel, real2int)
self.__constants = constants.declare(janiModel, experiment)
self.__stateVector = self.__createStateVector(janiModel, real2int)
self.__janiFunctions = functionsOf(janiModel)
self.__janiFunctions = functionsOf(janiModel, self.__stateVector)
self.__locations = self.__createLocations(janiModel["automata"])
(
self.__transitionGroups,
......
......@@ -3,6 +3,7 @@ import sys
from jsonschema.exceptions import ValidationError
# Error communication
errorFormat = "{type:<8} {message}"
OperatorNotSupportedMessage = "Operator {} not supported"
ExpressionNotSupportedMessage = "Expression {} not supported"
......@@ -21,57 +22,77 @@ NotSupportedModelType = 'JANI2PINS supports only model of type "lts", "dtmc" and
NotSupportedVariable = "JANI2PINS does not support variable: {}"
NotSupportedFunction = (
"JANI2PINS does not support function: {}, because it contains jani-model variables."
)
NotSupportedWindowsFeature = (
"The compilation of PINS models is only supported under Linux & macOS"
)
def notSupportedOperator(operator) -> None:
print(OperatorNotSupportedMessage.format(repr(operator)))
message = OperatorNotSupportedMessage.format(repr(operator))
print(errorFormat.format(type="Error:", message=message))
sys.exit(1)
def notSupportedExpression(expression) -> None:
print(ExpressionNotSupportedMessage.format(repr(expression)))
message = ExpressionNotSupportedMessage.format(repr(expression))
print(errorFormat.format(type="Error:", message=message))
sys.exit(1)
def endWithConstantsHaveToBeSpecifiedError(parameter: str):
print(ConstantsHaveToBeSpecifiedMessage.format(parameter))
message = ConstantsHaveToBeSpecifiedMessage.format(parameter)
print(errorFormat.format(type="Error:", message=message))
sys.exit(1)
def endWithWrongConstantTypeError(constantName: str, constantType: str):
print(NotSupportedTypeMessage.format("constant", constantName, constantType))
message = NotSupportedTypeMessage.format("constant", constantName, constantType)
print(errorFormat.format(type="Error:", message=message))
sys.exit(1)
def endWithWrongModeError(mode: str):
print(NotSupportedModeMessage.format(mode))
message = NotSupportedModeMessage.format(mode)
print(errorFormat.format(type="Error:", message=message))
sys.exit(1)
def endWithWrongJANIInput(error: ValidationError):
print(IncorrectJANIModel1)
print(error.message)
message = IncorrectJANIModel1
print(errorFormat.format(type="Error:", message=message))
print(errorFormat.format(type="", message=error.message))
sys.exit(1)
def endWithWrongJANIVersion():
print(WrongVersionNumber)
message = WrongVersionNumber
print(errorFormat.format(type="Error:", message=message))
sys.exit(1)
def endWithNotSupportedModelType():
print(NotSupportedModelType)
message = NotSupportedModelType
print(errorFormat.format(type="Error:", message=message))
sys.exit(1)
def endWithNotSupportedVariable(variableName: str):
print(NotSupportedVariable.format(variableName))
message = NotSupportedVariable.format(variableName)
print(errorFormat.format(type="Error:", message=message))
sys.exit(1)
def endWithNotSupportedWindowsFeature():
print(NotSupportedWindowsFeature)
message = NotSupportedWindowsFeature
print(errorFormat.format(type="Error:", message=message))
sys.exit(1)
def endWithNotSupportedFunction(functionName: str):
message = NotSupportedFunction.format(functionName)
print(errorFormat.format(type="Error:", message=message))
sys.exit(1)
from os.path import join
import src.utilities.io.filesystem as filesystem
from src.pins.modules.locations import Locations
from src.pins.modules.stateVector import StateVector
from src.pins.plugin import PINS
from src.utilities.parser.expression.toExpression import createExperiments
def checkModel(jani_input_path, pinsImplementationPath, experiment=""):
matricesPath = join(pinsImplementationPath, "matrices.c")
guardImplementationPath = join(pinsImplementationPath, "guardImplementation.c")
modelSettingsPath = join(pinsImplementationPath, "modelSettings.c")
nextStatesFunctionsPath = join(pinsImplementationPath, "nextStatesFunctions.c")
pinsPlugin = PINS(
janiModel=filesystem.loadJANI(jani_input_path, False),
real2int=True,
experiment=createExperiments(experiment),
)
with open(matricesPath, "r") as matrices:
assert pinsPlugin.matrices == matrices.read()
with open(guardImplementationPath, "r") as guardImplementation:
assert pinsPlugin.guardImplementation == guardImplementation.read()
with open(modelSettingsPath, "r") as modelSettings:
assert pinsPlugin.modelSettings == modelSettings.read()
with open(nextStatesFunctionsPath, "r") as nextStatesFunctions:
assert pinsPlugin.nextStatesFunctions == nextStatesFunctions.read()
# Example Model
locations = Locations()
locations.addLocation("l1")
locations.addLocation("l0")
stateVector = StateVector()
emptyStateVector = StateVector()
stateVector.addAutomaton("A1", "l1")
stateVector.addVariable("condition", False, "bool", False)
variablesRenaming = {"condition": "RENAMED"}
# Example Expressions
constantExpression = False
identifierExpressionVariable = "condition"
identifierExpressionAutomaton = "A1"
identifierExpressionLocation = "l1"
unaryExpression = {"op": "¬", "exp": "condition"}
binaryExpression = {"op": "=", "left": unaryExpression, "right": "condition"}
ternaryExpression = {"op": "ite", "if": "condition", "then": 1, "else": 0}
This diff is collapsed.
#include <jani2pinsPlugin.h>
#ifndef GROUPAMOUNT
#define GROUPAMOUNT 1
#endif
//Create TransitionGroupGuards
guard_t **createTransitionGroupGuardInformation()
{
// Guards of each transition group
int *transitionGuards[GROUPAMOUNT] = {(int[]){0,1}};
int transitionGuardsSizes[GROUPAMOUNT] = {2};
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[1][3] = {{1,1,1}};
int *readDependencies(int group){
return readMatrix[group];
}
// Write Dependencies
int writeMatrix[1][3] = {{1,1,1}};
int *writeDependencies(int group){
return writeMatrix[group];
}
// Label Dependencies
int labelMatrix[2][3] = {{1,0,0},{0,1,0}};
int *labelDependencies(int label){
return labelMatrix[label];
}
// Do-not-accord
int DNAMatrix[1][1] = {{1}};
int *dnaGroup(int group){
return DNAMatrix[group];
}
// Necessary Enabling
int NESMatrix[2][1] = {{1},{1}};
int *necessaryEnabling(int guard){
return NESMatrix[guard];
}
// Necessary Disabling
int NDSMatrix[2][1] = {{1},{1}};
int *necessaryDisabling(int guard){
return NDSMatrix[guard];
}
// Maybe co-enabled
int MCEMatrix[2][2] = {{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 1;
}
// The amount of all defined labels
int labelAmount()
{
return 2;
}
// The amount of all defined guards
int guardAmount()
{
return 2;
}
// The length of the whole state vector
int stateVectorLength()
{
return 3;
}
// 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);