diff --git a/src/adapters/Smt2ExpressionAdapter.h b/src/adapters/Smt2ExpressionAdapter.h index 70c4d602e..7ced9fc6b 100644 --- a/src/adapters/Smt2ExpressionAdapter.h +++ b/src/adapters/Smt2ExpressionAdapter.h @@ -129,10 +129,10 @@ namespace storm { /*! Checks whether the variables in the given set are already declared and creates them if necessary * @param variables the set of variables to check */ - std::vector const checkForUndeclaredVariables(std::set const& variables){ + std::vector const checkForUndeclaredVariables(std::set const& variables){ std::vector result; carl::VariablePool& vPool = carl::VariablePool::getInstance(); - for (storm::Variable const& variableToCheck : variables){ + for (storm::RationalFunctionVariable const& variableToCheck : variables){ std::string const& variableString = vPool.getName(variableToCheck, useReadableVarNames); // first check if this variable is already declared bool alreadyDeclared=false; @@ -170,7 +170,7 @@ namespace storm { private: // The manager that can be used to build expressions. - storm::expressions::ExpressionManager& manager; + //storm::expressions::ExpressionManager& manager; // A flag to decide whether readable var names should be used instead of intern representation bool useReadableVarNames; // the declared variables for the different scopes diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 0c9838f2d..ab56fc03b 100644 --- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -49,7 +49,7 @@ namespace storm { template - std::vector SparseDtmcPrctlHelper::computeUntilProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> resultHint = boost::none) { + std::vector SparseDtmcPrctlHelper::computeUntilProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> resultHint) { // We need to identify the states which have to be taken out of the matrix, i.e. // all states that have probability 0 and 1 of satisfying the until-formula. std::pair statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates, psiStates); @@ -83,7 +83,7 @@ namespace storm { // Initialize the x vector with the hint (if available) or with 0.5 for each element. // This is the initial guess for the iterative solvers. It should be safe as for all // 'maybe' states we know that the probability is strictly larger than 0. - std::vector x(maybeStates.getNumberOfSetBits(), ValueType(0.5)); + std::vector x(maybeStates.getNumberOfSetBits(), storm::utility::convertNumber(0.5)); if(resultHint){ storm::utility::vector::selectVectorValues(x, maybeStates, resultHint.get()); } @@ -166,7 +166,7 @@ namespace storm { } template - std::vector SparseDtmcPrctlHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& totalStateRewardVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> resultHint = boost::none) { + std::vector SparseDtmcPrctlHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& totalStateRewardVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> resultHint) { return computeReachabilityRewards(transitionMatrix, backwardTransitions, [&] (uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates) { diff --git a/src/modelchecker/region/ApproximationModel.cpp b/src/modelchecker/region/ApproximationModel.cpp index 8cc47e18a..53fc2c513 100644 --- a/src/modelchecker/region/ApproximationModel.cpp +++ b/src/modelchecker/region/ApproximationModel.cpp @@ -1,9 +1,3 @@ -/* - * File: ApproximationModel.cpp - * Author: tim - * - * Created on August 7, 2015, 9:29 AM - */ #include #include "src/modelchecker/region/ApproximationModel.h" @@ -81,7 +75,7 @@ namespace storm { filter.set(this->solverData.initialStateIndex, true); this->solverData.player1Goal = std::make_unique>( storm::logic::isLowerBound(formula->getComparisonType()) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize, - formula->getBound(), + formula->getBound().convertToOtherValueType(), filter ); } @@ -386,7 +380,7 @@ namespace storm { } if(this->typeOfParametricModel == storm::models::ModelType::Dtmc){ //Invoke mdp model checking - std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(player2Goal, storm::utility::solver::MinMaxLinearEquationSolverFactory(), this->matrixData.matrix); + std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(player2Goal, storm::solver::GeneralMinMaxLinearEquationSolverFactory(), this->matrixData.matrix); solver->setTerminationCondition(std::move(terminationCondition)); storm::utility::policyguessing::solveMinMaxLinearEquationSystem(*solver, this->solverData.result, this->vectorData.vector, diff --git a/src/modelchecker/region/ParameterRegion.cpp b/src/modelchecker/region/ParameterRegion.cpp index 3860cab19..b04fda643 100644 --- a/src/modelchecker/region/ParameterRegion.cpp +++ b/src/modelchecker/region/ParameterRegion.cpp @@ -145,7 +145,7 @@ namespace storm { //The resulting subregion is the smallest region containing vertex and splittingPoint. VariableSubstitutionType subLower, subUpper; for(auto variableBound : this->lowerBoundaries){ - Variable variable = variableBound.first; + VariableType variable = variableBound.first; auto vertexEntry=vertex.find(variable); auto splittingPointEntry=splittingPoint.find(variable); subLower.insert(typename VariableSubstitutionType::value_type(variable, std::min(vertexEntry->second, splittingPointEntry->second))); @@ -281,17 +281,17 @@ namespace storm { template std::vector> ParameterRegion::getRegionsFromSettings(){ - STORM_LOG_THROW(storm::settings::regionSettings().isRegionsSet() || storm::settings::regionSettings().isRegionFileSet(), storm::exceptions::InvalidSettingsException, "Tried to obtain regions from the settings but no regions are specified."); - STORM_LOG_THROW(!(storm::settings::regionSettings().isRegionsSet() && storm::settings::regionSettings().isRegionFileSet()), storm::exceptions::InvalidSettingsException, "Regions are specified via file AND cmd line. Only one option is allowed."); + STORM_LOG_THROW(storm::settings::getModule().isRegionsSet() ||storm::settings::getModule().isRegionFileSet(), storm::exceptions::InvalidSettingsException, "Tried to obtain regions from the settings but no regions are specified."); + STORM_LOG_THROW(!(storm::settings::getModule().isRegionsSet() && storm::settings::getModule().isRegionFileSet()), storm::exceptions::InvalidSettingsException, "Regions are specified via file AND cmd line. Only one option is allowed."); std::string regionsString; - if(storm::settings::regionSettings().isRegionsSet()){ - regionsString = storm::settings::regionSettings().getRegionsFromCmdLine(); + if(storm::settings::getModule().isRegionsSet()){ + regionsString = storm::settings::getModule().getRegionsFromCmdLine(); } else{ //if we reach this point we can assume that the region is given as a file. - STORM_LOG_THROW(storm::parser::MappedFile::fileExistsAndIsReadable(storm::settings::regionSettings().getRegionFilePath().c_str()), storm::exceptions::InvalidSettingsException, "The path to the file in which the regions are specified is not valid."); - storm::parser::MappedFile mf(storm::settings::regionSettings().getRegionFilePath().c_str()); + STORM_LOG_THROW(storm::parser::MappedFile::fileExistsAndIsReadable(storm::settings::getModule().getRegionFilePath().c_str()), storm::exceptions::InvalidSettingsException, "The path to the file in which the regions are specified is not valid."); + storm::parser::MappedFile mf(storm::settings::getModule().getRegionFilePath().c_str()); regionsString = std::string(mf.getData(),mf.getDataSize()); } return parseMultipleRegions(regionsString); diff --git a/src/modelchecker/region/SamplingModel.cpp b/src/modelchecker/region/SamplingModel.cpp index 9ebecf525..2452b30da 100644 --- a/src/modelchecker/region/SamplingModel.cpp +++ b/src/modelchecker/region/SamplingModel.cpp @@ -89,7 +89,7 @@ namespace storm { filter.set(this->solverData.initialStateIndex, true); this->solverData.solveGoal = std::make_unique>( storm::logic::isLowerBound(formula->getComparisonType()) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize, - formula->getBound(), + formula->getBound().convertToOtherValueType(), filter ); } @@ -127,7 +127,7 @@ namespace storm { if(this->typeOfParametricModel == storm::models::ModelType::Dtmc){ storm::storage::SparseMatrix submatrix = instantiatedModel.getTransitionMatrix().getSubmatrix(true, this->maybeStates, this->maybeStates, true); submatrix.convertToEquationSystem(); - std::unique_ptr> solver = storm::utility::solver::LinearEquationSolverFactory().create(submatrix); + std::unique_ptr> solver = storm::solver::GeneralLinearEquationSolverFactory().create(submatrix); std::vector b; if(this->computeRewards){ b.resize(submatrix.getRowCount()); @@ -135,10 +135,10 @@ namespace storm { } else { b = instantiatedModel.getTransitionMatrix().getConstrainedRowSumVector(this->maybeStates, this->targetStates); } - solver->solveEquationSystem(this->solverData.result, b); + solver->solveEquations(this->solverData.result, b); } else if(this->typeOfParametricModel == storm::models::ModelType::Mdp){ storm::storage::SparseMatrix submatrix = instantiatedModel.getTransitionMatrix().getSubmatrix(true, this->maybeStates, this->maybeStates, false); - std::unique_ptr> solver = storm::utility::solver::MinMaxLinearEquationSolverFactory().create(submatrix); + std::unique_ptr> solver = storm::solver::GeneralMinMaxLinearEquationSolverFactory().create(submatrix); std::vector b = instantiatedModel.getTransitionMatrix().getConstrainedRowGroupSumVector(this->maybeStates, this->targetStates); storm::storage::BitVector targetChoices(b.size(), false); for(std::size_t i = 0; i newStateIndexMap(flexibleTransitions.getNumberOfRows(), flexibleTransitions.getNumberOfRows()); //initialize with some illegal index to easily check if a transition leads to an unselected state + std::vector newStateIndexMap(flexibleTransitions.getRowCount(), flexibleTransitions.getRowCount()); //initialize with some illegal index to easily check if a transition leads to an unselected state storm::storage::sparse::state_type newStateIndex=0; for(auto const& state : subsystem){ newStateIndexMap[state]=newStateIndex; @@ -171,7 +171,7 @@ namespace storm { ParametricType missingProbability=storm::utility::region::getNewFunction(storm::utility::one()); //go through columns: for(auto& entry: flexibleTransitions.getRow(oldStateIndex)){ - STORM_LOG_THROW(newStateIndexMap[entry.getColumn()]!=flexibleTransitions.getNumberOfRows(), storm::exceptions::UnexpectedException, "There is a transition to a state that should have been eliminated."); + STORM_LOG_THROW(newStateIndexMap[entry.getColumn()]!=flexibleTransitions.getRowCount(), storm::exceptions::UnexpectedException, "There is a transition to a state that should have been eliminated."); missingProbability-=entry.getValue(); matrixBuilder.addNextValue(newStateIndexMap[oldStateIndex],newStateIndexMap[entry.getColumn()], storm::utility::simplify(entry.getValue())); } @@ -236,8 +236,8 @@ namespace storm { simpleFormula = std::shared_ptr(new storm::logic::ProbabilityOperatorFormula(eventuallyFormula, storm::logic::OperatorInformation(boost::none, this->getSpecifiedFormula()->getBound()))); } //Check if the reachability function needs to be computed - if((storm::settings::regionSettings().getSmtMode()==storm::settings::modules::RegionSettings::SmtMode::FUNCTION) || - (storm::settings::regionSettings().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE)){ + if((storm::settings::getModule().getSmtMode()==storm::settings::modules::RegionSettings::SmtMode::FUNCTION) || + (storm::settings::getModule().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE)){ this->computeReachabilityFunction(*(this->getSimpleModel())->template as>()); } } @@ -428,8 +428,8 @@ namespace storm { template bool SparseDtmcRegionModelChecker::checkPoint(ParameterRegion& region, std::mapconst& point, bool favorViaFunction) { bool valueInBoundOfFormula; - if((storm::settings::regionSettings().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE) || - (!storm::settings::regionSettings().doSample() && favorViaFunction)){ + if((storm::settings::getModule().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE) || + (!storm::settings::getModule().doSample() && favorViaFunction)){ //evaluate the reachability function valueInBoundOfFormula = this->valueIsInBoundOfFormula(this->evaluateReachabilityFunction(point)); } @@ -485,7 +485,7 @@ namespace storm { template bool SparseDtmcRegionModelChecker::checkSmt(ParameterRegion& region) { - STORM_LOG_THROW((storm::settings::regionSettings().getSmtMode()==storm::settings::modules::RegionSettings::SmtMode::FUNCTION), storm::exceptions::NotImplementedException, "Selected SMT mode has not been implemented."); + STORM_LOG_THROW((storm::settings::getModule().getSmtMode()==storm::settings::modules::RegionSettings::SmtMode::FUNCTION), storm::exceptions::NotImplementedException, "Selected SMT mode has not been implemented."); if (region.getCheckResult()==RegionCheckResult::UNKNOWN){ //Sampling needs to be done (on a single point) checkPoint(region,region.getSomePoint(), true); diff --git a/src/modelchecker/region/SparseMdpRegionModelChecker.cpp b/src/modelchecker/region/SparseMdpRegionModelChecker.cpp index cd35efbdc..ce455cd85 100644 --- a/src/modelchecker/region/SparseMdpRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseMdpRegionModelChecker.cpp @@ -13,6 +13,8 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/RegionSettings.h" #include "src/solver/OptimizationDirection.h" +#include "src/solver/stateelimination/PrioritizedStateEliminator.h" +#include "src/solver/stateelimination/StaticStatePriorityQueue.h" #include "src/storage/sparse/StateType.h" #include "src/storage/FlexibleSparseMatrix.h" #include "src/utility/constants.h" @@ -102,9 +104,13 @@ namespace storm { //The states that we consider to eliminate storm::storage::BitVector considerToEliminate(submatrix.getRowGroupCount(), true); considerToEliminate.set(initialState, false); + + + std::vector statesToEliminate; for (auto const& state : considerToEliminate) { - bool eliminateThisState=true; - if(submatrix.getRowGroupSize(state) == 1){ + bool eliminateThisState=false; + if(submatrix.getRowGroupSize(state) == 1) { + eliminateThisState=true; //state is deterministic. Check if outgoing transitions are constant for(auto const& entry : submatrix.getRowGroup(state)){ if(!storm::utility::isConstant(entry.getValue())){ @@ -115,21 +121,20 @@ namespace storm { if(!storm::utility::isConstant(oneStepProbabilities[submatrix.getRowGroupIndices()[state]])){ eliminateThisState=false; } - } else { - eliminateThisState = false; } - if(eliminateThisState){ - storm::storage::FlexibleSparseMatrix::eliminateState(flexibleTransitions, oneStepProbabilities, state, submatrix.getRowGroupIndices()[state], flexibleBackwardTransitions, noStateRewards); - subsystem.set(state,false); + if(eliminateThisState) { + subsystem.set(state, false); + statesToEliminate.push_back(state); } } + storm::solver::stateelimination::PrioritizedStateEliminator(flexibleTransitions, flexibleBackwardTransitions, statesToEliminate, oneStepProbabilities); STORM_LOG_DEBUG("Eliminated " << subsystem.size() - subsystem.getNumberOfSetBits() << " of " << subsystem.size() << " states that had constant outgoing transitions."); //Build the simple model STORM_LOG_DEBUG("Building the resulting simplified model."); //The matrix. The flexibleTransitions matrix might have empty rows where states have been eliminated. //The new matrix should not have such rows. We therefore leave them out, but we have to change the indices of the states accordingly. - std::vector newStateIndexMap(flexibleTransitions.getNumberOfRows(), flexibleTransitions.getNumberOfRows()); //initialize with some illegal index + std::vector newStateIndexMap(flexibleTransitions.getRowCount(), flexibleTransitions.getRowCount()); //initialize with some illegal index storm::storage::sparse::state_type newStateIndex=0; for(auto const& state : subsystem){ newStateIndexMap[state]=newStateIndex; @@ -148,7 +153,7 @@ namespace storm { ParametricType missingProbability=storm::utility::region::getNewFunction(storm::utility::one()); //go through columns: for(auto& entry: flexibleTransitions.getRow(oldRow)){ - STORM_LOG_THROW(newStateIndexMap[entry.getColumn()]!=flexibleTransitions.getNumberOfRows(), storm::exceptions::UnexpectedException, "There is a transition to a state that should have been eliminated."); + STORM_LOG_THROW(newStateIndexMap[entry.getColumn()]!=flexibleTransitions.getRowCount(), storm::exceptions::UnexpectedException, "There is a transition to a state that should have been eliminated."); missingProbability-=entry.getValue(); matrixBuilder.addNextValue(curRow,newStateIndexMap[entry.getColumn()], storm::utility::simplify(entry.getValue())); } diff --git a/src/modelchecker/region/SparseRegionModelChecker.cpp b/src/modelchecker/region/SparseRegionModelChecker.cpp index d1c861a7c..a9172a204 100644 --- a/src/modelchecker/region/SparseRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseRegionModelChecker.cpp @@ -24,7 +24,6 @@ #include "src/exceptions/InvalidSettingsException.h" #include "src/exceptions/NotImplementedException.h" #include "src/exceptions/UnexpectedException.h" -#include "utility/ConversionHelper.h" #include "modelchecker/results/CheckResult.h" #include "modelchecker/results/ExplicitQuantitativeCheckResult.h" @@ -134,11 +133,11 @@ namespace storm { //Check if the approximation and the sampling model needs to be computed if(!this->isResultConstant()){ - if(this->isApproximationApplicable && storm::settings::regionSettings().doApprox()){ + if(this->isApproximationApplicable && storm::settings::getModule().doApprox()){ initializeApproximationModel(*this->getSimpleModel(), this->getSimpleFormula()); } - if(storm::settings::regionSettings().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE || - (!storm::settings::regionSettings().doSample() && storm::settings::regionSettings().getApproxMode()==storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST)){ + if(storm::settings::getModule().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE || + (!storm::settings::getModule().doSample() && storm::settings::getModule().getApproxMode()==storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST)){ initializeSamplingModel(*this->getSimpleModel(), this->getSimpleFormula()); } } else if (this->isResultConstant() && this->constantResult.get() == storm::utility::region::convertNumber(-1.0)){ @@ -241,10 +240,10 @@ namespace storm { //switches for the different steps. bool done=false; - STORM_LOG_WARN_COND( (!storm::settings::regionSettings().doApprox() || this->isApproximationApplicable), "the approximation is only correct if the model has only linear functions (more precisely: linear in a single parameter, i.e., functions like p*q are okay). As this is not the case, approximation is deactivated"); - bool doApproximation=storm::settings::regionSettings().doApprox() && this->isApproximationApplicable; - bool doSampling=storm::settings::regionSettings().doSample(); - bool doSmt=storm::settings::regionSettings().doSmt(); + STORM_LOG_WARN_COND( (!storm::settings::getModule().doApprox() || this->isApproximationApplicable), "the approximation is only correct if the model has only linear functions (more precisely: linear in a single parameter, i.e., functions like p*q are okay). As this is not the case, approximation is deactivated"); + bool doApproximation=storm::settings::getModule().doApprox() && this->isApproximationApplicable; + bool doSampling=storm::settings::getModule().doSample(); + bool doSmt=storm::settings::getModule().doSmt(); if(this->isResultConstant()){ STORM_LOG_DEBUG("Checking a region although the result is constant, i.e., independent of the region. This makes sense none."); @@ -317,7 +316,7 @@ namespace storm { bool proveAllSat; switch (region.getCheckResult()){ case RegionCheckResult::UNKNOWN: - switch(storm::settings::regionSettings().getApproxMode()){ + switch(storm::settings::getModule().getApproxMode()){ case storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST: //Sample a single point to know whether we should try to prove ALLSAT or ALLVIOLATED checkPoint(region,region.getSomePoint(), false); diff --git a/src/solver/Smt2SmtSolver.cpp b/src/solver/Smt2SmtSolver.cpp index cf0e3034a..a04e13148 100644 --- a/src/solver/Smt2SmtSolver.cpp +++ b/src/solver/Smt2SmtSolver.cpp @@ -115,7 +115,7 @@ namespace storm { writeCommand("( assert " + expressionAdapter->translateExpression(constraint) + " )", true); } - void Smt2SmtSolver::add(storm::Variable const& guard, typename storm::ArithConstraint const& constraint){ + void Smt2SmtSolver::add(storm::RationalFunctionVariable const& guard, typename storm::ArithConstraint const& constraint){ STORM_LOG_THROW((guard.getType()==carl::VariableType::VT_BOOL), storm::exceptions::IllegalArgumentException, "Tried to add a guarded constraint, but the guard is not of type bool."); //if some of the occurring variables are not declared yet, we will have to (including the guard!). std::set variables = constraint.lhs().gatherVariables(); @@ -128,7 +128,7 @@ namespace storm { writeCommand("( assert (=> " + guardName + " " + expressionAdapter->translateExpression(constraint) + " ) )", true); } - void Smt2SmtSolver::add(const storm::Variable& variable, bool value){ + void Smt2SmtSolver::add(const storm::RationalFunctionVariable& variable, bool value){ STORM_LOG_THROW((variable.getType()==carl::VariableType::VT_BOOL), storm::exceptions::IllegalArgumentException, "Tried to add a constraint that consists of a non-boolean variable."); std::set variableSet; variableSet.insert(variable); diff --git a/src/solver/Smt2SmtSolver.h b/src/solver/Smt2SmtSolver.h index 3f4f8b877..5f455cb3d 100644 --- a/src/solver/Smt2SmtSolver.h +++ b/src/solver/Smt2SmtSolver.h @@ -60,10 +60,10 @@ namespace storm { void add(typename storm::ArithConstraint const& constraint); // adds the given carl constraint that is guarded by the given guard. The guard should have type 'bool' - void add(storm::Variable const& guard, typename storm::ArithConstraint const& constraint); + void add(storm::RationalFunctionVariable const& guard, typename storm::ArithConstraint const& constraint); // asserts that the given variable has the given value. The variable should have type 'bool' - void add(storm::Variable const& variable, bool value); + void add(storm::RationalFunctionVariable const& variable, bool value); #endif virtual CheckResult check() override; diff --git a/src/solver/stateelimination/PrioritizedStateEliminator.cpp b/src/solver/stateelimination/PrioritizedStateEliminator.cpp index 1b8cca6ff..39586caea 100644 --- a/src/solver/stateelimination/PrioritizedStateEliminator.cpp +++ b/src/solver/stateelimination/PrioritizedStateEliminator.cpp @@ -5,10 +5,17 @@ #include "src/utility/macros.h" #include "src/utility/constants.h" +#include "StaticStatePriorityQueue.h" + namespace storm { namespace solver { namespace stateelimination { - + + template + PrioritizedStateEliminator::PrioritizedStateEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, std::vector const& statesToEliminate, std::vector& stateValues) + : PrioritizedStateEliminator(transitionMatrix, backwardTransitions, std::make_shared(statesToEliminate), stateValues) + {} + template PrioritizedStateEliminator::PrioritizedStateEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector& stateValues) : StateEliminator(transitionMatrix, backwardTransitions), priorityQueue(priorityQueue), stateValues(stateValues) { } diff --git a/src/solver/stateelimination/PrioritizedStateEliminator.h b/src/solver/stateelimination/PrioritizedStateEliminator.h index b31c58932..a20a769f0 100644 --- a/src/solver/stateelimination/PrioritizedStateEliminator.h +++ b/src/solver/stateelimination/PrioritizedStateEliminator.h @@ -15,7 +15,8 @@ namespace storm { typedef typename std::shared_ptr PriorityQueuePointer; PrioritizedStateEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector& stateValues); - + PrioritizedStateEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, std::vector const& statesToEliminate, std::vector& stateValues); + // Instantiaton of virtual methods. void updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) override; void updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) override; diff --git a/src/utility/region.h b/src/utility/region.h index fa740a9d8..94051ac49 100644 --- a/src/utility/region.h +++ b/src/utility/region.h @@ -27,7 +27,7 @@ namespace storm { //Obtain the correct type for Variables and Coefficients out of a given Function type #ifdef STORM_HAVE_CARL template - using VariableType = typename std::conditional<(std::is_same::value), storm::Variable, std::nullptr_t>::type; + using VariableType = typename std::conditional<(std::is_same::value), storm::RationalFunctionVariable, std::nullptr_t>::type; template using CoefficientType = typename std::conditional<(std::is_same::value), storm::RationalFunction::CoeffType, std::nullptr_t>::type; #else