diff --git a/src/storage/expressions/ExpressionEvaluation.h b/src/storage/expressions/ExpressionEvaluation.h index 71439792a..89a32b038 100644 --- a/src/storage/expressions/ExpressionEvaluation.h +++ b/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 { diff --git a/src/storage/parameters.h b/src/storage/parameters.h index 8a017638e..5313a0e23 100644 --- a/src/storage/parameters.h +++ b/src/storage/parameters.h @@ -13,8 +13,9 @@ namespace storm // typedef carl::MultivariatePolynomial Polynomial; typedef carl::Variable Variable; typedef carl::MultivariatePolynomial RawPolynomial; - typedef carl::FactorizedPolynomial Polynomial; -// typedef RawPolynomial Polynomial; +// typedef carl::FactorizedPolynomial Polynomial; + + typedef RawPolynomial Polynomial; typedef carl::CompareRelation CompareRelation; typedef carl::RationalFunction RationalFunction; diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp index 967e39813..109cebb8a 100644 --- a/src/stormParametric.cpp +++ b/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 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()) { diff --git a/src/utility/export.h b/src/utility/export.h index 943da4608..35386e6a8 100644 --- a/src/utility/export.h +++ b/src/utility/export.h @@ -25,7 +25,7 @@ void exportParametricMcResult(const ValueType& mcresult, storm::modelchecker::re // todo add checks. filestream << "!Parameters: "; std::set vars = mcresult.gatherVariables(); - std::copy(vars.begin(), vars.end(), std::ostream_iterator(filestream, " ")); + std::copy(vars.begin(), vars.end(), std::ostream_iterator(filestream, ", ")); filestream << std::endl; filestream << "!Result: " << mcresult << std::endl; filestream << "!Well-formed Constraints: " << std::endl;