diff --git a/src/builder/JaniProgramGraphBuilder.cpp b/src/builder/JaniProgramGraphBuilder.cpp index 41d6cba65..d6ecb3c23 100644 --- a/src/builder/JaniProgramGraphBuilder.cpp +++ b/src/builder/JaniProgramGraphBuilder.cpp @@ -50,7 +50,7 @@ namespace storm { // No check necessary currently, but at least we should statically check that the bounds are okay. storm::ppg::ProbabilisticProgramAction const& act = static_cast(edge.getAction()); if (isUserRestrictedVariable(act.getVariableIdentifier())) { - storm::storage::IntegerInterval const& bound = variableRestrictions.at(act.getVariableIdentifier()); + storm::storage::IntegerInterval const& bound = userVariableRestrictions.at(act.getVariableIdentifier()); storm::storage::IntegerInterval supportInterval = act.getSupportInterval(); STORM_LOG_THROW(bound.contains(supportInterval), storm::exceptions::NotSupportedException, "User provided bounds must contain all constant expressions"); } @@ -60,15 +60,15 @@ namespace storm { for(auto const& group : act) { for(auto const& assignment : group) { if (isUserRestrictedVariable(assignment.first)) { - assert(variableRestrictions.count(assignment.first) == 1); - storm::storage::IntegerInterval const& bound = variableRestrictions.at(assignment.first); + assert(userVariableRestrictions.count(assignment.first) == 1); + storm::storage::IntegerInterval const& bound = userVariableRestrictions.at(assignment.first); if (!assignment.second.containsVariables()) { // Constant assignments can be checked statically. // TODO we might still want to allow assignments which go out of bounds. STORM_LOG_THROW(bound.contains(assignment.second.evaluateAsInt()), storm::exceptions::NotSupportedException, "User provided bounds must contain all constant expressions"); } else { // TODO currently only fully bounded restrictions are supported; - assert(variableRestrictions.at(assignment.first).hasLeftBound() && variableRestrictions.at(assignment.first).hasRightBound()); + 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}); diff --git a/src/builder/JaniProgramGraphBuilder.h b/src/builder/JaniProgramGraphBuilder.h index 0e20e7d84..4f6c5fc9f 100644 --- a/src/builder/JaniProgramGraphBuilder.h +++ b/src/builder/JaniProgramGraphBuilder.h @@ -26,6 +26,11 @@ namespace storm { JaniProgramGraphBuilder(storm::ppg::ProgramGraph const& pg) : programGraph(pg) { rewards = programGraph.rewardVariables(); + constants = programGraph.constants(); + auto boundedVars = programGraph.constantAssigned(); + for(auto const& v : boundedVars) { + variableRestrictions.emplace(v, programGraph.supportForConstAssignedVariable(v)); + } } virtual ~JaniProgramGraphBuilder() { @@ -41,8 +46,14 @@ namespace storm { void restrictAllVariables(int64_t from, int64_t to) { for (auto const& v : programGraph.getVariables()) { - if(v.second.hasIntegerType()) { - variableRestrictions.emplace(v.first, storm::storage::IntegerInterval(from, to)); + if(isConstant(v.first)) { + continue; + } + if(variableRestrictions.count(v.first) > 0) { + continue; // Currently we ignore user bounds if we have bounded integers; + } + if(v.second.hasIntegerType() ) { + userVariableRestrictions.emplace(v.first, storm::storage::IntegerInterval(from, to)); } } } @@ -79,27 +90,44 @@ namespace storm { std::pair, storm::expressions::Expression> addVariableChecks(storm::ppg::ProgramEdge const& edge); - bool isUserRestrictedVariable(storm::ppg::ProgramVariableIdentifier i) { - return variableRestrictions.count(i) == 1 && !isRewardVariable(i); + bool isUserRestrictedVariable(storm::ppg::ProgramVariableIdentifier i) const { + return userVariableRestrictions.count(i) == 1 && !isRewardVariable(i); } - bool isRestrictedVariable(storm::ppg::ProgramVariableIdentifier i) { + bool isRestrictedVariable(storm::ppg::ProgramVariableIdentifier i) const { // Might be different from user restricted in near future. - return variableRestrictions.count(i) == 1 && !isRewardVariable(i); + return (variableRestrictions.count(i) == 1 && !isRewardVariable(i)) || isUserRestrictedVariable(i); + } + + storm::storage::IntegerInterval const& variableBounds(storm::ppg::ProgramVariableIdentifier i) const { + assert(isRestrictedVariable(i)); + if (userVariableRestrictions.count(i) == 1) { + return userVariableRestrictions.at(i); + } else { + return variableRestrictions.at(i); + } + } - bool isRewardVariable(storm::ppg::ProgramVariableIdentifier i) { + bool isRewardVariable(storm::ppg::ProgramVariableIdentifier i) const { return std::find(rewards.begin(), rewards.end(), i) != rewards.end(); } + bool isConstant(storm::ppg::ProgramVariableIdentifier i) const { + return std::find(constants.begin(), constants.end(), i) != constants.end(); + } + void addProcedureVariables(storm::jani::Model& model, storm::jani::Automaton& automaton) { for (auto const& v : programGraph.getVariables()) { - if (v.second.hasBooleanType()) { + if (isConstant(v.first)) { + storm::jani::Constant constant(v.second.getName(), v.second, programGraph.getInitialValue(v.first)); + model.addConstant(constant); + } else if (v.second.hasBooleanType()) { storm::jani::BooleanVariable* janiVar = new storm::jani::BooleanVariable(v.second.getName(), v.second, programGraph.getInitialValue(v.first), false); automaton.addVariable(*janiVar); variables.emplace(v.first, janiVar); } else if (isRestrictedVariable(v.first) && !isRewardVariable(v.first)) { - storm::storage::IntegerInterval const& bounds = variableRestrictions.at(v.first); + storm::storage::IntegerInterval const& bounds = variableBounds(v.first); if (bounds.hasLeftBound()) { if (bounds.hasRightBound()) { storm::jani::BoundedIntegerVariable* janiVar = new storm::jani::BoundedIntegerVariable (v.second.getName(), v.second, programGraph.getInitialValue(v.first), false, expManager->integer(bounds.getLeftBound().get()), expManager->integer(bounds.getRightBound().get())); @@ -139,7 +167,7 @@ namespace storm { } void addVariableOoBLocations(storm::jani::Automaton& automaton) { - for(auto const& restr : variableRestrictions) { + for(auto const& restr : userVariableRestrictions) { if(!isRewardVariable(restr.first)) { storm::jani::Location janiLoc(janiVariableOutOfBoundsLocationName(restr.first)); uint64_t locId = automaton.addLocation(janiLoc); @@ -150,8 +178,13 @@ namespace storm { } /// Transient variables std::vector rewards; - /// Restrictions on variables + /// Variables that are constants + std::vector constants; + /// Restrictions on variables (automatic) std::map variableRestrictions; + /// Restrictions on variables (provided by users) + std::map userVariableRestrictions; + /// Locations for variables that would have gone ot o std::map varOutOfBoundsLocations; std::map janiLocId; diff --git a/src/storage/IntegerInterval.h b/src/storage/IntegerInterval.h index 6965f0626..f662f1a6d 100644 --- a/src/storage/IntegerInterval.h +++ b/src/storage/IntegerInterval.h @@ -57,6 +57,29 @@ namespace storm { return true; } + void extend(int64_t val) { + if (hasLeftBound()) { + if(val < leftBound.get()) { + leftBound = val; + return; + } + } + if (hasRightBound()) { + if(val > rightBound.get()) { + rightBound = val; + } + } + } + + void extend(IntegerInterval const& i) { + if(i.hasLeftBound()) { + extend(i.getLeftBound().get()); + } + if(i.hasRightBound()) { + extend(i.getRightBound().get()); + } + } + boost::optional getLeftBound() const { return leftBound; } diff --git a/src/storage/ppg/ProgramGraph.cpp b/src/storage/ppg/ProgramGraph.cpp index 1b1388eda..ab094b273 100644 --- a/src/storage/ppg/ProgramGraph.cpp +++ b/src/storage/ppg/ProgramGraph.cpp @@ -67,11 +67,78 @@ namespace storm { return {true, pos}; } + + std::vector ProgramGraph::constantAssigned() const { + std::set contained; + for (auto const& act : deterministicActions) { + for (auto const& group : act.second) { + for (auto const& assignment : group) { + if (assignment.second.containsVariables()) { + contained.insert(assignment.first); + } + } + } + } + std::vector result; + for (auto const& varEntry : variables) { + if (contained.count(varEntry.second.getIndex()) == 0) { + // Currently we can only do this for integer assigned initials + if(initialValues.at(varEntry.second.getIndex()).containsVariables() || !varEntry.second.hasIntegerType()) { + continue; + } + result.push_back(varEntry.first); + } + } + return result; + } + + std::vector ProgramGraph::constants() const { + std::set contained; + for (auto const& act : deterministicActions) { + for (auto const& group : act.second) { + for (auto const& assignment : group) { + contained.insert(assignment.first); + } + } + } + for (auto const& act : probabilisticActions) { + contained.insert(act.second.getVariableIdentifier()); + } + std::vector result; + for (auto const& varEntry : variables) { + if (contained.count(varEntry.second.getIndex()) == 0) { + result.push_back(varEntry.first); + } + } + return result; + } + + storm::storage::IntegerInterval ProgramGraph::supportForConstAssignedVariable(ProgramVariableIdentifier i) const { + storm::storage::IntegerInterval support(initialValues.at(i).evaluateAsInt()); + for (auto const& act : deterministicActions) { + for (auto const& group : act.second) { + for (auto const& assignment : group) { + if (assignment.first == i) { + support.extend(assignment.second.evaluateAsInt()); + } + } + } + } + for (auto const& act : probabilisticActions) { + if(act.second.getVariableIdentifier() == i) { + support.extend(act.second.getSupportInterval()); + } + } + return support; + } + + std::vector ProgramGraph::rewardVariables() const { std::vector rewardCandidates = noeffectVariables(); std::vector result; for (auto const& var : rewardCandidates) { if(variables.at(var).hasIntegerType()) { + // TODO add some checks here; refine the evaluate as int stuff. if(initialValues.at(var).evaluateAsInt() == 0 && checkIfRewardVariableHelper(variables.at(var), this->deterministicActions).first) { result.push_back(var); diff --git a/src/storage/ppg/ProgramGraph.h b/src/storage/ppg/ProgramGraph.h index 99ab9a940..dc0c58ab6 100644 --- a/src/storage/ppg/ProgramGraph.h +++ b/src/storage/ppg/ProgramGraph.h @@ -209,6 +209,12 @@ namespace storm { std::vector rewardVariables() const; + std::vector constantAssigned() const; + + std::vector constants() const; + + storm::storage::IntegerInterval supportForConstAssignedVariable(ProgramVariableIdentifier i) const; + void checkValid() {