Output no states

Former-commit-id: d1548bb3fb

src/builder/ExplicitDFTModelBuilder.cpp

@@ -58,6 +58,7 @@ namespace storm {
                     STORM_LOG_ASSERT(mStates.getValue(pseudoStatePair.second) >= OFFSET_PSEUDO_STATE, "State is no pseudo state.");
                     STORM_LOG_TRACE("Create pseudo state from bit vector " << pseudoStatePair.second);
                     DFTStatePointer pseudoState = std::make_shared<storm::storage::DFTState<ValueType>>(pseudoStatePair.second, mDft, *mStateGenerationInfo, newIndex);
+                    pseudoState->construct();
                     STORM_LOG_ASSERT(pseudoStatePair.second == pseudoState->status(), "Pseudo states do not coincide.");
                     STORM_LOG_TRACE("Explore pseudo state " << mDft.getStateString(pseudoState) << " with id " << pseudoState->getId());
                     auto exploreResult = exploreStates(pseudoState, rowOffset, transitionMatrixBuilder, tmpMarkovianStates, modelComponents.exitRates);

src/builder/ExplicitDFTModelBuilderApprox.cpp

@@ -106,8 +106,7 @@ namespace storm {
 
             STORM_LOG_TRACE("State remapping: " << matrixBuilder.stateRemapping);
             STORM_LOG_TRACE("Markovian states: " << modelComponents.markovianStates);
-            STORM_LOG_DEBUG("Generated " << stateSize << " states");
-            STORM_LOG_DEBUG("Skipped " << skippedStates.size() << " states");
+            STORM_LOG_DEBUG("Model has " << stateSize << " states");
             STORM_LOG_DEBUG("Model is " << (generator.isDeterministicModel() ? "deterministic" : "non-deterministic"));
 
             // Build transition matrix
@@ -224,6 +223,8 @@ namespace storm {
 
         template<typename ValueType, typename StateType>
         void ExplicitDFTModelBuilderApprox<ValueType, StateType>::exploreStateSpace(double approximationThreshold) {
+            size_t nrExpandedStates = 0;
+            size_t nrSkippedStates = 0;
             // TODO Matthias: do not empty queue every time but break before
             while (!explorationQueue.empty()) {
                 // Get the first state in the queue
@@ -255,6 +256,7 @@ namespace storm {
 
                 if (currentState->isSkip(approximationThreshold, heuristic)) {
                     // Skip the current state
+                    ++nrSkippedStates;
                     STORM_LOG_TRACE("Skip expansion of state: " << dft.getStateString(currentState));
                     setMarkovian(true);
                     // Add transition to target state with temporary value 0
@@ -265,6 +267,7 @@ namespace storm {
                     matrixBuilder.finishRow();
                 } else {
                     // Explore the current state
+                    ++nrExpandedStates;
                     storm::generator::StateBehavior<ValueType, StateType> behavior = generator.expand(std::bind(&ExplicitDFTModelBuilderApprox::getOrAddStateIndex, this, std::placeholders::_1));
                     STORM_LOG_ASSERT(!behavior.empty(), "Behavior is empty.");
                     setMarkovian(behavior.begin()->isMarkovian());
@@ -273,6 +276,7 @@ namespace storm {
                     for (auto const& choice : behavior) {
                         // Add the probabilistic behavior to the matrix.
                         for (auto const& stateProbabilityPair : choice) {
+                            STORM_LOG_ASSERT(!storm::utility::isZero(stateProbabilityPair.second), "Probability zero.");
                             // Set transition to state id + offset. This helps in only remapping all previously skipped states.
                             matrixBuilder.addTransition(matrixBuilder.mappingOffset + stateProbabilityPair.first, stateProbabilityPair.second);
                             // Set heuristic values for reached states
@@ -291,6 +295,10 @@ namespace storm {
                     explorationQueue.fix();
                 }
             } // end exploration
+
+            STORM_LOG_INFO("Expanded " << nrExpandedStates << " states");
+            STORM_LOG_INFO("Skipped " << nrSkippedStates << " states");
+            STORM_LOG_ASSERT(nrSkippedStates == skippedStates.size(), "Nr skipped states is wrong");
         }
 
         template<typename ValueType, typename StateType>

src/modelchecker/dft/DFTModelChecker.cpp

@@ -169,6 +169,9 @@ namespace storm {
                     // Build model for lower bound
                     STORM_LOG_INFO("Getting model for lower bound...");
                     model = builder.getModelApproximation(true);
+                    // We only output the info from the lower bound as the info for the upper bound is the same
+                    STORM_LOG_INFO("No. states: " << model->getNumberOfStates());
+                    STORM_LOG_INFO("No. transitions: " << model->getNumberOfTransitions());
                     explorationTime += std::chrono::high_resolution_clock::now() - explorationStart;
                     // Check lower bound
                     std::unique_ptr<storm::modelchecker::CheckResult> result = checkModel(model, formula);
@@ -201,7 +204,7 @@ namespace storm {
                 STORM_LOG_INFO("Building Model...");
                 std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
                 // TODO Matthias: use only one builder if everything works again
-                if (approximationError >= 0.0) {
+                if (storm::settings::getModule<storm::settings::modules::DFTSettings>().isApproximationErrorSet()) {
                     storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
                     typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
                     builder.buildModel(labeloptions, 0);