Browse Source

add assertion for module indices in second

tempestpy_adaptions
Stefan Pranger 4 years ago
parent
commit
584fbf23c1
  1. 10
      src/storm-parsers/parser/PrismParser.cpp

10
src/storm-parsers/parser/PrismParser.cpp

@ -755,12 +755,16 @@ namespace storm {
this->observables.insert(observables.begin(), observables.end()); this->observables.insert(observables.begin(), observables.end());
// We need this list to be filled in both runs. // We need this list to be filled in both runs.
} }
storm::prism::Module PrismParser::createModule(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables, boost::optional<storm::expressions::Expression> const& invariant, std::vector<storm::prism::Command> const& commands, GlobalProgramInformation& globalProgramInformation) const { storm::prism::Module PrismParser::createModule(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables, boost::optional<storm::expressions::Expression> const& invariant, std::vector<storm::prism::Command> const& commands, GlobalProgramInformation& globalProgramInformation) const {
globalProgramInformation.moduleToIndexMap[moduleName] = globalProgramInformation.modules.size();
if (!this->secondRun) {
globalProgramInformation.moduleToIndexMap[moduleName] = globalProgramInformation.modules.size();
} else {
STORM_LOG_THROW(globalProgramInformation.moduleToIndexMap[moduleName] == globalProgramInformation.modules.size(), storm::exceptions::WrongFormatException, "Internal error while parsing: the index for module " << moduleName << " does not match the on in the first run.");
}
return storm::prism::Module(moduleName, booleanVariables, integerVariables, clockVariables, invariant.is_initialized()? invariant.get() : storm::expressions::Expression(), commands, this->getFilename()); return storm::prism::Module(moduleName, booleanVariables, integerVariables, clockVariables, invariant.is_initialized()? invariant.get() : storm::expressions::Expression(), commands, this->getFilename());
} }
bool PrismParser::isValidModuleRenaming(std::string const& oldModuleName, storm::prism::ModuleRenaming const& moduleRenaming, GlobalProgramInformation const& globalProgramInformation) const { bool PrismParser::isValidModuleRenaming(std::string const& oldModuleName, storm::prism::ModuleRenaming const& moduleRenaming, GlobalProgramInformation const& globalProgramInformation) const {
if (!this->secondRun) { if (!this->secondRun) {
auto const& renaming = moduleRenaming.getRenaming(); auto const& renaming = moduleRenaming.getRenaming();

Loading…
Cancel
Save