diff --git a/src/storm-pgcl-cli/storm-pgcl.cpp b/src/storm-pgcl-cli/storm-pgcl.cpp index b849cb264..5c66d3a75 100644 --- a/src/storm-pgcl-cli/storm-pgcl.cpp +++ b/src/storm-pgcl-cli/storm-pgcl.cpp @@ -14,6 +14,7 @@ #include "storm/exceptions/FileIoException.h" #include "storm/settings/modules/GeneralSettings.h" +#include "storm/settings/modules/ResourceSettings.h" #include "storm/settings/modules/PGCLSettings.h" #include "storm/settings/modules/CoreSettings.h" #include "storm/settings/modules/DebugSettings.h" @@ -28,6 +29,7 @@ void initializeSettings() { // Register all known settings modules. storm::settings::addModule(); + storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); @@ -80,7 +82,7 @@ int main(const int argc, const char** argv) { // To disable reward detection, uncomment the following line // TODO add a setting for this. // settings.filterRewardVariables = false; - storm::builder::JaniProgramGraphBuilder builder(*progGraph); + storm::builder::JaniProgramGraphBuilder builder(*progGraph, settings); if (storm::settings::getModule().isProgramVariableRestrictionSet()) { // TODO More fine grained control storm::storage::IntegerInterval restr = storm::storage::parseIntegerInterval(storm::settings::getModule().getProgramVariableRestrictions()); diff --git a/src/storm-pgcl/builder/JaniProgramGraphBuilder.cpp b/src/storm-pgcl/builder/JaniProgramGraphBuilder.cpp index 736dcad21..4741fc374 100644 --- a/src/storm-pgcl/builder/JaniProgramGraphBuilder.cpp +++ b/src/storm-pgcl/builder/JaniProgramGraphBuilder.cpp @@ -63,23 +63,24 @@ namespace storm { return storm::jani::OrderedAssignments(vec); } - std::vector JaniProgramGraphBuilder::buildProbabilisticDestinations(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge ) { + std::vector> JaniProgramGraphBuilder::buildProbabilisticDestinations(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge, storm::jani::TemplateEdge& templateEdge) { 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); - vec.emplace_back(janiLocId.at(edge.getTargetId()), assign.probability, assignment); + std::vector> vec; + for(auto const& assign : act) { + storm::jani::Assignment assignment(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); } return vec; } - std::vector JaniProgramGraphBuilder::buildDestinations(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge ) { + std::vector> JaniProgramGraphBuilder::buildDestinations(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge, storm::jani::TemplateEdge& templateEdge) { if (edge.getAction().isProbabilistic()) { - return buildProbabilisticDestinations(automaton, edge); + return buildProbabilisticDestinations(automaton, edge, templateEdge); } else { storm::jani::OrderedAssignments oa = buildOrderedAssignments(automaton, static_cast(edge.getAction())); - storm::jani::EdgeDestination dest(janiLocId.at(edge.getTargetId()), expManager->rational(1.0), oa); - return {dest}; + templateEdge.addDestination(storm::jani::TemplateEdgeDestination(oa)); + return {std::make_pair(janiLocId.at(edge.getTargetId()), expManager->rational(1.0))}; } } @@ -88,7 +89,7 @@ namespace storm { return in.simplify(); } - std::pair, storm::expressions::Expression> JaniProgramGraphBuilder::addVariableChecks(storm::ppg::ProgramEdge const& edge) { + std::pair, storm::expressions::Expression> JaniProgramGraphBuilder::addVariableChecks(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge) { std::vector edges; storm::expressions::Expression newGuard; newGuard = expManager->boolean(true); @@ -116,8 +117,10 @@ namespace storm { // TODO currently only fully bounded restrictions are supported; assert(userVariableRestrictions.at(assignment.first).hasLeftBound() && userVariableRestrictions.at(assignment.first).hasRightBound()); storm::expressions::Expression newCondition = simplifyExpression(edge.getCondition() && (assignment.second > bound.getRightBound().get() || assignment.second < bound.getLeftBound().get())); - storm::jani::EdgeDestination dest(varOutOfBoundsLocations.at(assignment.first), expManager->rational(1.0), storm::jani::OrderedAssignments()); - storm::jani::Edge e(janiLocId.at(edge.getSourceId()), storm::jani::Model::SILENT_ACTION_INDEX, boost::none, newCondition, {dest}); + + std::shared_ptr templateEdge = automaton.createTemplateEdge(newCondition); + templateEdge->addDestination(storm::jani::TemplateEdgeDestination()); + storm::jani::Edge e(janiLocId.at(edge.getSourceId()), storm::jani::Model::SILENT_ACTION_INDEX, boost::none, templateEdge, {varOutOfBoundsLocations.at(assignment.first)}, {expManager->rational(1.0)}); edges.push_back(e); newGuard = newGuard && assignment.second <= bound.getRightBound().get() && assignment.second >= bound.getLeftBound().get(); } @@ -133,17 +136,20 @@ namespace storm { for(auto it = programGraph.locationBegin(); it != programGraph.locationEnd(); ++it) { ppg::ProgramLocation const& loc = it->second; if (loc.nrOutgoingEdgeGroups() == 0) { - storm::jani::OrderedAssignments oa; - storm::jani::EdgeDestination dest(janiLocId.at(loc.id()), expManager->integer(1), oa); - storm::jani::Edge e(janiLocId.at(loc.id()), storm::jani::Model::SILENT_ACTION_INDEX, boost::none, expManager->boolean(true), {dest}); + std::shared_ptr templateEdge = automaton.createTemplateEdge(expManager->boolean(true)); + templateEdge->addDestination(storm::jani::TemplateEdgeDestination()); + storm::jani::Edge e(janiLocId.at(loc.id()), storm::jani::Model::SILENT_ACTION_INDEX, boost::none, templateEdge, {janiLocId.at(loc.id())}, {expManager->rational(1.0)}); automaton.addEdge(e); } else if (loc.nrOutgoingEdgeGroups() == 1) { for(auto const& edge : **(loc.begin())) { - std::pair, storm::expressions::Expression> checks = addVariableChecks(*edge); + std::pair, storm::expressions::Expression> checks = addVariableChecks(automaton, *edge); for(auto const& check : checks.first) { automaton.addEdge(check); } - storm::jani::Edge e(janiLocId.at(loc.id()), storm::jani::Model::SILENT_ACTION_INDEX, boost::none, simplifyExpression(edge->getCondition() && checks.second), buildDestinations(automaton, *edge)); + std::shared_ptr templateEdge = automaton.createTemplateEdge(simplifyExpression(edge->getCondition() && checks.second)); + std::vector> destinationLocationsAndProbabilities = buildDestinations(automaton, *edge, *templateEdge); + + storm::jani::Edge e(janiLocId.at(loc.id()), storm::jani::Model::SILENT_ACTION_INDEX, boost::none, templateEdge, destinationLocationsAndProbabilities); automaton.addEdge(e); } } else { @@ -152,15 +158,20 @@ namespace storm { { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Combi of nondeterminism and probabilistic choices within a loc not supported yet"); } else { - std::vector destinations; + std::shared_ptr templateEdge = automaton.createTemplateEdge(expManager->boolean(true)); + + std::vector destinationProbabilities; + std::vector destinationLocations; for(auto const& eg : loc) { // TODO add assignments assert(eg->nrEdges() < 2); // Otherwise, non-determinism occurs. assert(eg->nrEdges() > 0); // Empty edge groups should not occur in input. - uint64_t target = janiLocId.at((*eg->begin())->getTargetId()); - destinations.emplace_back(target, eg->getProbability()); + destinationLocations.push_back(janiLocId.at((*eg->begin())->getTargetId())); + destinationProbabilities.push_back(eg->getProbability()); + templateEdge->addDestination(storm::jani::TemplateEdgeDestination()); } - storm::jani::Edge e(janiLocId.at(it->second.id()), storm::jani::Model::SILENT_ACTION_INDEX, boost::none, expManager->boolean(true), destinations); + + storm::jani::Edge e(janiLocId.at(it->second.id()), storm::jani::Model::SILENT_ACTION_INDEX, boost::none, templateEdge, destinationLocations, destinationProbabilities); automaton.addEdge(e); } } diff --git a/src/storm-pgcl/builder/JaniProgramGraphBuilder.h b/src/storm-pgcl/builder/JaniProgramGraphBuilder.h index beb6c1aed..ad5feb8a4 100644 --- a/src/storm-pgcl/builder/JaniProgramGraphBuilder.h +++ b/src/storm-pgcl/builder/JaniProgramGraphBuilder.h @@ -69,7 +69,7 @@ namespace storm { storm::jani::Model* build(std::string const& name = "program_graph") { expManager = programGraph.getExpressionManager(); storm::jani::Model* model = new storm::jani::Model(name, storm::jani::ModelType::MDP, janiVersion, expManager); - storm::jani::Automaton mainAutomaton("main"); + storm::jani::Automaton mainAutomaton("main", expManager->declareIntegerVariable("pc")); addProcedureVariables(*model, mainAutomaton); janiLocId = addProcedureLocations(*model, mainAutomaton); addVariableOoBLocations(mainAutomaton); @@ -90,13 +90,13 @@ namespace storm { storm::jani::OrderedAssignments buildOrderedAssignments(storm::jani::Automaton& automaton, storm::ppg::DeterministicProgramAction const& act) ; void addEdges(storm::jani::Automaton& automaton); - std::vector buildDestinations(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge ); + std::vector> buildDestinations(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge, storm::jani::TemplateEdge& templateEdge); /** * Helper for probabilistic assignments */ - std::vector buildProbabilisticDestinations(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge ); + std::vector> buildProbabilisticDestinations(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge, storm::jani::TemplateEdge& templateEdge); - std::pair, storm::expressions::Expression> addVariableChecks(storm::ppg::ProgramEdge const& edge); + std::pair, storm::expressions::Expression> addVariableChecks(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge); bool isUserRestrictedVariable(storm::ppg::ProgramVariableIdentifier i) const { return userVariableRestrictions.count(i) == 1 && !isRewardVariable(i); diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index ff84b0f9b..78b32010c 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -64,7 +64,10 @@ namespace storm { std::pair player1Choices = this->abstractor.get().getPlayer1ChoiceRange(); for (uint64_t index = player1Choices.first; index < player1Choices.second; ++index) { - guards.push_back(this->abstractor.get().getGuard(index)); + storm::expressions::Expression guard = this->abstractor.get().getGuard(index); + if (!guard.isTrue() && !guard.isFalse()) { + guards.push_back(guard); + } } performRefinement(createGlobalRefinement(preprocessPredicates(guards, RefinementPredicates::Source::InitialGuard))); diff --git a/src/storm/storage/jani/OrderedAssignments.cpp b/src/storm/storage/jani/OrderedAssignments.cpp index 24ebf4b03..6433b0cfb 100644 --- a/src/storm/storage/jani/OrderedAssignments.cpp +++ b/src/storm/storage/jani/OrderedAssignments.cpp @@ -86,6 +86,10 @@ namespace storm { nonTransientAssignments.clear(); } + std::size_t OrderedAssignments::getNumberOfAssignments() const { + return allAssignments.size(); + } + int_fast64_t OrderedAssignments::getLowestLevel() const { return allAssignments.front()->getLevel(); } diff --git a/src/storm/storage/jani/OrderedAssignments.h b/src/storm/storage/jani/OrderedAssignments.h index 1cd9df215..c6318bafd 100644 --- a/src/storm/storage/jani/OrderedAssignments.h +++ b/src/storm/storage/jani/OrderedAssignments.h @@ -52,6 +52,11 @@ namespace storm { */ void clear(); + /*! + * Retrieves the total number of assignments. + */ + std::size_t getNumberOfAssignments() const; + /*! * Retrieves the lowest level among all assignments. Note that this may only be called if there is at least * one assignment. diff --git a/src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp b/src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp index 546f8fe09..aee1eeb24 100644 --- a/src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp +++ b/src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp @@ -8,7 +8,7 @@ #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/parser/PrismParser.h" -#include "storm/dtmc/DdPrismModelBuilder.h" +#include "storm/builder/DdPrismModelBuilder.h" #include "storm/models/symbolic/StandardRewardModel.h" #include "storm/models/symbolic/Dtmc.h" #include "storm/settings/SettingsManager.h"