Browse Source

Fixed tests

tempestpy_adaptions
TimQu 8 years ago
parent
commit
9350187895
  1. 4
      src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp
  2. 5
      src/storm-pars/storage/ParameterRegion.cpp
  3. 1
      src/storm-pars/storage/ParameterRegion.h

4
src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp

@ -91,8 +91,8 @@ namespace storm {
return result;
}
bool hasSatPoint = result == RegionResult::ExistsViolated || result == RegionResult::CenterViolated;
bool hasViolatedPoint = result == RegionResult::ExistsSat || result == RegionResult::CenterSat;
bool hasSatPoint = result == RegionResult::ExistsSat || result == RegionResult::CenterSat;
bool hasViolatedPoint = result == RegionResult::ExistsViolated || result == RegionResult::CenterViolated;
// Check if there is a point in the region for which the property is satisfied
auto vertices = region.getVerticesOfRegion(region.getVariables());

5
src/storm-pars/storage/ParameterRegion.cpp

@ -7,6 +7,11 @@
namespace storm {
namespace storage {
template<typename ParametricType>
ParameterRegion<ParametricType>::ParameterRegion() {
init();
}
template<typename ParametricType>
ParameterRegion<ParametricType>::ParameterRegion(Valuation const& lowerBoundaries, Valuation const& upperBoundaries) : lowerBoundaries(lowerBoundaries), upperBoundaries(upperBoundaries) {
init();

1
src/storm-pars/storage/ParameterRegion.h

@ -13,6 +13,7 @@ namespace storm {
typedef typename storm::utility::parametric::CoefficientType<ParametricType>::type CoefficientType;
typedef typename storm::utility::parametric::Valuation<ParametricType> Valuation;
ParameterRegion();
ParameterRegion(Valuation const& lowerBoundaries, Valuation const& upperBoundaries);
ParameterRegion(Valuation&& lowerBoundaries, Valuation&& upperBoundaries);
ParameterRegion(ParameterRegion const& other) = default;
Loading…
Cancel
Save