dehnert
7 years ago
19 changed files with 286 additions and 32 deletions
-
8src/storm-cli-utilities/model-handling.h
-
16src/storm/api/export.cpp
-
31src/storm/settings/modules/JaniExportSettings.cpp
-
10src/storm/settings/modules/JaniExportSettings.h
-
10src/storm/solver/helper/SoundValueIterationHelper.cpp
-
2src/storm/storage/jani/Assignment.cpp
-
3src/storm/storage/jani/Assignment.h
-
4src/storm/storage/jani/Automaton.cpp
-
2src/storm/storage/jani/Automaton.h
-
39src/storm/storage/jani/JSONExporter.cpp
-
4src/storm/storage/jani/JSONExporter.h
-
121src/storm/storage/jani/JaniLocationExpander.cpp
-
26src/storm/storage/jani/JaniLocationExpander.h
-
4src/storm/storage/jani/Location.cpp
-
3src/storm/storage/jani/Location.h
-
10src/storm/storage/jani/Model.cpp
-
13src/storm/storage/jani/Model.h
-
8src/storm/storage/jani/OrderedAssignments.cpp
-
4src/storm/storage/jani/OrderedAssignments.h
@ -0,0 +1,121 @@ |
|||
#include "storm/storage/jani/JaniLocationExpander.h"
|
|||
|
|||
#include "storm/storage/expressions/ExpressionManager.h"
|
|||
#include "storm/exceptions/NotSupportedException.h"
|
|||
#include "storm/exceptions/IllegalArgumentException.h"
|
|||
|
|||
|
|||
namespace storm { |
|||
namespace jani { |
|||
JaniLocationExpander::JaniLocationExpander(Model const& origModel) : original(origModel) { |
|||
|
|||
} |
|||
|
|||
void JaniLocationExpander::transform(std::string const& automatonName, std::string const& variableName) { |
|||
STORM_LOG_THROW(original.hasAutomaton(automatonName), storm::exceptions::IllegalArgumentException, "Model has no automaton with name " << automatonName << ". "); |
|||
STORM_LOG_THROW(original.getAutomaton(automatonName).hasVariable(variableName), storm::exceptions::IllegalArgumentException, "Automaton " << automatonName << " has no variable with name " << variableName << ". "); |
|||
newModel = original; |
|||
newModel.replaceAutomaton(newModel.getAutomatonIndex(automatonName), transformAutomaton(original.getAutomaton(automatonName), variableName)); |
|||
} |
|||
|
|||
|
|||
Model const& JaniLocationExpander::getResult() const { |
|||
return newModel; |
|||
} |
|||
|
|||
Automaton JaniLocationExpander::transformAutomaton(Automaton const& automaton, std::string const& variableName) { |
|||
|
|||
Automaton newAutomaton(automaton.getName(), automaton.getLocationExpressionVariable()); |
|||
int64_t initialVariableValue; |
|||
int64_t variableLowerBound; |
|||
int64_t variableUpperBound; |
|||
storm::expressions::Variable eliminatedExpressionVariable; |
|||
const storm::jani::Variable* variable; |
|||
|
|||
for (auto const& var : automaton.getVariables()) { |
|||
if (var.getName() == variableName) { |
|||
// This variable will be eliminated in the new automaton.
|
|||
STORM_LOG_THROW(var.hasInitExpression(), storm::exceptions::IllegalArgumentException, "Variable to be eliminated has to have an initexpression."); |
|||
STORM_LOG_THROW(var.isBoundedIntegerVariable(), storm::exceptions::IllegalArgumentException, "Variable to be eliminated has to be an bounded integer variable."); |
|||
STORM_LOG_THROW(!var.isTransient(), storm::exceptions::IllegalArgumentException, "Cannot eliminate transient variable"); |
|||
|
|||
variableUpperBound = var.asBoundedIntegerVariable().getUpperBound().evaluateAsInt(); |
|||
variableLowerBound = var.asBoundedIntegerVariable().getLowerBound().evaluateAsInt(); |
|||
initialVariableValue = var.getInitExpression().evaluateAsInt(); |
|||
variable = &var; |
|||
eliminatedExpressionVariable = var.getExpressionVariable(); |
|||
|
|||
} else { |
|||
// Other variables are just copied.
|
|||
newAutomaton.addVariable(var); |
|||
} |
|||
} |
|||
|
|||
STORM_LOG_THROW(!automaton.getInitialStatesRestriction().containsVariable({eliminatedExpressionVariable}), storm::exceptions::NotSupportedException, "Elimination of variable that occurs in the initial state restriction is not allowed"); |
|||
newAutomaton.setInitialStatesRestriction(automaton.getInitialStatesRestriction()); |
|||
|
|||
|
|||
std::map<storm::expressions::Variable, storm::expressions::Expression> substitutionMap; |
|||
std::map<std::string, std::vector<std::string>> locationNames; |
|||
std::map<uint64_t, std::map<int64_t, uint64_t>> locationVariableValueMap; |
|||
for (auto const& loc : automaton.getLocations()) { |
|||
locationNames[loc.getName()] = std::vector<std::string>(); |
|||
uint64_t origIndex = automaton.getLocationIndex(loc.getName()); |
|||
|
|||
for (int64_t i = variableLowerBound; i <= variableUpperBound; i++) { |
|||
std::string newLocationName = loc.getName() + "_" + variableName + "_" + std::to_string(i); |
|||
substitutionMap[eliminatedExpressionVariable] = original.getExpressionManager().integer(i); |
|||
std::cout << "eliminate " << eliminatedExpressionVariable.getName() << " with " << i << std::endl; |
|||
OrderedAssignments newAssignments = loc.getAssignments().clone(); |
|||
newAssignments.substitute(substitutionMap); |
|||
std::cout << newAssignments << std::endl; |
|||
uint64_t newLocationIndex = newAutomaton.addLocation(Location(newLocationName, newAssignments)); |
|||
|
|||
locationVariableValueMap[origIndex][i] = newLocationIndex; |
|||
locationNames[loc.getName()].push_back(newLocationName); |
|||
} |
|||
} |
|||
|
|||
|
|||
|
|||
for (auto const& edge : automaton.getEdges()) { |
|||
for (auto const& newValueAndLocation : locationVariableValueMap[edge.getSourceLocationIndex()]) { |
|||
substitutionMap[eliminatedExpressionVariable] = original.getExpressionManager().integer(newValueAndLocation.first); |
|||
|
|||
uint64_t newSourceIndex = newValueAndLocation.second; |
|||
storm::expressions::Expression newGuard = edge.getGuard().substitute(substitutionMap).simplify(); |
|||
if (!newGuard.containsVariables() && !newGuard.evaluateAsBool()) { |
|||
continue; |
|||
} |
|||
std::shared_ptr<storm::jani::TemplateEdge> templateEdge = std::make_shared<storm::jani::TemplateEdge>(newGuard); |
|||
|
|||
STORM_LOG_THROW(edge.getAssignments().empty(), storm::exceptions::NotImplementedException, "Support for edge-assignments is not implemented"); |
|||
|
|||
std::vector<std::pair<uint64_t, storm::expressions::Expression>> destinationLocationsAndProbabilities; |
|||
for (auto const& destination : edge.getDestinations()) { |
|||
OrderedAssignments oa(destination.getOrderedAssignments().clone()); |
|||
oa.substitute(substitutionMap); |
|||
int64_t value; |
|||
for (auto const& assignment : oa) { |
|||
if (assignment.getVariable() == *variable) { |
|||
oa.remove(assignment); |
|||
value = assignment.getAssignedExpression().evaluateAsInt(); |
|||
break; |
|||
} |
|||
} |
|||
TemplateEdgeDestination ted(oa); |
|||
templateEdge->addDestination(ted); |
|||
destinationLocationsAndProbabilities.emplace_back(locationVariableValueMap[destination.getLocationIndex()][value], destination.getProbability().substitute((substitutionMap))); |
|||
} |
|||
newAutomaton.addEdge(storm::jani::Edge(newSourceIndex, edge.getActionIndex(), edge.hasRate() ? boost::optional<storm::expressions::Expression>(edge.getRate().substitute(substitutionMap)) : boost::none, templateEdge, destinationLocationsAndProbabilities)); |
|||
|
|||
} |
|||
} |
|||
return newAutomaton; |
|||
|
|||
|
|||
} |
|||
|
|||
|
|||
} |
|||
} |
|||
@ -0,0 +1,26 @@ |
|||
#pragma once |
|||
|
|||
#include "storm/storage/jani/Model.h" |
|||
#include "storm/storage/jani/Automaton.h" |
|||
|
|||
|
|||
namespace storm { |
|||
namespace jani { |
|||
class JaniLocationExpander { |
|||
public: |
|||
JaniLocationExpander(Model const& original); |
|||
void transform(std::string const& automatonName, std::string const& variableName); |
|||
Model const& getResult() const; |
|||
|
|||
private: |
|||
Model const& original; |
|||
Model newModel; |
|||
|
|||
Automaton transformAutomaton(Automaton const& automaton, std::string const& variableName); |
|||
|
|||
|
|||
|
|||
}; |
|||
} |
|||
|
|||
} |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue