Commit 3d9af389 authored by Lars Schieffer's avatar Lars Schieffer
Browse files

update function bug

parent 5c84d0f9
import copy
import src.utilities.io.communication.errors as errors
import src.utilities.parser.expression.toDependency as dependency
import src.utilities.parser.expression.toRename as rename
......@@ -20,6 +22,7 @@ def functionsOf(model: dict, stateVector: StateVector) -> dict:
if "functions" in model:
for function in model["functions"]:
if not dependency.perform(function["body"], stateVector):
function = copy.deepcopy(function)
identifier = function["name"]
function["name"] = f"function_{identifier}"
functionByIdentifier[identifier] = function
......@@ -33,11 +36,12 @@ def functionsOf(model: dict, stateVector: StateVector) -> dict:
if "variables" in automaton:
variables = set(variable["name"] for variable in automaton["variables"])
for function in automaton["functions"]:
function = copy.deepcopy(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}"
function["name"] = f"function_{name}_{identifier}"
functionByIdentifier[identifier] = function
else:
errors.endWithNotSupportedFunction(function["name"])
......
......@@ -132,7 +132,7 @@ def localVariablesTo(
updatedIdentifier = dict()
for identifier in variables:
localIdentifier = f"{automaton}_{identifier}"
if localIdentifier in functions:
if identifier in functions:
updatedIdentifier[identifier] = "function_" + localIdentifier
else:
updatedIdentifier[identifier] = localIdentifier
......
{
"jani-version": 1,
"name": "euclid",
"type": "lts",
"features": [ "derived-operators" ],
"variables": [
{
"name": "term",
"type": "bool",
"initial-value": false
},
{
"name": "count",
"type": "int",
"initial-value": 1
}
],
"properties": [ {
"name": "Term",
"expression": {
"op": "filter",
"fun": "∀",
"values": {
"op": "=",
"left": {
"op": "Pmin",
"exp": {
"op": "F",
"exp": "term"
}
},
"right": 1
},
"states": {
"op": "initial"
}
}
} ],
"automata": [
{
"name": "One",
"locations": [
{
"name": "loc_1"
},
{
"name": "loc_0"
}
],
"initial-locations": [ "loc_1" ],
"edges": [
{
"location": "loc_1",
"guard": {
"exp": {
"op": "≠",
"left": {
"op": "%",
"left": "count",
"right": 3
},
"right": 2
}
},
"destinations": [ {
"location": "loc_1",
"assignments": [ {
"ref": "count",
"value": {
"op": "-",
"left": "count",
"right": 1
}
} ]
} ]
},
{
"location": "loc_1",
"guard": {
"exp": {
"op": "=",
"left": {
"op": "%",
"left": "count",
"right": 3
},
"right": 2
}
},
"destinations": [ {
"location": "loc_0",
"assignments": [ {
"ref": "term",
"value": true
} ]
} ]
}
]
}
],
"system": {
"elements": [ {
"automaton": "One"
} ]
}
}
\ No newline at end of file
#include <jani2pinsPlugin.h>
#ifndef GROUPAMOUNT
#define GROUPAMOUNT 2
#endif
//Create TransitionGroupGuards
guard_t **createTransitionGroupGuardInformation()
{
// Guards of each transition group
int *transitionGuards[GROUPAMOUNT] = {(int[]){0},(int[]){1}};
int transitionGuardsSizes[GROUPAMOUNT] = {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[2][3] = {{1,0,1},{1,1,1}};
int *readDependencies(int group){
return readMatrix[group];
}
// Write Dependencies
int writeMatrix[2][3] = {{1,0,1},{1,1,0}};
int *writeDependencies(int group){
return writeMatrix[group];
}
// Label Dependencies
int labelMatrix[2][3] = {{1,0,1},{1,0,1}};
int *labelDependencies(int label){
return labelMatrix[label];
}
// Do-not-accord
int DNAMatrix[2][2] = {{1,1},{1,1}};
int *dnaGroup(int group){
return DNAMatrix[group];
}
// Necessary Enabling
int NESMatrix[2][2] = {{1,1},{1,1}};
int *necessaryEnabling(int guard){
return NESMatrix[guard];
}
// Necessary Disabling
int NDSMatrix[2][2] = {{1,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 2;
}
// 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);
// 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, "One0");
lts_type_set_state_typeno(lts, 0, intSlot);
lts_type_set_state_name(lts, 1, "term");
lts_type_set_state_typeno(lts, 1, boolSlot);
lts_type_set_state_name(lts, 2, "count");
lts_type_set_state_typeno(lts, 2, 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);
// 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("tau"));
}
#include <jani2pinsPlugin.h>
#ifndef STATEVECTORLENGTH
#define STATEVECTORLENGTH 3
#endif
// Model Constants
// Transient Values
// Function Declarations
// Function Implementations
// The initial state vector
int iSV[STATEVECTORLENGTH] = {0, 0, 1};
int *initialStateVector()
{
return iSV;
}
// Successor function for PINS model using a LONG state vector.
int nextStateLong(model_t model, int group, int *sourceStateVector, TransitionCB callback, void *context)
{
int actionLabel[1];
transition_info_t transitionInformation = {actionLabel, group};
if (group == 0 && ((sourceStateVector[0] == 0) && ((remEuc(sourceStateVector[2],3)) != 2))){
actionLabel[0] = 0;
int targetStateVector[STATEVECTORLENGTH];
memcpy(targetStateVector, sourceStateVector, STATEVECTORLENGTH * sizeof(int));
int One00 = sourceStateVector[0];
int count0 = sourceStateVector[2];
int One01 = One00;
int count1 = count0;
if ((sourceStateVector[0] == 0) && ((remEuc(sourceStateVector[2],3)) != 2)){
One01 = 0;
}
if ((sourceStateVector[0] == 0) && ((remEuc(sourceStateVector[2],3)) != 2)){
count1 = (count0 - 1);
}
targetStateVector[0] = One01;
targetStateVector[2] = count1;
int copy[STATEVECTORLENGTH] = {0,1,0};
callback(context, &transitionInformation, targetStateVector, copy);
return 1;
}
if (group == 1 && ((sourceStateVector[0] == 0) && ((remEuc(sourceStateVector[2],3)) == 2))){
actionLabel[0] = 0;
int targetStateVector[STATEVECTORLENGTH];
memcpy(targetStateVector, sourceStateVector, STATEVECTORLENGTH * sizeof(int));
int One00 = sourceStateVector[0];
int term0 = sourceStateVector[1];
int One01 = One00;
int term1 = term0;
if ((sourceStateVector[0] == 0) && ((remEuc(sourceStateVector[2],3)) == 2)){
One01 = 1;
}
if ((sourceStateVector[0] == 0) && ((remEuc(sourceStateVector[2],3)) == 2)){
term1 = 1;
}
targetStateVector[0] = One01;
targetStateVector[1] = term1;
int copy[STATEVECTORLENGTH] = {0,0,1};
callback(context, &transitionInformation, targetStateVector, copy);