sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

JANI Export now preserves variable names correctly

main
sjunges 9 years ago
parent
57fd0fa2dd
commit
7bc6ce99fa
2 changed files with 53 additions and 38 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 77
      src/storm/storage/jani/JSONExporter.cpp
  2. 8
      src/storm/storage/jani/JSONExporter.h

77
src/storm/storage/jani/JSONExporter.cpp
View File

@ -32,6 +32,10 @@ namespace storm {
namespace jani {
modernjson::json buildExpression(storm::expressions::Expression const& exp, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables = VariableSet(), VariableSet const& localVariables = VariableSet()) {
return ExpressionToJson::translate(exp, constants, globalVariables, localVariables);
}
class CompositionJsonExporter : public CompositionVisitor {
public:
CompositionJsonExporter(bool allowRecursion) : allowRecursion(allowRecursion){
@ -145,7 +149,7 @@ namespace storm {
}
boost::any FormulaToJaniJson::visit(storm::logic::AtomicExpressionFormula const& f, boost::any const&) const {
return ExpressionToJson::translate(f.getExpression());
return buildExpression(f.getExpression(), model.getConstants(), model.getGlobalVariables());
}
boost::any FormulaToJaniJson::visit(storm::logic::AtomicLabelFormula const& f, boost::any const&) const {
@ -450,8 +454,8 @@ namespace storm {
}
}
modernjson::json ExpressionToJson::translate(storm::expressions::Expression const& expr) {
ExpressionToJson visitor;
modernjson::json ExpressionToJson::translate(storm::expressions::Expression const& expr, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables) {
ExpressionToJson visitor(constants, globalVariables, localVariables);
return boost::any_cast<modernjson::json>(expr.accept(visitor, boost::none));
}
@ -486,7 +490,18 @@ namespace storm {
return opDecl;
}
boost::any ExpressionToJson::visit(storm::expressions::VariableExpression const& expression, boost::any const&) {
return modernjson::json(expression.getVariableName());
if (globalVariables.hasVariable(expression.getVariable())) {
return modernjson::json(globalVariables.getVariable(expression.getVariable()).getName());
} else if (localVariables.hasVariable(expression.getVariable())) {
return modernjson::json(localVariables.getVariable(expression.getVariable()).getName());
} else {
for (auto const& constant : constants) {
if (constant.getExpressionVariable() == expression.getVariable()) {
return modernjson::json(constant.getName());
}
}
}
STORM_LOG_ASSERT(false, "Expression variable '" << expression.getVariableName() << "' not known in Jani data structures.");
}
boost::any ExpressionToJson::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression, boost::any const& data) {
modernjson::json opDecl;
@ -555,10 +570,6 @@ namespace storm {
}
modernjson::json buildExpression(storm::expressions::Expression const& exp) {
return ExpressionToJson::translate(exp);
}
modernjson::json buildConstantsArray(std::vector<storm::jani::Constant> const& constants) {
std::vector<modernjson::json> constantDeclarations;
@ -576,14 +587,14 @@ namespace storm {
}
constantEntry["type"] = typeDesc;
if(constant.isDefined()) {
constantEntry["value"] = buildExpression(constant.getExpression());
constantEntry["value"] = buildExpression(constant.getExpression(), constants);
}
constantDeclarations.push_back(constantEntry);
}
return modernjson::json(constantDeclarations);
}
modernjson::json buildVariablesArray(storm::jani::VariableSet const& varSet) {
modernjson::json buildVariablesArray(storm::jani::VariableSet const& varSet, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables = VariableSet()) {
std::vector<modernjson::json> variableDeclarations;
for(auto const& variable : varSet) {
modernjson::json varEntry;
@ -602,13 +613,13 @@ namespace storm {
assert(variable.isBoundedIntegerVariable());
typeDesc["kind"] = "bounded";
typeDesc["base"] = "int";
typeDesc["lower-bound"] = buildExpression(variable.asBoundedIntegerVariable().getLowerBound());
typeDesc["upper-bound"] = buildExpression(variable.asBoundedIntegerVariable().getUpperBound());
typeDesc["lower-bound"] = buildExpression(variable.asBoundedIntegerVariable().getLowerBound(), constants, globalVariables, localVariables);
typeDesc["upper-bound"] = buildExpression(variable.asBoundedIntegerVariable().getUpperBound(), constants, globalVariables, localVariables);
}
varEntry["type"] = typeDesc;
if(variable.hasInitExpression()) {
varEntry["initial-value"] = buildExpression(variable.getInitExpression());
varEntry["initial-value"] = buildExpression(variable.getInitExpression(), constants, globalVariables, localVariables);
}
variableDeclarations.push_back(varEntry);
}
@ -616,13 +627,13 @@ namespace storm {
}
modernjson::json buildAssignmentArray(storm::jani::OrderedAssignments const& orderedAssignments) {
modernjson::json buildAssignmentArray(storm::jani::OrderedAssignments const& orderedAssignments, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables) {
std::vector<modernjson::json> assignmentDeclarations;
bool addIndex = orderedAssignments.hasMultipleLevels();
for(auto const& assignment : orderedAssignments) {
modernjson::json assignmentEntry;
assignmentEntry["ref"] = assignment.getVariable().getName();
assignmentEntry["value"] = buildExpression(assignment.getAssignedExpression());
assignmentEntry["value"] = buildExpression(assignment.getAssignedExpression(), constants, globalVariables, localVariables);
if(addIndex) {
assignmentEntry["index"] = assignment.getLevel();
}
@ -631,14 +642,14 @@ namespace storm {
return modernjson::json(assignmentDeclarations);
}
modernjson::json buildLocationsArray(std::vector<storm::jani::Location> const& locations) {
modernjson::json buildLocationsArray(std::vector<storm::jani::Location> const& locations, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables) {
std::vector<modernjson::json> locationDeclarations;
for(auto const& location : locations) {
modernjson::json locEntry;
locEntry["name"] = location.getName();
// TODO support invariants?
if (!location.getAssignments().empty()) {
locEntry["transient-values"] = buildAssignmentArray(location.getAssignments());
locEntry["transient-values"] = buildAssignmentArray(location.getAssignments(), constants, globalVariables, localVariables);
}
locationDeclarations.push_back(locEntry);
}
@ -653,7 +664,7 @@ namespace storm {
return modernjson::json(names);
}
modernjson::json buildDestinations(std::vector<EdgeDestination> const& destinations, std::map<uint64_t, std::string> const& locationNames) {
modernjson::json buildDestinations(std::vector<EdgeDestination> const& destinations, std::map<uint64_t, std::string> const& locationNames, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables) {
assert(destinations.size() > 0);
std::vector<modernjson::json> destDeclarations;
for(auto const& destination : destinations) {
@ -666,17 +677,17 @@ namespace storm {
}
}
if (!prob1) {
destEntry["probability"]["exp"] = buildExpression(destination.getProbability());
destEntry["probability"]["exp"] = buildExpression(destination.getProbability(), constants, globalVariables, localVariables);
}
if (!destination.getOrderedAssignments().empty()) {
destEntry["assignments"] = buildAssignmentArray(destination.getOrderedAssignments());
destEntry["assignments"] = buildAssignmentArray(destination.getOrderedAssignments(), constants, globalVariables, localVariables);
}
destDeclarations.push_back(destEntry);
}
return modernjson::json(destDeclarations);
}
modernjson::json buildEdges(std::vector<Edge> const& edges , std::map<uint64_t, std::string> const& actionNames, std::map<uint64_t, std::string> const& locationNames) {
modernjson::json buildEdges(std::vector<Edge> const& edges , std::map<uint64_t, std::string> const& actionNames, std::map<uint64_t, std::string> const& locationNames, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables) {
std::vector<modernjson::json> edgeDeclarations;
for(auto const& edge : edges) {
if (edge.getGuard().isFalse()) {
@ -689,14 +700,14 @@ namespace storm {
edgeEntry["action"] = actionNames.at(edge.getActionIndex());
}
if(edge.hasRate()) {
edgeEntry["rate"]["exp"] = buildExpression(edge.getRate());
edgeEntry["rate"]["exp"] = buildExpression(edge.getRate(), constants, globalVariables, localVariables);
}
if (!edge.getGuard().isTrue()) {
edgeEntry["guard"]["exp"] = buildExpression(edge.getGuard());
edgeEntry["guard"]["exp"] = buildExpression(edge.getGuard(), constants, globalVariables, localVariables);
}
edgeEntry["destinations"] = buildDestinations(edge.getDestinations(), locationNames);
edgeEntry["destinations"] = buildDestinations(edge.getDestinations(), locationNames, constants, globalVariables, localVariables);
if (!edge.getAssignments().empty()) {
edgeEntry["assignments"] = buildAssignmentArray(edge.getAssignments());
edgeEntry["assignments"] = buildAssignmentArray(edge.getAssignments(), constants, globalVariables, localVariables);
}
edgeDeclarations.push_back(edgeEntry);
@ -704,18 +715,18 @@ namespace storm {
return modernjson::json(edgeDeclarations);
}
modernjson::json buildAutomataArray(std::vector<storm::jani::Automaton> const& automata, std::map<uint64_t, std::string> const& actionNames) {
modernjson::json buildAutomataArray(std::vector<storm::jani::Automaton> const& automata, std::map<uint64_t, std::string> const& actionNames, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables) {
std::vector<modernjson::json> automataDeclarations;
for(auto const& automaton : automata) {
modernjson::json autoEntry;
autoEntry["name"] = automaton.getName();
autoEntry["variables"] = buildVariablesArray(automaton.getVariables());
autoEntry["variables"] = buildVariablesArray(automaton.getVariables(), constants, globalVariables, automaton.getVariables());
if(automaton.hasRestrictedInitialStates()) {
autoEntry["restrict-initial"]["exp"] = buildExpression(automaton.getInitialStatesRestriction());
autoEntry["restrict-initial"]["exp"] = buildExpression(automaton.getInitialStatesRestriction(), constants, globalVariables, automaton.getVariables());
}
autoEntry["locations"] = buildLocationsArray(automaton.getLocations());
autoEntry["locations"] = buildLocationsArray(automaton.getLocations(), constants, globalVariables, automaton.getVariables());
autoEntry["initial-locations"] = buildInitialLocations(automaton);
autoEntry["edges"] = buildEdges(automaton.getEdges(), actionNames, automaton.buildIdToLocationNameMap());
autoEntry["edges"] = buildEdges(automaton.getEdges(), actionNames, automaton.buildIdToLocationNameMap(), constants, globalVariables, automaton.getVariables());
automataDeclarations.push_back(autoEntry);
}
return modernjson::json(automataDeclarations);
@ -728,9 +739,9 @@ namespace storm {
jsonStruct["type"] = to_string(janiModel.getModelType());
jsonStruct["actions"] = buildActionArray(janiModel.getActions());
jsonStruct["constants"] = buildConstantsArray(janiModel.getConstants());
jsonStruct["variables"] = buildVariablesArray(janiModel.getGlobalVariables());
jsonStruct["restrict-initial"]["exp"] = buildExpression(janiModel.getInitialStatesRestriction());
jsonStruct["automata"] = buildAutomataArray(janiModel.getAutomata(), janiModel.getActionIndexToNameMap());
jsonStruct["variables"] = buildVariablesArray(janiModel.getGlobalVariables(), janiModel.getConstants(), janiModel.getGlobalVariables());
jsonStruct["restrict-initial"]["exp"] = buildExpression(janiModel.getInitialStatesRestriction(), janiModel.getConstants(), janiModel.getGlobalVariables());
jsonStruct["automata"] = buildAutomataArray(janiModel.getAutomata(), janiModel.getActionIndexToNameMap(), janiModel.getConstants(), janiModel.getGlobalVariables());
jsonStruct["system"] = CompositionJsonExporter::translate(janiModel.getSystemComposition());
std::vector<std::string> standardFeatureVector = {"derived-operators"};
jsonStruct["features"] = standardFeatureVector;

8
src/storm/storage/jani/JSONExporter.h
View File

@ -18,7 +18,7 @@ namespace storm {
class ExpressionToJson : public storm::expressions::ExpressionVisitor {
public:
static modernjson::json translate(storm::expressions::Expression const& expr);
static modernjson::json translate(storm::expressions::Expression const& expr, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables);
virtual boost::any visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data);
virtual boost::any visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data);
@ -30,7 +30,11 @@ namespace storm {
virtual boost::any visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const& data);
virtual boost::any visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const& data);
virtual boost::any visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const& data);
private:
ExpressionToJson(std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables) : constants(constants), globalVariables(globalVariables), localVariables(localVariables) {}
std::vector<storm::jani::Constant> const& constants;
VariableSet const& globalVariables;
VariableSet const& localVariables;
};
class FormulaToJaniJson : public storm::logic::FormulaVisitor {

Write Preview
Loading…
Cancel
Save