Fixed issue that could cause wrong models to be generated.

Former-commit-id: 8f1f9b4612

src/builder/ExplicitPrismModelBuilder.cpp

@@ -13,7 +13,7 @@
 namespace storm {
     namespace builder {
         template <typename ValueType, typename IndexType>
-        ExplicitPrismModelBuilder<ValueType, IndexType>::StateInformation::StateInformation(uint64_t bitsPerState) : stateStorage(bitsPerState, 1000000), bitsPerState(bitsPerState), reachableStates() {
+        ExplicitPrismModelBuilder<ValueType, IndexType>::StateInformation::StateInformation(uint64_t bitsPerState) : stateStorage(bitsPerState, 10000000), bitsPerState(bitsPerState), reachableStates() {
             // Intentionally left empty.
         }
         
@@ -97,7 +97,7 @@ namespace storm {
             // Start by defining the undefined constants in the model.
             storm::prism::Program preparedProgram;
             if (options.constantDefinitions) {
-                 preparedProgram = program.defineUndefinedConstants(options.constantDefinitions.get());
+                preparedProgram = program.defineUndefinedConstants(options.constantDefinitions.get());
             } else {
                 preparedProgram = program;
             }
@@ -220,6 +220,7 @@ namespace storm {
                 int_fast64_t assignedValue = evaluator.asInt(assignmentIt->getExpression());
                 STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'.");
                 newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound);
+                STORM_LOG_ASSERT(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) == assignedValue, "Writing to the bit vector bucket failed.");
             }
             
             // Check that we processed all assignments.
@@ -328,7 +329,7 @@ namespace storm {
                         choice.addProbability(stateIndex, probability);
                         probabilitySum += probability;
                     }
-                    
+
                     // Check that the resulting distribution is in fact a distribution.
                     STORM_LOG_THROW(!discreteTimeModel || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ").");
                 }

src/storage/BitVector.cpp

@@ -459,7 +459,7 @@ namespace storm {
                 bucketVector[bucket] = (bucketVector[bucket] & ~mask) | (value << (64 - (bitIndexInBucket + numberOfBits)));
             } else if (bitIndexInBucket + numberOfBits > 64) {
                 // Write the part of the value that falls into the first bucket.
-                bucketVector[bucket] = (bucketVector[bucket] & ~mask) | (value >> (64 - bitIndexInBucket));
+                bucketVector[bucket] = (bucketVector[bucket] & ~mask) | (value >> (numberOfBits + (bitIndexInBucket - 64)));
                 ++bucket;
                 
                 // Compute the remaining number of bits.

src/storage/prism/BooleanVariable.cpp

@@ -11,7 +11,7 @@ namespace storm {
         }
         
         std::ostream& operator<<(std::ostream& stream, BooleanVariable const& variable) {
-            stream << variable.getName() << ": bool " << variable.getInitialValueExpression() << ";";
+            stream << variable.getName() << ": bool init" << variable.getInitialValueExpression() << ";";
             return stream;
         }
         

src/utility/cli.h

@@ -294,7 +294,13 @@ namespace storm {
                     
                     std::cout << "Performing bisimulation minimization... ";
                     typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options;
-                    options.weak = storm::settings::bisimulationSettings().isWeakBisimulationSet();
+                    if (formula) {
+                        options = storm::storage::DeterministicModelBisimulationDecomposition<double>::Options(*model, *formula.get());
+                    }
+                    if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) {
+                        options.weak = true;
+                        options.bounded = false;
+                    }
                     
                     storm::storage::DeterministicModelBisimulationDecomposition<double> bisimulationDecomposition(*dtmc, options);
                     model = bisimulationDecomposition.getQuotient();
@@ -373,8 +379,8 @@ namespace storm {
                     std::unique_ptr<storm::modelchecker::CheckResult> result;
                     if (model->getType() == storm::models::DTMC) {
                         std::shared_ptr<storm::models::Dtmc<double>> dtmc = model->as<storm::models::Dtmc<double>>();
-//                        storm::modelchecker::SparseDtmcPrctlModelChecker<double> modelchecker(*dtmc);
-                        storm::modelchecker::SparseDtmcEliminationModelChecker<double> modelchecker(*dtmc);
+                        storm::modelchecker::SparseDtmcPrctlModelChecker<double> modelchecker(*dtmc);
+//                        storm::modelchecker::SparseDtmcEliminationModelChecker<double> modelchecker(*dtmc);
                         result = modelchecker.check(*formula.get());
                     } else if (model->getType() == storm::models::MDP) {
                         std::shared_ptr<storm::models::Mdp<double>> mdp = model->as<storm::models::Mdp<double>>();

test/functional/storage/BitVectorTest.cpp

@@ -98,6 +98,7 @@ TEST(BitVectorTest, SetFromInt) {
     EXPECT_FALSE(vector.get(62));
     EXPECT_TRUE(vector.get(63));
     
+    vector = storm::storage::BitVector(77);
     vector.setFromInt(62, 4, 15);
 
     EXPECT_TRUE(vector.get(62));
@@ -108,6 +109,14 @@ TEST(BitVectorTest, SetFromInt) {
     vector.setFromInt(62, 5, 17);
 }
 
+TEST(BitVectorTest, GetSetInt) {
+    storm::storage::BitVector vector(77);
+
+    vector.setFromInt(63, 3, 2);
+    EXPECT_EQ(2, vector.getAsInt(63, 3));
+}
+
+
 TEST(BitVectorDeathTest, GetSetAssertion) {
 	storm::storage::BitVector vector(32);