Commit 57d98e69 authored by Lars Schieffer's avatar Lars Schieffer
Browse files

update to symbolic without egl

parent 5216fdf4
......@@ -22,6 +22,7 @@ def instancesOf(model: dict, functions: dict) -> list:
elements = [element["automaton"] for element in system["elements"]]
inputEnable = inputEnabledIn(system)
automataByName = {automaton["name"]: automaton for automaton in model["automata"]}
ndLabels = []
instances = []
for index, automaton in enumerate(elements):
uniqueNumber = elements[:index].count(automaton)
......@@ -29,8 +30,9 @@ def instancesOf(model: dict, functions: dict) -> list:
edgesByLocation = edgesByLocationOf(
automataByName[automaton], functions, inputEnable[index]
)
edges = edgesByLabelOf(edgesByLocation, instance)
edges, nonDet = edgesByLabelOf(edgesByLocation, instance)
instances.append(edges)
ndLabels.append(nonDet)
if "syncs" not in system:
syncs = []
......@@ -45,6 +47,10 @@ 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
]
for synchronisation in syncs:
result = synchronisation["result"] if "result" in synchronisation else "tau"
syncVector = synchronisation["synchronise"]
......@@ -52,20 +58,62 @@ def instancesOf(model: dict, functions: dict) -> list:
for index, label in enumerate(syncVector):
if label:
edges.append(instances[index][label])
edges = flattenOf(edges)
for edge in edges:
if isLocal(syncVector) or ndProblem(syncVector, ndLabels):
edges = flattenOf(edges)
for edge in edges:
updatedLabel = str(len(updatedSyncs))
synchronise = []
for index, entry in enumerate(syncVector):
if entry:
updatedInstances[index][updatedLabel] = [edge.pop(0)]
synchronise.append(updatedLabel)
else:
synchronise.append(None)
synchronisation = {"result": result, "synchronise": synchronise}
updatedSyncs.append(synchronisation)
else:
updatedLabel = str(len(updatedSyncs))
synchronise = []
for index, entry in enumerate(syncVector):
if entry:
instances[index][updatedLabel] = [edge.pop(0)]
updatedInstances[index][updatedLabel] = edges.pop(0)
synchronise.append(updatedLabel)
else:
synchronise.append(None)
synchronisation = {"result": result, "synchronise": synchronise}
updatedSyncs.append(synchronisation)
model["system"]["syncs"] = updatedSyncs
return instances
return updatedInstances
def isLocal(synchronisation: list) -> bool:
"""
Function Description:
Return wether transition are executed locally in automaton.
Function Parameters:
synchronisation: list
Single synchronisation vector in jani-model system
"""
return len(synchronisation) - synchronisation.count(None) == 1
def ndProblem(synchronisation: list, ndLabels: dict) -> bool:
"""
Function Description:
Return wether non deterministic choice can occur in synchronised labels.
Function Parameters:
synchronisation: list
Single synchronisation vector in jani-model system
ndLabels: dict
Labels with non deterministic choices
"""
containND = []
for index, label in enumerate(synchronisation):
containND.append(label in ndLabels[index])
return any(containND)
def inputEnabledIn(system: dict) -> list:
......@@ -184,7 +232,7 @@ def edgesByLocationOf(automaton: dict, functions: dict, inputEnable: list) -> di
if location not in edgesByLocation:
edgesByLocation[location] = {}
if label not in edgesByLocation[location]:
edgesByLocation[location][label] = []
edgesByLocation[location][label] = {"edges": [], "amount": 0}
edge = updateGuardOf(edge, automatonLocals, name, functions)
for index, destination in enumerate(edge["destinations"]):
......@@ -192,11 +240,13 @@ def edgesByLocationOf(automaton: dict, functions: dict, inputEnable: list) -> di
destination, automatonLocals, name, functions,
)
edgesByLocation[location][label].append(edge)
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]:
edgesByLocation[location][identifier] = [selfLoop(identifier, location)]
loop = selfLoop(identifier, location)
edgesByLocation[location][identifier] = {"edges": [loop], "amount": 1}
return edgesByLocation
......@@ -228,11 +278,14 @@ def edgesByLabelOf(edgesByLocation: dict, automaton: str) -> dict:
Name of automaton
"""
edgesByLabel = dict()
ndLabels = set()
for edges in edgesByLocation.values():
for label, edges in edges.items():
if edges["amount"] > 1:
ndLabels.add(label)
if label not in edgesByLabel:
edgesByLabel[label] = []
for edge in edges:
for edge in edges["edges"]:
individual = edgeHelper.unificationOf(edge, automaton)
edgesByLabel[label] += individual
return edgesByLabel
return edgesByLabel, ndLabels
......@@ -145,7 +145,11 @@ def maybeCoEnabledMatrixString(guards: ModelGuards) -> str:
intersections = []
for automaton in vLocations:
intersections.append(
bool(hLocations[automaton].intersection(vLocations[automaton]))
bool(
set(hLocations[automaton]).intersection(
set(vLocations[automaton])
)
)
)
maybeRow.append(str(int(all(intersections))))
else:
......
......@@ -15,21 +15,23 @@ def nextStateFunctionsOf(pinsModel: Model) -> str:
stateVector = pinsModel.getStateVector()
modelLocations = pinsModel.getLocations()
functions = createFunctionImplementationString(pinsModel.getFunctions())
constants = "\n".join(
["// Model Constants"]
+ pinsModel.getConstants()
+ ["// Transient Values"]
+ [variable for variable in stateVector.getTransientVariables().values()]
)
constants = "\n".join(["// Model Constants"] + pinsModel.getConstants())
nextStatesLong = createNextStatesString(pinsModel, StateVectorMode.LONG)
nextStatesR2W = createNextStatesString(pinsModel, StateVectorMode.R2W)
actionsR2W = createActionsString(pinsModel, StateVectorMode.R2W)
guardsLong = modelGuards.evaluationCode(
stateVector, modelLocations, StateVectorMode.LONG
)
guardsLong = (
createTransientDeclaration(pinsModel, StateVectorMode.LONG, False) + guardsLong
)
guardsShort = modelGuards.evaluationCode(
stateVector, modelLocations, StateVectorMode.SHORT
)
guardsShort = (
createTransientDeclaration(pinsModel, StateVectorMode.SHORT, False)
+ guardsShort
)
labelEvaluationLong = ("\n" + indent * " ").join(guardsLong)
labelEvaluationShort = ("\n" + indent * " ").join(guardsShort)
initialStateVector = getInitialStateVectorString(stateVector, modelLocations)
......@@ -48,6 +50,55 @@ def nextStateFunctionsOf(pinsModel: Model) -> str:
return code
def createTransientDeclaration(
pinsModel: Model, mode: StateVectorMode, groups: bool
) -> list:
transients = pinsModel.getStateVector().getTransientVariables()
modelLocations = pinsModel.getLocations()
stateVector = pinsModel.getStateVector()
declaration = ["// Transient Values"]
declaration += [variable for variable in transients.values()]
if groups:
for index, group in enumerate(pinsModel.getTransitionGroups()):
groupLocations = group.getAutomataLocations()
if mode != StateVectorMode.LONG:
dependencies = group.getReadDependencies()
readStateVector = stateVector.getShiftedStateVector(dependencies)
else:
readStateVector = stateVector
for automaton, locations in groupLocations.items():
for location, transient in locations.items():
if transient:
for variable, expression in transient.items():
expression = string.perform(
expression, modelLocations, readStateVector
)
pinsLocation = modelLocations.getLocationNumber(location)
slot = readStateVector.getPositions()[automaton]
updateString = f"if (group == {index} && sourceStateVector[{slot}] == {pinsLocation}){{{variable}={expression};}}"
declaration.append(updateString)
else:
guards = pinsModel.getGuards()
for index, guard in enumerate(guards.getOrder()):
if mode != StateVectorMode.LONG:
dependencies = guards.getDependencies(guard)
readStateVector = stateVector.getShiftedStateVector(dependencies)
else:
readStateVector = stateVector
for automaton, locations in guards.getLocations(guard).items():
for location, transient in locations.items():
if transient:
for variable, expression in transient.items():
expression = string.perform(
expression, modelLocations, readStateVector
)
pinsLocation = modelLocations.getLocationNumber(location)
slot = readStateVector.getPositions()[automaton]
updateString = f"if (stateVectorLabel == {index} && sourceStateVector[{slot}] == {pinsLocation}){{{variable}={expression};}}"
declaration.append(updateString)
return declaration
def createFunctionImplementationString(janiFunctions) -> str:
functionImplementations = ["// Function Declarations"]
functionIdentifiers = {
......@@ -101,7 +152,7 @@ def createNextStatesString(pinsModel: Model, mode: StateVectorMode) -> str:
stateVector = pinsModel.getStateVector()
modelLocations = pinsModel.getLocations()
actions = pinsModel.getActions()
nextState = []
nextState = createTransientDeclaration(pinsModel, mode, True)
for groupNumber, group in enumerate(transitionGroups):
groupEnableString = group.nextStatesEnableCode(
stateVector, modelLocations, mode
......@@ -122,7 +173,7 @@ def createActionsString(pinsModel: Model, mode: StateVectorMode) -> str:
stateVector = pinsModel.getStateVector()
modelLocations = pinsModel.getLocations()
actions = pinsModel.getActions()
nextState = []
nextState = createTransientDeclaration(pinsModel, mode, True)
for groupNumber, group in enumerate(transitionGroups):
groupNumberString = "group == {}".format(groupNumber)
nextState.append("if ({}){{".format(groupNumberString))
......
......@@ -52,12 +52,14 @@ class Model:
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.__locations = self.__createLocations(
janiModel["automata"], self.__janiFunctions
)
(
self.__transitionGroups,
self.__guards,
self.__actions,
) = self.__createTransitionGroups(janiModel)
) = self.__createTransitionGroups(janiModel, self.__locations)
def getConstants(self) -> List[str]:
return self.__constants
......@@ -80,7 +82,7 @@ class Model:
def getFunctions(self) -> dict:
return self.__janiFunctions
def __createLocations(self, janiAutomata: list) -> Locations:
def __createLocations(self, janiAutomata: list, functions: dict) -> Locations:
"""
Function Description:
Create Locations datastructure from automata locations
......@@ -88,10 +90,12 @@ class Model:
Function Parameters:
janiAutomata: list
Automata in JANI-Model
functions: dict
Defined functions in PINS model
"""
locations = Locations()
for automaton in janiAutomata:
locations.addAutomaton(automaton)
locations.addAutomaton(automaton, functions)
return locations
def __createStateVector(self, janiModel: dict, real2int: bool) -> StateVector:
......@@ -110,7 +114,7 @@ class Model:
return stateVector
def __createTransitionGroups(
self, janiModel: dict
self, janiModel: dict, pinsLocations: Locations
) -> (List[TransitionGroup], ModelGuards, Actions):
"""
Function Description:
......@@ -119,6 +123,8 @@ 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"]
......@@ -135,8 +141,6 @@ class Model:
transitionGroupGuards = ModelGuards()
transitionGroups = []
# Add groups of synchronized actions to PINS-Model
synchronisedActions = set()
edgeLabels = Actions()
if "syncs" in system:
for sync in system["syncs"]:
......@@ -145,45 +149,30 @@ class Model:
edgeLabels.addLabel(result)
group = []
groupGuards = []
transientVariables = dict()
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[name]),
)
)
locations = dict()
for automatonIndex, label in enumerate(syncVector):
old = system["elements"][automatonIndex]["automaton"]
if label:
synchronisedActions.add(label)
edges = instances[automatonIndex][label]
edges = rename.updateAutomatonName(
edges, old, uniqueNames[automatonIndex]
)
group += edges
guards = []
for transitionIndex, arc in enumerate(edges):
updatedGuard = []
for condition in arc["enable"]:
updatedGuard.append(
rename.variables(
condition,
dict(),
transientVariables,
"",
dict(),
)
)
guards.append(updatedGuard)
edges[transitionIndex]["enable"] = updatedGuard
guards = [edge["enable"] for edge in edges]
groupGuards.append(guards)
transitionGroupGuards.addGuard(guards, self.__stateVector)
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
result, group, groupGuards, self.__stateVector, locations
)
transitionGroups.append(synchronisedGroup)
......@@ -192,22 +181,24 @@ class Model:
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()}
for edge in edges:
location = edge["location"]
update = {}
if location in transientUpdates:
update = transientUpdates[location]
locations[uniqueNames[index]][location] = update
name = system["elements"][index]["automaton"]
transientVariables = transientValuesOf(
edge["location"], transientVariablesOf(janiAutomata[name]),
)
edgeLabels.addLabel("tau")
edge["enable"] = rename.variables(
edge["enable"], dict(), transientVariables, "", dict()
)
groupGuards = [edge["enable"]]
transitionGroups.append(
TransitionGroup(
"tau", [edge], [groupGuards], self.__stateVector
"tau", [edge], [groupGuards], self.__stateVector, locations
)
)
transitionGroupGuards.addGuard(groupGuards, self.__stateVector)
transitionGroupGuards.addGuard(
groupGuards, self.__stateVector, pinsLocations
)
return transitionGroups, transitionGroupGuards, edgeLabels
......@@ -3,7 +3,7 @@ import src.utilities.parser.expression.toString as string
from src.pins.modules.locations import Locations
from src.pins.modules.stateVector import StateVector, StateVectorMode
evaluationStringPlaceholder = "if(stateVectorLabel == {}) {{return {};}}"
evaluationStringPlaceholder = "if (stateVectorLabel == {}) {{return {};}}"
class ModelGuards:
......@@ -31,7 +31,9 @@ class ModelGuards:
self.__dependencies = {}
self.__locations = {}
def addGuard(self, guard: list, stateVector: StateVector) -> None:
def addGuard(
self, guard: list, stateVector: StateVector, locations: Locations
) -> None:
"""
Function Description:
Add guard to ModelGuards datastructure, if first occurrence
......@@ -46,12 +48,16 @@ class ModelGuards:
self.__positions[repr(guard)] = len(self.__positions)
self.__order.append(repr(guard))
self.__individuals[repr(guard)] = guard
self.__locations[repr(guard)] = self.automataLocations(guard, stateVector)
self.__locations[repr(guard)] = self.automataLocations(
guard, stateVector, locations
)
self.__dependencies[repr(guard)] = createGuardDependencies(
guard, stateVector
guard, self.__locations[repr(guard)], stateVector
)
def automataLocations(self, groupGuards: list, stateVector: StateVector) -> dict:
def automataLocations(
self, groupGuards: list, stateVector: StateVector, pinsLocations: Locations
) -> dict:
"""
Function Description:
Extract automata locations from guards, to achieve mapping from guards to location
......@@ -67,9 +73,15 @@ class ModelGuards:
for guard in automaton:
if type(guard) == dict and "left" in guard:
if stateVector.isAutomaton(guard["left"]):
name = str(guard["left"]).split("_instance_")[-2]
location = guard["right"]
transients = pinsLocations.getTransients(name)
update = {}
if location in transients:
update = transients[location]
if guard["left"] not in locations:
locations[guard["left"]] = set()
locations[guard["left"]].add(guard["right"])
locations[guard["left"]] = dict()
locations[guard["left"]][location] = update
return locations
def evaluationCode(
......@@ -182,7 +194,9 @@ def guardToString(
return expressionOf([guard], stateVector, modelLocations)
def createGuardDependencies(guard: list, stateVector: StateVector) -> list:
def createGuardDependencies(
guard: list, locations: dict, stateVector: StateVector
) -> list:
"""
Function Description:
Retrieve dependencies of transition group guards
......@@ -195,6 +209,10 @@ def createGuardDependencies(guard: list, stateVector: StateVector) -> list:
"""
dependencies = []
for conditions in guard:
for individual_condition in conditions:
dependencies += dependency.perform(individual_condition, stateVector)
for individual in conditions:
dependencies += dependency.perform(individual, stateVector)
for automaton in locations.values():
for transient in automaton.values():
for update in transient.values():
dependencies += dependency.perform(update, stateVector)
return list(set(dependencies))
import src.jani.variables as variablesHelper
import src.utilities.parser.expression.toRename as renameHelper
class Locations:
"""
Class Description:
Datastructure, holding information about the automata locations in PINS-Model
Class Attributes:
__locations: str
__locations: dict
All locations, which occur in automata
__transients: dict
Updated values dependent on location, with automaton's name as key
"""
def __init__(self):
self.__locations = {}
self.__transients = {}
def addLocation(self, location: str) -> None:
"""
......@@ -23,7 +30,7 @@ class Locations:
if location not in self.__locations:
self.__locations[location] = {"position": len(self.__locations)}
def addAutomaton(self, automaton: dict) -> None:
def addAutomaton(self, automaton: dict, functions: dict) -> None:
"""
Function Description:
Add all locations of automaton to location datastructure
......@@ -31,9 +38,33 @@ class Locations:
Function Parameters:
automaton: dict
Adding all locations in automaton to Location datastructure
functions: dict
Defined functions in PINS model
"""
automatonName = automaton["name"]
self.__transients[automatonName] = {}
localFunctions = set()
if "functions" in automaton:
for function in automaton["functions"]:
localFunctions.add(function["name"])
localVariables = variablesHelper.variablesOf(automaton)
automatonLocals = localFunctions.union(localVariables)
for location in automaton["locations"]:
self.addLocation(location["name"])
locationName = location["name"]
self.addLocation(locationName)
if "transient-values" in location:
transients = dict()
for transient in location["transient-values"]:
update = transient["value"]
update = renameHelper.localVariablesTo(
update, automatonLocals, automatonName, functions
)
transients[transient["ref"]] = update
self.__transients[automatonName][locationName] = transients
def getTransients(self, automaton: str) -> dict:
return self.__transients[automaton]
def getLocationNumber(self, location: str) -> int:
"""
......
......@@ -161,9 +161,7 @@ class StateVector:
else:
slotType = kind
if transient:
declaration = "static const {} {} = {};".format(
"int", identifier, str(int(initial))
)
declaration = "{} {} = {};".format("int", identifier, str(int(initial)))
self.__transientVariables[identifier] = declaration
else:
self.addSlot(identifier, initial, slotType, SlotMode.VARIABLE)
......
......@@ -61,15 +61,29 @@ class TransitionGroup:
Guards of transition group
stateVector: StateVector
The dependent state vector, for creating read and write dependencies
locations: dict
Edges location in automata
"""
def __init__(self, label: str, edges: list, guards: list, stateVector: StateVector):
def __init__(
self,
label: str,
edges: list,
guards: list,
stateVector: StateVector,
locations: dict,