added export of constraints and resultfile

Former-commit-id: 9389adfeae

src/adapters/extendedCarl.h

@@ -12,8 +12,8 @@
 #include <carl/core/MultivariatePolynomial.h>
 #include <carl/core/RationalFunction.h>
 #include <carl/core/VariablePool.h>
+#include <carl/core/Constraint.h>
 
-#undef LOG_ASSERT
 namespace carl
 {
 template<typename C, typename O, typename P>
@@ -31,6 +31,5 @@ inline size_t hash_value(carl::RationalFunction<Pol> const& f)
 
 }
 
-#include "src/exceptions/ExceptionMacros.h"
 
 #endif

src/modelchecker/reachability/CollectConstraints.h

@@ -0,0 +1,63 @@
+/** 
+ * @file:   CollectConstraints.h
+ * @author: Sebastian Junges
+ *
+ * @since October 8, 2014
+ */
+
+#pragma once
+#include "src/models/Dtmc.h"
+
+
+namespace storm {
+namespace modelchecker {
+	namespace reachability {
+		template<typename ValueType>
+		class CollectConstraints
+		{
+			private:
+				std::unordered_set<carl::Constraint<ValueType>> wellformedConstraintSet;
+				std::unordered_set<carl::Constraint<ValueType>> graphPreservingConstraintSet;
+
+			public:
+				std::unordered_set<carl::Constraint<ValueType>> const&  wellformedConstraints() const {
+					return this->wellformedConstraintSet;
+				}
+				
+				std::unordered_set<carl::Constraint<ValueType>> const&  graphPreservingConstraints() const {
+					return this->graphPreservingConstraintSet;
+				}
+				
+				void process(storm::models::Dtmc<ValueType> const& dtmc) 
+				{
+					for(uint_fast64_t state = 0; state < dtmc.getNumberOfStates(); ++state)
+					{
+						ValueType sum;
+						assert(storm::utility::isZero(sum));
+						for(auto const& transition : dtmc.getRows(state))
+						{
+							sum += transition.getValue();
+							if(!transition.getValue().isConstant())
+							{
+								wellformedConstraintSet.emplace(transition.getValue() - 1, storm::CompareRelation::LEQ);
+								wellformedConstraintSet.emplace(transition.getValue(), storm::CompareRelation::GEQ);
+								graphPreservingConstraintSet.emplace(transition.getValue(), storm::CompareRelation::GT);
+							}
+						}
+						assert(!sum.isConstant() || storm::utility::isOne(sum));
+						if(!sum.isConstant()) {
+							wellformedConstraintSet.emplace(sum - 1, storm::CompareRelation::EQ);
+						}
+
+					}
+				}
+
+				void operator()(storm::models::Dtmc<ValueType> const& dtmc) 
+				{
+					process(dtmc);
+				}
+
+		};	
+	}
+}
+}

src/modelchecker/reachability/DirectEncoding.h

@@ -90,7 +90,7 @@ namespace storm
 					
 					smt2 << ("reachability");
 					
-					carl::CompareRelation thresholdRelation = lessequal ? carl::CompareRelation::LE : carl::CompareRelation::GE;
+					carl::CompareRelation thresholdRelation = lessequal ? carl::CompareRelation::LEQ : carl::CompareRelation::GEQ;
 					smt2 <<  carl::Constraint<Polynomial>(initStateReachSum - threshold, thresholdRelation);
 					smt2 << carl::io::smt2flag::CHECKSAT;
 					smt2 << carl::io::smt2flag::MODEL;

src/settings/Option.h

