From 4c09f9ce29c23532ca5a71fe473e0670bf2f19a9 Mon Sep 17 00:00:00 2001 From: Mavo Date: Mon, 4 Jan 2016 11:17:44 +0100 Subject: [PATCH] Minor improvements Former-commit-id: 63dfd49048df5ec636ca9dd163249e0ea3de76c3 --- src/parser/DFTGalileoParser.cpp | 12 +++++------- src/solver/Z3SmtSolver.cpp | 2 +- src/storm-dyftee.cpp | 1 + 3 files changed, 7 insertions(+), 8 deletions(-) diff --git a/src/parser/DFTGalileoParser.cpp b/src/parser/DFTGalileoParser.cpp index e3368bbe3..97b095f22 100644 --- a/src/parser/DFTGalileoParser.cpp +++ b/src/parser/DFTGalileoParser.cpp @@ -41,7 +41,7 @@ namespace storm { template bool DFTGalileoParser::readFile(const std::string& filename) { // constants - std::string topleveltoken = "toplevel"; + std::string toplevelToken = "toplevel"; std::string toplevelId; std::ifstream file; @@ -57,23 +57,21 @@ namespace storm { std::string line; bool generalSuccess = true; - while(std::getline(file, line)) - { + while(std::getline(file, line)) { bool success = true; STORM_LOG_TRACE("Parsing: " << line); size_t commentstarts = line.find("//"); line = line.substr(0, commentstarts); size_t firstsemicolon = line.find(";"); line = line.substr(0, firstsemicolon); - if (line.find_first_not_of(' ') == std::string::npos) - { + if (line.find_first_not_of(' ') == std::string::npos) { // Only whitespace continue; } // Top level indicator. - if(boost::starts_with(line, topleveltoken)) { - toplevelId = stripQuotsFromName(line.substr(topleveltoken.size() + 1)); + if(boost::starts_with(line, toplevelToken)) { + toplevelId = stripQuotsFromName(line.substr(toplevelToken.size() + 1)); } else { diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp index 1c3495335..eba059635 100644 --- a/src/solver/Z3SmtSolver.cpp +++ b/src/solver/Z3SmtSolver.cpp @@ -323,7 +323,7 @@ namespace storm { std::vector Z3SmtSolver::getUnsatAssumptions() { #ifdef STORM_HAVE_Z3 - STORM_LOG_THROW(lastResult == SmtSolver::CheckResult::Unsat, storm::exceptions::InvalidStateException, "Unable to generate unsatisfiable core of assumptions, because the last check did not determine the formulas to be unsatisfiable.") + STORM_LOG_THROW(lastResult == SmtSolver::CheckResult::Unsat, storm::exceptions::InvalidStateException, "Unable to generate unsatisfiable core of assumptions, because the last check did not determine the formulas to be unsatisfiable."); STORM_LOG_THROW(lastCheckAssumptions, storm::exceptions::InvalidStateException, "Unable to generate unsatisfiable core of assumptions, because the last check did not involve assumptions."); z3::expr_vector z3UnsatAssumptions = this->solver->unsat_core(); diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index 7040db9ad..1d2696594 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -13,6 +13,7 @@ int main(int argc, char** argv) { if(argc < 2) { std::cout << "Storm-DyFTeE should be called with a filename as argument." << std::endl; + return 1; } storm::utility::setUp();