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

Merged master and added correct row group creation to MarkovAutomaton parser. 

Former-commit-id: dcd9368634
tempestpy_adaptions
dehnert 11 years ago
parent
584a79f974 68a6e533be
commit
d092897247
5 changed files with 44 additions and 8 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. 8
      src/models/MarkovAutomaton.h
  2. 4
      src/parser/MarkovAutomatonSparseTransitionParser.cpp
  3. 20
      src/solver/GurobiLpSolver.cpp
  4. 18
      test/functional/solver/GurobiLpSolverTest.cpp
  5. 2
      test/functional/storage/MaximalEndComponentDecompositionTest.cpp

8
src/models/MarkovAutomaton.h
View File

@ -187,14 +187,18 @@ namespace storm {
virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector<T> const* firstValue = nullptr, std::vector<T> const* secondValue = nullptr, std::vector<uint_fast64_t> const* stateColoring = nullptr, std::vector<std::string> const* colors = nullptr, std::vector<uint_fast64_t>* scheduler = nullptr, bool finalizeOutput = true) const override {
AbstractModel<T>::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<T>::const_rows row = this->transitionMatrix.getRow(choice);
typename storm::storage::SparseMatrix<T>::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.

4
src/parser/MarkovAutomatonSparseTransitionParser.cpp
View File

@ -139,7 +139,7 @@ namespace storm {
MarkovAutomatonSparseTransitionParser::ResultType MarkovAutomatonSparseTransitionParser::secondPass(char* buf, SupportedLineEndingsEnum lineEndings, FirstPassResult const& firstPassResult) {
ResultType result(firstPassResult);
storm::storage::SparseMatrixBuilder<double> matrixBuilder(firstPassResult.numberOfChoices, firstPassResult.highestStateIndex + 1, firstPassResult.numberOfNonzeroEntries);
storm::storage::SparseMatrixBuilder<double> 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.

20
src/solver/GurobiLpSolver.cpp
View File

@ -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 {

18
test/functional/solver/GurobiLpSolverTest.cpp
View File

@ -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));

2
test/functional/storage/MaximalEndComponentDecompositionTest.cpp
View File

@ -75,7 +75,7 @@ TEST(MaximalEndComponentDecomposition, FullSystem2) {
storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny2.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny2.lab", "", "");
std::shared_ptr<storm::models::MarkovAutomaton<double>> markovAutomaton = parser.getModel<storm::models::MarkovAutomaton<double>>();
storm::storage::MaximalEndComponentDecomposition<double> mecDecomposition;
ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition<double>(*markovAutomaton));

Write Preview
Loading…
Cancel
Save