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

Allow more than 2 outgoing transitions

tempestpy_adaptions
Jip Spel 6 years ago
parent
7c19299488
commit
9d02519b01
2 changed files with 56 additions and 38 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. 7
      src/storm-pars/analysis/LatticeExtender.cpp
  2. 87
      src/storm-pars/analysis/MonotonicityChecker.cpp

7
src/storm-pars/analysis/LatticeExtender.cpp
View File

@ -67,8 +67,6 @@ namespace storm {
for (auto rowItr = row.begin(); rowItr != row.end(); ++rowItr) {
stateMap[i].set(rowItr->getColumn(), true);
}
// TODO: allow more than 2 transitions? or fix this in preprocessing?
STORM_LOG_THROW(stateMap[i].getNumberOfSetBits() <= 2, storm::exceptions::NotSupportedException, "Only two outgoing transitions per state allowed");
}
// Create the Lattice
@ -128,8 +126,7 @@ namespace storm {
if (check && successors.getNumberOfSetBits() == 1) {
// As there is only one successor the current state and its successor must be at the same nodes.
lattice->addToNode(stateNumber, lattice->getNode(successors.getNextSetIndex(0)));
} else if (check && successors.getNumberOfSetBits() > 1) {
// TODO: allow more than 2 transitions?
} else if (check && successors.getNumberOfSetBits() == 2) {
// Otherwise, check how the two states compare, and add if the comparison is possible.
uint_fast64_t successor1 = successors.getNextSetIndex(0);
uint_fast64_t successor2 = successors.getNextSetIndex(successor1 + 1);
@ -149,6 +146,8 @@ namespace storm {
} else {
return std::make_tuple(lattice, successor1, successor2);
}
} else if (check && successors.getNumberOfSetBits() > 2) {
// TODO
}
}
// Nothing changed and not done yet

87
src/storm-pars/analysis/MonotonicityChecker.cpp
View File

@ -21,21 +21,23 @@ namespace storm {
lattice->toDotFile(myfile);
myfile.close();
STORM_PRINT("Given assumptions: " << std::endl);
bool first = true;
for (auto itr = assumptions.begin(); itr != assumptions.end(); ++itr) {
if (!first) {
STORM_PRINT(" ^ ");
} else {
STORM_PRINT(" ");
if (assumptions.size() > 0) {
STORM_PRINT("Given assumptions: " << std::endl);
bool first = true;
for (auto itr = assumptions.begin(); itr != assumptions.end(); ++itr) {
if (!first) {
STORM_PRINT(" ^ ");
} else {
STORM_PRINT(" ");
}
first = false;
std::shared_ptr<storm::expressions::BinaryRelationExpression> expression = *itr;
auto var1 = expression->getFirstOperand();
auto var2 = expression->getSecondOperand();
STORM_PRINT("(" << var1->getIdentifier() << " > " << var2->getIdentifier() << ")");
}
first = false;
std::shared_ptr<storm::expressions::BinaryRelationExpression> expression = *itr;
auto var1 = expression->getFirstOperand();
auto var2 = expression->getSecondOperand();
STORM_PRINT("(" << var1->getIdentifier() << " > " << var2->getIdentifier() << ")");
STORM_PRINT(std::endl);
}
STORM_PRINT(std::endl);
std::map<carl::Variable, std::pair<bool, bool>> varsMonotone = analyseMonotonicity(i, lattice, matrix);
for (auto itr2 = varsMonotone.begin(); itr2 != varsMonotone.end(); ++itr2) {
@ -75,34 +77,49 @@ namespace storm {
auto first = (*row.begin());
if (first.getValue() != ValueType(1)) {
auto second = (*(++row.begin()));
std::map<uint_fast64_t, ValueType> transitions;
for (auto itr = row.begin(); itr != row.end(); ++itr) {
transitions.insert(std::pair<uint_fast64_t, ValueType>((*itr).getColumn(), (*itr).getValue()));
}
std::string color = "";
auto val = first.getValue();
auto vars = val.gatherVariables();
for (auto itr = vars.begin(); itr != vars.end(); ++itr) {
auto derivative = val.derivative(*itr);
STORM_LOG_THROW(derivative.isConstant(), storm::exceptions::NotSupportedException, "Expecting derivative to be constant");
if (varsMonotone.find(*itr) == varsMonotone.end()) {
varsMonotone[*itr].first = true;
varsMonotone[*itr].second = true;
}
auto compare = lattice->compare(first.getColumn(), second.getColumn());
std::pair<bool, bool>* value = &varsMonotone.find(*itr)->second;
std::pair<bool, bool> old = *value;
if (compare == storm::analysis::Lattice::ABOVE) {
value->first &=derivative.constantPart() >= 0;
value->second &=derivative.constantPart() <= 0;
} else if (compare == storm::analysis::Lattice::BELOW) {
value->first &=derivative.constantPart() <= 0;
value->second &=derivative.constantPart() >= 0;
} else if (compare == storm::analysis::Lattice::SAME) {
// Behaviour doesn't matter, as they are at the same level
} else {
value->first = false;
value->second = false;
for (auto itr2 = transitions.begin(); itr2 != transitions.end(); ++itr2) {
for (auto itr3 = transitions.begin(); itr3 != transitions.end(); ++itr3) {
// TODO improve
auto derivative2 = (*itr2).second.derivative(*itr);
auto derivative3 = (*itr3).second.derivative(*itr);
STORM_LOG_THROW(derivative2.isConstant() && derivative3.isConstant(), storm::exceptions::NotSupportedException, "Expecting derivative to be constant");
auto compare = lattice->compare((*itr2).first, (*itr3).first);
if (compare == storm::analysis::Lattice::ABOVE) {
value->first &=derivative2.constantPart() >= 0;
value->second &=derivative2.constantPart() <= 0;
} else if (compare == storm::analysis::Lattice::BELOW) {
value->first &=derivative3.constantPart() <= 0;
value->second &=derivative3.constantPart() >= 0;
} else if (compare == storm::analysis::Lattice::SAME) {
// Behaviour doesn't matter, as they are at the same level
} else {
value->first = false;
value->second = false;
}
}
}
if ((value->first != old.first) && (value->second != old.second)) {
color = "color = red, ";
} else if ((value->first != old.first)) {
@ -114,10 +131,12 @@ namespace storm {
}
}
myfile << "\t" << i << " -> " << first.getColumn() << "[" << color << "label=\"" << first.getValue() << "\"];"
<< std::endl;
myfile << "\t" << i << " -> " << second.getColumn() << "[" << color << "label=\"" << second.getValue() << "\"];"
<< std::endl;
for (auto itr = transitions.begin(); itr != transitions.end(); ++itr) {
myfile << "\t" << i << " -> " << itr->first << "[" << color << "label=\"" << itr->second << "\"];"
<< std::endl;
}
myfile << "\t edge[style=\"\"];" << std::endl;
} else {
myfile << "\t" << i << " -> " << first.getColumn() << "[label=\"" << first.getValue() << "\"];"

Write Preview
Loading…
Cancel
Save