diff --git a/src/counterexamples/MinimalLabelSetGenerator.h b/src/counterexamples/MinimalLabelSetGenerator.h index 6ba3cff90..d6f33b71d 100644 --- a/src/counterexamples/MinimalLabelSetGenerator.h +++ b/src/counterexamples/MinimalLabelSetGenerator.h @@ -339,7 +339,7 @@ namespace storm { variableNameBuffer.str(""); variableNameBuffer.clear(); variableNameBuffer << "p" << state; - error = GRBaddvar(model, 0, nullptr, nullptr, maximizeProbability ? (labeledMdp.getLabeledStates("init").get(state) ? -0.5 : 0) : 0, 0.0, 1.0, GRB_CONTINUOUS, variableNameBuffer.str().c_str()); + error = GRBaddvar(model, 0, nullptr, nullptr, maximizeProbability ? (labeledMdp.getInitialStates().get(state) ? -0.5 : 0) : 0, 0.0, 1.0, GRB_CONTINUOUS, variableNameBuffer.str().c_str()); if (error) { LOG4CPLUS_ERROR(logger, "Could not create Gurobi variable (" << GRBgeterrormsg(env) << ")."); throw storm::exceptions::InvalidStateException() << "Could not create Gurobi variable (" << GRBgeterrormsg(env) << ")."; @@ -492,7 +492,7 @@ namespace storm { static uint_fast64_t assertProbabilityGreaterThanThreshold(GRBenv* env, GRBmodel* model, storm::models::Mdp const& labeledMdp, VariableInformation const& variableInformation, T probabilityThreshold) { uint_fast64_t numberOfConstraintsCreated = 0; int error = 0; - storm::storage::BitVector const& initialStates = labeledMdp.getLabeledStates("init"); + storm::storage::BitVector const& initialStates = labeledMdp.getInitialStates(); if (initialStates.getNumberOfSetBits() != 1) { LOG4CPLUS_ERROR(logger, "Must have exactly one initial state, but got " << initialStates.getNumberOfSetBits() << "instead."); throw storm::exceptions::InvalidStateException() << "Must have exactly one initial state, but got " << initialStates.getNumberOfSetBits() << "instead."; @@ -792,7 +792,7 @@ namespace storm { // For all states except for the initial state, assert that there is a selected incoming transition // in the subsystem if there is one selected action in the current state. - if (!labeledMdp.getLabeledStates("init").get(state)) { + if (!labeledMdp.getInitialStates().get(state)) { std::vector variables; std::vector coefficients; @@ -1035,7 +1035,7 @@ namespace storm { // Check whether the model was optimized, so we can read off the solution. if (checkGurobiModelIsOptimized(env, model)) { double reachabilityProbability = 0; - storm::storage::BitVector const& initialStates = labeledMdp.getLabeledStates("init"); + storm::storage::BitVector const& initialStates = labeledMdp.getInitialStates(); for (auto initialState : initialStates) { error = GRBgetdblattrelement(model, GRB_DBL_ATTR_X, variableInformation.stateToProbabilityVariableIndexMap.at(initialState), &reachabilityProbability); if (error) { diff --git a/src/modelchecker/csl/AbstractModelChecker.h b/src/modelchecker/csl/AbstractModelChecker.h index 67c9e512f..7a839bb4f 100644 --- a/src/modelchecker/csl/AbstractModelChecker.h +++ b/src/modelchecker/csl/AbstractModelChecker.h @@ -130,22 +130,18 @@ public: std::cout << std::endl; LOG4CPLUS_INFO(logger, "Model checking formula\t" << stateFormula.toString()); std::cout << "Model checking formula:\t" << stateFormula.toString() << std::endl; - storm::storage::BitVector* result = nullptr; + storm::storage::BitVector result; try { result = stateFormula.check(*this); LOG4CPLUS_INFO(logger, "Result for initial states:"); std::cout << "Result for initial states:" << std::endl; - for (auto initialState : model.getLabeledStates("init")) { - LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result->get(initialState) ? "satisfied" : "not satisfied")); - std::cout << "\t" << initialState << ": " << result->get(initialState) << std::endl; + for (auto initialState : model.getInitialStates()) { + LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result.get(initialState) ? "satisfied" : "not satisfied")); + std::cout << "\t" << initialState << ": " << result.get(initialState) << std::endl; } - delete result; } catch (std::exception& e) { std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl; LOG4CPLUS_ERROR(logger, "Error during computation: " << e.what() << "Skipping property."); - if (result != nullptr) { - delete result; - } } std::cout << std::endl << "-------------------------------------------" << std::endl; } @@ -160,21 +156,17 @@ public: std::cout << std::endl; LOG4CPLUS_INFO(logger, "Model checking formula\t" << noBoundFormula.toString()); std::cout << "Model checking formula:\t" << noBoundFormula.toString() << std::endl; - std::vector* result = nullptr; + std::vector result; try { result = this->checkNoBoundOperator(noBoundFormula); LOG4CPLUS_INFO(logger, "Result for initial states:"); std::cout << "Result for initial states:" << std::endl; - for (auto initialState : model.getLabeledStates("init")) { + for (auto initialState : model.getInitialStates()) { LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (*result)[initialState]); std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl; } - delete result; } catch (std::exception& e) { std::cout << "Error during computation: " << e.what() << " Skipping property." << std::endl; - if (result != nullptr) { - delete result; - } } std::cout << std::endl << "-------------------------------------------" << std::endl; } diff --git a/src/modelchecker/ltl/AbstractModelChecker.h b/src/modelchecker/ltl/AbstractModelChecker.h index 9a0459181..8cc06cdbd 100644 --- a/src/modelchecker/ltl/AbstractModelChecker.h +++ b/src/modelchecker/ltl/AbstractModelChecker.h @@ -114,22 +114,18 @@ public: std::cout << std::endl; LOG4CPLUS_INFO(logger, "Model checking formula\t" << ltlFormula.toString()); std::cout << "Model checking formula:\t" << ltlFormula.toString() << std::endl; - storm::storage::BitVector* result = nullptr; + storm::storage::BitVector result; try { result = ltlFormula.check(*this); LOG4CPLUS_INFO(logger, "Result for initial states:"); std::cout << "Result for initial states:" << std::endl; - for (auto initialState : model.getLabeledStates("init")) { - LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result->get(initialState) ? "satisfied" : "not satisfied")); - std::cout << "\t" << initialState << ": " << result->get(initialState) << std::endl; + for (auto initialState : model.getInitialStates()) { + LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result.get(initialState) ? "satisfied" : "not satisfied")); + std::cout << "\t" << initialState << ": " << result.get(initialState) << std::endl; } - delete result; } catch (std::exception& e) { std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl; LOG4CPLUS_ERROR(logger, "Error during computation: " << e.what() << "Skipping property."); - if (result != nullptr) { - delete result; - } } std::cout << std::endl << "-------------------------------------------" << std::endl; } diff --git a/src/modelchecker/prctl/AbstractModelChecker.h b/src/modelchecker/prctl/AbstractModelChecker.h index 2c1287d35..f9245b93d 100644 --- a/src/modelchecker/prctl/AbstractModelChecker.h +++ b/src/modelchecker/prctl/AbstractModelChecker.h @@ -120,15 +120,6 @@ public: } } - /*! - * Retrieves the initial states of the model. - * - * @return A bit vector that represents the initial states of the model. - */ - storm::storage::BitVector const& getInitialStates() const { - return model.getLabeledStates("init"); - } - /*! * Checks the given abstract prctl formula on the model and prints the result (depending on the actual type of the formula) * for all initial states, i.e. states that carry the atomic proposition "init". @@ -158,7 +149,7 @@ public: result = stateFormula.check(*this); LOG4CPLUS_INFO(logger, "Result for initial states:"); std::cout << "Result for initial states:" << std::endl; - for (auto initialState : this->getInitialStates()) { + for (auto initialState : model.getInitialStates()) { LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result.get(initialState) ? "satisfied" : "not satisfied")); std::cout << "\t" << initialState << ": " << result.get(initialState) << std::endl; } @@ -184,7 +175,7 @@ public: result = this->checkNoBoundOperator(noBoundFormula); LOG4CPLUS_INFO(logger, "Result for initial states:"); std::cout << "Result for initial states:" << std::endl; - for (auto initialState : this->getInitialStates()) { + for (auto initialState : model.getInitialStates()) { LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << result[initialState]); std::cout << "\t" << initialState << ": " << result[initialState] << std::endl; } diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 01e1eb8eb..03245000d 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -98,7 +98,7 @@ public: // Check if we already know the result (i.e. probability 0) for all initial states and // don't compute anything in this case. - if (this->getInitialStates().isDisjointFrom(statesWithProbabilityGreater0)) { + if (this->getModel().getInitialStates().isDisjointFrom(statesWithProbabilityGreater0)) { LOG4CPLUS_INFO(logger, "The probabilities for the initial states were determined in a preprocessing step." << " No exact probabilities were computed."); // Set the values for all maybe-states to 0.5 to indicate that their probability values are not 0 (and @@ -251,7 +251,7 @@ public: std::vector result(this->getModel().getNumberOfStates()); // Check whether we need to compute exact probabilities for some states. - if (this->getInitialStates().isDisjointFrom(maybeStates) || qualitative) { + if (this->getModel().getInitialStates().isDisjointFrom(maybeStates) || qualitative) { if (qualitative) { LOG4CPLUS_INFO(logger, "The formula was checked qualitatively. No exact probabilities were computed."); } else { @@ -409,7 +409,7 @@ public: std::vector result(this->getModel().getNumberOfStates()); // Check whether we need to compute exact rewards for some states. - if (this->getInitialStates().isDisjointFrom(maybeStates)) { + if (this->getModel().getInitialStates().isDisjointFrom(maybeStates)) { LOG4CPLUS_INFO(logger, "The rewards for the initial states were determined in a preprocessing step." << " No exact rewards were computed."); // Set the values for all maybe-states to 1 to indicate that their reward values diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index e6a4ff69c..f399c0e68 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -102,7 +102,7 @@ namespace storm { // Check if we already know the result (i.e. probability 0) for all initial states and // don't compute anything in this case. - if (this->getInitialStates().isDisjointFrom(statesWithProbabilityGreater0)) { + if (this->getModel().getInitialStates().isDisjointFrom(statesWithProbabilityGreater0)) { LOG4CPLUS_INFO(logger, "The probabilities for the initial states were determined in a preprocessing step." << " No exact probabilities were computed."); // Set the values for all maybe-states to 0.5 to indicate that their probability values are not 0 (and @@ -282,7 +282,7 @@ namespace storm { std::vector result(this->getModel().getNumberOfStates()); // Check whether we need to compute exact probabilities for some states. - if (this->getInitialStates().isDisjointFrom(maybeStates) || qualitative) { + if (this->getModel().getInitialStates().isDisjointFrom(maybeStates) || qualitative) { if (qualitative) { LOG4CPLUS_INFO(logger, "The formula was checked qualitatively. No exact probabilities were computed."); } else { @@ -466,7 +466,7 @@ namespace storm { std::vector result(this->getModel().getNumberOfStates()); // Check whether we need to compute exact rewards for some states. - if (this->getInitialStates().isDisjointFrom(maybeStates)) { + if (this->getModel().getInitialStates().isDisjointFrom(maybeStates)) { LOG4CPLUS_INFO(logger, "The rewards for the initial states were determined in a preprocessing step." << " No exact rewards were computed."); // Set the values for all maybe-states to 1 to indicate that their reward values