From 1934bdd801308894ddf3841956b832b8a379bd3a Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 22 Sep 2013 22:03:50 +0200 Subject: [PATCH] Disabled MinimalLabelSetGenerator test code in storm.cpp and fixed minor issue in ExplicitModelAdapter that treated constant strings incorrectly. Former-commit-id: 11a31be820994c2d5d704e33b1ad8fb3113c217f --- src/adapters/ExplicitModelAdapter.cpp | 96 ++++++++++++++------------- src/storm.cpp | 17 ++--- 2 files changed, 58 insertions(+), 55 deletions(-) diff --git a/src/adapters/ExplicitModelAdapter.cpp b/src/adapters/ExplicitModelAdapter.cpp index 3963ec81b..5371ebfaa 100644 --- a/src/adapters/ExplicitModelAdapter.cpp +++ b/src/adapters/ExplicitModelAdapter.cpp @@ -48,55 +48,57 @@ namespace storm { } void ExplicitModelAdapter::defineUndefinedConstants(std::string const& constantDefinitionString) { - // Parse the string that defines the undefined constants of the model and make sure that it contains exactly - // one value for each undefined constant of the model. - std::vector definitions; - boost::split(definitions, constantDefinitionString, boost::is_any_of(",")); - for (auto& definition : definitions) { - boost::trim(definition); - - // Check whether the token could be a legal constant definition. - uint_fast64_t positionOfAssignmentOperator = definition.find('='); - if (positionOfAssignmentOperator == std::string::npos) { - throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: syntax error."; - } - - // Now extract the variable name and the value from the string. - std::string constantName = definition.substr(0, positionOfAssignmentOperator); - boost::trim(constantName); - std::string value = definition.substr(positionOfAssignmentOperator + 1); - boost::trim(value); - - // Check whether the constant is a legal undefined constant of the program and if so, of what type it is. - if (program.hasUndefinedBooleanConstant(constantName)) { - if (value == "true") { - program.getUndefinedBooleanConstantExpression(constantName)->define(true); - } else if (value == "false") { - program.getUndefinedBooleanConstantExpression(constantName)->define(false); - } else { - throw storm::exceptions::InvalidArgumentException() << "Illegal value for boolean constant: " << value << "."; - } - } else if (program.hasUndefinedIntegerConstant(constantName)) { - try { - int_fast64_t integerValue = std::stoi(value); - program.getUndefinedIntegerConstantExpression(constantName)->define(integerValue); - } catch (std::invalid_argument const&) { - throw storm::exceptions::InvalidArgumentException() << "Illegal value of integer constant: " << value << "."; - } catch (std::out_of_range const&) { - throw storm::exceptions::InvalidArgumentException() << "Illegal value of integer constant: " << value << " (value too big)."; - } - } else if (program.hasUndefinedDoubleConstant(constantName)) { - try { - double doubleValue = std::stod(value); - program.getUndefinedDoubleConstantExpression(constantName)->define(doubleValue); - } catch (std::invalid_argument const&) { - throw storm::exceptions::InvalidArgumentException() << "Illegal value of double constant: " << value << "."; - } catch (std::out_of_range const&) { - throw storm::exceptions::InvalidArgumentException() << "Illegal value of double constant: " << value << " (value too big)."; + if (!constantDefinitionString.empty()) { + // Parse the string that defines the undefined constants of the model and make sure that it contains exactly + // one value for each undefined constant of the model. + std::vector definitions; + boost::split(definitions, constantDefinitionString, boost::is_any_of(",")); + for (auto& definition : definitions) { + boost::trim(definition); + + // Check whether the token could be a legal constant definition. + uint_fast64_t positionOfAssignmentOperator = definition.find('='); + if (positionOfAssignmentOperator == std::string::npos) { + throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: syntax error."; } - } else { - throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: unknown undefined constant " << constantName << "."; + // Now extract the variable name and the value from the string. + std::string constantName = definition.substr(0, positionOfAssignmentOperator); + boost::trim(constantName); + std::string value = definition.substr(positionOfAssignmentOperator + 1); + boost::trim(value); + + // Check whether the constant is a legal undefined constant of the program and if so, of what type it is. + if (program.hasUndefinedBooleanConstant(constantName)) { + if (value == "true") { + program.getUndefinedBooleanConstantExpression(constantName)->define(true); + } else if (value == "false") { + program.getUndefinedBooleanConstantExpression(constantName)->define(false); + } else { + throw storm::exceptions::InvalidArgumentException() << "Illegal value for boolean constant: " << value << "."; + } + } else if (program.hasUndefinedIntegerConstant(constantName)) { + try { + int_fast64_t integerValue = std::stoi(value); + program.getUndefinedIntegerConstantExpression(constantName)->define(integerValue); + } catch (std::invalid_argument const&) { + throw storm::exceptions::InvalidArgumentException() << "Illegal value of integer constant: " << value << "."; + } catch (std::out_of_range const&) { + throw storm::exceptions::InvalidArgumentException() << "Illegal value of integer constant: " << value << " (value too big)."; + } + } else if (program.hasUndefinedDoubleConstant(constantName)) { + try { + double doubleValue = std::stod(value); + program.getUndefinedDoubleConstantExpression(constantName)->define(doubleValue); + } catch (std::invalid_argument const&) { + throw storm::exceptions::InvalidArgumentException() << "Illegal value of double constant: " << value << "."; + } catch (std::out_of_range const&) { + throw storm::exceptions::InvalidArgumentException() << "Illegal value of double constant: " << value << " (value too big)."; + } + + } else { + throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: unknown undefined constant " << constantName << "."; + } } } } diff --git a/src/storm.cpp b/src/storm.cpp index 48912384e..24e82f039 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -335,14 +335,15 @@ int main(const int argc, const char* argv[]) { 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) { - std::shared_ptr> labeledMdp = model->as>(); - storm::storage::BitVector const& finishedStates = labeledMdp->getLabeledStates("finished"); - storm::storage::BitVector const& allCoinsEqual1States = labeledMdp->getLabeledStates("all_coins_equal_1"); - storm::storage::BitVector targetStates = finishedStates & allCoinsEqual1States; - storm::counterexamples::MinimalLabelSetGenerator::getMinimalLabelSet(*labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.3, true, true); - } + +// Enable the following lines to test the MinimalLabelSetGenerator. +// if (model->getType() == storm::models::MDP) { +// std::shared_ptr> labeledMdp = model->as>(); +// storm::storage::BitVector const& finishedStates = labeledMdp->getLabeledStates("finished"); +// storm::storage::BitVector const& allCoinsEqual1States = labeledMdp->getLabeledStates("all_coins_equal_1"); +// storm::storage::BitVector targetStates = finishedStates & allCoinsEqual1States; +// storm::counterexamples::MinimalLabelSetGenerator::getMinimalLabelSet(*labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.3, true, true); +// } } // Perform clean-up and terminate.