From 1a0bf89671704ddbb36038d7097b99f6173eb68f Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@rwth-aachen.de>
Date: Tue, 11 Aug 2015 13:15:05 +0200
Subject: [PATCH] minor changes...
Former-commit-id: d4932f03431da27158115b3ffe9b91b9b80ea171
---
src/modelchecker/region/SparseDtmcRegionModelChecker.cpp | 4 ++--
src/modelchecker/region/SparseDtmcRegionModelChecker.h | 8 +++++---
src/utility/regions.cpp | 9 ++-------
3 files changed, 9 insertions(+), 12 deletions(-)
diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp
index e507a23d5..ba87f778f 100644
--- a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp
+++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp
@@ -236,7 +236,7 @@ namespace storm {
STORM_LOG_THROW(this->probabilityOperatorFormula!=nullptr, storm::exceptions::InvalidStateException, "Tried to analyze a region although no property has been specified" );
STORM_LOG_DEBUG("Analyzing the region " << region.toString());
-
+ //std::cout << "Analyzing the region " << region.toString() << std::endl;
//switches for the different steps.
bool done=false;
@@ -395,7 +395,7 @@ namespace storm {
}
break;
default:
- STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The checkresult of the current region should not be conclusive, i.e. it should be either EXISTSSAT or EXISTSVIOLATED or UNKNOWN");
+ STORM_LOG_WARN("The checkresult of the current region should not be conclusive, i.e. it should be either EXISTSSAT or EXISTSVIOLATED or UNKNOWN in order to apply approximative probabilities");
}
if(region.getCheckResult()==RegionCheckResult::UNKNOWN){
diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.h b/src/modelchecker/region/SparseDtmcRegionModelChecker.h
index 0dca1f257..0e37c51e2 100644
--- a/src/modelchecker/region/SparseDtmcRegionModelChecker.h
+++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.h
@@ -31,9 +31,7 @@ namespace storm {
};
class ParameterRegion;
- class ApproximationModel;
- class SamplingModel;
-
+
explicit SparseDtmcRegionModelChecker(storm::models::sparse::Dtmc<ParametricType> const& model);
/*!
@@ -81,6 +79,10 @@ namespace storm {
private:
+ class ApproximationModel;
+ class SamplingModel;
+
+
/*!
* Computes a model with a single target and a single sink state.
* Eliminates all states for which the outgoing transitions are constant.
diff --git a/src/utility/regions.cpp b/src/utility/regions.cpp
index 1cd013f81..92a072ad3 100644
--- a/src/utility/regions.cpp
+++ b/src/utility/regions.cpp
@@ -56,13 +56,8 @@ namespace storm {
template<>
storm::RationalNumber convertNumber<std::string, storm::RationalNumber>(std::string const& number){
- if(number.find('e')!=std::string::npos){
- //carl::rationalize does not seem to like the scientific notation like (e-05).
- //A quick and easy fix is to parse the number as double and then as a rational number.
- STORM_LOG_WARN("Parsing number " + number + " might result in precision issues as we are going to interprete it as double and then convert the double to a rational number")
- return convertNumber<double, storm::RationalNumber>(convertNumber<std::string, double>(number));
- }
- return carl::rationalize<storm::RationalNumber>(number);
+ //We parse the number as double and then convert it to a a rational number.
+ return convertNumber<double, storm::RationalNumber>(convertNumber<std::string, double>(number));
}