Browse Source

remove output, copy observability when modules are used

tempestpy_adaptions
Sebastian Junges 7 years ago
parent
commit
6ab286f420
  1. 2
      src/storm/generator/NextStateGenerator.cpp
  2. 4
      src/storm/parser/PrismParser.cpp

2
src/storm/generator/NextStateGenerator.cpp

@ -158,9 +158,7 @@ namespace storm {
uint32_t NextStateGenerator<ValueType, StateType>::observabilityClass(CompressedState const &state) const {
if (this->mask.size() == 0) {
this->mask = computeObservabilityMask(variableInformation);
std::cout << mask.size() << std::endl;
}
std::cout << state.size() << std::endl;
return unpackStateToObservabilityClass(state, observabilityMap, mask);
}

4
src/storm/parser/PrismParser.cpp

@ -631,7 +631,7 @@ namespace storm {
for (auto const& variable : moduleToRename.getBooleanVariables()) {
auto const& renamingPair = renaming.find(variable.getName());
STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Boolean variable '" << variable.getName() << " was not renamed.");
bool observable = false; // TODO
bool observable = variable.isObservable();
booleanVariables.push_back(storm::prism::BooleanVariable(manager->getVariable(renamingPair->second), variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(), observable, this->getFilename(), get_line(qi::_1)));
}
@ -640,7 +640,7 @@ namespace storm {
for (auto const& variable : moduleToRename.getIntegerVariables()) {
auto const& renamingPair = renaming.find(variable.getName());
STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Integer variable '" << variable.getName() << " was not renamed.");
bool observable = false; // TODO
bool observable = variable.isObservable();
integerVariables.push_back(storm::prism::IntegerVariable(manager->getVariable(renamingPair->second), variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(), observable, this->getFilename(), get_line(qi::_1)));
}

Loading…
Cancel
Save