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

update autoconcurrency example

parent 3072472d
{
"jani-version": 1,
"name": "instances",
"name": "autoconcurrency",
"type": "lts",
"features": [ "derived-operators" ],
"actions": [ {
"name": "a"
} ],
"variables": [ {
"name": "term",
"type": "bool",
"initial-value": false
} ],
"properties": [ {
"name": "Term",
"name": "P",
"expression": {
"op": "filter",
"fun": "∀",
......@@ -22,7 +17,7 @@
"op": "Pmin",
"exp": {
"op": "F",
"exp": "term"
"exp": true
}
},
"right": 1
......@@ -34,7 +29,7 @@
} ],
"automata": [
{
"name": "One",
"name": "Receive",
"locations": [
{
"name": "loc_1"
......@@ -55,14 +50,11 @@
]
},
{
"name": "Two",
"name": "Send",
"locations": [
{
"name": "loc_1"
},
{
"name": "loc_4"
},
{
"name": "loc_0"
}
......@@ -73,18 +65,7 @@
"location": "loc_1",
"action": "a",
"destinations": [ {
"location": "loc_4"
} ]
},
{
"location": "loc_4",
"action": "a",
"destinations": [ {
"location": "loc_0",
"assignments": [ {
"ref": "term",
"value": true
} ]
"location": "loc_0"
} ]
}
]
......@@ -93,13 +74,13 @@
"system": {
"elements": [
{
"automaton": "One"
},
"automaton": "Receive"
},
{
"automaton": "One"
"automaton": "Receive"
},
{
"automaton": "Two"
"automaton": "Send"
}
],
"syncs": [ {
......@@ -109,14 +90,13 @@
"a"
],
"result": "a"
} ,
{
}, {
"synchronise": [
null,
"a",
"a"
],
"result": "a"
} ]
} ]
}
}
\ No newline at end of file
#include <jani2pinsPlugin.h>
// Read dependencies to state vector
int readMatrix[2][4] = {{1,0,1,1},{0,1,1,1}};
int readMatrix[2][3] = {{1,0,1},{0,1,1}};
int *readDependencies(int group){
return readMatrix[group];
}
// Write Dependencies
int writeMatrix[2][4] = {{1,0,1,1},{0,1,1,1}};
int writeMatrix[2][3] = {{1,0,1},{0,1,1}};
int *writeDependencies(int group){
return writeMatrix[group];
}
// Label Dependencies
int labelMatrix[3][4] = {{1,0,0,0},{0,0,1,0},{0,1,0,0}};
int labelMatrix[3][3] = {{1,0,0},{0,0,1},{0,1,0}};
int *labelDependencies(int label){
return labelMatrix[label];
}
......
......@@ -20,7 +20,7 @@ int guardAmount()
// The length of the whole state vector
int stateVectorLength()
{
return 4;
return 3;
}
// Initialise the PINS model
......@@ -43,14 +43,12 @@ void initModel(model_t model)
// Define StateVector
lts_type_set_state_length(lts, stateVectorLength());
lts_type_set_state_name(lts, 0, "One_instance_0");
lts_type_set_state_name(lts, 0, "Receive_instance_0");
lts_type_set_state_typeno(lts, 0, intSlot);
lts_type_set_state_name(lts, 1, "One_instance_1");
lts_type_set_state_name(lts, 1, "Receive_instance_1");
lts_type_set_state_typeno(lts, 1, intSlot);
lts_type_set_state_name(lts, 2, "Two_instance_0");
lts_type_set_state_name(lts, 2, "Send_instance_0");
lts_type_set_state_typeno(lts, 2, intSlot);
lts_type_set_state_name(lts, 3, "term");
lts_type_set_state_typeno(lts, 3, boolSlot);
// Define StateLabels
lts_type_set_state_label_count(lts, labelAmount());
......
#include <jani2pinsPlugin.h>
#ifndef STATEVECTORLENGTH
#define STATEVECTORLENGTH 6
#define STATEVECTORLENGTH 3
#endif
// Model Constants
......@@ -9,7 +9,7 @@
// Function Implementations
// The initial state vector
int iSV[STATEVECTORLENGTH] = {0, 0, 0, 0, 0, 0};
int iSV[STATEVECTORLENGTH] = {0, 0, 0};
int *initialStateVector()
{
return iSV;
......@@ -25,27 +25,17 @@ int nextStateLong(model_t model, int group, int *sourceStateVector, TransitionCB
actionLabel[0] = 0;
int targetStateVector[STATEVECTORLENGTH];
memcpy(targetStateVector, sourceStateVector, STATEVECTORLENGTH * sizeof(int));
int P1_instance_01 = sourceStateVector[0];
int P3_instance_01 = sourceStateVector[2];
int term11 = sourceStateVector[3];
int term31 = sourceStateVector[5];
int Receive_instance_01 = sourceStateVector[0];
int Send_instance_01 = sourceStateVector[2];
if (sourceStateVector[0] == 0){
P1_instance_01 = 1;
}
if (sourceStateVector[0] == 0){
term11 = 1;
}
if (sourceStateVector[2] == 0){
P3_instance_01 = 1;
Receive_instance_01 = 1;
}
if (sourceStateVector[2] == 0){
term31 = 1;
Send_instance_01 = 1;
}
targetStateVector[0] = P1_instance_01;
targetStateVector[2] = P3_instance_01;
targetStateVector[3] = term11;
targetStateVector[5] = term31;
int copy[STATEVECTORLENGTH] = {0,1,0,0,1,0};
targetStateVector[0] = Receive_instance_01;
targetStateVector[2] = Send_instance_01;
int copy[STATEVECTORLENGTH] = {0,1,0};
callback(context, &transitionInformation, targetStateVector, copy);
return 1;
}
......@@ -53,27 +43,17 @@ int nextStateLong(model_t model, int group, int *sourceStateVector, TransitionCB
actionLabel[0] = 0;
int targetStateVector[STATEVECTORLENGTH];
memcpy(targetStateVector, sourceStateVector, STATEVECTORLENGTH * sizeof(int));
int P2_instance_01 = sourceStateVector[1];
int P3_instance_01 = sourceStateVector[2];
int term21 = sourceStateVector[4];
int term31 = sourceStateVector[5];
if (sourceStateVector[1] == 0){
P2_instance_01 = 1;
}
int Receive_instance_11 = sourceStateVector[1];
int Send_instance_01 = sourceStateVector[2];
if (sourceStateVector[1] == 0){
term21 = 1;
Receive_instance_11 = 1;
}
if (sourceStateVector[2] == 0){
P3_instance_01 = 1;
Send_instance_01 = 1;
}
if (sourceStateVector[2] == 0){
term31 = 1;
}
targetStateVector[1] = P2_instance_01;
targetStateVector[2] = P3_instance_01;
targetStateVector[4] = term21;
targetStateVector[5] = term31;
int copy[STATEVECTORLENGTH] = {1,0,0,1,0,0};
targetStateVector[1] = Receive_instance_11;
targetStateVector[2] = Send_instance_01;
int copy[STATEVECTORLENGTH] = {1,0,0};
callback(context, &transitionInformation, targetStateVector, copy);
return 1;
}
......@@ -89,52 +69,32 @@ int nextStateR2W(model_t model, int group, int *sourceStateVector, TransitionCB
if (group == 0 && ((sourceStateVector[0] == 0) && (sourceStateVector[1] == 0))){
actionLabel[0] = 0;
int targetStateVector[dm_ones_in_row(GBgetDMInfoMustWrite(model), group)];
int P1_instance_01 = sourceStateVector[0];
int P3_instance_01 = sourceStateVector[1];
int term11;
int term31;
if (sourceStateVector[0] == 0){
P1_instance_01 = 1;
}
int Receive_instance_01 = sourceStateVector[0];
int Send_instance_01 = sourceStateVector[1];
if (sourceStateVector[0] == 0){
term11 = 1;
}
if (sourceStateVector[1] == 0){
P3_instance_01 = 1;
Receive_instance_01 = 1;
}
if (sourceStateVector[1] == 0){
term31 = 1;
Send_instance_01 = 1;
}
targetStateVector[0] = P1_instance_01;
targetStateVector[1] = P3_instance_01;
targetStateVector[2] = term11;
targetStateVector[3] = term31;
targetStateVector[0] = Receive_instance_01;
targetStateVector[1] = Send_instance_01;
callback(context, &transitionInformation, targetStateVector, NULL);
return 1;
}
if (group == 1 && ((sourceStateVector[0] == 0) && (sourceStateVector[1] == 0))){
actionLabel[0] = 0;
int targetStateVector[dm_ones_in_row(GBgetDMInfoMustWrite(model), group)];
int P2_instance_01 = sourceStateVector[0];
int P3_instance_01 = sourceStateVector[1];
int term21;
int term31;
int Receive_instance_11 = sourceStateVector[0];
int Send_instance_01 = sourceStateVector[1];
if (sourceStateVector[0] == 0){
P2_instance_01 = 1;
}
if (sourceStateVector[0] == 0){
term21 = 1;
}
if (sourceStateVector[1] == 0){
P3_instance_01 = 1;
Receive_instance_11 = 1;
}
if (sourceStateVector[1] == 0){
term31 = 1;
Send_instance_01 = 1;
}
targetStateVector[0] = P2_instance_01;
targetStateVector[1] = P3_instance_01;
targetStateVector[2] = term21;
targetStateVector[3] = term31;
targetStateVector[0] = Receive_instance_11;
targetStateVector[1] = Send_instance_01;
callback(context, &transitionInformation, targetStateVector, NULL);
return 1;
}
......@@ -150,52 +110,32 @@ int actionsR2W(model_t model, int group, int *sourceStateVector, TransitionCB ca
if (group == 0){
actionLabel[0] = 0;
int targetStateVector[dm_ones_in_row(GBgetDMInfoMustWrite(model), group)];
int P1_instance_01 = sourceStateVector[0];
int P3_instance_01 = sourceStateVector[1];
int term11;
int term31;
if (sourceStateVector[0] == 0){
P1_instance_01 = 1;
}
int Receive_instance_01 = sourceStateVector[0];
int Send_instance_01 = sourceStateVector[1];
if (sourceStateVector[0] == 0){
term11 = 1;
Receive_instance_01 = 1;
}
if (sourceStateVector[1] == 0){
P3_instance_01 = 1;
Send_instance_01 = 1;
}
if (sourceStateVector[1] == 0){
term31 = 1;
}
targetStateVector[0] = P1_instance_01;
targetStateVector[1] = P3_instance_01;
targetStateVector[2] = term11;
targetStateVector[3] = term31;
targetStateVector[0] = Receive_instance_01;
targetStateVector[1] = Send_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 P2_instance_01 = sourceStateVector[0];
int P3_instance_01 = sourceStateVector[1];
int term21;
int term31;
if (sourceStateVector[0] == 0){
P2_instance_01 = 1;
}
int Receive_instance_11 = sourceStateVector[0];
int Send_instance_01 = sourceStateVector[1];
if (sourceStateVector[0] == 0){
term21 = 1;
}
if (sourceStateVector[1] == 0){
P3_instance_01 = 1;
Receive_instance_11 = 1;
}
if (sourceStateVector[1] == 0){
term31 = 1;
Send_instance_01 = 1;
}
targetStateVector[0] = P2_instance_01;
targetStateVector[1] = P3_instance_01;
targetStateVector[2] = term21;
targetStateVector[3] = term31;
targetStateVector[0] = Receive_instance_11;
targetStateVector[1] = Send_instance_01;
callback(context, &transitionInformation, targetStateVector, NULL);
return 1;
}
......
#include <jani2pinsPlugin.h>
// Read dependencies to state vector
int readMatrix[2][4] = {{1,0,1,1},{0,1,1,1}};
int readMatrix[2][3] = {{1,0,1},{0,1,1}};
int *readDependencies(int group){
return readMatrix[group];
}
// Write Dependencies
int writeMatrix[2][4] = {{1,0,1,1},{0,1,1,1}};
int writeMatrix[2][3] = {{1,0,1},{0,1,1}};
int *writeDependencies(int group){
return writeMatrix[group];
}
// Label Dependencies
int labelMatrix[3][4] = {{1,0,0,0},{0,0,1,0},{0,1,0,0}};
int labelMatrix[3][3] = {{1,0,0},{0,0,1},{0,1,0}};
int *labelDependencies(int label){
return labelMatrix[label];
}
......
......@@ -20,7 +20,7 @@ int guardAmount()
// The length of the whole state vector
int stateVectorLength()
{
return 4;
return 3;
}
// Initialise the PINS model
......@@ -43,14 +43,12 @@ void initModel(model_t model)
// Define StateVector
lts_type_set_state_length(lts, stateVectorLength());
lts_type_set_state_name(lts, 0, "One_instance_0");
lts_type_set_state_name(lts, 0, "Receive_instance_0");
lts_type_set_state_typeno(lts, 0, intSlot);
lts_type_set_state_name(lts, 1, "One_instance_1");
lts_type_set_state_name(lts, 1, "Receive_instance_1");
lts_type_set_state_typeno(lts, 1, intSlot);
lts_type_set_state_name(lts, 2, "Two_instance_0");
lts_type_set_state_name(lts, 2, "Send_instance_0");
lts_type_set_state_typeno(lts, 2, intSlot);
lts_type_set_state_name(lts, 3, "term");
lts_type_set_state_typeno(lts, 3, boolSlot);
// Define StateLabels
lts_type_set_state_label_count(lts, labelAmount());
......
#include <jani2pinsPlugin.h>
#ifndef STATEVECTORLENGTH
#define STATEVECTORLENGTH 6
#define STATEVECTORLENGTH 3
#endif
// Model Constants
......@@ -9,7 +9,7 @@
// Function Implementations
// The initial state vector
int iSV[STATEVECTORLENGTH] = {0, 0, 0, 0, 0, 0};
int iSV[STATEVECTORLENGTH] = {0, 0, 0};
int *initialStateVector()
{
return iSV;
......@@ -25,27 +25,17 @@ int nextStateLong(model_t model, int group, int *sourceStateVector, TransitionCB
actionLabel[0] = 0;
int targetStateVector[STATEVECTORLENGTH];
memcpy(targetStateVector, sourceStateVector, STATEVECTORLENGTH * sizeof(int));
int P1_instance_01 = sourceStateVector[0];
int P3_instance_01 = sourceStateVector[2];
int term11 = sourceStateVector[3];
int term31 = sourceStateVector[5];
int Receive_instance_01 = sourceStateVector[0];
int Send_instance_01 = sourceStateVector[2];
if (sourceStateVector[0] == 0){
P1_instance_01 = 1;
}
if (sourceStateVector[0] == 0){
term11 = 1;
}
if (sourceStateVector[2] == 0){
P3_instance_01 = 1;
Receive_instance_01 = 1;
}
if (sourceStateVector[2] == 0){
term31 = 1;
Send_instance_01 = 1;
}
targetStateVector[0] = P1_instance_01;
targetStateVector[2] = P3_instance_01;
targetStateVector[3] = term11;
targetStateVector[5] = term31;
int copy[STATEVECTORLENGTH] = {0,1,0,0,1,0};
targetStateVector[0] = Receive_instance_01;
targetStateVector[2] = Send_instance_01;
int copy[STATEVECTORLENGTH] = {0,1,0};
callback(context, &transitionInformation, targetStateVector, copy);
return 1;
}
......@@ -53,27 +43,17 @@ int nextStateLong(model_t model, int group, int *sourceStateVector, TransitionCB
actionLabel[0] = 0;
int targetStateVector[STATEVECTORLENGTH];
memcpy(targetStateVector, sourceStateVector, STATEVECTORLENGTH * sizeof(int));
int P2_instance_01 = sourceStateVector[1];
int P3_instance_01 = sourceStateVector[2];
int term21 = sourceStateVector[4];
int term31 = sourceStateVector[5];
if (sourceStateVector[1] == 0){
P2_instance_01 = 1;
}
int Receive_instance_11 = sourceStateVector[1];
int Send_instance_01 = sourceStateVector[2];
if (sourceStateVector[1] == 0){
term21 = 1;
Receive_instance_11 = 1;
}
if (sourceStateVector[2] == 0){
P3_instance_01 = 1;
Send_instance_01 = 1;
}
if (sourceStateVector[2] == 0){
term31 = 1;
}
targetStateVector[1] = P2_instance_01;
targetStateVector[2] = P3_instance_01;
targetStateVector[4] = term21;
targetStateVector[5] = term31;
int copy[STATEVECTORLENGTH] = {1,0,0,1,0,0};
targetStateVector[1] = Receive_instance_11;
targetStateVector[2] = Send_instance_01;
int copy[STATEVECTORLENGTH] = {1,0,0};
callback(context, &transitionInformation, targetStateVector, copy);
return 1;
}
......@@ -89,52 +69,32 @@ int nextStateR2W(model_t model, int group, int *sourceStateVector, TransitionCB
if (group == 0 && ((sourceStateVector[0] == 0) && (sourceStateVector[1] == 0))){
actionLabel[0] = 0;
int targetStateVector[dm_ones_in_row(GBgetDMInfoMustWrite(model), group)];
int P1_instance_01 = sourceStateVector[0];
int P3_instance_01 = sourceStateVector[1];
int term11 = sourceStateVector[2];
int term31 = sourceStateVector[3];
if (sourceStateVector[0] == 0){
P1_instance_01 = 1;
}
int Receive_instance_01 = sourceStateVector[0];
int Send_instance_01 = sourceStateVector[1];
if (sourceStateVector[0] == 0){
term11 = 1;
}
if (sourceStateVector[1] == 0){
P3_instance_01 = 1;
Receive_instance_01 = 1;
}
if (sourceStateVector[1] == 0){
term31 = 1;
Send_instance_01 = 1;
}
targetStateVector[0] = P1_instance_01;
targetStateVector[1] = P3_instance_01;
targetStateVector[2] = term11;
targetStateVector[3] = term31;
targetStateVector[0] = Receive_instance_01;
targetStateVector[1] = Send_instance_01;
callback(context, &transitionInformation, targetStateVector, NULL);
return 1;
}
if (group == 1 && ((sourceStateVector[0] == 0) && (sourceStateVector[1] == 0))){
actionLabel[0] = 0;
int targetStateVector[dm_ones_in_row(GBgetDMInfoMustWrite(model), group)];
int P2_instance_01 = sourceStateVector[0];
int P3_instance_01 = sourceStateVector[1];
int term21 = sourceStateVector[2];
int term31 = sourceStateVector[3];
int Receive_instance_11 = sourceStateVector[0];
int Send_instance_01 = sourceStateVector[1];
if (sourceStateVector[0] == 0){
P2_instance_01 = 1;
}
if (sourceStateVector[0] == 0){
term21 = 1;
}
if (sourceStateVector[1] == 0){
P3_instance_01 = 1;
Receive_instance_11 = 1;
}
if (sourceStateVector[1] == 0){
term31 = 1;
Send_instance_01 = 1;
}
targetStateVector[0] = P2_instance_01;
targetStateVector[1] = P3_instance_01;
targetStateVector[2] = term21;
targetStateVector[3] = term31;
targetStateVector[0] = Receive_instance_11;
targetStateVector[1] = Send_instance_01;