@@ -284,11 +284,11 @@ namespace storm {
                 STORM_LOG_THROW(!longName.empty(), storm::exceptions::IllegalArgumentException, "Unable to construct option with empty name.");
                 STORM_LOG_THROW(!moduleName.empty(), storm::exceptions::IllegalArgumentException, "Unable to construct option with empty module name.");
                 
-                bool longNameContainsNonAlpha = std::find_if(longName.begin(), longName.end(), [](char c) { return !std::isalpha(c); }) != longName.end();
-                STORM_LOG_THROW(!longNameContainsNonAlpha, storm::exceptions::IllegalArgumentException, "Unable to construct option with illegal name.");
+                bool longNameContainsNonAlpha = std::find_if(longName.begin(), longName.end(), [](char c) { return !(std::isalpha(c) || std::isdigit(c)); }) != longName.end();
+                STORM_LOG_THROW(!longNameContainsNonAlpha, storm::exceptions::IllegalArgumentException, "Unable to construct option with illegal long name '" << longName << "'.");
                 
-                bool shortNameContainsNonAlpha = std::find_if(shortName.begin(), shortName.end(), [](char c) { return !std::isalpha(c); }) != shortName.end();
-                STORM_LOG_THROW(!shortNameContainsNonAlpha, storm::exceptions::IllegalArgumentException, "Unable to construct option with illegal name.");
+                bool shortNameContainsNonAlpha = std::find_if(shortName.begin(), shortName.end(), [](char c) { return !(std::isalpha(c) || std::isdigit(c)); }) != shortName.end();
+                STORM_LOG_THROW(!shortNameContainsNonAlpha, storm::exceptions::IllegalArgumentException, "Unable to construct option with illegal short name '" << shortName << "'.");
 
                 // Then index all arguments.
                 for (auto const& argument : arguments) {

src/settings/modules/ParametricSettings.cpp

@@ -10,12 +10,21 @@ namespace storm {
             const std::string ParametricSettings::entryStatesLastOptionName = "entrylast";
             const std::string ParametricSettings::maximalSccSizeOptionName = "sccsize";
             const std::string ParametricSettings::sortTrivialSccOptionName = "sorttrivial";
+            const std::string ParametricSettings::encodeSmt2StrategyOptionName = "smt2strategy";
+            const std::string ParametricSettings::exportSmt2DestinationPathOptionName = "smt2path";
+            const std::string ParametricSettings::exportResultDestinationPathOptionName = "resultfile";
             
             ParametricSettings::ParametricSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, entryStatesLastOptionName, true, "Sets whether the entry states are eliminated last.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, sortTrivialSccOptionName, true, "Sets whether the trivial SCCs are to be eliminated in descending order with respect to their distances from the initial state.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, maximalSccSizeOptionName, true, "Sets the maximal size of the SCCs for which state elimination is applied.")
                                 .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("maxsize", "The maximal size of an SCC on which state elimination is applied.").setDefaultValueUnsignedInteger(20).setIsOptional(true).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, encodeSmt2StrategyOptionName, true, "Set the smt2 encoding strategy.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("strategy", "the used strategy").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, exportSmt2DestinationPathOptionName, true, "A path to a file where the result should be saved.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "the location.").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, exportResultDestinationPathOptionName, true, "A path to a file where the smt2 encoding should be saved.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "the location.").build()).build());
             }
             
             bool ParametricSettings::isEliminateEntryStatesLastSet() const {
@@ -30,6 +39,40 @@ namespace storm {
                 return this->getOption(sortTrivialSccOptionName).getHasOptionBeenSet();
             }
             
+            bool ParametricSettings::exportResultToFile() const {
+                return this->getOption(exportResultDestinationPathOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string ParametricSettings::exportResultPath() const {
+                return this->getOption(exportResultDestinationPathOptionName).getArgumentByName("path").getValueAsString();
+            }
+            
+            bool ParametricSettings::exportToSmt2File() const {
+                return this->getOption(exportSmt2DestinationPathOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string ParametricSettings::exportSmt2Path() const {
+                return this->getOption(exportSmt2DestinationPathOptionName).getArgumentByName("path").getValueAsString();
+            }
+            
+            ParametricSettings::Smt2EncodingStrategy ParametricSettings::smt2EncodingStrategy() const {
+                std::string strategy = this->getOption(encodeSmt2StrategyOptionName).getArgumentByName("strategy").getValueAsString();
+                
+                if(strategy == "fts") {
+                    return Smt2EncodingStrategy::FULL_TRANSITION_SYSTEM;
+                } else if(strategy == "rf") {
+                    return Smt2EncodingStrategy::RATIONAL_FUNCTION;
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown smt2encoding strategy '" << strategy << "'.");
+                }
+                
+                
+               
+            }
+            
+            
+            
+            
         } // namespace modules
     } // namespace settings
 } // namespace storm

src/settings/modules/ParametricSettings.h

@@ -12,6 +12,17 @@ namespace storm {
              */
             class ParametricSettings : public ModuleSettings {
             public:
+				/**
+				 * A type for saving the Smt2EncondingStrategy.
+				 * 
+				 * FULL_TRANSITION_SYSTEM: The transition system should be reduced only with very basic operations.
+				 * ONLY_SCC_ENTRY_STATES: Scc elimination should be performed, but no further reduction.
+				 * HIGH_INDEGREE:  State elimination but for states with a high indegree.
+				 * RATIONAL_FUNCTION: The smt file should contain only the rational function.
+				 */
+				enum class Smt2EncodingStrategy {FULL_TRANSITION_SYSTEM, ONLY_SCC_ENTRY_STATES, HIGH_INDEGREE, RATIONAL_FUNCTION};
+				
+				
                 /*!
                  * Creates a new set of parametric model checking settings that is managed by the given manager.
                  *
@@ -41,12 +52,46 @@ namespace storm {
                  */
                 bool isSortTrivialSccsSet() const;
 				
+				/**
+				 * Retrieves whether the model checking result should be exported to a file.
+                 * @return  True iff the result should be exported to a file.
+                 */
+				bool exportResultToFile() const;
+				
+				/**
+				 * The path to a file location which should contain the model checking result.
+                 * @return A path to a file location.
+                 */
+				std::string exportResultPath() const;
+				
+				/**
+				 * Retrieves whether the encoding of the transition system should be exported to a file. 
+				 * @return True iff the smt file should be encoded.
+				 */
+				bool exportToSmt2File() const;
+				
+				/**
+				 * The path to a file location which should contain the smt2 encoding.
+                 * @return A path to a file location.
+                 */
+				std::string exportSmt2Path() const;
+				
+				/**
+				 * Retrieves which encoding strategy should be used for generating the smt2 file.
+                 * @return The encoding strategy to be used.
+                 */
+				Smt2EncodingStrategy smt2EncodingStrategy() const;
+				
+				
                 const static std::string moduleName;
                 
             private:
                 const static std::string entryStatesLastOptionName;
                 const static std::string maximalSccSizeOptionName;
                 const static std::string sortTrivialSccOptionName;
+				const static std::string encodeSmt2StrategyOptionName;
+				const static std::string exportSmt2DestinationPathOptionName;
+				const static std::string exportResultDestinationPathOptionName;
             };
             
         } // namespace modules

src/storage/parameters.h

@@ -11,7 +11,10 @@
 namespace storm
 {
 	typedef carl::MultivariatePolynomial<cln::cl_RA> Polynomial;
-	//typedef Parameter  carl::Variable							;
+	typedef carl::Variable  Variable;
+	
+	
+	typedef carl::CompareRelation CompareRelation;
 	typedef carl::RationalFunction<Polynomial> RationalFunction;
 }
 #endif

src/stormParametric.cpp

@@ -6,7 +6,10 @@
 #include "src/exceptions/BaseException.h"
 #include "src/utility/macros.h"
 #include "src/utility/cli.h"
+#include "src/utility/export.h"
+#include "src/modelchecker/reachability/CollectConstraints.h"
 
+#include "src/modelchecker/reachability/DirectEncoding.h"
 #include "src/modelchecker/reachability/SparseSccModelChecker.h"
 #include "src/storage/parameters.h"
 /*!
@@ -31,20 +34,52 @@ int main(const int argc, const char** argv) {
         storm::prism::Program program = storm::parser::PrismParser::parse(programFile);
         std::shared_ptr<storm::models::AbstractModel<storm::RationalFunction>> model = storm::adapters::ExplicitModelAdapter<storm::RationalFunction>::translateProgram(program, constants);
         
+        
+        
         model->printModelInformationToStream(std::cout);
 
         // Program Translation Time Measurement, End
         std::chrono::high_resolution_clock::time_point programTranslationEnd = std::chrono::high_resolution_clock::now();
         std::cout << "Parsing and translating the model took " << std::chrono::duration_cast<std::chrono::milliseconds>(programTranslationEnd - programTranslationStart).count() << "ms." << std::endl << std::endl;
 
+        std::shared_ptr<storm::models::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::Dtmc<storm::RationalFunction>>();
+        assert(dtmc);
+        storm::modelchecker::reachability::CollectConstraints<storm::RationalFunction> constraintCollector;
+        constraintCollector(*dtmc);
+
+        
         storm::modelchecker::reachability::SparseSccModelChecker<storm::RationalFunction> modelChecker;
         
         STORM_LOG_THROW(storm::settings::generalSettings().isPctlPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to perform model checking without a property.");
         std::shared_ptr<storm::properties::prctl::PrctlFilter<double>> filterFormula = storm::parser::PrctlParser::parsePrctlFormula(storm::settings::generalSettings().getPctlProperty());
         
-        storm::RationalFunction value = modelChecker.computeReachabilityProbability(*model->as<storm::models::Dtmc<storm::RationalFunction>>(), filterFormula);
+        storm::RationalFunction value = modelChecker.computeReachabilityProbability(*dtmc, filterFormula);
         STORM_PRINT_AND_LOG(std::endl << "computed value " << value << std::endl);
         
+        // Get variables from parameter definitions in prism program.
+        std::set<storm::Variable> parameters;
+        for(auto constant : program.getConstants())
+        {
+            if(!constant.isDefined())
+            {
+                carl::Variable p = carl::VariablePool::getInstance().findVariableWithName(constant.getName());
+                assert(p != storm::Variable::NO_VARIABLE);
+                parameters.insert(p);
+            }
+        }
+        // 
+        STORM_LOG_ASSERT(parameters == value.gatherVariables(), "Parameters in result and program definition do not coincide.");
+        
+        if(storm::settings::parametricSettings().exportResultToFile()) {
+            storm::utility::exportParametricMcResult(value, constraintCollector);
+        }
+        
+        if(storm::settings::parametricSettings().exportToSmt2File()) {
+            storm::modelchecker::reachability::DirectEncoding dec;
+            //storm::utility::exportStreamToFile(dec.encodeAsSmt2(modelChecker.getMatrix(), parameters,));
+        }
+        
+
         // All operations have now been performed, so we clean up everything and terminate.
         storm::utility::cli::cleanUp();
         return 0;
@@ -172,16 +207,7 @@ int main(const int argc, const char** argv) {
 //
 //    modelchecker::reachability::DirectEncoding dec;
 //    std::vector<carl::Variable> parameters;
-//    for(auto constant : mProgram.getConstants())
-//    {
-//        if(!constant.isDefined())
-//        {
-//            std::cout << constant.getName() << std::endl;
-//            carl::Variable p = carl::VariablePool::getInstance().findVariableWithName(constant.getName());
-//            assert(p != carl::Variable::NO_VARIABLE);
-//            parameters.push_back(p);
-//        }
-//    }
+    
 //    return dec.encodeAsSmt2(subdtmc, parameters, subdtmc.getLabeledStates("init"), subdtmc.getLabeledStates("__targets__"), mpq_class(1,2));
 //    
 //}

src/utility/cli.h

@@ -62,13 +62,15 @@ namespace storm {
              */
             void initializeLogger() {
                 logger = log4cplus::Logger::getInstance(LOG4CPLUS_TEXT("main"));
-                auto loglevel = storm::settings::debugSettings().isTraceSet() ? log4cplus::TRACE_LOG_LEVEL : storm::settings::debugSettings().isDebugSet() ? log4cplus::DEBUG_LOG_LEVEL : log4cplus::WARN_LOG_LEVEL;
-                logger.setLogLevel(loglevel);
                 log4cplus::SharedAppenderPtr consoleLogAppender(new log4cplus::ConsoleAppender());
                 consoleLogAppender->setName("mainConsoleAppender");
-                consoleLogAppender->setThreshold(loglevel);
                 consoleLogAppender->setLayout(std::auto_ptr<log4cplus::Layout>(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %b:%L: %m%n")));
                 logger.addAppender(consoleLogAppender);
+				auto loglevel = storm::settings::debugSettings().isTraceSet() ? log4cplus::TRACE_LOG_LEVEL : storm::settings::debugSettings().isDebugSet() ? log4cplus::DEBUG_LOG_LEVEL : log4cplus::WARN_LOG_LEVEL;
+                logger.setLogLevel(loglevel);
+				consoleLogAppender->setThreshold(loglevel);
+                
+                
             }
             
             /*!

src/utility/constants.h

@@ -204,6 +204,58 @@ inline storm::storage::LabeledValues<double> constantInfinity() {
     
 /*! @endcond */
 
+template<typename T>
+inline bool isConstant(T const& v) 
+{
+	return true;
+}
+
+
+#ifdef PARAMETRIC_SYSTEMS
+template<>
+inline bool isConstant(storm::RationalFunction const& r)
+{
+	return r.isConstant();
+}
+
+template<>
+inline bool isConstant(storm::Polynomial const& p)
+{
+	return p.isConstant();
+}
+#endif
+
+
+
+template<typename T>
+inline bool isZero(T const& v)
+{
+	return v == T(0);
+}
+
+template<>
+inline bool isZero(double const& d)
+{
+	double precision = storm::settings::generalSettings().getPrecision();
+	return std::abs(d) < precision;
+}
+
+#ifdef PARAMETRIC_SYSTEMS
+template<>
+inline bool isZero(storm::RationalFunction const& r)
+{
+	return r.isZero();
+}
+
+template<>
+inline bool isZero(storm::Polynomial const& p)
+{
+	return p.isZero();
+}
+#endif
+
+
+
 template<typename T>
 inline bool isOne(T const& sum)
 {

src/utility/export.h

@@ -0,0 +1,51 @@
+/** 
+ * @file:   export.h
+ * @author: Sebastian Junges
+ *
+ * @since October 7, 2014
+ */
+
+#ifndef STORM_UTILITY_EXPORT_H_
+#define STORM_UTILITY_EXPORT_H_
+
+#include <iostream>
+
+#include "src/storage/parameters.h"
+#include "src/settings/modules/ParametricSettings.h"
+#include "src/modelchecker/reachability/CollectConstraints.h"
+
+namespace storm {
+namespace utility {
+
+template<typename ValueType>	
+void exportParametricMcResult(const ValueType& mcresult, storm::modelchecker::reachability::CollectConstraints<storm::RationalFunction> const& constraintCollector) {
+	std::string path = storm::settings::parametricSettings().exportResultPath();
+	std::ofstream filestream;
+	filestream.open(path);
+	// todo add checks.
+	filestream << "!Parameters: ";
+	std::set<storm::Variable> vars = mcresult.gatherVariables();
+	std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::Variable>(filestream, " "));
+	filestream << std::endl;
+	filestream << "!Result: " << mcresult << std::endl;
+	filestream << "!Well-formed Constraints: " << std::endl;
+	std::copy(constraintCollector.wellformedConstraints().begin(), constraintCollector.wellformedConstraints().end(), std::ostream_iterator<carl::Constraint<ValueType>>(filestream, "\n"));
+	filestream << "!Graph-preserving Constraints: " << std::endl;
+	std::copy(constraintCollector.graphPreservingConstraints().begin(), constraintCollector.graphPreservingConstraints().end(), std::ostream_iterator<carl::Constraint<ValueType>>(filestream, "\n"));
+	filestream.close();
+}
+
+void exportStringStreamToFile(std::stringstream& stream, std::string filepath) {
+	// todo add checks.
+	std::ofstream filestream;
+	filestream.open(filepath);
+	filestream << stream.str();
+	filestream.close();
+}
+
+}
+}
+
+
+
+#endif