sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Several fixes. MinimalLabelSetGenerator can now treat labeled values. 

Former-commit-id: 0fc3d8ead3
tempestpy_adaptions
dehnert 11 years ago
parent
a99bdf1b17
commit
129fd296d6
7 changed files with 13 additions and 12 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 10
      src/counterexamples/MinimalLabelSetGenerator.h
  2. 3
      src/ir/Command.cpp
  3. 2
      src/ir/Command.h
  4. 2
      src/ir/Update.cpp
  5. 2
      src/ir/Update.h
  6. 2
      src/models/AbstractModel.h
  7. 4
      src/storm.cpp

10
src/counterexamples/MinimalLabelSetGenerator.h
View File

@ -120,7 +120,7 @@ namespace storm {
ChoiceInformation result;
storm::storage::SparseMatrix<T> const& transitionMatrix = labeledMdp.getTransitionMatrix();
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = labeledMdp.getNondeterministicChoiceIndices();
std::vector<std::list<uint_fast64_t>> const& choiceLabeling = labeledMdp.getChoiceLabeling();
std::vector<std::set<uint_fast64_t>> const& choiceLabeling = labeledMdp.getChoiceLabeling();
// Now traverse all choices of all relevant states and check whether there is a relevant target state.
// If so, the associated labels become relevant. Also, if a choice of relevant state has at least one
@ -489,7 +489,7 @@ namespace storm {
* @param probabilityThreshold The probability that the subsystem must exceed.
* @return The total number of constraints that were created.
*/
static uint_fast64_t assertProbabilityGreaterThanThreshold(GRBenv* env, GRBmodel* model, storm::models::Mdp<T> const& labeledMdp, VariableInformation const& variableInformation, T probabilityThreshold) {
static uint_fast64_t assertProbabilityGreaterThanThreshold(GRBenv* env, GRBmodel* model, storm::models::Mdp<T> const& labeledMdp, VariableInformation const& variableInformation, double probabilityThreshold) {
uint_fast64_t numberOfConstraintsCreated = 0;
int error = 0;
storm::storage::BitVector const& initialStates = labeledMdp.getInitialStates();
@ -555,7 +555,7 @@ namespace storm {
static uint_fast64_t assertChoicesImplyLabels(GRBenv* env, GRBmodel* model, storm::models::Mdp<T> const& labeledMdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) {
uint_fast64_t numberOfConstraintsCreated = 0;
int error = 0;
std::vector<std::list<uint_fast64_t>> const& choiceLabeling = labeledMdp.getChoiceLabeling();
std::vector<std::set<uint_fast64_t>> const& choiceLabeling = labeledMdp.getChoiceLabeling();
for (auto state : stateInformation.relevantStates) {
std::list<uint_fast64_t>::const_iterator choiceVariableIndicesIterator = variableInformation.stateToChoiceVariablesIndexMap.at(state).begin();
for (auto choice : choiceInformation.relevantChoicesForRelevantStates.at(state)) {
@ -916,7 +916,7 @@ namespace storm {
* @param includeSchedulerCuts If set to true, additional constraints are asserted that reduce the set of
* possible choices.
*/
static void buildConstraintSystem(GRBenv* env, GRBmodel* model, storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation, T probabilityThreshold, bool includeSchedulerCuts = false) {
static void buildConstraintSystem(GRBenv* env, GRBmodel* model, storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation, double probabilityThreshold, bool includeSchedulerCuts = false) {
// Assert that the reachability probability in the subsystem exceeds the given threshold.
uint_fast64_t numberOfConstraints = assertProbabilityGreaterThanThreshold(env, model, labeledMdp, variableInformation, probabilityThreshold);
@ -1054,7 +1054,7 @@ namespace storm {
public:
static std::unordered_set<uint_fast64_t> getMinimalLabelSet(storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, T probabilityThreshold, bool checkThresholdFeasible = false, bool includeSchedulerCuts = false) {
static std::unordered_set<uint_fast64_t> getMinimalLabelSet(storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool checkThresholdFeasible = false, bool includeSchedulerCuts = false) {
#ifdef STORM_HAVE_GUROBI
// (0) Check whether the MDP is indeed labeled.
if (!labeledMdp.hasChoiceLabels()) {

3
src/ir/Command.cpp
View File

@ -23,7 +23,7 @@ namespace storm {
// Nothing to do here.
}
Command::Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState)
Command::Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState& variableState)
: actionName(oldCommand.getActionName()), guardExpression(oldCommand.guardExpression->clone(renaming, variableState)), globalIndex(newGlobalIndex) {
auto renamingPair = renaming.find(this->actionName);
if (renamingPair != renaming.end()) {
@ -32,6 +32,7 @@ namespace storm {
this->updates.reserve(oldCommand.getNumberOfUpdates());
for (Update const& update : oldCommand.updates) {
this->updates.emplace_back(update, variableState.getNextGlobalUpdateIndex(), renaming, variableState);
variableState.nextGlobalUpdateIndex++;
}
}

2
src/ir/Command.h
View File

@ -54,7 +54,7 @@ namespace storm {
* replaced with.
* @param variableState An object knowing about the variables in the system.
*/
Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState);
Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState& variableState);
/*!
* Retrieves the action name of this command.

2
src/ir/Update.cpp
View File

@ -23,7 +23,7 @@ namespace storm {
// Nothing to do here.
}
Update::Update(Update const& update, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) : globalIndex(newGlobalIndex) {
Update::Update(Update const& update, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState& variableState) : globalIndex(newGlobalIndex) {
for (auto const& variableAssignmentPair : update.booleanAssignments) {
if (renaming.count(variableAssignmentPair.first) > 0) {
this->booleanAssignments[renaming.at(variableAssignmentPair.first)] = Assignment(variableAssignmentPair.second, renaming, variableState);

2
src/ir/Update.h
View File

@ -53,7 +53,7 @@ namespace storm {
* replaced with.
* @param variableState An object knowing about the variables in the system.
*/
Update(Update const& update, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState);
Update(Update const& update, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState& variableState);
/*!
* Retrieves the expression for the likelihood of this update.

2
src/models/AbstractModel.h
View File

@ -212,7 +212,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
std::vector<uint_fast64_t> rowIndications(numberOfStates + 1);
std::vector<uint_fast64_t> columnIndications(numberOfTransitions);
std::vector<TransitionType> values(numberOfTransitions, selectionFunction(0));
std::vector<TransitionType> values(numberOfTransitions, TransitionType());
// First, we need to count how many backward transitions each state has.
for (uint_fast64_t i = 0; i < numberOfStates; ++i) {

4
src/storm.cpp
View File

@ -337,11 +337,11 @@ int main(const int argc, const char* argv[]) {
// Enable the following lines to test the MinimalLabelSetGenerator.
// if (model->getType() == storm::models::MDP) {
// std::shared_ptr<storm::models::Mdp<double>> labeledMdp = model->as<storm::models::Mdp<double>>();
// std::shared_ptr<storm::models::Mdp<storm::storage::LabeledValues<double>>> labeledMdp = model->as<storm::models::Mdp<storm::storage::LabeledValues<double>>>();
// storm::storage::BitVector const& finishedStates = labeledMdp->getLabeledStates("finished");
// storm::storage::BitVector const& allCoinsEqual1States = labeledMdp->getLabeledStates("all_coins_equal_1");
// storm::storage::BitVector targetStates = finishedStates & allCoinsEqual1States;
// storm::counterexamples::MinimalLabelSetGenerator<double>::getMinimalLabelSet(*labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.3, true, true);
// storm::counterexamples::MinimalLabelSetGenerator<storm::storage::LabeledValues<double>>::getMinimalLabelSet(*labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.3, true, true);
// }
}

Write Preview
Loading…
Cancel
Save