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

fix bug thorugh brp

parent 304320a7
......@@ -86,9 +86,13 @@ def getInitialStateVectorString(
stateVector: StateVector, modelLocations: Locations
) -> str:
initial = []
for slot in stateVector.getInitialValues():
slotValue = string.perform(slot, modelLocations)
initial.append(slotValue)
for index, slot in enumerate(stateVector.getNames()):
value = stateVector.getInitialValues()[index]
if stateVector.isAutomaton(slot):
value = str(modelLocations.getLocationNumber(value))
else:
value = string.perform(value, modelLocations)
initial.append(value)
return ", ".join(initial)
......
......@@ -196,7 +196,5 @@ def createGuardDependencies(guard: list, stateVector: StateVector) -> list:
dependencies = []
for conditions in guard:
for individual_condition in conditions:
dependencies += dependency.perform(
individual_condition, stateVector.getNames()
)
dependencies += dependency.perform(individual_condition, stateVector)
return list(set(dependencies))
......@@ -205,13 +205,9 @@ class TransitionGroup:
jointDependencies = []
for edge in groupEdges:
for condition in edge["enable"]:
jointDependencies += dependency.perform(
condition, stateVector.getNames()
)
jointDependencies += dependency.perform(condition, stateVector)
for change in edge["changes"]:
jointDependencies += dependency.perform(
change["value"], stateVector.getNames()
)
jointDependencies += dependency.perform(change["value"], stateVector)
return set(jointDependencies)
def __writeBy(self, groupEdges: list, stateVector: StateVector) -> set:
......@@ -228,9 +224,7 @@ class TransitionGroup:
jointDependencies = []
for edge in groupEdges:
for change in edge["changes"]:
jointDependencies += dependency.perform(
change["ref"], stateVector.getNames()
)
jointDependencies += dependency.perform(change["ref"], stateVector)
return set(jointDependencies)
def __groupChangesCode(
......@@ -285,7 +279,9 @@ class TransitionGroup:
condition, stateVector, modelLocations, mode
)
if mode == StateVectorMode.R2W:
onlyReadStateVectorR2W = stateVector.getShiftedStateVector(onlyRead)
onlyReadStateVectorR2W = readStateVector.getShiftedStateVector(
onlyRead, haltShift=True
)
writeStateVector = stateVector.getShiftedStateVector(self.__write)
edgeChange = self.__changeCode(
change,
......@@ -367,12 +363,15 @@ class TransitionGroup:
readIndex: int
Index of variables to read from
"""
updateValue = string.perform(
expression=change["value"],
modelLocations=modelLocations,
stateVector=readStateVector,
readIndex=str(readIndex),
)
if writeStateVector.isAutomaton(change["ref"]):
updateValue = str(modelLocations.getLocationNumber(change["value"]))
else:
updateValue = string.perform(
expression=change["value"],
modelLocations=modelLocations,
stateVector=readStateVector,
readIndex=str(readIndex),
)
# If symbolic transition group or transient variable update values instead of state vector slot
if writeStateVector.isTransient(change["ref"]):
slotName = "transient_{}{}".format(
......
......@@ -162,4 +162,7 @@ void pins_model_init(model_t model) {
// Add Action guards
GBsetGuardsInfo(model, createTransitionGroupGuardInformation());
// Printing Guards in stdout
GBprintStateLabelGroupInfo(stdout, model);
}
\ No newline at end of file
......@@ -2,9 +2,10 @@ from typing import Union
import src.utilities.io.communication.errors as errors
import src.utilities.parser.supportedTypes as supportedTypes
from src.pins.modules.stateVector import StateVector
def handleOperator(expression: dict, dependencies: list) -> list:
def handleOperator(expression: dict, stateVector: StateVector) -> list:
"""
Function Description:
Handle the expression, according its containing operator
......@@ -15,28 +16,34 @@ def handleOperator(expression: dict, dependencies: list) -> list:
dependencies: dict
list of dependencies
"""
dependencies = stateVector.getNames()
if expression["op"] in supportedTypes.unaryOperator:
return perform(expression["exp"], dependencies)
return perform(expression["exp"], stateVector)
elif expression["op"] in supportedTypes.binaryOperator:
lhsDependencies = perform(expression["left"], dependencies)
rhsDependencies = perform(expression["right"], dependencies)
return lhsDependencies + rhsDependencies
lhsDependencies = perform(expression["left"], stateVector)
rhsDependencies = perform(expression["right"], stateVector)
if any(stateVector.isAutomaton(dependency) for dependency in lhsDependencies):
return lhsDependencies
else:
return lhsDependencies + rhsDependencies
elif expression["op"] in supportedTypes.ternaryOperator:
ifDependencies = perform(expression["if"], dependencies)
thenDependencies = perform(expression["then"], dependencies)
elseDependencies = perform(expression["else"], dependencies)
ifDependencies = perform(expression["if"], stateVector)
thenDependencies = perform(expression["then"], stateVector)
elseDependencies = perform(expression["else"], stateVector)
if expression["op"] in supportedTypes.iteOperator:
return ifDependencies + thenDependencies + elseDependencies
elif expression["op"] in supportedTypes.functionOperator:
argumentDependency = []
for argument in expression["args"]:
argumentDependency += perform(argument, dependencies)
argumentDependency += perform(argument, stateVector)
return argumentDependency
else:
errors.notSupportedOperator(expression["op"])
def perform(expression: Union[bool, int, float, dict], dependencies: list) -> list:
def perform(
expression: Union[bool, int, float, dict], stateVector: StateVector
) -> list:
"""
Function Description:
Retrieve all occurring dependencies in the expression
......@@ -47,15 +54,16 @@ def perform(expression: Union[bool, int, float, dict], dependencies: list) -> li
dependencies: dict
list of dependencies
"""
dependencies = stateVector.getNames()
if type(expression) in {bool, int, float}:
return []
elif type(expression) == str and expression in dependencies:
return [expression]
elif type(expression) == dict:
if "op" in expression:
return handleOperator(expression, dependencies)
return handleOperator(expression, stateVector)
elif "ref" in expression and "value" in expression:
refDependencies = perform(expression["ref"], dependencies)
valueDependencies = perform(expression["value"], dependencies)
refDependencies = perform(expression["ref"], stateVector)
valueDependencies = perform(expression["value"], stateVector)
return refDependencies + valueDependencies
return []
......@@ -39,8 +39,6 @@ def handleIdentifier(
"""
if stateVector and expression in stateVector.getPositions():
return "sourceStateVector[{}]".format(stateVector.getPositions()[expression])
elif modelLocations.isLocation(expression):
return str(modelLocations.getLocationNumber(expression))
elif stateVector.isTransient(expression):
return "transient_" + expression + str(readIndex)
elif stateVector.isConstant(expression):
......@@ -125,7 +123,7 @@ def handleImplicationOperator(
"""
left = perform(expression["left"], modelLocations, stateVector, readIndex)
if stateVector.isAutomaton(expression["left"]):
right = perform(expression["right"], modelLocations)
right = str(modelLocations.getLocationNumber(expression["right"]))
else:
right = perform(expression["right"], modelLocations, stateVector, readIndex)
return "(!({}) || ({}))".format(left, right)
......@@ -155,7 +153,7 @@ def handleInfixOperator(
op = binaryOperator[expression["op"]]
# If slot change is representing location change in automaton
if stateVector.isAutomaton(expression["left"]):
right = perform(expression["right"], modelLocations)
right = str(modelLocations.getLocationNumber(expression["right"]))
else:
right = perform(expression["right"], modelLocations, stateVector, readIndex)
return "({}{}{})".format(left, op, right)
......
This diff is collapsed.
{
"jani-version": 1,
"name": "single_process",
"type": "lts",
"features": [ "derived-operators" ],
"actions": [
{
"name": "switch_on"
},
{
"name": "on"
},
{
"name": "switch_off"
}
],
"variables": [
{
"name": "term",
"type": "bool",
"initial-value": false
},
{
"name": "clicks",
"type": "int",
"initial-value": 0
},
{
"name": "warrenty",
"type": "int",
"initial-value": 25
}
],
"properties": [ {
"name": "Term",
"expression": {
"op": "filter",
"fun": "∀",
"values": {
"op": "=",
"left": {
"op": "Pmin",
"exp": {
"op": "F",
"exp": "term"
}
},
"right": 1
},
"states": {
"op": "initial"
}
}
} ],
"automata": [
{
"name": "Switch_On",
"locations": [
{
"name": "loc_1"
},
{
"name": "loc_0"
},
{
"name": "loc_7"
}
],
"initial-locations": [ "loc_1" ],
"edges": [
{
"location": "loc_1",
"action": "switch_on",
"guard": {
"exp": {
"op": "∧",
"left": {
"op": "≥",
"left": "warrenty",
"right": 0
},
"right": {
"op": "<",
"left": "clicks",
"right": 10
}
}
},
"destinations": [ {
"location": "loc_7",
"assignments": [ {
"ref": "clicks",
"value": {
"op": "+",
"left": "clicks",
"right": 1
}
} ]
} ]
},
{
"location": "loc_1",
"guard": {
"exp": {
"op": "∨",
"left": {
"op": "=",
"left": "warrenty",
"right": 0
},
"right": {
"op": "≥",
"left": "clicks",
"right": 5
}
}
},
"destinations": [ {
"location": "loc_0",
"assignments": [ {
"ref": "term",
"value": true
} ]
} ]
},
{
"location": "loc_7",
"action": "on",
"guard": {
"exp": {
"op": "≥",
"left": "warrenty",
"right": 0
}
},
"destinations": [ {
"location": "loc_7",
"assignments": [ {
"ref": "warrenty",
"value": {
"op": "-",
"left": "warrenty",
"right": 1
}
} ]
} ]
},
{
"location": "loc_7",
"action": "switch_off",
"destinations": [ {
"location": "loc_1",
"assignments": [ {
"ref": "clicks",
"value": {
"op": "+",
"left": "clicks",
"right": 1
}
} ]
} ]
},
{
"location": "loc_7",
"guard": {
"exp": {
"op": "=",
"left": "warrenty",
"right": 0
}
},
"destinations": [ {
"location": "loc_0",
"assignments": [ {
"ref": "term",
"value": true
} ]
} ]
}
]
}
],
"system": {
"elements": [ {
"automaton": "Switch_On"
} ],
"syncs": [
{
"synchronise": [ "switch_on" ],
"result": "switch_on"
},
{
"synchronise": [ "on" ],
"result": "on"
},
{
"synchronise": [ "switch_off" ],
"result": "switch_off"
}
]
}
}
\ No newline at end of file
{
"jani-version": 1,
"name": "three_processes",
"type": "lts",
"features": [ "derived-operators" ],
"actions": [
{
"name": "switch_on"
},
{
"name": "on"
},
{
"name": "switch_off"
}
],
"variables": [
{
"name": "term",
"type": "bool",
"initial-value": false
},
{
"name": "clicks",
"type": "int",
"initial-value": 0
},
{
"name": "warrenty",
"type": "int",
"initial-value": 25
}
],
"properties": [ {
"name": "Term",
"expression": {
"op": "filter",
"fun": "∀",
"values": {
"op": "=",
"left": {
"op": "Pmin",
"exp": {
"op": "F",
"exp": "term"
}
},
"right": 1
},
"states": {
"op": "initial"
}
}
} ],
"automata": [
{
"name": "Switch_On",
"locations": [
{
"name": "loc_1"
},
{
"name": "loc_0"
},
{
"name": "loc_6"
}
],
"initial-locations": [ "loc_1" ],
"edges": [
{
"location": "loc_1",
"action": "switch_on",
"destinations": [ {
"location": "loc_6",
"assignments": [ {
"ref": "clicks",
"value": {
"op": "+",
"left": "clicks",
"right": 1
}
} ]
} ]
},
{
"location": "loc_1",
"guard": {
"exp": {
"op": "∨",
"left": {
"op": "=",
"left": "warrenty",
"right": 0
},
"right": {
"op": "≥",
"left": "clicks",
"right": 5
}
}
},
"destinations": [ {
"location": "loc_0",
"assignments": [ {
"ref": "term",
"value": true
} ]
} ]
},
{
"location": "loc_6",
"action": "on",
"destinations": [ {
"location": "loc_6",
"assignments": [ {
"ref": "warrenty",
"value": {
"op": "-",
"left": "warrenty",
"right": 1
}
} ]
} ]
},
{
"location": "loc_6",
"action": "switch_off",
"destinations": [ {
"location": "loc_1",
"assignments": [ {
"ref": "clicks",
"value": {
"op": "+",
"left": "clicks",
"right": 1
}
} ]
} ]
},
{
"location": "loc_6",
"guard": {
"exp": {
"op": "=",
"left": "warrenty",
"right": 0
}
},
"destinations": [ {
"location": "loc_0",
"assignments": [ {
"ref": "term",
"value": true
} ]
} ]
}
]
},
{
"name": "Warrenty",
"locations": [ {
"name": "loc_1"
} ],
"initial-locations": [ "loc_1" ],
"edges": [
{
"location": "loc_1",
"action": "on",
"guard": {
"exp": {
"op": "≥",
"left": "warrenty",
"right": 0
}
},
"destinations": [ {
"location": "loc_1"
} ]
}
]
},
{
"name": "Clicks",
"locations": [ {
"name": "loc_1"
} ],
"initial-locations": [ "loc_1" ],
"edges": [
{