sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

first working version of next-state generator for PRISM models 

Former-commit-id: 548a725e25
tempestpy_adaptions
dehnert 9 years ago
parent
9eec5b140c
commit
fad28df7d6
30 changed files with 195 additions and 158 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 17
      src/builder/ExplicitPrismModelBuilder.cpp
  2. 2
      src/builder/ExplicitPrismModelBuilder.h
  3. 31
      src/generator/Choice.cpp
  4. 23
      src/generator/Choice.h
  5. 5
      src/generator/CompressedState.cpp
  6. 2
      src/generator/CompressedState.h
  7. 62
      src/generator/PrismNextStateGenerator.cpp
  8. 2
      src/generator/PrismNextStateGenerator.h
  9. 7
      src/generator/StateBehavior.cpp
  10. 2
      src/generator/StateBehavior.h
  11. 8
      src/generator/VariableInformation.cpp
  12. 3
      src/generator/VariableInformation.h
  13. 41
      src/storage/BitVector.cpp
  14. 2
      src/storage/BitVector.h
  15. 2
      src/storage/BitVectorHashMap.cpp
  16. 2
      src/storage/BitVectorHashMap.h
  17. 10
      src/storage/Distribution.cpp
  18. 26
      src/storage/Distribution.h
  19. 4
      src/storage/prism/Program.cpp
  20. 32
      test/functional/builder/ExplicitPrismModelBuilderTest.cpp
  21. 8
      test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
  22. 2
      test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
  23. 2
      test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
  24. 8
      test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
  25. 2
      test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
  26. 2
      test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
  27. 18
      test/functional/storage/BitVectorHashMapTest.cpp
  28. 18
      test/functional/storage/BitVectorTest.cpp
  29. 2
      test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp
  30. 8
      test/functional/utility/GraphTest.cpp

17
src/builder/ExplicitPrismModelBuilder.cpp
View File

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

2
src/builder/ExplicitPrismModelBuilder.h
View File

@ -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;

31
src/generator/Choice.cpp
View File

@ -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>;
}
}

23
src/generator/Choice.h
View File

@ -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.
*/

5
src/generator/CompressedState.cpp
View File

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

2
src/generator/CompressedState.h
View File

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

62
src/generator/PrismNextStateGenerator.cpp
View File

@ -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>;
}
}

2
src/generator/PrismNextStateGenerator.h
View File

@ -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 {

7
src/generator/StateBehavior.cpp
View File

@ -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>;
}
}

2
src/generator/StateBehavior.h
View File

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

8
src/generator/VariableInformation.cpp
View File

@ -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 {

3
src/generator/VariableInformation.h
View File

@ -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;

41
src/storage/BitVector.cpp
View File

@ -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());
}
}

2
src/storage/BitVector.h
View File

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

2
src/storage/BitVectorHashMap.cpp
View File

@ -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.");

2
src/storage/BitVectorHashMap.h
View File

@ -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

10
src/storage/Distribution.cpp
View File

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

26
src/storage/Distribution.h
View File

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

4
src/storage/prism/Program.cpp
View File

@ -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()) {

32
test/functional/builder/ExplicitPrismModelBuilderTest.cpp
View File

@ -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());
}

8
test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
View File

@ -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();

2
test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
View File

@ -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());

2
test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
View File

@ -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());

8
test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
View File

@ -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();

2
test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
View File

@ -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);

2
test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
View File

@ -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);

18
test/functional/storage/BitVectorHashMapTest.cpp
View File

@ -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);

18
test/functional/storage/BitVectorTest.cpp
View File

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

2
test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp
View File

@ -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>>();

8
test/functional/utility/GraphTest.cpp
View File

@ -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);

Write Preview
Loading…
Cancel
Save