diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.cpp b/src/storm-gspn/builder/JaniGSPNBuilder.cpp index fa01450de..6744e3c43 100644 --- a/src/storm-gspn/builder/JaniGSPNBuilder.cpp +++ b/src/storm-gspn/builder/JaniGSPNBuilder.cpp @@ -108,7 +108,7 @@ namespace storm { for (auto const& inPlaceEntry : trans.getInputPlaces()) { destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() >= inPlaceEntry.second); if (trans.getOutputPlaces().count(inPlaceEntry.first) == 0) { - assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first])->getExpressionVariable() - inPlaceEntry.second); + assignments.emplace_back(storm::jani::LValue(*vars[inPlaceEntry.first]), (vars[inPlaceEntry.first])->getExpressionVariable() - inPlaceEntry.second); } } for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) { @@ -116,9 +116,9 @@ namespace storm { } for (auto const& outputPlaceEntry : trans.getOutputPlaces()) { if (trans.getInputPlaces().count(outputPlaceEntry.first) == 0) { - assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second ); + assignments.emplace_back(storm::jani::LValue(*vars[outputPlaceEntry.first]), (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second ); } else { - assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second - trans.getInputPlaces().at(outputPlaceEntry.first)); + assignments.emplace_back(storm::jani::LValue(*vars[outputPlaceEntry.first]), (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second - trans.getInputPlaces().at(outputPlaceEntry.first)); } } destguard = destguard.simplify(); @@ -147,7 +147,7 @@ namespace storm { for (auto const& inPlaceEntry : trans.getInputPlaces()) { guard = guard && (vars[inPlaceEntry.first]->getExpressionVariable() >= inPlaceEntry.second); if (trans.getOutputPlaces().count(inPlaceEntry.first) == 0) { - assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first])->getExpressionVariable() - inPlaceEntry.second); + assignments.emplace_back(storm::jani::LValue(*vars[inPlaceEntry.first]), (vars[inPlaceEntry.first])->getExpressionVariable() - inPlaceEntry.second); } } for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) { @@ -155,9 +155,9 @@ namespace storm { } for (auto const& outputPlaceEntry : trans.getOutputPlaces()) { if (trans.getInputPlaces().count(outputPlaceEntry.first) == 0) { - assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second ); + assignments.emplace_back(storm::jani::LValue(*vars[outputPlaceEntry.first]), (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second ); } else { - assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second - trans.getInputPlaces().at(outputPlaceEntry.first)); + assignments.emplace_back(storm::jani::LValue(*vars[outputPlaceEntry.first]), (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second - trans.getInputPlaces().at(outputPlaceEntry.first)); } } @@ -257,7 +257,7 @@ namespace storm { auto exprVar = expressionManager->declareBooleanVariable(name); auto const& janiVar = model->addVariable(*storm::jani::makeBooleanVariable(name, exprVar, expressionManager->boolean(false), true)); - storm::jani::Assignment assignment(janiVar, transientValue); + storm::jani::Assignment assignment(storm::jani::LValue(janiVar), transientValue); model->getAutomata().front().getLocations().front().addTransientAssignment(assignment); return janiVar; } diff --git a/src/storm-pgcl-cli/storm-pgcl.cpp b/src/storm-pgcl-cli/storm-pgcl.cpp index 2c81dc945..30a72a09b 100644 --- a/src/storm-pgcl-cli/storm-pgcl.cpp +++ b/src/storm-pgcl-cli/storm-pgcl.cpp @@ -41,7 +41,8 @@ void initializeSettings() { void handleJani(storm::jani::Model& model) { auto const& jani = storm::settings::getModule(); storm::converter::JaniConversionOptions options(jani); - storm::api::transformJani(model, {}, options); + std::vector properties; + storm::api::transformJani(model, properties, options); if (storm::settings::getModule().isToJaniSet()) { storm::api::exportJaniToFile(model, {}, storm::settings::getModule().getWriteToJaniFilename(), jani.isCompactJsonSet()); } else { diff --git a/src/storm-pgcl/builder/JaniProgramGraphBuilder.cpp b/src/storm-pgcl/builder/JaniProgramGraphBuilder.cpp index 0db2787bb..bcb569917 100644 --- a/src/storm-pgcl/builder/JaniProgramGraphBuilder.cpp +++ b/src/storm-pgcl/builder/JaniProgramGraphBuilder.cpp @@ -53,9 +53,9 @@ namespace storm { if(isRewardVariable(assignment.first)) { std::unordered_map eval; eval.emplace((variables.at(assignment.first))->getExpressionVariable(), expManager->integer(0)); - vec.emplace_back(*(variables.at(assignment.first)), assignment.second.substitute(eval).simplify(), level); + vec.emplace_back(storm::jani::LValue(*(variables.at(assignment.first))), assignment.second.substitute(eval).simplify(), level); } else { - vec.emplace_back(*(variables.at(assignment.first)), assignment.second, level); + vec.emplace_back(storm::jani::LValue(*(variables.at(assignment.first))), assignment.second, level); } } ++level; @@ -67,7 +67,7 @@ namespace storm { storm::ppg::ProbabilisticProgramAction const& act = static_cast(edge.getAction()); std::vector> vec; for(auto const& assign : act) { - storm::jani::Assignment assignment(automaton.getVariables().getVariable(act.getVariableName()), expManager->integer(assign.value), 0); + storm::jani::Assignment assignment(storm::jani::LValue(automaton.getVariables().getVariable(act.getVariableName())), expManager->integer(assign.value), 0); templateEdge.addDestination(storm::jani::TemplateEdgeDestination(storm::jani::OrderedAssignments(assignment))); vec.emplace_back(janiLocId.at(edge.getTargetId()), assign.probability); } diff --git a/src/storm-pgcl/builder/JaniProgramGraphBuilder.h b/src/storm-pgcl/builder/JaniProgramGraphBuilder.h index 08edb3220..ba3f1bd4e 100644 --- a/src/storm-pgcl/builder/JaniProgramGraphBuilder.h +++ b/src/storm-pgcl/builder/JaniProgramGraphBuilder.h @@ -142,7 +142,7 @@ namespace storm { storm::jani::Location janiLoc(janiLocationName(it->second.id())); for(auto const& label : programGraph.getLabels(it->second.id())) { assert(labelVars.count(label) > 0); - janiLoc.addTransientAssignment(storm::jani::Assignment(*(labelVars.at(label)), expManager->boolean(true))); + janiLoc.addTransientAssignment(storm::jani::Assignment(storm::jani::LValue(*(labelVars.at(label))), expManager->boolean(true))); } result[it->second.id()] = automaton.addLocation(janiLoc); if (it->second.isInitial()) {