Commit 39a9f3e5 authored by Lars Schieffer's avatar Lars Schieffer
Browse files

add input-enable semantics

parent 3d9af389
[pytest]
; addopts= -n4
addopts= -n4
junit_family=xunit1
\ No newline at end of file
......@@ -7,7 +7,7 @@ from src.pins.modules.locations import Locations
from src.pins.modules.stateVector import StateVector
def edgesByAutomatonOf(model: dict, functions: dict) -> dict:
def instancesOf(model: dict, functions: dict) -> list:
"""
Function Description:
Customise jani-model automata, so that valid PINS model composition.
......@@ -19,59 +19,65 @@ def edgesByAutomatonOf(model: dict, functions: dict) -> dict:
Defined functions in PINS model
"""
system = model["system"]
elements = system["elements"]
ndLabels = dict()
edgesByAutomaton = dict()
for automaton in model["automata"]:
name = automaton["name"]
edgesByLocation = edgesByLocationOf(automaton, functions)
edgesByAutomaton[name], ndLabels[name] = edgesByLabelOf(edgesByLocation, name)
elements = [element["automaton"] for element in system["elements"]]
inputEnable = [
element["input-enable"] if "input-enable" in element else []
for element in system["elements"]
]
automataByName = {automaton["name"]: automaton for automaton in model["automata"]}
ndLabels = []
instances = []
for index, automaton in enumerate(elements):
uniqueNumber = elements[:index].count(automaton)
instance = f"{automaton}_instance_{uniqueNumber}"
edgesByLocation = edgesByLocationOf(
automataByName[automaton], functions, inputEnable[index]
)
edges, nonDet = edgesByLabelOf(edgesByLocation, instance)
instances.append(edges)
ndLabels.append(nonDet)
if "syncs" not in system:
syncs = []
for index, element in enumerate(elements):
automaton = element["automaton"]
for label in edgesByAutomaton[automaton]:
if not label == "tau":
synchronise = [None] * len(elements)
for index, instant in enumerate(instances):
for label in instant:
if label != "tau" and label not in inputEnable[index]:
synchronise = [None] * len(instances)
synchronise[index] = label
sync = {"result": label, "synchronise": synchronise}
syncs.append(sync)
model["system"]["syncs"] = syncs
oldLabels = {automaton["name"]: set() for automaton in model["automata"]}
flattenSyncs = []
updatedSyncs = []
removeLabel = [set() for number in range(len(instances))]
for synchronisation in system["syncs"]:
result = synchronisation["result"] if "result" in synchronisation else "tau"
syncVector = synchronisation["synchronise"]
if isLocal(syncVector) or ndProblem(syncVector, ndLabels, elements):
if isLocal(syncVector) or ndProblem(syncVector, ndLabels):
edges = []
for index, label in enumerate(syncVector):
if label:
automaton = elements[index]["automaton"]
edges.append(edgesByAutomaton[automaton][label])
oldLabels[automaton].add(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:
automaton = elements[index]["automaton"]
edgesByAutomaton[automaton][updatedLabel] = [edge.pop(0)]
instances[index][updatedLabel] = [edge.pop(0)]
updatedVector.append(updatedLabel)
else:
updatedVector.append(None)
synchronisation = {"result": result, "synchronise": updatedVector}
flattenSyncs.append(synchronisation)
updatedSyncs.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)
return edgesByAutomaton
updatedSyncs.append(synchronisation)
model["system"]["syncs"] = updatedSyncs
for index, labels in enumerate(removeLabel):
for label in list(labels):
instances[index].pop(label, None)
return instances
def isLocal(synchronisation: list) -> bool:
......@@ -86,7 +92,7 @@ def isLocal(synchronisation: list) -> bool:
return len(synchronisation) - synchronisation.count(None) == 1
def ndProblem(synchronisation: list, ndLabels: dict, elements: dict) -> bool:
def ndProblem(synchronisation: list, ndLabels: dict) -> bool:
"""
Function Description:
Return wether non deterministic choice can occur in synchronised labels.
......@@ -96,13 +102,10 @@ def ndProblem(synchronisation: list, ndLabels: dict, elements: dict) -> bool:
Single synchronisation vector in jani-model system
ndLabels: dict
Labels with non deterministic choices
elements: dict
Automata instances in automata composition
"""
containND = []
for index, label in enumerate(synchronisation):
automaton = elements[index]["automaton"]
containND.append(label in ndLabels[automaton])
containND.append(label in ndLabels[index])
return any(containND)
......@@ -175,7 +178,7 @@ def updateAssignmentsOf(
return assignments
def edgesByLocationOf(automaton: dict, functions: dict) -> dict:
def edgesByLocationOf(automaton: dict, functions: dict, inputEnable: list) -> dict:
"""
Function Description:
Gather edges of jani-model automaton according their automaton locations.
......@@ -185,6 +188,8 @@ def edgesByLocationOf(automaton: dict, functions: dict) -> dict:
jani-model automaton
functions: dict
Defined functions in PINS model
inputEnable: list
Input-enabled edges
"""
name = automaton["name"]
edgesByLocation = dict()
......@@ -212,9 +217,29 @@ def edgesByLocationOf(automaton: dict, functions: dict) -> dict:
edgesByLocation[location][label]["edges"].append(edge)
edgesByLocation[location][label]["amount"] += len(edge["destinations"])
for location in edgesByLocation:
for identifier in inputEnable:
if identifier not in edgesByLocation[location]:
loop = [selfLoop(identifier, location)]
edgesByLocation[location][identifier] = {"edges": loop, "amount": 1}
return edgesByLocation
def selfLoop(label: str, location: str) -> dict:
"""
Function Description:
Build self loop edge according to the jani-model specification
Function Parameters:
label: str
label of transition
location: str
location in automaton
"""
destination = {"location": location}
return {"action": label, "location": location, "destinations": [destination]}
def edgesByLabelOf(edgesByLocation: dict, automaton: str) -> dict:
"""
Function Description:
......
......@@ -123,13 +123,14 @@ class Model:
janiAutomata = {
automaton["name"]: automaton for automaton in janiModel["automata"]
}
actionsOfAutomata = strategy.edgesByAutomatonOf(janiModel, self.__janiFunctions)
janiSystem = janiModel["system"]
names = {element["automaton"]: 0 for element in janiSystem["elements"]}
elements = []
for element in janiSystem["elements"]:
elements.append(element["automaton"] + str(names[element["automaton"]]))
names[element["automaton"]] += 1
instances = strategy.instancesOf(janiModel, self.__janiFunctions)
system = janiModel["system"]
elements = [element["automaton"] for element in system["elements"]]
uniqueNames = []
for index, automaton in enumerate(elements):
uniqueNumber = elements[:index].count(automaton)
uniqueNames.append(f"{automaton}_instance_{uniqueNumber}")
# Collecting all used guards in the PINS-Model
transitionGroupGuards = ModelGuards()
......@@ -137,37 +138,37 @@ class Model:
# Add groups of synchronized actions to PINS-Model
synchronisedActions = set()
edgeLabels = Actions()
if "syncs" in janiSystem:
for sync in janiSystem["syncs"]:
syncTable = sync["synchronise"]
syncLabel = sync["result"] if "result" in sync else "tau"
edgeLabels.addLabel(syncLabel)
if "syncs" in system:
for sync in system["syncs"]:
syncVector = sync["synchronise"]
result = sync["result"] if "result" in sync else "tau"
edgeLabels.addLabel(result)
group = []
groupGuards = []
transientVariables = dict()
for automatonIndex, edgesLabel in enumerate(syncTable):
automatonName = janiSystem["elements"][automatonIndex]["automaton"]
if edgesLabel:
edges = actionsOfAutomata[automatonName][edgesLabel]
for index, label in enumerate(syncVector):
if label:
edges = instances[index][label]
name = system["elements"][index]["automaton"]
transientVariables.update(
transientValuesOf(
edges[0]["location"],
transientVariablesOf(janiAutomata[automatonName]),
transientVariablesOf(janiAutomata[name]),
)
)
for automatonIndex, edgesLabel in enumerate(syncTable):
automatonName = janiSystem["elements"][automatonIndex]["automaton"]
if edgesLabel:
synchronisedActions.add(edgesLabel)
edges = actionsOfAutomata[automatonName][edgesLabel]
for automatonIndex, label in enumerate(syncVector):
old = system["elements"][automatonIndex]["automaton"]
if label:
synchronisedActions.add(label)
edges = instances[automatonIndex][label]
edges = rename.updateAutomatonName(
edges, automatonName, elements[automatonIndex]
edges, old, uniqueNames[automatonIndex]
)
group += edges
guards = []
for transitionIndex, transition in enumerate(edges):
for transitionIndex, arc in enumerate(edges):
updatedGuard = []
for condition in transition["enable"]:
for condition in arc["enable"]:
updatedGuard.append(
rename.variables(
condition,
......@@ -182,22 +183,21 @@ class Model:
groupGuards.append(guards)
transitionGroupGuards.addGuard(guards, self.__stateVector)
synchronisedGroup = TransitionGroup(
syncLabel, group, groupGuards, self.__stateVector
result, group, groupGuards, self.__stateVector
)
transitionGroups.append(synchronisedGroup)
# Add edges, which don't participate in synchronization as transition groups
for automatonIndex, automatonName in enumerate(janiSystem["elements"]):
automatonName = automatonName["automaton"]
if "tau" in actionsOfAutomata[automatonName]:
edgesOfAutomaton = actionsOfAutomata[automatonName]["tau"]
edgesOfAutomaton = rename.updateAutomatonName(
edgesOfAutomaton, automatonName, elements[automatonIndex]
)
for edge in edgesOfAutomaton:
# Add tau edges to PINS model
for index, instance in enumerate(instances):
if "tau" in instance:
edges = instance["tau"]
old = system["elements"][index]["automaton"]
edges = rename.updateAutomatonName(edges, old, uniqueNames[index])
for edge in edges:
name = system["elements"][index]["automaton"]
transientVariables = transientValuesOf(
edge["location"],
transientVariablesOf(janiAutomata[automatonName]),
edge["location"], transientVariablesOf(janiAutomata[name]),
)
edgeLabels.addLabel("tau")
edge["enable"] = rename.variables(
......
......@@ -84,9 +84,11 @@ class StateVector:
for automaton in initialLocations:
instances[automaton] = names.count(automaton)
for instance in instances:
for index in range(instances[instance]):
self.addAutomaton(instance + str(index), initialLocations[instance])
for automaton in instances:
for uniqueNumber in range(instances[automaton]):
self.addAutomaton(
f"{automaton}_instance_{uniqueNumber}", initialLocations[automaton]
)
for automaton in janiModel["automata"]:
if "variables" in automaton:
......
......@@ -43,15 +43,15 @@ void initModel(model_t model)
// Define StateVector
lts_type_set_state_length(lts, stateVectorLength());
lts_type_set_state_name(lts, 0, "sender0");
lts_type_set_state_name(lts, 0, "sender_instance_0");
lts_type_set_state_typeno(lts, 0, intSlot);
lts_type_set_state_name(lts, 1, "receiver0");
lts_type_set_state_name(lts, 1, "receiver_instance_0");
lts_type_set_state_typeno(lts, 1, intSlot);
lts_type_set_state_name(lts, 2, "checker0");
lts_type_set_state_name(lts, 2, "checker_instance_0");
lts_type_set_state_typeno(lts, 2, intSlot);
lts_type_set_state_name(lts, 3, "channelK0");
lts_type_set_state_name(lts, 3, "channelK_instance_0");
lts_type_set_state_typeno(lts, 3, intSlot);
lts_type_set_state_name(lts, 4, "channelL0");
lts_type_set_state_name(lts, 4, "channelL_instance_0");
lts_type_set_state_typeno(lts, 4, intSlot);
lts_type_set_state_name(lts, 5, "s");
lts_type_set_state_typeno(lts, 5, intSlot);
......
......@@ -43,7 +43,7 @@ void initModel(model_t model)
// Define StateVector
lts_type_set_state_length(lts, stateVectorLength());
lts_type_set_state_name(lts, 0, "main0");
lts_type_set_state_name(lts, 0, "main_instance_0");
lts_type_set_state_typeno(lts, 0, intSlot);
lts_type_set_state_name(lts, 1, "main_draw1");
lts_type_set_state_typeno(lts, 1, intSlot);
......
......@@ -43,11 +43,11 @@ void initModel(model_t model)
// Define StateVector
lts_type_set_state_length(lts, stateVectorLength());
lts_type_set_state_name(lts, 0, "counter0");
lts_type_set_state_name(lts, 0, "counter_instance_0");
lts_type_set_state_typeno(lts, 0, intSlot);
lts_type_set_state_name(lts, 1, "partyA0");
lts_type_set_state_name(lts, 1, "partyA_instance_0");
lts_type_set_state_typeno(lts, 1, intSlot);
lts_type_set_state_name(lts, 2, "partyB0");
lts_type_set_state_name(lts, 2, "partyB_instance_0");
lts_type_set_state_typeno(lts, 2, intSlot);
lts_type_set_state_name(lts, 3, "b");
lts_type_set_state_typeno(lts, 3, intSlot);
......
......@@ -43,13 +43,13 @@ void initModel(model_t model)
// Define StateVector
lts_type_set_state_length(lts, stateVectorLength());
lts_type_set_state_name(lts, 0, "counter0");
lts_type_set_state_name(lts, 0, "counter_instance_0");
lts_type_set_state_typeno(lts, 0, intSlot);
lts_type_set_state_name(lts, 1, "process10");
lts_type_set_state_name(lts, 1, "process1_instance_0");
lts_type_set_state_typeno(lts, 1, intSlot);
lts_type_set_state_name(lts, 2, "process20");
lts_type_set_state_name(lts, 2, "process2_instance_0");
lts_type_set_state_typeno(lts, 2, intSlot);
lts_type_set_state_name(lts, 3, "process30");
lts_type_set_state_name(lts, 3, "process3_instance_0");
lts_type_set_state_typeno(lts, 3, intSlot);
lts_type_set_state_name(lts, 4, "c");
lts_type_set_state_typeno(lts, 4, intSlot);
......
......@@ -43,7 +43,7 @@ void initModel(model_t model)
// Define StateVector
lts_type_set_state_length(lts, stateVectorLength());
lts_type_set_state_name(lts, 0, "One0");
lts_type_set_state_name(lts, 0, "One_instance_0");
lts_type_set_state_typeno(lts, 0, intSlot);
lts_type_set_state_name(lts, 1, "term");
lts_type_set_state_typeno(lts, 1, boolSlot);
......
......@@ -25,17 +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 One00 = sourceStateVector[0];
int One_instance_00 = sourceStateVector[0];
int count0 = sourceStateVector[2];
int One01 = One00;
int One_instance_01 = One_instance_00;
int count1 = count0;
if ((sourceStateVector[0] == 0) && ((remEuc(sourceStateVector[2],3)) != 2)){
One01 = 0;
One_instance_01 = 0;
}
if ((sourceStateVector[0] == 0) && ((remEuc(sourceStateVector[2],3)) != 2)){
count1 = (count0 - 1);
}
targetStateVector[0] = One01;
targetStateVector[0] = One_instance_01;
targetStateVector[2] = count1;
int copy[STATEVECTORLENGTH] = {0,1,0};
callback(context, &transitionInformation, targetStateVector, copy);
......@@ -45,17 +45,17 @@ int nextStateLong(model_t model, int group, int *sourceStateVector, TransitionCB
actionLabel[0] = 0;
int targetStateVector[STATEVECTORLENGTH];
memcpy(targetStateVector, sourceStateVector, STATEVECTORLENGTH * sizeof(int));
int One00 = sourceStateVector[0];
int One_instance_00 = sourceStateVector[0];
int term0 = sourceStateVector[1];
int One01 = One00;
int One_instance_01 = One_instance_00;
int term1 = term0;
if ((sourceStateVector[0] == 0) && ((remEuc(sourceStateVector[2],3)) == 2)){
One01 = 1;
One_instance_01 = 1;
}
if ((sourceStateVector[0] == 0) && ((remEuc(sourceStateVector[2],3)) == 2)){
term1 = 1;
}
targetStateVector[0] = One01;
targetStateVector[0] = One_instance_01;
targetStateVector[1] = term1;
int copy[STATEVECTORLENGTH] = {0,0,1};
callback(context, &transitionInformation, targetStateVector, copy);
......@@ -72,17 +72,17 @@ int nextStateR2W(model_t model, int group, int *sourceStateVector, TransitionCB
if (group == 0 && ((sourceStateVector[0] == 0) && ((remEuc(sourceStateVector[1],3)) != 2))){
actionLabel[0] = 0;
int targetStateVector[dm_ones_in_row(GBgetDMInfoMustWrite(model), group)];
int One00 = sourceStateVector[0];
int One_instance_00 = sourceStateVector[0];
int count0 = sourceStateVector[1];
int One01 = One00;
int One_instance_01 = One_instance_00;
int count1 = count0;
if ((sourceStateVector[0] == 0) && ((remEuc(sourceStateVector[1],3)) != 2)){
One01 = 0;
One_instance_01 = 0;
}
if ((sourceStateVector[0] == 0) && ((remEuc(sourceStateVector[1],3)) != 2)){
count1 = (count0 - 1);
}
targetStateVector[0] = One01;
targetStateVector[0] = One_instance_01;
targetStateVector[1] = count1;
callback(context, &transitionInformation, targetStateVector, NULL);
return 1;
......@@ -90,17 +90,17 @@ int nextStateR2W(model_t model, int group, int *sourceStateVector, TransitionCB
if (group == 1 && ((sourceStateVector[0] == 0) && ((remEuc(sourceStateVector[2],3)) == 2))){
actionLabel[0] = 0;
int targetStateVector[dm_ones_in_row(GBgetDMInfoMustWrite(model), group)];
int One00 = sourceStateVector[0];
int One_instance_00 = sourceStateVector[0];
int term0 = sourceStateVector[1];
int One01 = One00;
int One_instance_01 = One_instance_00;
int term1 = term0;
if ((sourceStateVector[0] == 0) && ((remEuc(sourceStateVector[2],3)) == 2)){
One01 = 1;
One_instance_01 = 1;
}
if ((sourceStateVector[0] == 0) && ((remEuc(sourceStateVector[2],3)) == 2)){
term1 = 1;
}
targetStateVector[0] = One01;
targetStateVector[0] = One_instance_01;
targetStateVector[1] = term1;
callback(context, &transitionInformation, targetStateVector, NULL);
return 1;
......@@ -116,17 +116,17 @@ 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 One00 = sourceStateVector[0];
int One_instance_00 = sourceStateVector[0];
int count0 = sourceStateVector[1];
int One01 = One00;
int One_instance_01 = One_instance_00;
int count1 = count0;
if ((sourceStateVector[0] == 0) && ((remEuc(sourceStateVector[1],3)) != 2)){
One01 = 0;
One_instance_01 = 0;
}
if ((sourceStateVector[0] == 0) && ((remEuc(sourceStateVector[1],3)) != 2)){
count1 = (count0 - 1);
}
targetStateVector[0] = One01;
targetStateVector[0] = One_instance_01;
targetStateVector[1] = count1;
callback(context, &transitionInformation, targetStateVector, NULL);
return 1;
......@@ -134,17 +134,17 @@ int actionsR2W(model_t model, int group, int *sourceStateVector, TransitionCB ca
if (group == 1){
actionLabel[0] = 0;
int targetStateVector[dm_ones_in_row(GBgetDMInfoMustWrite(model), group)];
int One00 = sourceStateVector[0];
int One_instance_00 = sourceStateVector[0];
int term0 = sourceStateVector[1];
int One01 = One00;
int One_instance_01 = One_instance_00;
int term1 = term0;
if ((sourceStateVector[0] == 0) && ((remEuc(sourceStateVector[2],3)) == 2)){
One01 = 1;
One_instance_01 = 1;
}
if ((sourceStateVector[0] == 0) && ((remEuc(sourceStateVector[2],3)) == 2)){
term1 = 1;
}
targetStateVector[0] = One01;
targetStateVector[0] = One_instance_01;
targetStateVector[1] = term1;
callback(context, &transitionInformation, targetStateVector, NULL);
return 1;
......
......@@ -43,7 +43,7 @@ void initModel(model_t model)
// Define StateVector
lts_type_set_state_length(lts, stateVectorLength());
lts_type_set_state_name(lts, 0, "Main0");
lts_type_set_state_name(lts, 0, "Main_instance_0");
lts_type_set_state_typeno(lts, 0, intSlot);
lts_type_set_state_name(lts, 1, "Main_increase");
lts_type_set_state_typeno(lts, 1, intSlot);
......
......@@ -31,14 +31,14 @@ int nextStateLong(model_t model, int group, int *sourceStateVector, TransitionCB
actionLabel[0] = 0;
int targetStateVector[STATEVECTORLENGTH];
memcpy(targetStateVector, sourceStateVector, STATEVECTORLENGTH * sizeof(int));
int Main00 = sourceStateVector[0];
int Main_increase0 = sourceStateVector[1];
int Main_instance_00 = sourceStateVector[0];
int test0 = sourceStateVector[2];
int Main01 = Main00;
int Main_increase1 = Main_increase0;
int Main_instance_01 = Main_instance_00;
int test1 = test0;
if (sourceStateVector[0] == 0){
Main01 = 1;
Main_instance_01 = 1;
}
if (sourceStateVector[0] == 0){
test1 = function_fac(test0);
......@@ -46,8 +46,8 @@ int nextStateLong(model_t model, int group, int *sourceStateVector, TransitionCB
if (sourceStateVector[0] == 0){
Main_increase1 = 1;
}
targetStateVector[0] = Main01;
targetStateVector[1] = Main_increase1;
targetStateVector[0] = Main_instance_01;
targetStateVector[2] = test1;
int copy[STATEVECTORLENGTH] = {0,0,0};
callback(context, &transitionInformation, targetStateVector, copy);
......@@ -57,17 +57,17 @@ int nextStateLong(model_t model, int group, int *sourceStateVector, TransitionCB
actionLabel[0] = 0;
int targetStateVector[STATEVECTORLENGTH];
memcpy(targetStateVector, sourceStateVector, STATEVECTORLENGTH * sizeof(int));
int Main00 = sourceStateVector[0];
int Main_instance_00 = sourceStateVector[0];
int test0 = sourceStateVector[2];
int Main01 = Main00;