From fad28df7d626159be5348c9b4466e5697647e66e Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 26 Feb 2016 17:34:38 +0100
Subject: [PATCH] first working version of next-state generator for PRISM
models
Former-commit-id: 548a725e254bcbb924de20f37f24c93fcd916c9b
---
src/builder/ExplicitPrismModelBuilder.cpp | 17 +++--
src/builder/ExplicitPrismModelBuilder.h | 2 +-
src/generator/Choice.cpp | 31 +++-------
src/generator/Choice.h | 23 ++-----
src/generator/CompressedState.cpp | 5 +-
src/generator/CompressedState.h | 2 +-
src/generator/PrismNextStateGenerator.cpp | 62 ++++++++++---------
src/generator/PrismNextStateGenerator.h | 2 +
src/generator/StateBehavior.cpp | 7 ++-
src/generator/StateBehavior.h | 2 +-
src/generator/VariableInformation.cpp | 8 ++-
src/generator/VariableInformation.h | 3 +-
src/storage/BitVector.cpp | 41 +++++++-----
src/storage/BitVector.h | 2 +-
src/storage/BitVectorHashMap.cpp | 2 +-
src/storage/BitVectorHashMap.h | 2 +-
src/storage/Distribution.cpp | 10 +++
src/storage/Distribution.h | 26 ++++++--
src/storage/prism/Program.cpp | 4 ++
.../builder/ExplicitPrismModelBuilderTest.cpp | 32 +++++-----
.../GmmxxCtmcCslModelCheckerTest.cpp | 8 +--
.../GmmxxDtmcPrctlModelCheckerTest.cpp | 2 +-
.../GmmxxMdpPrctlModelCheckerTest.cpp | 2 +-
.../NativeCtmcCslModelCheckerTest.cpp | 8 +--
.../MilpPermissiveSchedulerTest.cpp | 2 +-
.../SmtPermissiveSchedulerTest.cpp | 2 +-
.../storage/BitVectorHashMapTest.cpp | 18 +++++-
test/functional/storage/BitVectorTest.cpp | 18 ------
...sticModelBisimulationDecompositionTest.cpp | 2 +-
test/functional/utility/GraphTest.cpp | 8 +--
30 files changed, 195 insertions(+), 158 deletions(-)
diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp
index 232d7f263..c0188de50 100644
--- a/src/builder/ExplicitPrismModelBuilder.cpp
+++ b/src/builder/ExplicitPrismModelBuilder.cpp
@@ -175,7 +175,7 @@ namespace storm {
}
template <typename ValueType, typename RewardModelType, typename StateType>
- ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::ExplicitPrismModelBuilder(storm::prism::Program const& program, Options const& options) : program(program), options(options), variableInformation(program), internalStateInformation(variableInformation.getTotalBitOffset()) {
+ ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::ExplicitPrismModelBuilder(storm::prism::Program const& program, Options const& options) : program(program), options(options) {
// Start by defining the undefined constants in the model.
if (options.constantDefinitions) {
this->program = program.defineUndefinedConstants(options.constantDefinitions.get());
@@ -226,6 +226,12 @@ namespace storm {
// Now that the program is fixed, we we need to substitute all constants with their concrete value.
this->program = program.substituteConstants();
+
+ // Create the variable information for the transformed program.
+ this->variableInformation = VariableInformation(this->program);
+
+ // Create the internal state storage.
+ this->internalStateInformation = InternalStateInformation(variableInformation.getTotalBitOffset(true));
}
template <typename ValueType, typename RewardModelType, typename StateType>
@@ -331,7 +337,7 @@ namespace storm {
std::function<StateType (CompressedState const&)> stateToIdCallback = std::bind(&ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::getOrAddStateIndex, this, std::placeholders::_1);
// Let the generator create all initial states.
- generator.getInitialStates(stateToIdCallback);
+ this->internalStateInformation.initialStateIndices = generator.getInitialStates(stateToIdCallback);
// Now explore the current state until there is no more reachable state.
uint_fast64_t currentRow = 0;
@@ -403,13 +409,13 @@ namespace storm {
}
// Add the probabilistic behavior to the matrix.
- for (auto const& stateProbabilityPair : behavior) {
+ for (auto const& stateProbabilityPair : choice) {
transitionMatrixBuilder.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second);
}
// Add the rewards to the reward models.
auto builderIt = rewardModelBuilders.begin();
- auto choiceRewardIt = behavior.getChoiceRewards().begin();
+ auto choiceRewardIt = choice.getChoiceRewards().begin();
for (auto const& rewardModel : selectedRewardModels) {
if (rewardModel.get().hasStateActionRewards()) {
builderIt->stateActionRewardVector.push_back(*choiceRewardIt);
@@ -437,7 +443,6 @@ namespace storm {
// Determine whether we have to combine different choices to one or whether this model can have more than
// one choice per state.
bool deterministicModel = program.isDeterministicModel();
- bool discreteTimeModel = program.isDiscreteTimeModel();
// Prepare the transition matrix builder and the reward model builders.
storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0);
@@ -477,7 +482,7 @@ namespace storm {
STORM_LOG_TRACE("Making the states satisfying " << terminalExpression.get() << " terminal.");
}
- modelComponents.choiceLabeling = buildMatrices(program, variableInformation, selectedRewardModels, internalStateInformation, options.buildCommandLabels, deterministicModel, discreteTimeModel, transitionMatrixBuilder, rewardModelBuilders, terminalExpression);
+ modelComponents.choiceLabeling = buildMatrices(selectedRewardModels, transitionMatrixBuilder, rewardModelBuilders, terminalExpression);
modelComponents.transitionMatrix = transitionMatrixBuilder.build();
// Now finalize all reward models.
diff --git a/src/builder/ExplicitPrismModelBuilder.h b/src/builder/ExplicitPrismModelBuilder.h
index 54fe9cf30..a5e09bfae 100644
--- a/src/builder/ExplicitPrismModelBuilder.h
+++ b/src/builder/ExplicitPrismModelBuilder.h
@@ -45,7 +45,7 @@ namespace storm {
public:
// A structure holding information about the reachable state space while building it.
struct InternalStateInformation {
- InternalStateInformation(uint64_t bitsPerState);
+ InternalStateInformation(uint64_t bitsPerState = 64);
// This member stores all the states and maps them to their unique indices.
storm::storage::BitVectorHashMap<StateType> stateStorage;
diff --git a/src/generator/Choice.cpp b/src/generator/Choice.cpp
index f80831ca0..9202f2c5e 100644
--- a/src/generator/Choice.cpp
+++ b/src/generator/Choice.cpp
@@ -1,5 +1,7 @@
#include "src/generator/Choice.h"
+#include "src/adapters/CarlAdapter.h"
+
#include "src/utility/constants.h"
namespace storm {
@@ -61,30 +63,10 @@ namespace storm {
return totalMass;
}
- template<typename ValueType, typename StateType>
- ValueType& Choice<ValueType, StateType>::getOrAddEntry(StateType const& state) {
- auto stateProbabilityPair = distribution.find(state);
-
- if (stateProbabilityPair == distribution.end()) {
- distribution[state] = ValueType();
- }
- return distribution.at(state);
- }
-
- template<typename ValueType, typename StateType>
- ValueType const& Choice<ValueType, StateType>::getOrAddEntry(StateType const& state) const {
- auto stateProbabilityPair = distribution.find(state);
-
- if (stateProbabilityPair == distribution.end()) {
- distribution[state] = ValueType();
- }
- return distribution.at(state);
- }
-
template<typename ValueType, typename StateType>
void Choice<ValueType, StateType>::addProbability(StateType const& state, ValueType const& value) {
totalMass += value;
- distribution[state] += value;
+ distribution.addProbability(state, value);
}
template<typename ValueType, typename StateType>
@@ -97,6 +79,11 @@ namespace storm {
return choiceRewards;
}
+ template<typename ValueType, typename StateType>
+ bool Choice<ValueType, StateType>::isMarkovian() const {
+ return markovian;
+ }
+
template<typename ValueType, typename StateType>
std::size_t Choice<ValueType, StateType>::size() const {
return distribution.size();
@@ -112,5 +99,7 @@ namespace storm {
return out;
}
+ template class Choice<double>;
+ template class Choice<storm::RationalFunction>;
}
}
\ No newline at end of file
diff --git a/src/generator/Choice.h b/src/generator/Choice.h
index 95810bfb2..76b6c8d16 100644
--- a/src/generator/Choice.h
+++ b/src/generator/Choice.h
@@ -96,24 +96,6 @@ namespace storm {
*/
ValueType getTotalMass() const;
- /*!
- * Retrieves the entry in the choice that is associated with the given state and creates one if none exists,
- * yet.
- *
- * @param state The state for which to add the entry.
- * @return A reference to the entry that is associated with the given state.
- */
- ValueType& getOrAddEntry(StateType const& state);
-
- /*!
- * Retrieves the entry in the choice that is associated with the given state and creates one if none exists,
- * yet.
- *
- * @param state The state for which to add the entry.
- * @return A reference to the entry that is associated with the given state.
- */
- ValueType const& getOrAddEntry(StateType const& state) const;
-
/*!
* Adds the given probability value to the given state in the underlying distribution.
*/
@@ -129,6 +111,11 @@ namespace storm {
*/
std::vector<ValueType> const& getChoiceRewards() const;
+ /*!
+ * Retrieves whether the choice is Markovian.
+ */
+ bool isMarkovian() const;
+
/*!
* Retrieves the size of the distribution associated with this choice.
*/
diff --git a/src/generator/CompressedState.cpp b/src/generator/CompressedState.cpp
index 1f71d2407..c63504ebb 100644
--- a/src/generator/CompressedState.cpp
+++ b/src/generator/CompressedState.cpp
@@ -7,7 +7,7 @@ namespace storm {
namespace generator {
template<typename ValueType>
- static void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<ValueType>& evaluator) {
+ void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<ValueType>& evaluator) {
for (auto const& booleanVariable : variableInformation.booleanVariables) {
evaluator.setBooleanValue(booleanVariable.variable, state.get(booleanVariable.bitOffset));
}
@@ -17,6 +17,7 @@ namespace storm {
}
-
+ template void unpackStateIntoEvaluator<double>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<double>& evaluator);
+ template void unpackStateIntoEvaluator<storm::RationalFunction>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<storm::RationalFunction>& evaluator);
}
}
\ No newline at end of file
diff --git a/src/generator/CompressedState.h b/src/generator/CompressedState.h
index 512db591f..52f0b4a62 100644
--- a/src/generator/CompressedState.h
+++ b/src/generator/CompressedState.h
@@ -22,7 +22,7 @@ namespace storm {
* @param evaluator The evaluator into which to load the state.
*/
template<typename ValueType>
- static void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<ValueType>& evaluator);
+ void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<ValueType>& evaluator);
}
}
diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp
index f8243998f..ad3ce3080 100644
--- a/src/generator/PrismNextStateGenerator.cpp
+++ b/src/generator/PrismNextStateGenerator.cpp
@@ -8,7 +8,7 @@ namespace storm {
namespace generator {
template<typename ValueType, typename StateType>
- PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation, bool buildChoiceLabeling) : program(program), selectedRewardModels(), buildChoiceLabeling(buildChoiceLabeling), variableInformation(variableInformation), evaluator(), comparator() {
+ PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation, bool buildChoiceLabeling) : program(program), selectedRewardModels(), buildChoiceLabeling(buildChoiceLabeling), variableInformation(variableInformation), evaluator(program.getManager()), comparator() {
// Intentionally left empty.
}
@@ -57,15 +57,15 @@ namespace storm {
// First, construct the state rewards, as we may return early if there are no choices later and we already
// need the state rewards then.
for (auto const& rewardModel : selectedRewardModels) {
- ValueType stateReward = storm::utility::zero<ValueType>();
- if (rewardModel->hasStateRewards()) {
- for (auto const& stateReward : rewardModel->getStateRewards()) {
+ ValueType stateRewardValue = storm::utility::zero<ValueType>();
+ if (rewardModel.get().hasStateRewards()) {
+ for (auto const& stateReward : rewardModel.get().getStateRewards()) {
if (evaluator.asBool(stateReward.getStatePredicateExpression())) {
- stateReward += ValueType(evaluator.asRational(stateReward.getRewardValueExpression()));
+ stateRewardValue += ValueType(evaluator.asRational(stateReward.getRewardValueExpression()));
}
}
}
- result.addStateReward(stateReward);
+ result.addStateReward(stateRewardValue);
}
// If a terminal expression was set and we must not expand this state, return now.
@@ -94,21 +94,22 @@ namespace storm {
// For CTMCs, we need to keep track of the total exit rate to scale the action rewards later. For DTMCs
// this is equal to the number of choices, which is why we initialize it like this here.
- ValueType totalExitRate = static_cast<ValueType>(totalNumberOfChoices);
+ ValueType totalExitRate = program.isDiscreteTimeModel() ? static_cast<ValueType>(totalNumberOfChoices) : storm::utility::zero<ValueType>();
// Iterate over all choices and combine the probabilities/rates into one choice.
for (auto const& choice : allChoices) {
for (auto const& stateProbabilityPair : choice) {
if (program.isDiscreteTimeModel()) {
- globalChoice.getOrAddEntry(stateProbabilityPair.first) += stateProbabilityPair.second / totalNumberOfChoices;
- if (hasStateActionRewards) {
- totalExitRate += choice.getTotalMass();
- }
+ globalChoice.addProbability(stateProbabilityPair.first, stateProbabilityPair.second / totalNumberOfChoices);
} else {
- globalChoice.getOrAddEntry(stateProbabilityPair.first) += stateProbabilityPair.second;
+ globalChoice.addProbability(stateProbabilityPair.first, stateProbabilityPair.second);
}
}
+ if (hasStateActionRewards && !program.isDiscreteTimeModel()) {
+ totalExitRate += choice.getTotalMass();
+ }
+
if (buildChoiceLabeling) {
globalChoice.addChoiceLabels(choice.getChoiceLabels());
}
@@ -116,18 +117,18 @@ namespace storm {
// Now construct the state-action reward for all selected reward models.
for (auto const& rewardModel : selectedRewardModels) {
- ValueType stateActionReward = storm::utility::zero<ValueType>();
- if (rewardModel->hasStateActionRewards()) {
- for (auto const& stateActionReward : rewardModel->getStateActionRewards()) {
+ ValueType stateActionRewardValue = storm::utility::zero<ValueType>();
+ if (rewardModel.get().hasStateActionRewards()) {
+ for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) {
for (auto const& choice : allChoices) {
if (stateActionReward.getActionIndex() == choice.getActionIndex() && evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
- stateActionReward += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) / totalExitRate;
+ stateActionRewardValue += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass() / totalExitRate;
}
}
}
}
- globalChoice.addChoiceReward(stateActionReward);
+ globalChoice.addChoiceReward(stateActionRewardValue);
}
// Move the newly fused choice in place.
@@ -266,15 +267,15 @@ namespace storm {
// Create the state-action reward for the newly created choice.
for (auto const& rewardModel : selectedRewardModels) {
- ValueType stateActionReward = storm::utility::zero<ValueType>();
- if (rewardModel->hasStateActionRewards()) {
- for (auto const& stateActionReward : rewardModel->getStateActionRewards()) {
+ ValueType stateActionRewardValue = storm::utility::zero<ValueType>();
+ if (rewardModel.get().hasStateActionRewards()) {
+ for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) {
if (stateActionReward.getActionIndex() == choice.getActionIndex() && evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
- stateActionReward += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass();
+ stateActionRewardValue += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass();
}
}
}
- choice.addChoiceReward(stateActionReward);
+ choice.addChoiceReward(stateActionRewardValue);
}
// Check that the resulting distribution is in fact a distribution.
@@ -290,7 +291,7 @@ namespace storm {
std::vector<Choice<ValueType>> result;
for (uint_fast64_t actionIndex : program.getSynchronizingActionIndices()) {
- boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> optionalActiveCommandLists = getActiveCommandsByActionIndex(program, evaluator, actionIndex);
+ boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> optionalActiveCommandLists = getActiveCommandsByActionIndex(actionIndex);
// Only process this action label, if there is at least one feasible solution.
if (optionalActiveCommandLists) {
@@ -317,7 +318,7 @@ namespace storm {
for (auto const& stateProbabilityPair : *currentTargetStates) {
// Compute the new state under the current update and add it to the set of new target states.
- CompressedState newTargetState = applyUpdate(stateProbabilityPair.first, state, update);
+ CompressedState newTargetState = applyUpdate(stateProbabilityPair.first, update);
newTargetStates->emplace(newTargetState, stateProbabilityPair.second * evaluator.asRational(update.getLikelihoodExpression()));
}
}
@@ -359,15 +360,15 @@ namespace storm {
// Create the state-action reward for the newly created choice.
for (auto const& rewardModel : selectedRewardModels) {
- ValueType stateActionReward = storm::utility::zero<ValueType>();
- if (rewardModel->hasStateActionRewards()) {
- for (auto const& stateActionReward : rewardModel->getStateActionRewards()) {
+ ValueType stateActionRewardValue = storm::utility::zero<ValueType>();
+ if (rewardModel.get().hasStateActionRewards()) {
+ for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) {
if (stateActionReward.getActionIndex() == choice.getActionIndex() && evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
- stateActionReward += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass();
+ stateActionRewardValue += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass();
}
}
}
- choice.addChoiceReward(stateActionReward);
+ choice.addChoiceReward(stateActionRewardValue);
}
// Dispose of the temporary maps.
@@ -393,5 +394,8 @@ namespace storm {
return result;
}
+
+ template class PrismNextStateGenerator<double>;
+ template class PrismNextStateGenerator<storm::RationalFunction>;
}
}
\ No newline at end of file
diff --git a/src/generator/PrismNextStateGenerator.h b/src/generator/PrismNextStateGenerator.h
index 6e400e0eb..e9c63502e 100644
--- a/src/generator/PrismNextStateGenerator.h
+++ b/src/generator/PrismNextStateGenerator.h
@@ -7,6 +7,8 @@
#include "src/storage/prism/Program.h"
#include "src/storage/expressions/ExpressionEvaluator.h"
+#include "src/utility/ConstantsComparator.h"
+
namespace storm {
namespace generator {
diff --git a/src/generator/StateBehavior.cpp b/src/generator/StateBehavior.cpp
index bd5d489b7..e14417779 100644
--- a/src/generator/StateBehavior.cpp
+++ b/src/generator/StateBehavior.cpp
@@ -1,5 +1,7 @@
#include "src/generator/StateBehavior.h"
+#include "src/adapters/CarlAdapter.h"
+
namespace storm {
namespace generator {
@@ -19,7 +21,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
- bool StateBehavior<ValueType, StateType>::setExpanded(bool newValue) {
+ void StateBehavior<ValueType, StateType>::setExpanded(bool newValue) {
this->expanded = newValue;
}
@@ -47,6 +49,9 @@ namespace storm {
std::vector<ValueType> const& StateBehavior<ValueType, StateType>::getStateRewards() const {
return stateRewards;
}
+
+ template class StateBehavior<double>;
+ template class StateBehavior<storm::RationalFunction>;
}
}
\ No newline at end of file
diff --git a/src/generator/StateBehavior.h b/src/generator/StateBehavior.h
index 9cbd26617..393c3280c 100644
--- a/src/generator/StateBehavior.h
+++ b/src/generator/StateBehavior.h
@@ -29,7 +29,7 @@ namespace storm {
/*!
* Sets whether the state was expanded.
*/
- bool setExpanded(bool newValue = true);
+ void setExpanded(bool newValue = true);
/*!
* Retrieves whether the state was expanded.
diff --git a/src/generator/VariableInformation.cpp b/src/generator/VariableInformation.cpp
index bb20c5225..a5be93a6e 100644
--- a/src/generator/VariableInformation.cpp
+++ b/src/generator/VariableInformation.cpp
@@ -45,8 +45,12 @@ namespace storm {
}
}
- uint_fast64_t VariableInformation::getTotalBitOffset() const {
- return totalBitOffset;
+ uint_fast64_t VariableInformation::getTotalBitOffset(bool roundTo64Bit) const {
+ uint_fast64_t result = totalBitOffset;
+ if (roundTo64Bit) {
+ result = ((result >> 6) + 1) << 6;
+ }
+ return result;
}
uint_fast64_t VariableInformation::getBitOffset(storm::expressions::Variable const& variable) const {
diff --git a/src/generator/VariableInformation.h b/src/generator/VariableInformation.h
index c77d8f965..8c2841dfd 100644
--- a/src/generator/VariableInformation.h
+++ b/src/generator/VariableInformation.h
@@ -49,8 +49,9 @@ namespace storm {
// A structure storing information about the used variables of the program.
struct VariableInformation {
+ VariableInformation() = default;
VariableInformation(storm::prism::Program const& program);
- uint_fast64_t getTotalBitOffset() const;
+ uint_fast64_t getTotalBitOffset(bool roundTo64Bit = false) const;
// Provide methods to access the bit offset and width of variables in the compressed state.
uint_fast64_t getBitOffset(storm::expressions::Variable const& variable) const;
diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp
index 38b94d852..3e25e488d 100644
--- a/src/storage/BitVector.cpp
+++ b/src/storage/BitVector.cpp
@@ -64,7 +64,7 @@ namespace storm {
// Intentionally left empty.
}
- BitVector::BitVector(uint_fast64_t length, bool init) : bitCount(length) {
+ BitVector::BitVector(uint_fast64_t length, bool init) : bitCount(length), buckets(nullptr) {
// Compute the correct number of buckets needed to store the given number of bits.
uint_fast64_t bucketCount = length >> 6;
if ((length & mod64mask) != 0) {
@@ -96,12 +96,12 @@ namespace storm {
// Intentionally left empty.
}
- BitVector::BitVector(uint_fast64_t bucketCount, uint_fast64_t bitCount) : bitCount(bitCount) {
+ BitVector::BitVector(uint_fast64_t bucketCount, uint_fast64_t bitCount) : bitCount(bitCount), buckets(nullptr) {
STORM_LOG_ASSERT((bucketCount << 6) == bitCount, "Bit count does not match number of buckets.");
buckets = new uint64_t[bucketCount]();
}
- BitVector::BitVector(BitVector const& other) : bitCount(other.bitCount) {
+ BitVector::BitVector(BitVector const& other) : bitCount(other.bitCount), buckets(nullptr) {
buckets = new uint64_t[other.bucketCount()];
std::copy_n(other.buckets, other.bucketCount(), buckets);
}
@@ -136,6 +136,11 @@ namespace storm {
}
return false;
}
+
+ BitVector::BitVector(BitVector&& other) : bitCount(other.bitCount), buckets(other.buckets) {
+ other.bitCount = 0;
+ other.buckets = nullptr;
+ }
BitVector& BitVector::operator=(BitVector&& other) {
// Only perform the assignment if the source and target are not identical.
@@ -202,11 +207,13 @@ namespace storm {
std::copy_n(buckets, this->bucketCount(), newBuckets);
if (init) {
newBuckets[this->bucketCount() - 1] |= ((1ull << (64 - (bitCount & mod64mask))) - 1ull);
- std::fill_n(newBuckets, newBucketCount - this->bucketCount(), -1ull);
+ std::fill_n(newBuckets + this->bucketCount(), newBucketCount - this->bucketCount(), -1ull);
} else {
- std::fill_n(newBuckets, newBucketCount - this->bucketCount(), 0);
+ std::fill_n(newBuckets + this->bucketCount(), newBucketCount - this->bucketCount(), 0);
+ }
+ if (buckets != nullptr) {
+ delete buckets;
}
- delete buckets;
buckets = newBuckets;
bitCount = newLength;
} else {
@@ -228,7 +235,9 @@ namespace storm {
if (newBucketCount < this->bucketCount()) {
uint64_t* newBuckets = new uint64_t[newBucketCount];
std::copy_n(buckets, newBucketCount, newBuckets);
- delete buckets;
+ if (buckets != nullptr) {
+ delete buckets;
+ }
buckets = newBuckets;
bitCount = newLength;
}
@@ -473,19 +482,19 @@ namespace storm {
bool BitVector::empty() const {
uint64_t* last = buckets + bucketCount();
- uint64_t* it = std::find(buckets, last, 0);
- return it != last;
+ uint64_t* it = std::find_if(buckets, last, [] (uint64_t const& a) { return a != 0; });
+ return it == last;
}
bool BitVector::full() const {
// Check that all buckets except the last one have all bits set.
uint64_t* last = buckets + bucketCount() - 1;
- for (uint64_t const* it = buckets; it != last; ++it) {
+ for (uint64_t const* it = buckets; it < last; ++it) {
if (*it != -1ull) {
return false;
}
}
-
+
// Now check whether the relevant bits are set in the last bucket.
uint64_t mask = ~((1ull << (64 - (bitCount & mod64mask))) - 1ull);
if ((*last & mask) != mask) {
@@ -627,7 +636,11 @@ namespace storm {
}
size_t BitVector::bucketCount() const {
- return bitCount >> 6;
+ size_t result = (bitCount >> 6);
+ if ((bitCount & mod64mask) != 0) {
+ ++result;
+ }
+ return result;
}
std::ostream& operator<<(std::ostream& out, BitVector const& bitvector) {
@@ -670,7 +683,7 @@ namespace storm {
namespace std {
- std::size_t hash<storm::storage::BitVector>::operator()(storm::storage::BitVector const& bv) const {
- return boost::hash_range(bv.bucketVector.begin(), bv.bucketVector.end());
+ std::size_t hash<storm::storage::BitVector>::operator()(storm::storage::BitVector const& bitvector) const {
+ return boost::hash_range(bitvector.buckets, bitvector.buckets + bitvector.bucketCount());
}
}
\ No newline at end of file
diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h
index a6ad89cc3..f15eef3ed 100644
--- a/src/storage/BitVector.h
+++ b/src/storage/BitVector.h
@@ -146,7 +146,7 @@ namespace storm {
*
* @param other The bit vector from which to move-construct.
*/
- BitVector(BitVector&& other) = default;
+ BitVector(BitVector&& other);
/*!
* Compares the given bit vector with the current one.
diff --git a/src/storage/BitVectorHashMap.cpp b/src/storage/BitVectorHashMap.cpp
index c184b764b..881fc016a 100644
--- a/src/storage/BitVectorHashMap.cpp
+++ b/src/storage/BitVectorHashMap.cpp
@@ -40,7 +40,7 @@ namespace storm {
std::pair<storm::storage::BitVector, ValueType> BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::operator*() const {
return map.getBucketAndValue(*indexIt);
}
-
+
template<class ValueType, class Hash1, class Hash2>
BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMap(uint64_t bucketSize, uint64_t initialSize, double loadFactor) : loadFactor(loadFactor), bucketSize(bucketSize), numberOfElements(0) {
STORM_LOG_ASSERT(bucketSize % 64 == 0, "Bucket size must be a multiple of 64.");
diff --git a/src/storage/BitVectorHashMap.h b/src/storage/BitVectorHashMap.h
index 3b0c7aa70..c53928b09 100644
--- a/src/storage/BitVectorHashMap.h
+++ b/src/storage/BitVectorHashMap.h
@@ -55,7 +55,7 @@ namespace storm {
* @param loadFactor The load factor that determines at which point the size of the underlying storage is
* increased.
*/
- BitVectorHashMap(uint64_t bucketSize, uint64_t initialSize, double loadFactor = 0.75);
+ BitVectorHashMap(uint64_t bucketSize = 64, uint64_t initialSize = 1000, double loadFactor = 0.75);
/*!
* Searches for the given key in the map. If it is found, the mapped-to value is returned. Otherwise, the
diff --git a/src/storage/Distribution.cpp b/src/storage/Distribution.cpp
index 516227277..5843e964b 100644
--- a/src/storage/Distribution.cpp
+++ b/src/storage/Distribution.cpp
@@ -78,6 +78,11 @@ namespace storm {
return this->distribution.begin();
}
+ template<typename ValueType, typename StateType>
+ typename Distribution<ValueType, StateType>::const_iterator Distribution<ValueType, StateType>::cbegin() const {
+ return this->begin();
+ }
+
template<typename ValueType, typename StateType>
typename Distribution<ValueType, StateType>::iterator Distribution<ValueType, StateType>::end() {
return this->distribution.end();
@@ -87,6 +92,11 @@ namespace storm {
typename Distribution<ValueType, StateType>::const_iterator Distribution<ValueType, StateType>::end() const {
return this->distribution.end();
}
+
+ template<typename ValueType, typename StateType>
+ typename Distribution<ValueType, StateType>::const_iterator Distribution<ValueType, StateType>::cend() const {
+ return this->end();
+ }
template<typename ValueType, typename StateType>
void Distribution<ValueType, StateType>::scale(StateType const& state) {
diff --git a/src/storage/Distribution.h b/src/storage/Distribution.h
index 39e6eb6f9..ba61f0fbd 100644
--- a/src/storage/Distribution.h
+++ b/src/storage/Distribution.h
@@ -17,7 +17,7 @@ namespace storm {
namespace storage {
- template<typename ValueType, typename StateType=storm::storage::sparse::state_type>
+ template<typename ValueType, typename StateType = uint32_t>
class Distribution {
public:
typedef boost::container::flat_map<StateType, ValueType> container_type;
@@ -43,7 +43,7 @@ namespace storm {
* @param other The distribution with which the current distribution is to be compared.
* @return True iff the two distributions are equal.
*/
- bool equals(Distribution<ValueType> const& other, storm::utility::ConstantsComparator<ValueType> const& comparator = storm::utility::ConstantsComparator<ValueType>()) const;
+ bool equals(Distribution<ValueType, StateType> const& other, storm::utility::ConstantsComparator<ValueType> const& comparator = storm::utility::ConstantsComparator<ValueType>()) const;
/*!
* Assigns the given state the given probability under this distribution.
@@ -73,7 +73,7 @@ namespace storm {
* entry is removed.
*/
void shiftProbability(StateType const& fromState, StateType const& toState, ValueType const& probability, storm::utility::ConstantsComparator<ValueType> const& comparator = storm::utility::ConstantsComparator<ValueType>());
-
+
/*!
* Retrieves an iterator to the elements in this distribution.
*
@@ -88,6 +88,13 @@ namespace storm {
*/
const_iterator begin() const;
+ /*!
+ * Retrieves an iterator to the elements in this distribution.
+ *
+ * @return The iterator to the elements in this distribution.
+ */
+ const_iterator cbegin() const;
+
/*!
* Retrieves an iterator past the elements in this distribution.
*
@@ -102,6 +109,13 @@ namespace storm {
*/
const_iterator end() const;
+ /*!
+ * Retrieves an iterator past the elements in this distribution.
+ *
+ * @return The iterator past the elements in this distribution.
+ */
+ const_iterator cend() const;
+
/*!
* Scales the distribution by multiplying all the probabilities with 1/p where p is the probability of moving
* to the given state and sets the probability of moving to the given state to zero. If the probability is
@@ -116,15 +130,15 @@ namespace storm {
*/
std::size_t size() const;
- bool less(Distribution<ValueType> const& other, storm::utility::ConstantsComparator<ValueType> const& comparator) const;
+ bool less(Distribution<ValueType, StateType> const& other, storm::utility::ConstantsComparator<ValueType> const& comparator) const;
private:
// A list of states and the probabilities that are assigned to them.
container_type distribution;
};
- template<typename ValueType>
- std::ostream& operator<<(std::ostream& out, Distribution<ValueType> const& distribution);
+ template<typename ValueType, typename StateType = uint32_t>
+ std::ostream& operator<<(std::ostream& out, Distribution<ValueType, StateType> const& distribution);
}
}
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index 0f5aea4a8..999cf2f30 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -81,6 +81,10 @@ namespace storm {
return modelType == ModelType::DTMC || modelType == ModelType::MDP;
}
+ bool Program::isDeterministicModel() const {
+ return modelType == ModelType::DTMC || modelType == ModelType::CTMC;
+ }
+
bool Program::hasUndefinedConstants() const {
for (auto const& constant : this->getConstants()) {
if (!constant.isDefined()) {
diff --git a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp
index 080b6c16f..c2151c74c 100644
--- a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp
+++ b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp
@@ -10,27 +10,27 @@
TEST(ExplicitPrismModelBuilderTest, Dtmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(677ul, model->getNumberOfStates());
EXPECT_EQ(867ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(8607ul, model->getNumberOfStates());
EXPECT_EQ(15113ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(273ul, model->getNumberOfStates());
EXPECT_EQ(397ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(1728ul, model->getNumberOfStates());
EXPECT_EQ(2505ul, model->getNumberOfTransitions());
}
@@ -41,27 +41,27 @@ TEST(ExplicitPrismModelBuilderTest, Ctmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(276ul, model->getNumberOfStates());
EXPECT_EQ(1120ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(3478ul, model->getNumberOfStates());
EXPECT_EQ(14639ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(12ul, model->getNumberOfStates());
EXPECT_EQ(22ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(810ul, model->getNumberOfStates());
EXPECT_EQ(3699ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(66ul, model->getNumberOfStates());
EXPECT_EQ(189ul, model->getNumberOfTransitions());
}
@@ -69,32 +69,32 @@ TEST(ExplicitPrismModelBuilderTest, Ctmc) {
TEST(ExplicitPrismModelBuilderTest, Mdp) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(169ul, model->getNumberOfStates());
EXPECT_EQ(436ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(364ul, model->getNumberOfStates());
EXPECT_EQ(654ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(272ul, model->getNumberOfStates());
EXPECT_EQ(492ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(1038ul, model->getNumberOfStates());
EXPECT_EQ(1282ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(4093ul, model->getNumberOfStates());
EXPECT_EQ(5585ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(37ul, model->getNumberOfStates());
EXPECT_EQ(59ul, model->getNumberOfTransitions());
}
\ No newline at end of file
diff --git a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
index b36983962..dc9512a38 100644
--- a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
@@ -34,7 +34,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_repairs");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program, options);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program, options).translate();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@@ -117,7 +117,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Embedded) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("up");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program, options);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program, options).translate();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@@ -179,7 +179,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Polling) {
std::shared_ptr<const storm::logic::Formula> formula(nullptr);
// Build the model.
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@@ -226,7 +226,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Tandem) {
typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
#endif
options.rewardModelsToBuild.insert("customers");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program, options);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program, options).translate();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
diff --git a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
index 1e131c335..36a139b9c 100644
--- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
@@ -284,7 +284,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRA) {
TEST(GmmxxDtmcPrctlModelCheckerTest, Conditional) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/test_conditional.pm");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
ASSERT_EQ(4ul, model->getNumberOfStates());
ASSERT_EQ(5ul, model->getNumberOfTransitions());
diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
index 725e1376d..93643fd52 100644
--- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
@@ -197,7 +197,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) {
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(4ul, model->getNumberOfStates());
EXPECT_EQ(11ul, model->getNumberOfTransitions());
diff --git a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
index 72788de80..0a1d8ee4c 100644
--- a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
+++ b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
@@ -32,7 +32,7 @@ TEST(NativeCtmcCslModelCheckerTest, Cluster) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_repairs");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program, options);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program, options).translate();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@@ -108,7 +108,7 @@ TEST(NativeCtmcCslModelCheckerTest, Embedded) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("up");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program, options);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program, options).translate();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@@ -163,7 +163,7 @@ TEST(NativeCtmcCslModelCheckerTest, Polling) {
std::shared_ptr<const storm::logic::Formula> formula(nullptr);
// Build the model.
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@@ -204,7 +204,7 @@ TEST(NativeCtmcCslModelCheckerTest, Tandem) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("customers");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program, options);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program, options).translate();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
diff --git a/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp b/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
index 75bea3570..657d36575 100644
--- a/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
+++ b/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
@@ -28,7 +28,7 @@ TEST(MilpPermissiveSchedulerTest, DieSelection) {
options.addConstantDefinitionsFromString(program, "");
options.buildCommandLabels = true;
- std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program, options)->as<storm::models::sparse::Mdp<double>>();
+ std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitPrismModelBuilder<double>(program, options).translate()->as<storm::models::sparse::Mdp<double>>();
boost::optional<storm::ps::SubMDPPermissiveScheduler<>> perms = storm::ps::computePermissiveSchedulerViaMILP<>(*mdp, formula02);
EXPECT_NE(perms, boost::none);
diff --git a/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp b/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
index 4d87796b8..2790cd86a 100644
--- a/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
+++ b/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
@@ -31,7 +31,7 @@ TEST(SmtPermissiveSchedulerTest, DieSelection) {
options.addConstantDefinitionsFromString(program, "");
options.buildCommandLabels = true;
- std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program, options)->as<storm::models::sparse::Mdp<double>>();
+ std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitPrismModelBuilder<double>(program, options).translate()->as<storm::models::sparse::Mdp<double>>();
// boost::optional<storm::ps::SubMDPPermissiveScheduler<>> perms = storm::ps::computePermissiveSchedulerViaSMT<>(*mdp, formula02);
// EXPECT_NE(perms, boost::none);
diff --git a/test/functional/storage/BitVectorHashMapTest.cpp b/test/functional/storage/BitVectorHashMapTest.cpp
index 616941f21..1149433fd 100644
--- a/test/functional/storage/BitVectorHashMapTest.cpp
+++ b/test/functional/storage/BitVectorHashMapTest.cpp
@@ -19,25 +19,41 @@ TEST(BitVectorHashMapTest, FindOrAdd) {
ASSERT_NO_THROW(map.findOrAdd(second, 2));
EXPECT_EQ(1ul, map.findOrAdd(first, 3));
-
+ EXPECT_EQ(2ul, map.findOrAdd(second, 3));
+
storm::storage::BitVector third(64);
third.set(10);
third.set(63);
ASSERT_NO_THROW(map.findOrAdd(third, 3));
+ EXPECT_EQ(1ul, map.findOrAdd(first, 2));
+ EXPECT_EQ(2ul, map.findOrAdd(second, 1));
+ EXPECT_EQ(3ul, map.findOrAdd(third, 1));
+
storm::storage::BitVector fourth(64);
fourth.set(12);
fourth.set(14);
ASSERT_NO_THROW(map.findOrAdd(fourth, 4));
+ EXPECT_EQ(1ul, map.findOrAdd(first, 2));
+ EXPECT_EQ(2ul, map.findOrAdd(second, 1));
+ EXPECT_EQ(3ul, map.findOrAdd(third, 1));
+ EXPECT_EQ(4ul, map.findOrAdd(fourth, 1));
+
storm::storage::BitVector fifth(64);
fifth.set(44);
fifth.set(55);
ASSERT_NO_THROW(map.findOrAdd(fifth, 5));
+ EXPECT_EQ(1ul, map.findOrAdd(first, 2));
+ EXPECT_EQ(2ul, map.findOrAdd(second, 1));
+ EXPECT_EQ(3ul, map.findOrAdd(third, 1));
+ EXPECT_EQ(4ul, map.findOrAdd(fourth, 1));
+ EXPECT_EQ(5ul, map.findOrAdd(fifth, 1));
+
storm::storage::BitVector sixth(64);
sixth.set(45);
sixth.set(55);
diff --git a/test/functional/storage/BitVectorTest.cpp b/test/functional/storage/BitVectorTest.cpp
index db92724fe..7266f829b 100644
--- a/test/functional/storage/BitVectorTest.cpp
+++ b/test/functional/storage/BitVectorTest.cpp
@@ -321,24 +321,6 @@ TEST(BitVectorTest, OperatorModulo) {
ASSERT_FALSE(moduloResult.get(i));
}
}
-
- storm::storage::BitVector vector3(31);
-
- for (uint_fast64_t i = 0; i < 15; ++i) {
- vector3.set(i, i % 2 == 0);
- }
-
-
-#ifndef NDEBUG
-#ifdef WINDOWS
- EXPECT_EXIT(vector1 % vector3, ::testing::ExitedWithCode(0), ".*");
-#else
- EXPECT_DEATH_IF_SUPPORTED(vector1 % vector3, "");
-#endif
-#else
- std::cerr << "WARNING: Not testing OperatorModulo size check, as assertions are disabled in release mode." << std::endl;
- SUCCEED();
-#endif
}
TEST(BitVectorTest, OperatorNot) {
diff --git a/test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp b/test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp
index 3754b03fd..fe0a199b7 100644
--- a/test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp
+++ b/test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp
@@ -14,7 +14,7 @@ TEST(NondeterministicModelBisimulationDecomposition, TwoDice) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
// Build the die model without its reward model.
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = model->as<storm::models::sparse::Mdp<double>>();
diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp
index d209998d7..4c6bf0d50 100644
--- a/test/functional/utility/GraphTest.cpp
+++ b/test/functional/utility/GraphTest.cpp
@@ -181,7 +181,7 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) {
TEST(GraphTest, ExplicitProb01) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
@@ -202,7 +202,7 @@ TEST(GraphTest, ExplicitProb01) {
TEST(GraphTest, ExplicitProb01MinMax) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@@ -217,7 +217,7 @@ TEST(GraphTest, ExplicitProb01MinMax) {
EXPECT_EQ(364ul, statesWithProbability01.second.getNumberOfSetBits());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@@ -238,7 +238,7 @@ TEST(GraphTest, ExplicitProb01MinMax) {
EXPECT_EQ(35ul, statesWithProbability01.second.getNumberOfSetBits());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);