Commit 1a62b6c8 authored by Lars Schieffer's avatar Lars Schieffer
Browse files

update code

parent 57d98e69
......@@ -24,12 +24,12 @@ def instancesOf(model: dict, functions: dict) -> list:
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]
)
for index, name in enumerate(elements):
unique = elements[:index].count(name)
instance = f"{name}_instance_{unique}"
enabled = inputEnable[index]
automaton = automataByName[name]
edgesByLocation = edgesByLocationOf(automaton, functions, enabled)
edges, nonDet = edgesByLabelOf(edgesByLocation, instance)
instances.append(edges)
ndLabels.append(nonDet)
......@@ -47,10 +47,7 @@ def instancesOf(model: dict, functions: dict) -> list:
syncs = system["syncs"]
updatedSyncs = []
updatedInstances = [
{"tau": instance["tau"]} if "tau" in instance else dict()
for instance in instances
]
updatedInstances = onlyTauIn(instances)
for synchronisation in syncs:
result = synchronisation["result"] if "result" in synchronisation else "tau"
syncVector = synchronisation["synchronise"]
......@@ -83,8 +80,25 @@ def instancesOf(model: dict, functions: dict) -> list:
synchronisation = {"result": result, "synchronise": synchronise}
updatedSyncs.append(synchronisation)
model["system"]["syncs"] = updatedSyncs
return updatedInstances
return updatedInstances, updatedSyncs
def onlyTauIn(instances: list) -> list:
"""
Function Description:
Declare list of instances, containing only tau edges
Function Parameters:
instances: list
List of instances
"""
updated = []
for instance in instances:
if "tau" in instance:
updated.append({"tau": instance["tau"]})
else:
updated.append(dict())
return updated
def isLocal(synchronisation: list) -> bool:
......@@ -236,9 +250,10 @@ def edgesByLocationOf(automaton: dict, functions: dict, inputEnable: list) -> di
edge = updateGuardOf(edge, automatonLocals, name, functions)
for index, destination in enumerate(edge["destinations"]):
edge["destinations"][index]["assignments"] = updateAssignmentsOf(
updated = updateAssignmentsOf(
destination, automatonLocals, name, functions,
)
edge["destinations"][index]["assignments"] = updated
edgesByLocation[location][label]["edges"].append(edge)
edgesByLocation[location][label]["amount"] += len(edge["destinations"])
......
......@@ -49,17 +49,15 @@ class Model:
self, janiModel: dict, real2int: bool, experiment={},
):
isSupported(janiModel, real2int)
automata = janiModel["automata"]
self.__constants = constants.declare(janiModel, experiment)
self.__stateVector = self.__createStateVector(janiModel, real2int)
self.__janiFunctions = functionsOf(janiModel, self.__stateVector)
self.__locations = self.__createLocations(
janiModel["automata"], self.__janiFunctions
)
(
self.__transitionGroups,
self.__guards,
self.__actions,
) = self.__createTransitionGroups(janiModel, self.__locations)
self.__locations = self.__createLocations(automata, self.__janiFunctions)
groups, guards, actions = self.__createTransitionGroups(janiModel)
self.__transitionGroups = groups
self.__guards = guards
self.__actions = actions
def getConstants(self) -> List[str]:
return self.__constants
......@@ -114,7 +112,7 @@ class Model:
return stateVector
def __createTransitionGroups(
self, janiModel: dict, pinsLocations: Locations
self, janiModel: dict
) -> (List[TransitionGroup], ModelGuards, Actions):
"""
Function Description:
......@@ -123,82 +121,73 @@ class Model:
Function Parameters:
janiModel: dict
Reference to JANI-Model
pinsLocations: Locations
Locations of PINS model
"""
janiAutomata = {
automaton["name"]: automaton for automaton in janiModel["automata"]
}
instances = strategy.instancesOf(janiModel, self.__janiFunctions)
instances, syncs = strategy.instancesOf(janiModel, self.__janiFunctions)
system = janiModel["system"]
elements = [element["automaton"] for element in system["elements"]]
uniqueNames = []
names = []
for index, automaton in enumerate(elements):
uniqueNumber = elements[:index].count(automaton)
uniqueNames.append(f"{automaton}_instance_{uniqueNumber}")
unique = elements[:index].count(automaton)
names.append(f"{automaton}_instance_{unique}")
# Collecting all used guards in the PINS-Model
transitionGroupGuards = ModelGuards()
modelGuards = ModelGuards()
transitionGroups = []
edgeLabels = Actions()
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 = []
locations = dict()
for automatonIndex, label in enumerate(syncVector):
old = system["elements"][automatonIndex]["automaton"]
if label:
edges = instances[automatonIndex][label]
edges = rename.updateAutomatonName(
edges, old, uniqueNames[automatonIndex]
)
group += edges
guards = [edge["enable"] for edge in edges]
groupGuards.append(guards)
transitionGroupGuards.addGuard(
guards, self.__stateVector, pinsLocations
)
transientUpdates = pinsLocations.getTransients(old)
locations[uniqueNames[automatonIndex]] = {}
for edge in edges:
location = edge["location"]
update = {}
if location in transientUpdates:
update = transientUpdates[location]
locations[uniqueNames[automatonIndex]][location] = update
synchronisedGroup = TransitionGroup(
result, group, groupGuards, self.__stateVector, locations
)
transitionGroups.append(synchronisedGroup)
for sync in syncs:
syncVector = sync["synchronise"]
result = sync["result"] if "result" in sync else "tau"
edgeLabels.addLabel(result)
group = []
groupGuards = []
locations = dict()
for automatonIndex, label in enumerate(syncVector):
name = system["elements"][automatonIndex]["automaton"]
updated = names[automatonIndex]
if label:
edges = instances[automatonIndex][label]
edges = rename.updateAutomatonName(edges, name, updated)
group += edges
guards = [edge["enable"] for edge in edges]
groupGuards.append(guards)
modelGuards.addGuard(guards, self.__stateVector, self.__locations)
transientUpdates = self.__locations.getTransients(name)
locations[updated] = {}
for edge in edges:
location = edge["location"]
update = {}
if location in transientUpdates:
update = transientUpdates[location]
locations[updated][location] = update
synchronisedGroup = TransitionGroup(
result, group, groupGuards, self.__stateVector, locations
)
transitionGroups.append(synchronisedGroup)
# Add tau edges to PINS model
for index, instance in enumerate(instances):
if "tau" in instance:
edges = instance["tau"]
old = system["elements"][index]["automaton"]
transientUpdates = pinsLocations.getTransients(old)
edges = rename.updateAutomatonName(edges, old, uniqueNames[index])
locations = {uniqueNames[index]: dict()}
name = system["elements"][index]["automaton"]
updated = names[index]
transientUpdates = self.__locations.getTransients(name)
edges = rename.updateAutomatonName(edges, name, updated)
locations = {updated: dict()}
for edge in edges:
location = edge["location"]
update = {}
if location in transientUpdates:
update = transientUpdates[location]
locations[uniqueNames[index]][location] = update
locations[names[index]][location] = update
name = system["elements"][index]["automaton"]
edgeLabels.addLabel("tau")
groupGuards = [edge["enable"]]
transitionGroups.append(
TransitionGroup(
"tau", [edge], [groupGuards], self.__stateVector, locations
)
modelGuards.addGuard(
groupGuards, self.__stateVector, self.__locations
)
transitionGroupGuards.addGuard(
groupGuards, self.__stateVector, pinsLocations
tauGroup = TransitionGroup(
"tau", [edge], [groupGuards], self.__stateVector, locations
)
return transitionGroups, transitionGroupGuards, edgeLabels
transitionGroups.append(tauGroup)
return transitionGroups, modelGuards, edgeLabels
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment