Browse Source

minor changes...

Former-commit-id: d4932f0343
tempestpy_adaptions
TimQu 9 years ago
parent
commit
1a0bf89671
  1. 4
      src/modelchecker/region/SparseDtmcRegionModelChecker.cpp
  2. 8
      src/modelchecker/region/SparseDtmcRegionModelChecker.h
  3. 9
      src/utility/regions.cpp

4
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){

8
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.

9
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));
}

Loading…
Cancel
Save