Browse Source

some adjustments to pgcl treatment caused by changes in JANI data structures

tempestpy_adaptions
dehnert 8 years ago
parent
commit
9bb65389c4
  1. 4
      src/storm-pgcl-cli/storm-pgcl.cpp
  2. 53
      src/storm-pgcl/builder/JaniProgramGraphBuilder.cpp
  3. 8
      src/storm-pgcl/builder/JaniProgramGraphBuilder.h
  4. 5
      src/storm/abstraction/MenuGameRefiner.cpp
  5. 4
      src/storm/storage/jani/OrderedAssignments.cpp
  6. 5
      src/storm/storage/jani/OrderedAssignments.h
  7. 2
      src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp

4
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::modules::GeneralSettings>();
storm::settings::addModule<storm::settings::modules::ResourceSettings>();
storm::settings::addModule<storm::settings::modules::PGCLSettings>();
storm::settings::addModule<storm::settings::modules::CoreSettings>();
storm::settings::addModule<storm::settings::modules::DebugSettings>();
@ -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<storm::settings::modules::PGCLSettings>().isProgramVariableRestrictionSet()) {
// TODO More fine grained control
storm::storage::IntegerInterval restr = storm::storage::parseIntegerInterval(storm::settings::getModule<storm::settings::modules::PGCLSettings>().getProgramVariableRestrictions());

53
src/storm-pgcl/builder/JaniProgramGraphBuilder.cpp

@ -63,23 +63,24 @@ namespace storm {
return storm::jani::OrderedAssignments(vec);
}
std::vector<storm::jani::EdgeDestination> JaniProgramGraphBuilder::buildProbabilisticDestinations(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge ) {
std::vector<std::pair<uint64_t, storm::expressions::Expression>> JaniProgramGraphBuilder::buildProbabilisticDestinations(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge, storm::jani::TemplateEdge& templateEdge) {
storm::ppg::ProbabilisticProgramAction const& act = static_cast<storm::ppg::ProbabilisticProgramAction const&>(edge.getAction());
std::vector<storm::jani::EdgeDestination> 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<std::pair<uint64_t, storm::expressions::Expression>> 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<storm::jani::EdgeDestination> JaniProgramGraphBuilder::buildDestinations(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge ) {
std::vector<std::pair<uint64_t, storm::expressions::Expression>> 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<storm::ppg::DeterministicProgramAction const&>(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<std::vector<storm::jani::Edge>, storm::expressions::Expression> JaniProgramGraphBuilder::addVariableChecks(storm::ppg::ProgramEdge const& edge) {
std::pair<std::vector<storm::jani::Edge>, storm::expressions::Expression> JaniProgramGraphBuilder::addVariableChecks(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge) {
std::vector<storm::jani::Edge> 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<storm::jani::TemplateEdge> 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<storm::jani::TemplateEdge> 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<std::vector<storm::jani::Edge>, storm::expressions::Expression> checks = addVariableChecks(*edge);
std::pair<std::vector<storm::jani::Edge>, 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<storm::jani::TemplateEdge> templateEdge = automaton.createTemplateEdge(simplifyExpression(edge->getCondition() && checks.second));
std::vector<std::pair<uint64_t, storm::expressions::Expression>> 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<storm::jani::EdgeDestination> destinations;
std::shared_ptr<storm::jani::TemplateEdge> templateEdge = automaton.createTemplateEdge(expManager->boolean(true));
std::vector<storm::expressions::Expression> destinationProbabilities;
std::vector<uint64_t> 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);
}
}

8
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<storm::jani::EdgeDestination> buildDestinations(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge );
std::vector<std::pair<uint64_t, storm::expressions::Expression>> buildDestinations(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge, storm::jani::TemplateEdge& templateEdge);
/**
* Helper for probabilistic assignments
*/
std::vector<storm::jani::EdgeDestination> buildProbabilisticDestinations(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge );
std::vector<std::pair<uint64_t, storm::expressions::Expression>> buildProbabilisticDestinations(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge, storm::jani::TemplateEdge& templateEdge);
std::pair<std::vector<storm::jani::Edge>, storm::expressions::Expression> addVariableChecks(storm::ppg::ProgramEdge const& edge);
std::pair<std::vector<storm::jani::Edge>, 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);

5
src/storm/abstraction/MenuGameRefiner.cpp

@ -64,7 +64,10 @@ namespace storm {
std::pair<uint64_t, uint64_t> 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)));

4
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();
}

5
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.

2
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"

Loading…
Cancel
Save