diff --git a/src/counterexamples/MinimalLabelSetGenerator.h b/src/counterexamples/MinimalLabelSetGenerator.h index d6f33b71d..89d53d874 100644 --- a/src/counterexamples/MinimalLabelSetGenerator.h +++ b/src/counterexamples/MinimalLabelSetGenerator.h @@ -120,7 +120,7 @@ namespace storm { ChoiceInformation result; storm::storage::SparseMatrix const& transitionMatrix = labeledMdp.getTransitionMatrix(); std::vector const& nondeterministicChoiceIndices = labeledMdp.getNondeterministicChoiceIndices(); - std::vector> const& choiceLabeling = labeledMdp.getChoiceLabeling(); + std::vector> 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 const& labeledMdp, VariableInformation const& variableInformation, T probabilityThreshold) { + static uint_fast64_t assertProbabilityGreaterThanThreshold(GRBenv* env, GRBmodel* model, storm::models::Mdp 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 const& labeledMdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { uint_fast64_t numberOfConstraintsCreated = 0; int error = 0; - std::vector> const& choiceLabeling = labeledMdp.getChoiceLabeling(); + std::vector> const& choiceLabeling = labeledMdp.getChoiceLabeling(); for (auto state : stateInformation.relevantStates) { std::list::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 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 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 getMinimalLabelSet(storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, T probabilityThreshold, bool checkThresholdFeasible = false, bool includeSchedulerCuts = false) { + static std::unordered_set getMinimalLabelSet(storm::models::Mdp 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()) { diff --git a/src/ir/Command.cpp b/src/ir/Command.cpp index 80e698b64..570789480 100644 --- a/src/ir/Command.cpp +++ b/src/ir/Command.cpp @@ -23,7 +23,7 @@ namespace storm { // Nothing to do here. } - Command::Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map const& renaming, storm::parser::prism::VariableState const& variableState) + Command::Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map 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++; } } diff --git a/src/ir/Command.h b/src/ir/Command.h index 4682ccda2..67a431949 100644 --- a/src/ir/Command.h +++ b/src/ir/Command.h @@ -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 const& renaming, storm::parser::prism::VariableState const& variableState); + Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map const& renaming, storm::parser::prism::VariableState& variableState); /*! * Retrieves the action name of this command. diff --git a/src/ir/Update.cpp b/src/ir/Update.cpp index cade7f022..08728bd4c 100644 --- a/src/ir/Update.cpp +++ b/src/ir/Update.cpp @@ -23,7 +23,7 @@ namespace storm { // Nothing to do here. } - Update::Update(Update const& update, uint_fast64_t newGlobalIndex, std::map const& renaming, storm::parser::prism::VariableState const& variableState) : globalIndex(newGlobalIndex) { + Update::Update(Update const& update, uint_fast64_t newGlobalIndex, std::map 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); diff --git a/src/ir/Update.h b/src/ir/Update.h index df7d4a258..88bdd4c16 100644 --- a/src/ir/Update.h +++ b/src/ir/Update.h @@ -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 const& renaming, storm::parser::prism::VariableState const& variableState); + Update(Update const& update, uint_fast64_t newGlobalIndex, std::map const& renaming, storm::parser::prism::VariableState& variableState); /*! * Retrieves the expression for the likelihood of this update. diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index 5a67c3e98..f32cb3ad4 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -212,7 +212,7 @@ class AbstractModel: public std::enable_shared_from_this> { std::vector rowIndications(numberOfStates + 1); std::vector columnIndications(numberOfTransitions); - std::vector values(numberOfTransitions, selectionFunction(0)); + std::vector values(numberOfTransitions, TransitionType()); // First, we need to count how many backward transitions each state has. for (uint_fast64_t i = 0; i < numberOfStates; ++i) { diff --git a/src/storm.cpp b/src/storm.cpp index 69072ba12..19ec8baee 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -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> labeledMdp = model->as>(); +// std::shared_ptr>> labeledMdp = model->as>>(); // 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::getMinimalLabelSet(*labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.3, true, true); +// storm::counterexamples::MinimalLabelSetGenerator>::getMinimalLabelSet(*labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.3, true, true); // } }