Browse Source

more intelligence in pgcl to jani

Former-commit-id: 92821aa541 [formerly 8436f9e0cc]
Former-commit-id: 5e202bda9a
main
sjunges 9 years ago
parent
commit
fd1a241921
  1. 8
      src/builder/JaniProgramGraphBuilder.cpp
  2. 55
      src/builder/JaniProgramGraphBuilder.h
  3. 23
      src/storage/IntegerInterval.h
  4. 67
      src/storage/ppg/ProgramGraph.cpp
  5. 6
      src/storage/ppg/ProgramGraph.h

8
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<storm::ppg::ProbabilisticProgramAction const&>(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});

55
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<std::vector<storm::jani::Edge>, 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<storm::ppg::ProgramVariableIdentifier> rewards;
/// Restrictions on variables
/// Variables that are constants
std::vector<storm::ppg::ProgramVariableIdentifier> constants;
/// Restrictions on variables (automatic)
std::map<uint64_t, storm::storage::IntegerInterval> variableRestrictions;
/// Restrictions on variables (provided by users)
std::map<uint64_t, storm::storage::IntegerInterval> userVariableRestrictions;
/// Locations for variables that would have gone ot o
std::map<uint64_t, uint64_t> varOutOfBoundsLocations;
std::map<storm::ppg::ProgramLocationIdentifier, uint64_t> janiLocId;

23
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<int64_t> getLeftBound() const {
return leftBound;
}

67
src/storage/ppg/ProgramGraph.cpp

@ -67,11 +67,78 @@ namespace storm {
return {true, pos};
}
std::vector<ProgramVariableIdentifier> ProgramGraph::constantAssigned() const {
std::set<ProgramVariableIdentifier> 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<ProgramVariableIdentifier> 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<ProgramVariableIdentifier> ProgramGraph::constants() const {
std::set<ProgramVariableIdentifier> 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<ProgramVariableIdentifier> 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<ProgramVariableIdentifier> ProgramGraph::rewardVariables() const {
std::vector<ProgramVariableIdentifier> rewardCandidates = noeffectVariables();
std::vector<ProgramVariableIdentifier> 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);

6
src/storage/ppg/ProgramGraph.h

@ -209,6 +209,12 @@ namespace storm {
std::vector<ProgramVariableIdentifier> rewardVariables() const;
std::vector<ProgramVariableIdentifier> constantAssigned() const;
std::vector<ProgramVariableIdentifier> constants() const;
storm::storage::IntegerInterval supportForConstAssignedVariable(ProgramVariableIdentifier i) const;
void checkValid() {

Loading…
Cancel
Save