diff --git a/CMakeLists.txt b/CMakeLists.txt index b1900b90e..87862088e 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -243,7 +243,7 @@ configure_file ( # Configure a header file to pass the storm version to the source code configure_file ( "${PROJECT_SOURCE_DIR}/storm-version.cpp.in" - "${PROJECT_SOURCE_DIR}/src/utility/storm-version.cpp" + "${PROJECT_BINARY_DIR}/src/utility/storm-version.cpp" ) # Add the binary dir include directory for storm-config.h diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index ca28a9d3e..89cdb7525 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -11,6 +11,7 @@ #include "src/utility/prism.h" #include "src/utility/macros.h" +#include "src/utility/ConstantsComparator.h" #include "src/exceptions/WrongFormatException.h" #include "src/exceptions/InvalidArgumentException.h" diff --git a/src/builder/ExplicitPrismModelBuilder.h b/src/builder/ExplicitPrismModelBuilder.h index b7ee7fa9c..5fa7e363c 100644 --- a/src/builder/ExplicitPrismModelBuilder.h +++ b/src/builder/ExplicitPrismModelBuilder.h @@ -24,6 +24,10 @@ #include "src/utility/prism.h" namespace storm { + namespace utility { + template class ConstantsComparator; + } + namespace builder { using namespace storm::utility::prism; diff --git a/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp b/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp index a3e900e50..ea84781a4 100644 --- a/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp @@ -45,8 +45,7 @@ namespace storm { std::unique_ptr HybridCtmcCslHelper::computeBoundedUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // If the time bounds are [0, inf], we rather call untimed reachability. - storm::utility::ConstantsComparator comparator; - if (comparator.isZero(lowerBound) && comparator.isInfinity(upperBound)) { + if (lowerBound == storm::utility::zero() && upperBound == storm::utility::infinity()) { return computeUntilProbabilities(model, rateMatrix, exitRateVector, phiStates, psiStates, qualitative, linearEquationSolverFactory); } @@ -61,11 +60,11 @@ namespace storm { STORM_LOG_INFO("Found " << statesWithProbabilityGreater0NonPsi.getNonZeroCount() << " 'maybe' states."); if (!statesWithProbabilityGreater0NonPsi.isZero()) { - if (comparator.isZero(upperBound)) { + if (upperBound == storm::utility::zero()) { // In this case, the interval is of the form [0, 0]. return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), psiStates.toAdd())); } else { - if (comparator.isZero(lowerBound)) { + if (lowerBound == storm::utility::zero()) { // In this case, the interval is of the form [0, t]. // Note that this excludes [0, inf] since this is untimed reachability and we considered this case earlier. @@ -93,7 +92,7 @@ namespace storm { return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), (psiStates || !statesWithProbabilityGreater0) && model.getReachableStates(), psiStates.toAdd(), statesWithProbabilityGreater0NonPsi, odd, subresult)); - } else if (comparator.isInfinity(upperBound)) { + } else if (upperBound == storm::utility::infinity()) { // In this case, the interval is of the form [t, inf] with t != 0. // Start by computing the (unbounded) reachability probabilities of reaching psi states while diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index deb458f42..e4bf7883f 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -25,8 +25,7 @@ namespace storm { uint_fast64_t numberOfStates = rateMatrix.getRowCount(); // If the time bounds are [0, inf], we rather call untimed reachability. - storm::utility::ConstantsComparator comparator; - if (comparator.isZero(lowerBound) && comparator.isInfinity(upperBound)) { + if (lowerBound == storm::utility::zero() && upperBound == storm::utility::infinity()) { return computeUntilProbabilities(rateMatrix, backwardTransitions, exitRates, phiStates, psiStates, qualitative, linearEquationSolverFactory); } @@ -44,12 +43,12 @@ namespace storm { STORM_LOG_INFO("Found " << statesWithProbabilityGreater0NonPsi.getNumberOfSetBits() << " 'maybe' states."); if (!statesWithProbabilityGreater0NonPsi.empty()) { - if (comparator.isZero(upperBound)) { + if (upperBound == storm::utility::zero()) { // In this case, the interval is of the form [0, 0]. result = std::vector(numberOfStates, storm::utility::zero()); storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); } else { - if (comparator.isZero(lowerBound)) { + if (lowerBound == storm::utility::zero()) { // In this case, the interval is of the form [0, t]. // Note that this excludes [0, inf] since this is untimed reachability and we considered this case earlier. @@ -77,7 +76,7 @@ namespace storm { storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0NonPsi, subresult); storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); - } else if (comparator.isInfinity(upperBound)) { + } else if (upperBound == storm::utility::infinity()) { // In this case, the interval is of the form [t, inf] with t != 0. // Start by computing the (unbounded) reachability probabilities of reaching psi states while diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index a16ec2089..61ba12df0 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -535,7 +535,7 @@ namespace storm { // treating all states that have some non-zero probability to go to a target state in one step. storm::storage::BitVector pseudoTargetStates(transitionMatrix.getRowCount()); for (std::size_t index = 0; index < oneStepProbabilities.size(); ++index) { - if (!comparator.isZero(oneStepProbabilities[index])) { + if (oneStepProbabilities[index] != storm::utility::zero()) { pseudoTargetStates.set(index); } } @@ -687,7 +687,7 @@ namespace storm { // Scale all entries in this row with (1 / (1 - loopProbability)) only in case there was a self-loop. std::size_t scaledSuccessors = 0; if (hasSelfLoop) { - STORM_LOG_ASSERT(!comparator.isOne(loopProbability), "Must not eliminate state with probability 1 self-loop."); + STORM_LOG_ASSERT(loopProbability != storm::utility::one(), "Must not eliminate state with probability 1 self-loop."); loopProbability = storm::utility::one() / (storm::utility::one() - loopProbability); storm::utility::simplify(loopProbability); for (auto& entry : matrix.getRow(state)) { @@ -940,16 +940,13 @@ namespace storm { typename SparseDtmcEliminationModelChecker::FlexibleSparseMatrix SparseDtmcEliminationModelChecker::getFlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix, bool setAllValuesToOne) { FlexibleSparseMatrix flexibleMatrix(matrix.getRowCount()); - // A comparator used for comparing probabilities. - storm::utility::ConstantsComparator comparator; - for (typename FlexibleSparseMatrix::index_type rowIndex = 0; rowIndex < matrix.getRowCount(); ++rowIndex) { typename storm::storage::SparseMatrix::const_rows row = matrix.getRow(rowIndex); flexibleMatrix.reserveInRow(rowIndex, row.getNumberOfEntries()); for (auto const& element : row) { // If the probability is zero, we skip this entry. - if (comparator.isZero(element.getValue())) { + if (element.getValue() == storm::utility::zero()) { continue; } diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index 7dd35bb17..0648ad9e5 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -66,9 +66,6 @@ namespace storm { void eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions, boost::optional>& stateRewards, bool removeForwardTransitions = true, bool constrained = false, storm::storage::BitVector const& predecessorConstraint = storm::storage::BitVector()); std::vector getStatePriorities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities); - - // A comparator that can be used to compare constants. - storm::utility::ConstantsComparator comparator; }; } // namespace modelchecker diff --git a/src/models/sparse/Dtmc.cpp b/src/models/sparse/Dtmc.cpp index 80dabaa2c..733c8497c 100644 --- a/src/models/sparse/Dtmc.cpp +++ b/src/models/sparse/Dtmc.cpp @@ -4,6 +4,7 @@ #include "src/exceptions/NotImplementedException.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/utility/constants.h" +#include "src/utility/ConstantsComparator.h" namespace storm { namespace models { @@ -197,6 +198,7 @@ namespace storm { template void Dtmc::ConstraintCollector::process(storm::models::sparse::Dtmc const& dtmc) { + storm::utility::ConstantsComparator comparator; for(uint_fast64_t state = 0; state < dtmc.getNumberOfStates(); ++state) { ValueType sum = storm::utility::zero(); for (auto const& transition : dtmc.getRows(state)) { diff --git a/src/models/sparse/Dtmc.h b/src/models/sparse/Dtmc.h index 730f3d03e..f5537a561 100644 --- a/src/models/sparse/Dtmc.h +++ b/src/models/sparse/Dtmc.h @@ -68,9 +68,6 @@ namespace storm { // on the parameter values. std::unordered_set> graphPreservingConstraintSet; - // A comparator that is used for - storm::utility::ConstantsComparator comparator; - public: /*! * Constructs the a constraint collector for the given DTMC. The constraints are built and ready for diff --git a/src/models/sparse/Mdp.cpp b/src/models/sparse/Mdp.cpp index 4d62741e9..7d26280df 100644 --- a/src/models/sparse/Mdp.cpp +++ b/src/models/sparse/Mdp.cpp @@ -5,6 +5,7 @@ #include "src/adapters/CarlAdapter.h" #include "src/models/sparse/StandardRewardModel.h" +#include "src/utility/ConstantsComparator.h" namespace storm { namespace models { diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp index f362da110..b861f8f2c 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp @@ -14,6 +14,7 @@ #include "src/utility/graph.h" #include "src/utility/constants.h" +#include "src/utility/ConstantsComparator.h" #include "src/exceptions/IllegalFunctionCallException.h" #include "src/exceptions/InvalidOptionException.h" #include "src/exceptions/InvalidArgumentException.h" @@ -718,15 +719,16 @@ namespace storm { } Partition initialPartition; + storm::utility::ConstantsComparator comparator; if (options.measureDrivenInitialPartition) { STORM_LOG_THROW(options.phiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi states."); STORM_LOG_THROW(options.psiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without psi states."); - initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, options.phiStates.get(), options.psiStates.get(), bisimulationType, options.keepRewards, options.bounded); + initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, options.phiStates.get(), options.psiStates.get(), bisimulationType, options.keepRewards, options.bounded, comparator); } else { - initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions, options.keepRewards); + initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions, options.keepRewards, comparator); } - partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, options.keepRewards, options.buildQuotient); + partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, options.keepRewards, options.buildQuotient, comparator); } template @@ -745,15 +747,16 @@ namespace storm { } Partition initialPartition; + storm::utility::ConstantsComparator comparator; if (options.measureDrivenInitialPartition) { STORM_LOG_THROW(options.phiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states."); STORM_LOG_THROW(options.psiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states."); - initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, options.phiStates.get(), options.psiStates.get(), bisimulationType, options.keepRewards, options.bounded); + initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, options.phiStates.get(), options.psiStates.get(), bisimulationType, options.keepRewards, options.bounded, comparator); } else { - initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions, options.keepRewards); + initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions, options.keepRewards, comparator); } - partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, options.keepRewards, options.buildQuotient); + partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, options.keepRewards, options.buildQuotient, comparator); } template @@ -764,7 +767,7 @@ namespace storm { template template - void DeterministicModelBisimulationDecomposition::buildQuotient(ModelType const& model, std::set const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType, bool keepRewards) { + void DeterministicModelBisimulationDecomposition::buildQuotient(ModelType const& model, std::set const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType, bool keepRewards, storm::utility::ConstantsComparator const& comparator) { // In order to create the quotient model, we need to construct // (a) the new transition matrix, // (b) the new labeling, @@ -889,7 +892,7 @@ namespace storm { template template - void DeterministicModelBisimulationDecomposition::partitionRefinement(ModelType const& model, std::set const& atomicPropositions, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool keepRewards, bool buildQuotient) { + void DeterministicModelBisimulationDecomposition::partitionRefinement(ModelType const& model, std::set const& atomicPropositions, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool keepRewards, bool buildQuotient, storm::utility::ConstantsComparator const& comparator) { std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now(); // Initially, all blocks are potential splitter, so we insert them in the splitterQueue. @@ -909,7 +912,7 @@ namespace storm { splitter->unmarkAsSplitter(); // Now refine the partition using the current splitter. - refinePartition(model.getTransitionMatrix(), backwardTransitions, *splitter, partition, bisimulationType, splitterQueue); + refinePartition(model.getTransitionMatrix(), backwardTransitions, *splitter, partition, bisimulationType, splitterQueue, comparator); } std::chrono::high_resolution_clock::duration refinementTime = std::chrono::high_resolution_clock::now() - refinementStart; @@ -928,7 +931,7 @@ namespace storm { // If we are required to build the quotient model, do so now. if (buildQuotient) { - this->buildQuotient(model, atomicPropositions, partition, bisimulationType, keepRewards); + this->buildQuotient(model, atomicPropositions, partition, bisimulationType, keepRewards, comparator); } std::chrono::high_resolution_clock::duration extractionTime = std::chrono::high_resolution_clock::now() - extractionStart; @@ -949,7 +952,7 @@ namespace storm { } template - void DeterministicModelBisimulationDecomposition::refineBlockProbabilities(Block& block, Partition& partition, BisimulationType bisimulationType, std::deque& splitterQueue) { + void DeterministicModelBisimulationDecomposition::refineBlockProbabilities(Block& block, Partition& partition, BisimulationType bisimulationType, std::deque& splitterQueue, storm::utility::ConstantsComparator const& comparator) { // Sort the states in the block based on their probabilities. std::sort(partition.getBegin(block), partition.getEnd(block), [&partition] (std::pair const& a, std::pair const& b) { return a.second < b.second; } ); @@ -998,8 +1001,8 @@ namespace storm { } template - void DeterministicModelBisimulationDecomposition::refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, std::deque& splitterQueue) { - std::vector splitPoints = getSplitPointsWeak(block, partition); + void DeterministicModelBisimulationDecomposition::refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, std::deque& splitterQueue, storm::utility::ConstantsComparator const& comparator) { + std::vector splitPoints = getSplitPointsWeak(block, partition, comparator); // Restore the original begin of the block. block.setBegin(block.getOriginalBegin()); @@ -1118,7 +1121,7 @@ namespace storm { } template - std::vector DeterministicModelBisimulationDecomposition::getSplitPointsWeak(Block& block, Partition& partition) { + std::vector DeterministicModelBisimulationDecomposition::getSplitPointsWeak(Block& block, Partition& partition, storm::utility::ConstantsComparator const& comparator) { std::vector result; // We first scale all probabilities with (1-p[s]) where p[s] is the silent probability of state s. std::for_each(partition.getStatesAndValues().begin() + block.getOriginalBegin(), partition.getStatesAndValues().begin() + block.getBegin(), [&] (std::pair& stateValuePair) { @@ -1168,7 +1171,7 @@ namespace storm { } template - void DeterministicModelBisimulationDecomposition::refinePartition(storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, BisimulationType bisimulationType, std::deque& splitterQueue) { + void DeterministicModelBisimulationDecomposition::refinePartition(storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, BisimulationType bisimulationType, std::deque& splitterQueue, storm::utility::ConstantsComparator const& comparator) { std::list predecessorBlocks; // Iterate over all states of the splitter and check its predecessors. @@ -1307,7 +1310,7 @@ namespace storm { continue; } - refineBlockProbabilities(*blockPtr, partition, bisimulationType, splitterQueue); + refineBlockProbabilities(*blockPtr, partition, bisimulationType, splitterQueue, comparator); } } else { // In this case, we are computing a weak bisimulation on a DTMC. // If the splitter was a predecessor of itself and we are computing a weak bisimulation, we need to update @@ -1324,7 +1327,7 @@ namespace storm { // If the splitter is also the predecessor block, we must not refine it at this point. if (&block != &splitter) { - refineBlockWeak(block, partition, forwardTransitions, backwardTransitions, splitterQueue); + refineBlockWeak(block, partition, forwardTransitions, backwardTransitions, splitterQueue, comparator); } else { // Restore the begin of the block. block.setBegin(block.getOriginalBegin()); @@ -1340,7 +1343,7 @@ namespace storm { template template - typename DeterministicModelBisimulationDecomposition::Partition DeterministicModelBisimulationDecomposition::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, BisimulationType bisimulationType, bool keepRewards, bool bounded) { + typename DeterministicModelBisimulationDecomposition::Partition DeterministicModelBisimulationDecomposition::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, BisimulationType bisimulationType, bool keepRewards, bool bounded, storm::utility::ConstantsComparator const& comparator) { std::pair statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates, psiStates); boost::optional representativePsiState; @@ -1353,7 +1356,7 @@ namespace storm { // If the model has state rewards, we need to consider them, because otherwise reward properties are not // preserved. if (keepRewards && model.hasRewardModel()) { - this->splitRewards(model.getUniqueRewardModel()->second.getStateRewardVector(), partition); + this->splitRewards(model.getUniqueRewardModel()->second.getStateRewardVector(), partition, comparator); } // If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent @@ -1436,7 +1439,7 @@ namespace storm { template template - typename DeterministicModelBisimulationDecomposition::Partition DeterministicModelBisimulationDecomposition::getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, BisimulationType bisimulationType, boost::optional> const& atomicPropositions, bool keepRewards) { + typename DeterministicModelBisimulationDecomposition::Partition DeterministicModelBisimulationDecomposition::getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, BisimulationType bisimulationType, boost::optional> const& atomicPropositions, bool keepRewards, storm::utility::ConstantsComparator const& comparator) { Partition partition(model.getNumberOfStates(), bisimulationType == BisimulationType::WeakDtmc); if (atomicPropositions) { @@ -1458,7 +1461,7 @@ namespace storm { // If the model has state rewards, we need to consider them, because otherwise reward properties are not // preserved. if (keepRewards && model.hasRewardModel()) { - this->splitRewards(model.getUniqueRewardModel()->second.getStateRewardVector(), partition); + this->splitRewards(model.getUniqueRewardModel()->second.getStateRewardVector(), partition, comparator); } // If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent @@ -1489,7 +1492,7 @@ namespace storm { } template - void DeterministicModelBisimulationDecomposition::splitRewards(std::vector const& stateRewardVector, Partition& partition) { + void DeterministicModelBisimulationDecomposition::splitRewards(std::vector const& stateRewardVector, Partition& partition, storm::utility::ConstantsComparator const& comparator) { for (auto& block : partition.getBlocks()) { std::sort(partition.getBegin(block), partition.getEnd(block), [&stateRewardVector] (std::pair const& a, std::pair const& b) { return stateRewardVector[a.first] < stateRewardVector[b.first]; } ); diff --git a/src/storage/DeterministicModelBisimulationDecomposition.h b/src/storage/DeterministicModelBisimulationDecomposition.h index 56cbbd590..3b0fba916 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.h +++ b/src/storage/DeterministicModelBisimulationDecomposition.h @@ -15,6 +15,10 @@ #include "src/utility/OsDetection.h" namespace storm { + namespace utility { + template class ConstantsComparator; + } + namespace storage { /*! @@ -455,9 +459,10 @@ namespace storm { * @param bisimulationType The kind of bisimulation that is to be computed. * @param buildQuotient If set, the quotient model is built and may be retrieved using the getQuotient() * method. + * @param comparator A comparator used for comparing constants. */ template - void partitionRefinement(ModelType const& model, std::set const& atomicPropositions, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool keepRewards, bool buildQuotient); + void partitionRefinement(ModelType const& model, std::set const& atomicPropositions, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool keepRewards, bool buildQuotient, storm::utility::ConstantsComparator const& comparator); /*! * Refines the partition based on the provided splitter. After calling this method all blocks are stable @@ -471,8 +476,9 @@ namespace storm { * @param bisimulationType The kind of bisimulation that is to be computed. * @param splitterQueue A queue into which all blocks that were split are inserted so they can be treated * as splitters in the future. + * @param comparator A comparator used for comparing constants. */ - void refinePartition(storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, BisimulationType bisimulationType, std::deque& splitterQueue); + void refinePartition(storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, BisimulationType bisimulationType, std::deque& splitterQueue, storm::utility::ConstantsComparator const& comparator); /*! * Refines the block based on their probability values (leading into the splitter). @@ -482,18 +488,20 @@ namespace storm { * @param bisimulationType The kind of bisimulation that is to be computed. * @param splitterQueue A queue into which all blocks that were split are inserted so they can be treated * as splitters in the future. + * @param comparator A comparator used for comparing constants. */ - void refineBlockProbabilities(Block& block, Partition& partition, BisimulationType bisimulationType, std::deque& splitterQueue); + void refineBlockProbabilities(Block& block, Partition& partition, BisimulationType bisimulationType, std::deque& splitterQueue, storm::utility::ConstantsComparator const& comparator); - void refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, std::deque& splitterQueue); + void refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, std::deque& splitterQueue, storm::utility::ConstantsComparator const& comparator); /*! * Determines the split offsets in the given block. * * @param block The block that is to be analyzed for splits. * @param partition The partition that contains the block. + * @param comparator A comparator used for comparing constants. */ - std::vector getSplitPointsWeak(Block& block, Partition& partition); + std::vector getSplitPointsWeak(Block& block, Partition& partition, storm::utility::ConstantsComparator const& comparator); /*! * Builds the quotient model based on the previously computed equivalence classes (stored in the blocks @@ -506,9 +514,10 @@ namespace storm { * @param partition The previously computed partition. This is used for quickly retrieving the block of a * state. * @param bisimulationType The kind of bisimulation that is to be computed. + * @param comparator A comparator used for comparing constants. */ template - void buildQuotient(ModelType const& model, std::set const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType, bool keepRewards); + void buildQuotient(ModelType const& model, std::set const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType, bool keepRewards, storm::utility::ConstantsComparator const& comparator); /*! * Creates the measure-driven initial partition for reaching psi states from phi states. @@ -521,10 +530,11 @@ namespace storm { * @param bisimulationType The kind of bisimulation that is to be computed. * @param bounded If set to true, the initial partition will be chosen in such a way that preserves bounded * reachability queries. + * @param comparator A comparator used for comparing constants. * @return The resulting partition. */ template - Partition getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, BisimulationType bisimulationType, bool keepRewards = true, bool bounded = false); + Partition getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, BisimulationType bisimulationType, bool keepRewards = true, bool bounded = false, storm::utility::ConstantsComparator const& comparator = storm::utility::ConstantsComparator()); /*! * Creates the initial partition based on all the labels in the given model. @@ -534,10 +544,11 @@ namespace storm { * @param bisimulationType The kind of bisimulation that is to be computed. * @param atomicPropositions The set of atomic propositions to respect. If not given, then all atomic * propositions of the model are respected. + * @param comparator A comparator used for comparing constants. * @return The resulting partition. */ template - Partition getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, BisimulationType bisimulationType, boost::optional> const& atomicPropositions = boost::optional>(), bool keepRewards = true); + Partition getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, BisimulationType bisimulationType, boost::optional> const& atomicPropositions = boost::optional>(), bool keepRewards = true, storm::utility::ConstantsComparator const& comparator = storm::utility::ConstantsComparator()); /*! * Splits all blocks of the given partition into a block that contains all divergent states and another block @@ -565,14 +576,12 @@ namespace storm { * * @param stateRewardVector The state reward vector of the model. * @param partition The partition that is to be split. + * @param comparator A comparator used for comparing constants. */ - void splitRewards(std::vector const& stateRewardVector, Partition& partition); + void splitRewards(std::vector const& stateRewardVector, Partition& partition, storm::utility::ConstantsComparator const& comparator); // If required, a quotient model is built and stored in this member. std::shared_ptr> quotient; - - // A comparator that is used for determining whether two probabilities are considered to be equal. - storm::utility::ConstantsComparator comparator; }; } } diff --git a/src/storage/StronglyConnectedComponentDecomposition.cpp b/src/storage/StronglyConnectedComponentDecomposition.cpp index c49e6977f..fe2c60e4e 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storage/StronglyConnectedComponentDecomposition.cpp @@ -188,7 +188,7 @@ namespace storm { p.push_back(currentState); for (auto const& successor : transitionMatrix.getRowGroup(currentState)) { - if (subsystem.get(successor.getColumn()) && !comparator.isZero(successor.getValue())) { + if (subsystem.get(successor.getColumn()) && successor.getValue() != storm::utility::zero()) { if (currentState == successor.getColumn()) { statesWithSelfLoop.set(currentState); } diff --git a/src/storage/StronglyConnectedComponentDecomposition.h b/src/storage/StronglyConnectedComponentDecomposition.h index 12da304da..9d4e8f157 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.h +++ b/src/storage/StronglyConnectedComponentDecomposition.h @@ -180,9 +180,6 @@ namespace storm { * is increased. */ void performSccDecompositionGCM(storm::storage::SparseMatrix const& transitionMatrix, uint_fast64_t startState, storm::storage::BitVector& statesWithSelfLoop, storm::storage::BitVector const& subsystem, uint_fast64_t& currentIndex, storm::storage::BitVector& hasPreorderNumber, std::vector& preorderNumbers, std::vector& s, std::vector& p, storm::storage::BitVector& stateHasScc, std::vector& stateToSccMapping, uint_fast64_t& sccCount); - - // A comparator that is used to compare values. - storm::utility::ConstantsComparator comparator; }; } } diff --git a/src/utility/ConstantsComparator.cpp b/src/utility/ConstantsComparator.cpp new file mode 100644 index 000000000..de027d541 --- /dev/null +++ b/src/utility/ConstantsComparator.cpp @@ -0,0 +1,142 @@ +#include "src/utility/ConstantsComparator.h" + +#include "src/utility/constants.h" +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" + +namespace storm { + namespace utility { + template + bool ConstantsComparator::isOne(ValueType const& value) const { + return value == one(); + } + + template + bool ConstantsComparator::isZero(ValueType const& value) const { + return value == zero(); + } + + template + bool ConstantsComparator::isEqual(ValueType const& value1, ValueType const& value2) const { + return value1 == value2; + } + + template + bool ConstantsComparator::isConstant(ValueType const& value) const { + return true; + } + + template + bool ConstantsComparator::isInfinity(ValueType const& value) const { + return false; + } + + ConstantsComparator::ConstantsComparator() : precision(static_cast(storm::settings::generalSettings().getPrecision())) { + // Intentionally left empty. + } + + ConstantsComparator::ConstantsComparator(float precision) : precision(precision) { + // Intentionally left empty. + } + + bool ConstantsComparator::isOne(float const& value) const { + return std::abs(value - one()) <= precision; + } + + bool ConstantsComparator::isZero(float const& value) const { + return std::abs(value) <= precision; + } + + bool ConstantsComparator::isEqual(float const& value1, float const& value2) const { + return std::abs(value1 - value2) <= precision; + } + + bool ConstantsComparator::isConstant(float const& value) const { + return true; + } + + bool ConstantsComparator::isInfinity(float const& value) const { + return value == storm::utility::infinity(); + } + + ConstantsComparator::ConstantsComparator() : precision(storm::settings::generalSettings().getPrecision()) { + // Intentionally left empty. + } + + ConstantsComparator::ConstantsComparator(double precision) : precision(precision) { + // Intentionally left empty. + } + + bool ConstantsComparator::isOne(double const& value) const { + return std::abs(value - one()) <= precision; + } + + bool ConstantsComparator::isZero(double const& value) const { + return std::abs(value) <= precision; + } + + bool ConstantsComparator::isInfinity(double const& value) const { + return value == infinity(); + } + + bool ConstantsComparator::isEqual(double const& value1, double const& value2) const { + return std::abs(value1 - value2) <= precision; + } + + bool ConstantsComparator::isConstant(double const& value) const { + return true; + } + +#ifdef STORM_HAVE_CARL + ConstantsComparator::ConstantsComparator() { + // Intentionally left empty. + } + + bool ConstantsComparator::isOne(storm::RationalFunction const& value) const { + return value.isOne(); + } + + bool ConstantsComparator::isZero(storm::RationalFunction const& value) const { + return value.isZero(); + } + + bool ConstantsComparator::isEqual(storm::RationalFunction const& value1, storm::RationalFunction const& value2) const { + return value1 == value2; + } + + bool ConstantsComparator::isConstant(storm::RationalFunction const& value) const { + return value.isConstant(); + } + + ConstantsComparator::ConstantsComparator() { + // Intentionally left empty. + } + + bool ConstantsComparator::isOne(storm::Polynomial const& value) const { + return value.isOne(); + } + + bool ConstantsComparator::isZero(storm::Polynomial const& value) const { + return value.isZero(); + } + + bool ConstantsComparator::isEqual(storm::Polynomial const& value1, storm::Polynomial const& value2) const { + return value1 == value2; + } + + bool ConstantsComparator::isConstant(storm::Polynomial const& value) const { + return value.isConstant(); + } +#endif + + // Explicit instantiations. + template class ConstantsComparator; + template class ConstantsComparator; + template class ConstantsComparator; + +#ifdef STORM_HAVE_CARL + template class ConstantsComparator; + template class ConstantsComparator; +#endif + } +} \ No newline at end of file diff --git a/src/utility/ConstantsComparator.h b/src/utility/ConstantsComparator.h new file mode 100644 index 000000000..d04641084 --- /dev/null +++ b/src/utility/ConstantsComparator.h @@ -0,0 +1,109 @@ +#ifndef STORM_UTILITY_CONSTANTSCOMPARATOR_H_ +#define STORM_UTILITY_CONSTANTSCOMPARATOR_H_ + +#include "src/adapters/CarlAdapter.h" + +namespace storm { + namespace utility { + // A class that can be used for comparing constants. + template + class ConstantsComparator { + public: + // This needs to be in here, otherwise the template specializations are not used properly. + ConstantsComparator(); + + bool isOne(ValueType const& value) const; + + bool isZero(ValueType const& value) const; + + bool isEqual(ValueType const& value1, ValueType const& value2) const; + + bool isConstant(ValueType const& value) const; + + bool isInfinity(ValueType const& value) const; + + private: + ValueType precision; + }; + + // For floats we specialize this class and consider the comparison modulo some predefined precision. + template<> + class ConstantsComparator { + public: + ConstantsComparator(); + + ConstantsComparator(float precision); + + bool isOne(float const& value) const; + + bool isZero(float const& value) const; + + bool isEqual(float const& value1, float const& value2) const; + + bool isConstant(float const& value) const; + + bool isInfinity(float const& value) const; + + private: + // The precision used for comparisons. + float precision; + }; + + // For doubles we specialize this class and consider the comparison modulo some predefined precision. + template<> + class ConstantsComparator { + public: + ConstantsComparator(); + + ConstantsComparator(double precision); + + bool isOne(double const& value) const; + + bool isZero(double const& value) const; + + bool isInfinity(double const& value) const; + + bool isEqual(double const& value1, double const& value2) const; + + bool isConstant(double const& value) const; + + private: + // The precision used for comparisons. + double precision; + }; + +#ifdef STORM_HAVE_CARL + template<> + class ConstantsComparator { + public: + ConstantsComparator(); + + bool isOne(storm::RationalFunction const& value) const; + + bool isZero(storm::RationalFunction const& value) const; + + bool isEqual(storm::RationalFunction const& value1, storm::RationalFunction const& value2) const; + + bool isConstant(storm::RationalFunction const& value) const; + }; + + template<> + class ConstantsComparator { + public: + ConstantsComparator(); + + bool isOne(storm::Polynomial const& value) const; + + bool isZero(storm::Polynomial const& value) const; + + bool isEqual(storm::Polynomial const& value1, storm::Polynomial const& value2) const; + + bool isConstant(storm::Polynomial const& value) const; + }; + +#endif + + } +} + +#endif /* STORM_UTILITY_CONSTANTSCOMPARATOR_H_ */ \ No newline at end of file diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp index c3edc2639..ae348ccce 100644 --- a/src/utility/constants.cpp +++ b/src/utility/constants.cpp @@ -59,153 +59,14 @@ namespace storm { return value; } - // For floats we specialize this class and consider the comparison modulo some predefined precision. - template<> - class ConstantsComparator { - public: - ConstantsComparator(); - - ConstantsComparator(float precision); - - bool isOne(float const& value) const; - - bool isZero(float const& value) const; - - bool isEqual(float const& value1, float const& value2) const; - - bool isConstant(float const& value) const; - - private: - // The precision used for comparisons. - float precision; - }; - - // For doubles we specialize this class and consider the comparison modulo some predefined precision. - template<> - class ConstantsComparator { - public: - ConstantsComparator(); - - ConstantsComparator(double precision); - - bool isOne(double const& value) const; - - bool isZero(double const& value) const; - - bool isInfinity(double const& value) const; - - bool isEqual(double const& value1, double const& value2) const; - - bool isConstant(double const& value) const; - - private: - // The precision used for comparisons. - double precision; - }; - #ifdef STORM_HAVE_CARL template<> RationalFunction& simplify(RationalFunction& value); template<> RationalFunction&& simplify(RationalFunction&& value); - - template<> - class ConstantsComparator { - public: - ConstantsComparator(); - - bool isOne(storm::RationalFunction const& value) const; - - bool isZero(storm::RationalFunction const& value) const; - - bool isEqual(storm::RationalFunction const& value1, storm::RationalFunction const& value2) const; - - bool isConstant(storm::RationalFunction const& value) const; - }; - - template<> - class ConstantsComparator { - public: - ConstantsComparator(); - - bool isOne(storm::Polynomial const& value) const; - - bool isZero(storm::Polynomial const& value) const; - - bool isEqual(storm::Polynomial const& value1, storm::Polynomial const& value2) const; - - bool isConstant(storm::Polynomial const& value) const; - }; #endif - template - bool ConstantsComparator::isOne(ValueType const& value) const { - return value == one(); - } - - template - bool ConstantsComparator::isZero(ValueType const& value) const { - return value == zero(); - } - - template - bool ConstantsComparator::isEqual(ValueType const& value1, ValueType const& value2) const { - return value1 == value2; - } - - ConstantsComparator::ConstantsComparator() : precision(static_cast(storm::settings::generalSettings().getPrecision())) { - // Intentionally left empty. - } - - ConstantsComparator::ConstantsComparator(float precision) : precision(precision) { - // Intentionally left empty. - } - - bool ConstantsComparator::isOne(float const& value) const { - return std::abs(value - one()) <= precision; - } - - bool ConstantsComparator::isZero(float const& value) const { - return std::abs(value) <= precision; - } - - bool ConstantsComparator::isEqual(float const& value1, float const& value2) const { - return std::abs(value1 - value2) <= precision; - } - - bool ConstantsComparator::isConstant(float const& value) const { - return true; - } - - ConstantsComparator::ConstantsComparator() : precision(storm::settings::generalSettings().getPrecision()) { - // Intentionally left empty. - } - - ConstantsComparator::ConstantsComparator(double precision) : precision(precision) { - // Intentionally left empty. - } - - bool ConstantsComparator::isOne(double const& value) const { - return std::abs(value - one()) <= precision; - } - - bool ConstantsComparator::isZero(double const& value) const { - return std::abs(value) <= precision; - } - - bool ConstantsComparator::isInfinity(double const& value) const { - return value == infinity(); - } - - bool ConstantsComparator::isEqual(double const& value1, double const& value2) const { - return std::abs(value1 - value2) <= precision; - } - - bool ConstantsComparator::isConstant(double const& value) const { - return true; - } - #ifdef STORM_HAVE_CARL template<> RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) { @@ -229,46 +90,6 @@ namespace storm { value.simplify(); return std::move(value); } - - ConstantsComparator::ConstantsComparator() { - // Intentionally left empty. - } - - bool ConstantsComparator::isOne(storm::RationalFunction const& value) const { - return value.isOne(); - } - - bool ConstantsComparator::isZero(storm::RationalFunction const& value) const { - return value.isZero(); - } - - bool ConstantsComparator::isEqual(storm::RationalFunction const& value1, storm::RationalFunction const& value2) const { - return value1 == value2; - } - - bool ConstantsComparator::isConstant(storm::RationalFunction const& value) const { - return value.isConstant(); - } - - ConstantsComparator::ConstantsComparator() { - // Intentionally left empty. - } - - bool ConstantsComparator::isOne(storm::Polynomial const& value) const { - return value.isOne(); - } - - bool ConstantsComparator::isZero(storm::Polynomial const& value) const { - return value.isZero(); - } - - bool ConstantsComparator::isEqual(storm::Polynomial const& value1, storm::Polynomial const& value2) const { - return value1 == value2; - } - - bool ConstantsComparator::isConstant(storm::Polynomial const& value) const { - return value.isConstant(); - } #endif template @@ -289,10 +110,7 @@ namespace storm { return std::move(matrixEntry); } - // explicit instantiations - // double - template class ConstantsComparator; - + // Explicit instantiations. template double one(); template double zero(); template double infinity(); @@ -305,9 +123,6 @@ namespace storm { template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - // float - template class ConstantsComparator; - template float one(); template float zero(); template float infinity(); @@ -319,9 +134,6 @@ namespace storm { template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - - // int - template class ConstantsComparator; template int one(); template int zero(); @@ -336,9 +148,6 @@ namespace storm { template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); #ifdef STORM_HAVE_CARL - template class ConstantsComparator; - template class ConstantsComparator; - template RationalFunction one(); template RationalFunction zero(); template storm::RationalFunction infinity(); diff --git a/src/utility/constants.h b/src/utility/constants.h index ae2b2c0be..f18590ef3 100644 --- a/src/utility/constants.h +++ b/src/utility/constants.h @@ -1,5 +1,5 @@ -#ifndef STORM_UTILITY_CONSTANTSCOMPARATOR_H_ -#define STORM_UTILITY_CONSTANTSCOMPARATOR_H_ +#ifndef STORM_UTILITY_CONSTANTS_H_ +#define STORM_UTILITY_CONSTANTS_H_ #ifdef max # undef max @@ -12,7 +12,6 @@ #include #include - namespace storm { // Forward-declare MatrixEntry class. @@ -37,24 +36,6 @@ namespace storm { template ValueType simplify(ValueType value); - // A class that can be used for comparing constants. - template - class ConstantsComparator { - public: - // This needs to be in here, otherwise the template specializations are not used properly. - ConstantsComparator(); - - bool isOne(ValueType const& value) const; - - bool isZero(ValueType const& value) const; - - bool isEqual(ValueType const& value1, ValueType const& value2) const; - - bool isConstant(ValueType const& value) const; - - bool isInfinity(ValueType const& value) const; - }; - template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); @@ -63,4 +44,4 @@ namespace storm { } } -#endif /* STORM_UTILITY_CONSTANTSCOMPARATOR_H_ */ \ No newline at end of file +#endif /* STORM_UTILITY_CONSTANTS_H_ */ \ No newline at end of file diff --git a/src/utility/numerical.h b/src/utility/numerical.h index f7b0fd40b..c63151936 100644 --- a/src/utility/numerical.h +++ b/src/utility/numerical.h @@ -12,8 +12,7 @@ namespace storm { namespace numerical { template std::tuple> getFoxGlynnCutoff(ValueType lambda, ValueType underflow, ValueType overflow, ValueType accuracy) { - storm::utility::ConstantsComparator comparator; - STORM_LOG_THROW(!comparator.isZero(lambda), storm::exceptions::InvalidArgumentException, "Error in Fox-Glynn algorithm: lambda must not be zero."); + STORM_LOG_THROW(lambda != storm::utility::zero(), storm::exceptions::InvalidArgumentException, "Error in Fox-Glynn algorithm: lambda must not be zero."); // This code is a modified version of the one in PRISM. According to their implementation, for lambda // smaller than 400, we compute the result using the naive method. diff --git a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp index 4747e90e1..706f8eef3 100644 --- a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp @@ -7,6 +7,7 @@ #include "src/builder/ExplicitPrismModelBuilder.h" #include "src/solver/GmmxxLinearEquationSolver.h" +#include "src/models/sparse/StandardRewardModel.h" #include "src/modelchecker/csl/SparseCtmcCslModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" diff --git a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp index 96656c9ba..d607551fc 100644 --- a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp @@ -8,6 +8,7 @@ #include "src/storage/dd/DdType.h" #include "src/utility/solver.h" +#include "src/models/symbolic/StandardRewardModel.h" #include "src/modelchecker/csl/HybridCtmcCslModelChecker.h" #include "src/modelchecker/results/HybridQuantitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" diff --git a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp index ebfc2bbe6..96c6075b0 100644 --- a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp @@ -7,6 +7,7 @@ #include "src/builder/ExplicitPrismModelBuilder.h" #include "src/utility/solver.h" +#include "src/models/sparse/StandardRewardModel.h" #include "src/modelchecker/csl/SparseCtmcCslModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" diff --git a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp index cff5e8d3d..13792718d 100644 --- a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp @@ -8,6 +8,7 @@ #include "src/storage/dd/DdType.h" #include "src/utility/solver.h" +#include "src/models/symbolic/StandardRewardModel.h" #include "src/modelchecker/csl/HybridCtmcCslModelChecker.h" #include "src/modelchecker/results/HybridQuantitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" diff --git a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp index e7bcd7e65..47508830e 100644 --- a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp @@ -10,7 +10,7 @@ #include "src/parser/FormulaParser.h" #include "src/parser/PrismParser.h" #include "src/builder/DdPrismModelBuilder.h" -#include "src/models/symbolic/Dtmc.h" +#include "src/models/symbolic/Mdp.h" #include "src/models/symbolic/StandardRewardModel.h" #include "src/settings/SettingsManager.h" diff --git a/test/functional/storage/BitVectorTest.cpp b/test/functional/storage/BitVectorTest.cpp index f363f9679..408c286c9 100644 --- a/test/functional/storage/BitVectorTest.cpp +++ b/test/functional/storage/BitVectorTest.cpp @@ -113,7 +113,7 @@ TEST(BitVectorTest, GetSetInt) { storm::storage::BitVector vector(77); vector.setFromInt(63, 3, 2); - EXPECT_EQ(2, vector.getAsInt(63, 3)); + EXPECT_EQ(2ul, vector.getAsInt(63, 3)); } @@ -143,8 +143,8 @@ TEST(BitVectorTest, Resize) { vector.resize(70); - ASSERT_EQ(70, vector.size()); - ASSERT_EQ(32, vector.getNumberOfSetBits()); + ASSERT_EQ(70ul, vector.size()); + ASSERT_EQ(32ul, vector.getNumberOfSetBits()); for (uint_fast64_t i = 0; i < 32; ++i) { ASSERT_TRUE(vector.get(i)); @@ -158,8 +158,8 @@ TEST(BitVectorTest, Resize) { vector.resize(72, true); - ASSERT_EQ(72, vector.size()); - ASSERT_EQ(34, vector.getNumberOfSetBits()); + ASSERT_EQ(72ul, vector.size()); + ASSERT_EQ(34ul, vector.getNumberOfSetBits()); for (uint_fast64_t i = 0; i < 32; ++i) { ASSERT_TRUE(vector.get(i)); @@ -174,15 +174,15 @@ TEST(BitVectorTest, Resize) { } vector.resize(16, 0); - ASSERT_EQ(16, vector.size()); - ASSERT_EQ(16, vector.getNumberOfSetBits()); + ASSERT_EQ(16ul, vector.size()); + ASSERT_EQ(16ul, vector.getNumberOfSetBits()); for (uint_fast64_t i = 0; i < 16; ++i) { ASSERT_TRUE(vector.get(i)); } vector.resize(65, 1); - ASSERT_EQ(65, vector.size()); + ASSERT_EQ(65ul, vector.size()); ASSERT_TRUE(vector.full()); } @@ -445,7 +445,7 @@ TEST(BitVectorTest, NumberOfSetBits) { vector.set(i, i % 2 == 0); } - ASSERT_EQ(16, vector.getNumberOfSetBits()); + ASSERT_EQ(16ul, vector.getNumberOfSetBits()); } TEST(BitVectorTest, NumberOfSetBitsBeforeIndex) { diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 4acf5b489..33a67b197 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -369,12 +369,12 @@ TEST(CuddDd, BddOddTest) { storm::dd::Add dd = manager->getIdentity(x.first); storm::dd::Odd odd; ASSERT_NO_THROW(odd = storm::dd::Odd(dd)); - EXPECT_EQ(9, odd.getTotalOffset()); - EXPECT_EQ(12, odd.getNodeCount()); + EXPECT_EQ(9ul, odd.getTotalOffset()); + EXPECT_EQ(12ul, odd.getNodeCount()); std::vector ddAsVector; ASSERT_NO_THROW(ddAsVector = dd.toVector()); - EXPECT_EQ(9, ddAsVector.size()); + EXPECT_EQ(9ul, ddAsVector.size()); for (uint_fast64_t i = 0; i < ddAsVector.size(); ++i) { EXPECT_TRUE(i+1 == ddAsVector[i]); } diff --git a/test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp b/test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp index d8c0433a2..50e0e28ac 100644 --- a/test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp +++ b/test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp @@ -3,9 +3,9 @@ #include "src/parser/AutoParser.h" #include "src/storage/SparseMatrix.h" #include "src/storage/StronglyConnectedComponentDecomposition.h" +#include "src/models/sparse/StandardRewardModel.h" #include "src/models/sparse/MarkovAutomaton.h" - TEST(StronglyConnectedComponentDecomposition, SmallSystemFromMatrix) { storm::storage::SparseMatrixBuilder matrixBuilder(6, 6); ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 0, 0.3));