diff --git a/src/modelchecker/reachability/SparseSccModelChecker.cpp b/src/modelchecker/reachability/SparseSccModelChecker.cpp index bcb4a8f05..12707dbd9 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.cpp +++ b/src/modelchecker/reachability/SparseSccModelChecker.cpp @@ -2,6 +2,7 @@ #include +#include "src/storage/parameters.h" #include "src/storage/StronglyConnectedComponentDecomposition.h" #include "src/utility/graph.h" #include "src/utility/vector.h" @@ -26,7 +27,7 @@ namespace storm { // If the initial state is known to have either probability 0 or 1, we can directly return the result. if (!maybeStates.get(initialStateIndex)) { - return statesWithProbability0.get(initialStateIndex) ? 0 : 1; + return statesWithProbability0.get(initialStateIndex) ? storm::utility::constantZero() : storm::utility::constantOne(); } // Determine the set of states that is reachable from the initial state without jumping over a target state. @@ -131,7 +132,7 @@ namespace storm { } // Scale all entries in this row with (1 / (1 - loopProbability)). - loopProbability = 1 / (1 - loopProbability); + loopProbability = storm::utility::constantOne() / (storm::utility::constantOne() - loopProbability); for (auto& entry : matrix.getRow(state)) { entry.setValue(entry.getValue() * loopProbability); } @@ -155,7 +156,7 @@ namespace storm { // Make sure we have found the probability and set it to zero. LOG_THROW(multiplyElement != predecessorForwardTransitions.end(), storm::exceptions::InvalidStateException, "No probability for successor found."); ValueType multiplyFactor = multiplyElement->getValue(); - multiplyElement->setValue(0); + multiplyElement->setValue(storm::utility::constantZero()); // At this point, we need to update the (forward) transitions of the predecessor. typename FlexibleSparseMatrix::row_type::iterator first1 = predecessorForwardTransitions.begin(); @@ -298,7 +299,10 @@ namespace storm { template class FlexibleSparseMatrix; template class SparseSccModelChecker; - + #ifdef PARAMETRIC_SYSTEMS + template class FlexibleSparseMatrix; + template class SparseSccModelChecker; + #endif } // namespace reachability } // namespace modelchecker } // namespace storm \ No newline at end of file diff --git a/src/storm.cpp b/src/storm.cpp index 5e0b2d724..35f9cc928 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -230,12 +230,12 @@ int main(const int argc, const char* argv[]) { - storm::modelchecker::reachability::SparseSccModelChecker modelChecker; + storm::modelchecker::reachability::SparseSccModelChecker modelChecker; storm::storage::BitVector trueStates(model->getNumberOfStates(), true); storm::storage::BitVector targetStates = model->getLabeledStates("observe0Greater1"); // storm::storage::BitVector targetStates = model->getLabeledStates("one"); // storm::storage::BitVector targetStates = model->getLabeledStates("elected"); - double value = modelChecker.computeReachabilityProbability(*model->as>(), trueStates, targetStates); + storm::RationalFunction value = modelChecker.computeReachabilityProbability(*model->as>(), trueStates, targetStates); std::cout << "computed value " << value << std::endl; if (s->isSet("mincmd")) {