diff --git a/src/adapters/ExplicitModelAdapter.cpp b/src/adapters/ExplicitModelAdapter.cpp index 417d5cf40..004a6acdb 100644 --- a/src/adapters/ExplicitModelAdapter.cpp +++ b/src/adapters/ExplicitModelAdapter.cpp @@ -20,6 +20,7 @@ #include #include +#include #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" @@ -27,7 +28,7 @@ extern log4cplus::Logger logger; bool ExplicitModelAdapterOptionsRegistered = storm::settings::Settings::registerNewModule([] (storm::settings::Settings* instance) -> bool { instance->addOption(storm::settings::OptionBuilder("ExplicitModelAdapter", "constants", "", "Specifies the constant replacements to use in Explicit Models").addArgument(storm::settings::ArgumentBuilder::createStringArgument("constantString", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3").addValidationFunctionString( - [] (std::string const& s) -> bool { + [] (std::string const s, std::string& errorMessageTarget) -> bool { // since regex is not yet implemented in gccs C++11, we have to check by hand std::vector constants; // split for single assignment expressions @@ -36,18 +37,27 @@ bool ExplicitModelAdapterOptionsRegistered = storm::settings::Settings::register std::vector constant; boost::split(constant, *it, boost::is_any_of("=")); if (constant.size() != 2) { + std::ostringstream stream; + stream << "Expected one \"=\" in constant definition: \"" << *it << "\"" << std::endl; + errorMessageTarget.append(stream.str()); return false; } // Constant Name check bool error = false; - std::for_each(constant.at(0).cbegin(), constant.at(0).cend(), [&error] (const std::string::value_type value) -> void { + std::for_each(constant.at(0).cbegin(), constant.at(0).cend(), [&error, &errorMessageTarget] (const std::string::value_type value) -> void { if (!(('a' <= value && value <= 'z') || ('A' <= value && value <= 'Z') || ('0' <= value && value <= '9'))) { + std::ostringstream stream; + stream << "Illegal character in constant name: \"" << value << "\"" << std::endl; + errorMessageTarget.append(stream.str()); error = true; } }); // Value Check - std::for_each(constant.at(1).cbegin(), constant.at(1).cend(), [&error] (const std::string::value_type value) -> void { + std::for_each(constant.at(1).cbegin(), constant.at(1).cend(), [&error, &errorMessageTarget] (const std::string::value_type value) -> void { if (!(('a' <= value && value <= 'z') || ('A' <= value && value <= 'Z') || ('0' <= value && value <= '9'))) { + std::ostringstream stream; + stream << "Illegal character in constant value: \"" << value << "\"" << std::endl; + errorMessageTarget.append(stream.str()); error = true; } }); diff --git a/src/counterexamples/MinimalLabelSetGenerator.h b/src/counterexamples/MinimalLabelSetGenerator.h index de9a71b94..c182891aa 100644 --- a/src/counterexamples/MinimalLabelSetGenerator.h +++ b/src/counterexamples/MinimalLabelSetGenerator.h @@ -71,7 +71,9 @@ namespace storm { std::unordered_map stateToProbabilityVariableIndexMap; std::unordered_map problematicStateToVariableIndexMap; std::unordered_map, uint_fast64_t, PairHash> problematicTransitionToVariableIndexMap; - uint_fast64_t nextFreeVariableIndex = 0; + uint_fast64_t nextFreeVariableIndex; + + VariableInformation() : nextFreeVariableIndex(0) {} }; /*! diff --git a/src/storm.cpp b/src/storm.cpp index b3442375e..48912384e 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -332,7 +332,8 @@ int main(const int argc, const char* argv[]) { } else if (s->isSet("symbolic")) { std::string const arg = s->getOptionByLongName("symbolic").getArgument(0).getValueAsString(); storm::adapters::ExplicitModelAdapter adapter(storm::parser::PrismParserFromFile(arg)); - std::shared_ptr> model = adapter.getModel("K=1"); + std::string const constants = s->getOptionByLongName("constants").getArgument(0).getValueAsString(); + std::shared_ptr> model = adapter.getModel(constants); model->printModelInformationToStream(std::cout); if (model->getType() == storm::models::MDP) {