Too tired for a message.

Former-commit-id: cfe6fc9037

src/storage/expressions/ExpressionEvaluation.h

@@ -110,7 +110,8 @@ namespace storm {
 				auto it =  mSharedState->find(varName);
 				if(it != mSharedState->end())
 				{
-                    mValue = T(typename T::PolyType(typename T::PolyType::PolyType(it->second), cache));
+                    mValue = convertVariableToPolynomial(it->second);
+//                    mValue = T(typename T::PolyType(typename T::PolyType::PolyType(it->second), cache));
 				}
 				else
 				{

src/storage/parameters.h

@@ -13,8 +13,9 @@ namespace storm
 //	typedef carl::MultivariatePolynomial<cln::cl_RA> Polynomial;
 	typedef carl::Variable  Variable;
     typedef carl::MultivariatePolynomial<cln::cl_RA> RawPolynomial;
-    typedef carl::FactorizedPolynomial<RawPolynomial> Polynomial;
-//    typedef RawPolynomial Polynomial;
+//    typedef carl::FactorizedPolynomial<RawPolynomial> Polynomial;
+
+    typedef RawPolynomial Polynomial;
 	
 	typedef carl::CompareRelation CompareRelation;
 	typedef carl::RationalFunction<Polynomial> RationalFunction;

src/stormParametric.cpp

@@ -10,7 +10,7 @@
 #include "src/utility/export.h"
 #include "src/modelchecker/reachability/CollectConstraints.h"
 
-#include "src/modelchecker/reachability/DirectEncoding.h"
+//#include "src/modelchecker/reachability/DirectEncoding.h"
 #include "src/storage/DeterministicModelStrongBisimulationDecomposition.h"
 #include "src/modelchecker/reachability/SparseSccModelChecker.h"
 #include "src/storage/parameters.h"
@@ -171,7 +171,9 @@ int main(const int argc, const char** argv) {
         storm::modelchecker::reachability::SparseSccModelChecker<storm::RationalFunction> modelchecker;
 
         storm::RationalFunction valueFunction = modelchecker.computeReachabilityProbability(*dtmc, filterFormula);
-        STORM_PRINT_AND_LOG(std::endl << "computed value " << valueFunction << std::endl);
+//        STORM_PRINT_AND_LOG(std::endl << "Result: (" << carl::computePolynomial(valueFunction.nominator()) << ") / (" << carl::computePolynomial(valueFunction.denominator()) << ")" << std::endl);
+        STORM_PRINT_AND_LOG(std::endl << "Result: (" << valueFunction.nominator() << ") / (" << valueFunction.denominator() << ")" << std::endl);
+        STORM_PRINT_AND_LOG(std::endl << "Result: " << valueFunction << std::endl);
     
 //    // Perform bisimulation minimization if requested.
 //    if (storm::settings::generalSettings().isBisimulationSet()) {
@@ -180,7 +182,7 @@ int main(const int argc, const char** argv) {
 //        
 //        dtmc->printModelInformationToStream(std::cout);
 //    }
-//
+
 //    storm::RationalFunction valueFunction2 = modelchecker.computeReachabilityProbability(*dtmc, filterFormula);
 //    STORM_PRINT_AND_LOG(std::endl << "computed value2 " << valueFunction2 << std::endl);
 //
@@ -198,7 +200,7 @@ int main(const int argc, const char** argv) {
                 parameters.insert(p);
             }
         }
-        //
+    
         STORM_LOG_ASSERT(parameters == valueFunction.gatherVariables(), "Parameters in result and program definition do not coincide.");
         
         if(storm::settings::parametricSettings().exportResultToFile()) {

src/utility/export.h

@@ -25,7 +25,7 @@ void exportParametricMcResult(const ValueType& mcresult, storm::modelchecker::re
 	// todo add checks.
 	filestream << "!Parameters: ";
 	std::set<storm::Variable> vars = mcresult.gatherVariables();
-	std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::Variable>(filestream, " "));
+	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;