From 94d8a46b1d6057d091e3fdec772868e0784c64ae Mon Sep 17 00:00:00 2001 From: masawei Date: Tue, 5 Nov 2013 22:20:15 +0100 Subject: [PATCH] Fixed some compile errors originating from the introductionof the new storm::storage::VectorSet. - Also handled the case of a missing --prctl while using the counterexample generation. - Remark: Some documentation for the VectorSet would have been nice. Former-commit-id: c687b674547a1c887f3926d634cacaff54d790e5 --- .../MILPMinimalLabelSetGenerator.h | 2 +- src/models/Dtmc.h | 9 ++++----- src/storm.cpp | 15 ++++++++++++--- 3 files changed, 17 insertions(+), 9 deletions(-) diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index aa24cb073..5f0d10a75 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -20,7 +20,7 @@ extern "C" { #endif #include "src/models/Mdp.h" -#include "src/ir/program.h" +#include "src/ir/Program.h" #include "src/exceptions/NotImplementedException.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/InvalidStateException.h" diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 5c4fb3e63..c21d06d2f 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -142,7 +142,7 @@ public: storm::models::AtomicPropositionsLabeling(this->getStateLabeling(), subSysStates), boost::optional>(), boost::optional>(), - boost::optional>>()); + boost::optional>>()); } // Does the vector have the right size? @@ -159,7 +159,6 @@ public: // 1. Get all necessary information from the old transition matrix storm::storage::SparseMatrix const & origMat = this->getTransitionMatrix(); - uint_fast64_t const stateCount = origMat.getColumnCount(); // Iterate over all rows. Count the number of all transitions from the old system to be // transfered to the new one. Also build a mapping from the state number of the old system @@ -276,16 +275,16 @@ public: newTransitionRewards = newTransRewards; } - boost::optional>> newChoiceLabels; + boost::optional>> newChoiceLabels; if(this->hasChoiceLabels()) { // Get the choice label sets and move the needed values to the front. - std::vector> newChoice(this->getChoiceLabeling()); + std::vector> newChoice(this->getChoiceLabeling()); storm::utility::vector::selectVectorValues(newChoice, subSysStates, newChoice); // Throw away all values after the last state and set the choice label set for s_b as empty. newChoice.resize(newStateCount); - newChoice[newStateCount - 1] = std::set(); + newChoice[newStateCount - 1] = storm::storage::VectorSet(); newChoiceLabels = newChoice; } diff --git a/src/storm.cpp b/src/storm.cpp index a9015da6d..4621f7413 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -260,13 +260,17 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker /*! * Handles the counterexample generation control. + * + * @param parser An AutoParser to get the model from. */ void generateCounterExample(storm::parser::AutoParser parser) { LOG4CPLUS_INFO(logger, "Starting counterexample generation."); LOG4CPLUS_INFO(logger, "Testing inputs..."); + storm::settings::Settings* s = storm::settings::Settings::getInstance(); + //First test output directory. - std::string outPath = storm::settings::Settings::getInstance()->getOptionByLongName("counterExample").getArgument(0).getValueAsString(); + std::string outPath = s->getOptionByLongName("counterExample").getArgument(0).getValueAsString(); if(outPath.back() != '/' && outPath.back() != '\\') { LOG4CPLUS_ERROR(logger, "The output path is not valid."); return; @@ -289,13 +293,18 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker LOG4CPLUS_INFO(logger, "Model is a DTMC."); // Get specified PRCTL formulas. - std::string const chosenPrctlFile = storm::settings::Settings::getInstance()->getOptionByLongName("prctl").getArgument(0).getValueAsString(); + if(!s->isSet("prctl")) { + LOG4CPLUS_ERROR(logger, "No PRCTL formula file specified."); + return; + } + + std::string const chosenPrctlFile = s->getOptionByLongName("prctl").getArgument(0).getValueAsString(); LOG4CPLUS_INFO(logger, "Parsing prctl file: " << chosenPrctlFile << "."); std::list*> formulaList = storm::parser::PrctlFileParser(chosenPrctlFile); // Test for each formula if a counterexample can be generated for it. if(formulaList.size() == 0) { - LOG4CPLUS_ERROR(logger, "No PRCTL formula file specified."); + LOG4CPLUS_ERROR(logger, "No PRCTL formula found."); return; }