Fixed a bug in the option system and MILP-based cex generator. Now everything should work for the demo. :)

Former-commit-id: 3676ec7023

src/counterexamples/MILPMinimalLabelSetGenerator.h

@@ -156,7 +156,6 @@ namespace storm {
 
                 // Finally, determine the set of labels that are known to be taken.
                 result.knownLabels = storm::utility::counterexamples::getGuaranteedLabelSet(labeledMdp, psiStates, result.allRelevantLabels);
-                std::cout << "Found " << result.allRelevantLabels.size() << " relevant labels and " << result.knownLabels.size() << " known labels." << std::endl;
                 LOG4CPLUS_DEBUG(logger, "Found " << result.allRelevantLabels.size() << " relevant labels and " << result.knownLabels.size() << " known labels.");
 
                 return result;
@@ -948,7 +947,7 @@ namespace storm {
                     if ((strictBound && maximalReachabilityProbability < probabilityThreshold) || (!strictBound && maximalReachabilityProbability <= probabilityThreshold)) {
                         throw storm::exceptions::InvalidArgumentException() << "Given probability threshold " << probabilityThreshold << " can not be " << (strictBound ? "achieved" : "exceeded") << " in model with maximal reachability probability of " << maximalReachabilityProbability << ".";
                     }
-                    std::cout << "Maximal reachability in model determined to be " << maximalReachabilityProbability << "." << std::endl;
+                    std::cout << std::endl << "Maximal reachability in model is " << maximalReachabilityProbability << "." << std::endl << std::endl;
                 }
 
                 // (2) Identify relevant and problematic states.
@@ -987,19 +986,21 @@ namespace storm {
              * @param formulaPtr A pointer to a safety formula. The outermost operator must be a probabilistic bound operator with a strict upper bound. The nested
              * formula can be either an unbounded until formula or an eventually formula.
              */
-            static void computeCounterexample(storm::prism::Program const& program, storm::models::Mdp<T> const& labeledMdp, std::shared_ptr<storm::properties::prctl::AbstractPrctlFormula<double>> const & formulaPtr) {
-                std::cout << std::endl << "Generating minimal label counterexample for formula " << formulaPtr->toString() << std::endl;
+            static void computeCounterexample(storm::prism::Program const& program, storm::models::Mdp<T> const& labeledMdp, std::shared_ptr<storm::properties::prctl::AbstractPrctlFormula<double>> const& formula) {
+                std::cout << std::endl << "Generating minimal label counterexample for formula " << formula->toString() << std::endl;
                 // First, we need to check whether the current formula is an Until-Formula.
-                auto probBoundFormula = std::dynamic_pointer_cast<storm::properties::prctl::ProbabilisticBoundOperator<double>>(formulaPtr);
-                if (probBoundFormula == nullptr) {
+                std::shared_ptr<storm::properties::prctl::ProbabilisticBoundOperator<double>> probBoundFormula = std::dynamic_pointer_cast<storm::properties::prctl::ProbabilisticBoundOperator<double>>(formula);
+                if (probBoundFormula.get() == nullptr) {
                     LOG4CPLUS_ERROR(logger, "Illegal formula " << probBoundFormula->toString() << " for counterexample generation.");
                     throw storm::exceptions::InvalidPropertyException() << "Illegal formula " << probBoundFormula->toString() << " for counterexample generation.";
                 }
+                
+                // Check whether we were given an upper bound, because counterexample generation is limited to this case.
                 if (probBoundFormula->getComparisonOperator() != storm::properties::ComparisonType::LESS && probBoundFormula->getComparisonOperator() != storm::properties::ComparisonType::LESS_EQUAL) {
                     LOG4CPLUS_ERROR(logger, "Illegal comparison operator in formula " << probBoundFormula->toString() << ". Only upper bounds are supported for counterexample generation.");
                     throw storm::exceptions::InvalidPropertyException() << "Illegal comparison operator in formula " << probBoundFormula->toString() << ". Only upper bounds are supported for counterexample generation.";
                 }
-                bool strictBound = !(probBoundFormula->getComparisonOperator() == storm::properties::ComparisonType::LESS);
+                bool strictBound = probBoundFormula->getComparisonOperator() == storm::properties::ComparisonType::LESS;
 
                 // Now derive the probability threshold we need to exceed as well as the phi and psi states. Simultaneously, check whether the formula is of a valid shape.
                 double bound = probBoundFormula->getBound();
@@ -1007,22 +1008,22 @@ namespace storm {
                 storm::storage::BitVector phiStates;
                 storm::storage::BitVector psiStates;
                 storm::modelchecker::prctl::SparseMdpPrctlModelChecker<T> modelchecker(labeledMdp);
-                try {
-                    auto untilFormula = std::dynamic_pointer_cast<storm::properties::prctl::Until<double>>(pathFormula);
-                    
+                
+                std::shared_ptr<storm::properties::prctl::Until<double>> untilFormula = std::dynamic_pointer_cast<storm::properties::prctl::Until<double>>(pathFormula);
+                if(untilFormula.get() != nullptr) {
                     phiStates = untilFormula->getLeft()->check(modelchecker);
                     psiStates = untilFormula->getRight()->check(modelchecker);
-                } catch (std::bad_cast const&) {
+                    
+                } if (std::dynamic_pointer_cast<storm::properties::prctl::Eventually<double>>(pathFormula).get() != nullptr) {
                     // If the nested formula was not an until formula, it remains to check whether it's an eventually formula.
-                    try {
-                        auto eventuallyFormula = std::dynamic_pointer_cast<storm::properties::prctl::Eventually<double>>(pathFormula);
-                        
-                        phiStates = storm::storage::BitVector(labeledMdp.getNumberOfStates(), true);
-                        psiStates = eventuallyFormula->getChild()->check(modelchecker);
-                    } catch (std::bad_cast const&) {
-                        // If the nested formula is neither an until nor a finally formula, we throw an exception.
-                        throw storm::exceptions::InvalidPropertyException() << "Formula nested inside probability bound operator must be an until or eventually formula for counterexample generation.";
-                    }
+                    std::shared_ptr<storm::properties::prctl::Eventually<double>> eventuallyFormula = std::dynamic_pointer_cast<storm::properties::prctl::Eventually<double>>(pathFormula);
+                    
+                    phiStates = storm::storage::BitVector(labeledMdp.getNumberOfStates(), true);
+                    psiStates = eventuallyFormula->getChild()->check(modelchecker);
+                    
+                } else {
+                    // If the nested formula is neither an until nor a finally formula, we throw an exception.
+                    throw storm::exceptions::InvalidPropertyException() << "Formula nested inside probability bound operator must be an until or eventually formula for counterexample generation.";
                 }
                 
                 // Delegate the actual computation work to the function of equal name.

src/counterexamples/SMTMinimalCommandSetGenerator.h

@@ -1660,7 +1660,7 @@ namespace storm {
                     if ((strictBound && maximalReachabilityProbability < probabilityThreshold) || (!strictBound && maximalReachabilityProbability <= probabilityThreshold)) {
                         throw storm::exceptions::InvalidArgumentException() << "Given probability threshold " << probabilityThreshold << " can not be " << (strictBound ? "achieved" : "exceeded") << " in model with maximal reachability probability of " << maximalReachabilityProbability << ".";
                     }
-                    std::cout << "Maximal reachability in model determined to be " << maximalReachabilityProbability << "." << std::endl;
+                    std::cout << std::endl << "Maximal reachability in model determined is " << maximalReachabilityProbability << "." << std::endl;
                 }
                 
                 // (2) Identify all states and commands that are relevant, because only these need to be considered later.

src/settings/ArgumentBase.cpp

@@ -30,6 +30,12 @@ namespace storm {
             return t;
         }
         
+        template <>
+        std::string ArgumentBase::convertFromString(std::string const& valueAsString, bool& conversionSuccessful) {
+            conversionSuccessful = true;
+            return valueAsString;
+        }
+        
         template <>
         bool ArgumentBase::convertFromString<bool>(std::string const& s, bool& ok) {
             static const std::string lowerTrueString = "true";

src/settings/SettingsManager.cpp

@@ -302,7 +302,8 @@ namespace storm {
                 // Now set the provided argument values one by one.
                 for (uint_fast64_t i = 0; i < argumentCache.size(); ++i) {
                     ArgumentBase& argument = option->getArgument(i);
-                    argument.setFromStringValue(argumentCache[i]);
+                    bool conversionOk = argument.setFromStringValue(argumentCache[i]);
+                    STORM_LOG_THROW(conversionOk, storm::exceptions::OptionParserException, "Conversion of value of argument '" << argument.getName() << "' to its type failed.");
                 }
                 
                 // In case there are optional arguments that were not set, we set them to their default value.

src/settings/modules/CounterexampleGeneratorSettings.cpp

@@ -14,7 +14,6 @@ namespace storm {
             CounterexampleGeneratorSettings::CounterexampleGeneratorSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
                 std::vector<std::string> techniques = {"maxsat", "milp"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, minimalCommandSetOptionName, true, "Computes a counterexample for the given model in terms of a minimal command set. Note that this requires the model to be given in a symbolic format.")
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file containing the properties for which counterexamples are to be generated.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build())
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used to derive the counterexample. Available are {milp, maxsat}").setDefaultValueString("maxsat").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(techniques)).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, encodeReachabilityOptionName, true, "Sets whether to encode reachability for MAXSAT-based minimal command counterexample generation.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, schedulerCutsOptionName, true, "Sets whether to add the scheduler cuts for MILP-based minimal command counterexample generation.").build());
@@ -24,9 +23,6 @@ namespace storm {
                 return this->getOption(minimalCommandSetOptionName).getHasOptionBeenSet();
             }
             
-            std::string CounterexampleGeneratorSettings::minimalCommandSetPropertyFilename() const {
-                return this->getOption(minimalCommandSetOptionName).getArgumentByName("filename").getValueAsString();
-            }
             
             bool CounterexampleGeneratorSettings::isUseMilpBasedMinimalCommandSetGenerationSet() const {
                 return this->getOption(minimalCommandSetOptionName).getArgumentByName("method").getValueAsString() == "milp";

src/settings/modules/CounterexampleGeneratorSettings.h

@@ -26,14 +26,6 @@ namespace storm {
                  */
                 bool isMinimalCommandGenerationSet() const;
                 
-                /*!
-                 * Retrieves the name of the file that contains the properties for which a minimal command set
-                 * counterexample is to be generated if the option to generate such a counterexample was set.
-                 *
-                 * @return The name of the file that contains the properties.
-                 */
-                std::string minimalCommandSetPropertyFilename() const;
-                
                 /*!
                  * Retrieves whether the MILP-based technique is to be used to generate a minimal command set
                  * counterexample.