diff --git a/src/models/MarkovAutomaton.h b/src/models/MarkovAutomaton.h index f75f17560..5f1a3aeb9 100644 --- a/src/models/MarkovAutomaton.h +++ b/src/models/MarkovAutomaton.h @@ -187,14 +187,18 @@ namespace storm { virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const override { AbstractModel::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); + for (uint_fast64_t i = 0; i < this->getNondeterministicChoiceIndices().size(); ++i) { + std::cout << i << ": " << this->getNondeterministicChoiceIndices()[i] << " "; + } + // Write the probability distributions for all the states. - for (uint_fast64_t state = 0, highestStateIndex = this->getNumberOfStates() - 1; state <= highestStateIndex; ++state) { + for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { uint_fast64_t rowCount = this->getNondeterministicChoiceIndices()[state + 1] - this->getNondeterministicChoiceIndices()[state]; bool highlightChoice = true; // For this, we need to iterate over all available nondeterministic choices in the current state. for (uint_fast64_t choice = 0; choice < rowCount; ++choice) { - typename storm::storage::SparseMatrix::const_rows row = this->transitionMatrix.getRow(choice); + typename storm::storage::SparseMatrix::const_rows row = this->transitionMatrix.getRow(this->getNondeterministicChoiceIndices()[state] + choice); if (scheduler != nullptr) { // If the scheduler picked the current choice, we will not make it dotted, but highlight it. diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp index f2942f730..6f5ff617c 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -139,7 +139,7 @@ namespace storm { MarkovAutomatonSparseTransitionParser::ResultType MarkovAutomatonSparseTransitionParser::secondPass(char* buf, SupportedLineEndingsEnum lineEndings, FirstPassResult const& firstPassResult) { ResultType result(firstPassResult); - storm::storage::SparseMatrixBuilder matrixBuilder(firstPassResult.numberOfChoices, firstPassResult.highestStateIndex + 1, firstPassResult.numberOfNonzeroEntries); + storm::storage::SparseMatrixBuilder matrixBuilder(firstPassResult.numberOfChoices, firstPassResult.highestStateIndex + 1, firstPassResult.numberOfNonzeroEntries, true); bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks"); @@ -160,6 +160,7 @@ namespace storm { if (fixDeadlocks) { for (uint_fast64_t index = lastsource + 1; index < source; ++index) { result.nondeterministicChoiceIndices[index] = currentChoice; + matrixBuilder.newRowGroup(currentChoice); matrixBuilder.addNextValue(currentChoice, index, 1); ++currentChoice; } @@ -172,6 +173,7 @@ namespace storm { if (source != lastsource) { // If we skipped to a new state we need to record the beginning of the choices in the nondeterministic choice indices. result.nondeterministicChoiceIndices[source] = currentChoice; + matrixBuilder.newRowGroup(currentChoice); } // Record that the current source was the last source. diff --git a/src/solver/GurobiLpSolver.cpp b/src/solver/GurobiLpSolver.cpp index 378a3e583..c06233942 100644 --- a/src/solver/GurobiLpSolver.cpp +++ b/src/solver/GurobiLpSolver.cpp @@ -61,14 +61,28 @@ namespace storm { } void GurobiLpSolver::setGurobiEnvironmentProperties() const { - // Enable the following line to only print the output of Gurobi if the debug flag is set. - int error = error = GRBsetintparam(env, "OutputFlag", storm::settings::Settings::getInstance()->isSet("debug") || storm::settings::Settings::getInstance()->isSet("gurobioutput") ? 1 : 0); + int error = 0; + + // Enable the following line to only print the output of Gurobi if the debug flag is set. + error = GRBsetintparam(env, "OutputFlag", storm::settings::Settings::getInstance()->isSet("debug") || storm::settings::Settings::getInstance()->isSet("gurobioutput") ? 1 : 0); + if (error) { + LOG4CPLUS_ERROR(logger, "Unable to set Gurobi Parameter OutputFlag (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + throw storm::exceptions::InvalidStateException() << "Unable to set Gurobi Parameter OutputFlag (" << GRBgeterrormsg(env) << ", error code " << error << ")."; + } // Enable the following line to restrict Gurobi to one thread only. error = GRBsetintparam(env, "Threads", storm::settings::Settings::getInstance()->getOptionByLongName("gurobithreads").getArgument(0).getValueAsUnsignedInteger()); - + if (error) { + LOG4CPLUS_ERROR(logger, "Unable to set Gurobi Parameter Threads (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + throw storm::exceptions::InvalidStateException() << "Unable to set Gurobi Parameter Threads (" << GRBgeterrormsg(env) << ", error code " << error << ")."; + } + // Enable the following line to force Gurobi to be as precise about the binary variables as required by the given precision option. error = GRBsetdblparam(env, "IntFeasTol", storm::settings::Settings::getInstance()->getOptionByLongName("gurobiinttol").getArgument(0).getValueAsDouble()); + if (error) { + LOG4CPLUS_ERROR(logger, "Unable to set Gurobi Parameter IntFeasTol (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + throw storm::exceptions::InvalidStateException() << "Unable to set Gurobi Parameter IntFeasTol (" << GRBgeterrormsg(env) << ", error code " << error << ")."; + } } void GurobiLpSolver::update() const { diff --git a/test/functional/solver/GurobiLpSolverTest.cpp b/test/functional/solver/GurobiLpSolverTest.cpp index 508c0882c..1ca524d8e 100644 --- a/test/functional/solver/GurobiLpSolverTest.cpp +++ b/test/functional/solver/GurobiLpSolverTest.cpp @@ -14,7 +14,9 @@ TEST(GurobiLpSolver, LPOptimizeMax) { ASSERT_NO_THROW(yIndex = solver.createContinuousVariable("y", storm::solver::LpSolver::VariableType::LOWER_BOUND, 0, 0, 2)); uint_fast64_t zIndex; ASSERT_NO_THROW(zIndex = solver.createContinuousVariable("z", storm::solver::LpSolver::VariableType::LOWER_BOUND, 0, 0, 1)); - + + ASSERT_NO_THROW(solver.update()); + ASSERT_NO_THROW(solver.addConstraint("", {xIndex, yIndex, zIndex}, {1, 1, 1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 12)); ASSERT_NO_THROW(solver.addConstraint("", {yIndex, zIndex, xIndex}, {0.5, 1, -1}, storm::solver::LpSolver::BoundType::EQUAL, 5)); ASSERT_NO_THROW(solver.addConstraint("", {yIndex, xIndex}, {1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 5.5)); @@ -50,6 +52,8 @@ TEST(GurobiLpSolver, LPOptimizeMin) { uint_fast64_t zIndex; ASSERT_NO_THROW(zIndex = solver.createContinuousVariable("z", storm::solver::LpSolver::VariableType::BOUNDED, 1, 5.7, -1)); + ASSERT_NO_THROW(solver.update()); + ASSERT_NO_THROW(solver.addConstraint("", {xIndex, yIndex, zIndex}, {1, 1, 1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 12)); ASSERT_NO_THROW(solver.addConstraint("", {yIndex, zIndex, xIndex}, {0.5, 1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 5)); ASSERT_NO_THROW(solver.addConstraint("", {yIndex, xIndex}, {1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 5.5)); @@ -85,6 +89,8 @@ TEST(GurobiLpSolver, MILPOptimizeMax) { uint_fast64_t zIndex; ASSERT_NO_THROW(zIndex = solver.createContinuousVariable("z", storm::solver::LpSolver::VariableType::LOWER_BOUND, 0, 0, 1)); + ASSERT_NO_THROW(solver.update()); + ASSERT_NO_THROW(solver.addConstraint("", {xIndex, yIndex, zIndex}, {1, 1, 1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 12)); ASSERT_NO_THROW(solver.addConstraint("", {yIndex, zIndex, xIndex}, {0.5, 1, -1}, storm::solver::LpSolver::BoundType::EQUAL, 5)); ASSERT_NO_THROW(solver.addConstraint("", {yIndex, xIndex}, {1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 5.5)); @@ -120,6 +126,8 @@ TEST(GurobiLpSolver, MILPOptimizeMin) { uint_fast64_t zIndex; ASSERT_NO_THROW(zIndex = solver.createIntegerVariable("z", storm::solver::LpSolver::VariableType::BOUNDED, 0, 5.7, -1)); + ASSERT_NO_THROW(solver.update()); + ASSERT_NO_THROW(solver.addConstraint("", {xIndex, yIndex, zIndex}, {1, 1, 1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 12)); ASSERT_NO_THROW(solver.addConstraint("", {yIndex, zIndex, xIndex}, {0.5, 1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 5)); ASSERT_NO_THROW(solver.addConstraint("", {yIndex, xIndex}, {1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 5.5)); @@ -155,6 +163,8 @@ TEST(GurobiLpSolver, LPInfeasible) { uint_fast64_t zIndex; ASSERT_NO_THROW(zIndex = solver.createContinuousVariable("z", storm::solver::LpSolver::VariableType::LOWER_BOUND, 0, 0, 1)); + ASSERT_NO_THROW(solver.update()); + ASSERT_NO_THROW(solver.addConstraint("", {xIndex, yIndex, zIndex}, {1, 1, 1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 12)); ASSERT_NO_THROW(solver.addConstraint("", {yIndex, zIndex, xIndex}, {0.5, 1, -1}, storm::solver::LpSolver::BoundType::EQUAL, 5)); ASSERT_NO_THROW(solver.addConstraint("", {yIndex, xIndex}, {1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 5.5)); @@ -187,6 +197,8 @@ TEST(GurobiLpSolver, MILPInfeasible) { uint_fast64_t zIndex; ASSERT_NO_THROW(zIndex = solver.createContinuousVariable("z", storm::solver::LpSolver::VariableType::LOWER_BOUND, 0, 0, 1)); + ASSERT_NO_THROW(solver.update()); + ASSERT_NO_THROW(solver.addConstraint("", {xIndex, yIndex, zIndex}, {1, 1, 1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 12)); ASSERT_NO_THROW(solver.addConstraint("", {yIndex, zIndex, xIndex}, {0.5, 1, -1}, storm::solver::LpSolver::BoundType::EQUAL, 5)); ASSERT_NO_THROW(solver.addConstraint("", {yIndex, xIndex}, {1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 5.5)); @@ -219,6 +231,8 @@ TEST(GurobiLpSolver, LPUnbounded) { uint_fast64_t zIndex; ASSERT_NO_THROW(zIndex = solver.createContinuousVariable("z", storm::solver::LpSolver::VariableType::LOWER_BOUND, 0, 0, 1)); + ASSERT_NO_THROW(solver.update()); + ASSERT_NO_THROW(solver.addConstraint("", {xIndex, yIndex, zIndex}, {1, 1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 12)); ASSERT_NO_THROW(solver.addConstraint("", {yIndex, xIndex}, {1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 5.5)); @@ -249,6 +263,8 @@ TEST(GurobiLpSolver, MILPUnbounded) { uint_fast64_t zIndex; ASSERT_NO_THROW(zIndex = solver.createContinuousVariable("z", storm::solver::LpSolver::VariableType::LOWER_BOUND, 0, 0, 1)); + ASSERT_NO_THROW(solver.update()); + ASSERT_NO_THROW(solver.addConstraint("", {xIndex, yIndex, zIndex}, {1, 1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 12)); ASSERT_NO_THROW(solver.addConstraint("", {yIndex, xIndex}, {1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 5.5)); diff --git a/test/functional/storage/MaximalEndComponentDecompositionTest.cpp b/test/functional/storage/MaximalEndComponentDecompositionTest.cpp index cacb33843..76f0cd125 100644 --- a/test/functional/storage/MaximalEndComponentDecompositionTest.cpp +++ b/test/functional/storage/MaximalEndComponentDecompositionTest.cpp @@ -75,7 +75,7 @@ TEST(MaximalEndComponentDecomposition, FullSystem2) { storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny2.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny2.lab", "", ""); std::shared_ptr> markovAutomaton = parser.getModel>(); - + storm::storage::MaximalEndComponentDecomposition mecDecomposition; ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition(*markovAutomaton));