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

towards merging, including a extension on the pstateeliminator, come back after generalizing the lra eliminator 

Former-commit-id: 8ce98b8287
main
sjunges 9 years ago
parent
93dc705b06
commit
31228486d3
13 changed files with 63 additions and 57 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 6
      src/adapters/Smt2ExpressionAdapter.h
  2. 6
      src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
  3. 10
      src/modelchecker/region/ApproximationModel.cpp
  4. 14
      src/modelchecker/region/ParameterRegion.cpp
  5. 8
      src/modelchecker/region/SamplingModel.cpp
  6. 14
      src/modelchecker/region/SparseDtmcRegionModelChecker.cpp
  7. 23
      src/modelchecker/region/SparseMdpRegionModelChecker.cpp
  8. 17
      src/modelchecker/region/SparseRegionModelChecker.cpp
  9. 4
      src/solver/Smt2SmtSolver.cpp
  10. 4
      src/solver/Smt2SmtSolver.h
  11. 9
      src/solver/stateelimination/PrioritizedStateEliminator.cpp
  12. 3
      src/solver/stateelimination/PrioritizedStateEliminator.h
  13. 2
      src/utility/region.h

6
src/adapters/Smt2ExpressionAdapter.h
View File

@ -129,10 +129,10 @@ namespace storm {
/*! Checks whether the variables in the given set are already declared and creates them if necessary /*! Checks whether the variables in the given set are already declared and creates them if necessary
* @param variables the set of variables to check * @param variables the set of variables to check
*/ */
std::vector<std::string> const checkForUndeclaredVariables(std::set<storm::Variable> const& variables){
std::vector<std::string> const checkForUndeclaredVariables(std::set<storm::RationalFunctionVariable> const& variables){
std::vector<std::string> result; std::vector<std::string> result;
carl::VariablePool& vPool = carl::VariablePool::getInstance(); 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); std::string const& variableString = vPool.getName(variableToCheck, useReadableVarNames);
// first check if this variable is already declared // first check if this variable is already declared
bool alreadyDeclared=false; bool alreadyDeclared=false;
@ -170,7 +170,7 @@ namespace storm {
private: private:
// The manager that can be used to build expressions. // 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 // A flag to decide whether readable var names should be used instead of intern representation
bool useReadableVarNames; bool useReadableVarNames;
// the declared variables for the different scopes // the declared variables for the different scopes

6
src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
View File

@ -49,7 +49,7 @@ namespace storm {
template<typename ValueType, typename RewardModelType> template<typename ValueType, typename RewardModelType>
std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeUntilProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory, boost::optional<std::vector<ValueType>> resultHint = boost::none) {
std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeUntilProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory, boost::optional<std::vector<ValueType>> resultHint) {
// We need to identify the states which have to be taken out of the matrix, i.e. // 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. // all states that have probability 0 and 1 of satisfying the until-formula.
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates, psiStates); std::pair<storm::storage::BitVector, storm::storage::BitVector> 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. // 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 // 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. // 'maybe' states we know that the probability is strictly larger than 0.
std::vector<ValueType> x(maybeStates.getNumberOfSetBits(), ValueType(0.5));
std::vector<ValueType> x(maybeStates.getNumberOfSetBits(), storm::utility::convertNumber<ValueType>(0.5));
if(resultHint){ if(resultHint){
storm::utility::vector::selectVectorValues(x, maybeStates, resultHint.get()); storm::utility::vector::selectVectorValues(x, maybeStates, resultHint.get());
} }
@ -166,7 +166,7 @@ namespace storm {
} }
template<typename ValueType, typename RewardModelType> template<typename ValueType, typename RewardModelType>
std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& totalStateRewardVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory, boost::optional<std::vector<ValueType>> resultHint = boost::none) {
std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& totalStateRewardVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory, boost::optional<std::vector<ValueType>> resultHint) {
return computeReachabilityRewards(transitionMatrix, backwardTransitions, return computeReachabilityRewards(transitionMatrix, backwardTransitions,
[&] (uint_fast64_t numberOfRows, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates) { [&] (uint_fast64_t numberOfRows, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates) {

10
src/modelchecker/region/ApproximationModel.cpp
View File

@ -1,9 +1,3 @@
/*
* File: ApproximationModel.cpp
* Author: tim
*
* Created on August 7, 2015, 9:29 AM
*/
#include <stdint.h> #include <stdint.h>
#include "src/modelchecker/region/ApproximationModel.h" #include "src/modelchecker/region/ApproximationModel.h"
@ -81,7 +75,7 @@ namespace storm {
filter.set(this->solverData.initialStateIndex, true); filter.set(this->solverData.initialStateIndex, true);
this->solverData.player1Goal = std::make_unique<storm::solver::BoundedGoal<ConstantType>>( this->solverData.player1Goal = std::make_unique<storm::solver::BoundedGoal<ConstantType>>(
storm::logic::isLowerBound(formula->getComparisonType()) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize, storm::logic::isLowerBound(formula->getComparisonType()) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize,
formula->getBound(),
formula->getBound().convertToOtherValueType<ConstantType>(),
filter filter
); );
} }
@ -386,7 +380,7 @@ namespace storm {
} }
if(this->typeOfParametricModel == storm::models::ModelType::Dtmc){ if(this->typeOfParametricModel == storm::models::ModelType::Dtmc){
//Invoke mdp model checking //Invoke mdp model checking
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ConstantType>> solver = storm::solver::configureMinMaxLinearEquationSolver(player2Goal, storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(), this->matrixData.matrix);
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ConstantType>> solver = storm::solver::configureMinMaxLinearEquationSolver(player2Goal, storm::solver::GeneralMinMaxLinearEquationSolverFactory<double>(), this->matrixData.matrix);
solver->setTerminationCondition(std::move(terminationCondition)); solver->setTerminationCondition(std::move(terminationCondition));
storm::utility::policyguessing::solveMinMaxLinearEquationSystem(*solver, storm::utility::policyguessing::solveMinMaxLinearEquationSystem(*solver,
this->solverData.result, this->vectorData.vector, this->solverData.result, this->vectorData.vector,

14
src/modelchecker/region/ParameterRegion.cpp
View File

@ -145,7 +145,7 @@ namespace storm {
//The resulting subregion is the smallest region containing vertex and splittingPoint. //The resulting subregion is the smallest region containing vertex and splittingPoint.
VariableSubstitutionType subLower, subUpper; VariableSubstitutionType subLower, subUpper;
for(auto variableBound : this->lowerBoundaries){ for(auto variableBound : this->lowerBoundaries){
Variable variable = variableBound.first;
VariableType variable = variableBound.first;
auto vertexEntry=vertex.find(variable); auto vertexEntry=vertex.find(variable);
auto splittingPointEntry=splittingPoint.find(variable); auto splittingPointEntry=splittingPoint.find(variable);
subLower.insert(typename VariableSubstitutionType::value_type(variable, std::min(vertexEntry->second, splittingPointEntry->second))); subLower.insert(typename VariableSubstitutionType::value_type(variable, std::min(vertexEntry->second, splittingPointEntry->second)));
@ -281,17 +281,17 @@ namespace storm {
template<typename ParametricType> template<typename ParametricType>
std::vector<ParameterRegion<ParametricType>> ParameterRegion<ParametricType>::getRegionsFromSettings(){ std::vector<ParameterRegion<ParametricType>> ParameterRegion<ParametricType>::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<storm::settings::modules::RegionSettings>().isRegionsSet() ||storm::settings::getModule<storm::settings::modules::RegionSettings>().isRegionFileSet(), storm::exceptions::InvalidSettingsException, "Tried to obtain regions from the settings but no regions are specified.");
STORM_LOG_THROW(!(storm::settings::getModule<storm::settings::modules::RegionSettings>().isRegionsSet() && storm::settings::getModule<storm::settings::modules::RegionSettings>().isRegionFileSet()), storm::exceptions::InvalidSettingsException, "Regions are specified via file AND cmd line. Only one option is allowed.");
std::string regionsString; std::string regionsString;
if(storm::settings::regionSettings().isRegionsSet()){
regionsString = storm::settings::regionSettings().getRegionsFromCmdLine();
if(storm::settings::getModule<storm::settings::modules::RegionSettings>().isRegionsSet()){
regionsString = storm::settings::getModule<storm::settings::modules::RegionSettings>().getRegionsFromCmdLine();
} }
else{ else{
//if we reach this point we can assume that the region is given as a file. //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<storm::settings::modules::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::getModule<storm::settings::modules::RegionSettings>().getRegionFilePath().c_str());
regionsString = std::string(mf.getData(),mf.getDataSize()); regionsString = std::string(mf.getData(),mf.getDataSize());
} }
return parseMultipleRegions(regionsString); return parseMultipleRegions(regionsString);

8
src/modelchecker/region/SamplingModel.cpp
View File

@ -89,7 +89,7 @@ namespace storm {
filter.set(this->solverData.initialStateIndex, true); filter.set(this->solverData.initialStateIndex, true);
this->solverData.solveGoal = std::make_unique<storm::solver::BoundedGoal<ConstantType>>( this->solverData.solveGoal = std::make_unique<storm::solver::BoundedGoal<ConstantType>>(
storm::logic::isLowerBound(formula->getComparisonType()) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize, storm::logic::isLowerBound(formula->getComparisonType()) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize,
formula->getBound(),
formula->getBound().convertToOtherValueType<ConstantType>(),
filter filter
); );
} }
@ -127,7 +127,7 @@ namespace storm {
if(this->typeOfParametricModel == storm::models::ModelType::Dtmc){ if(this->typeOfParametricModel == storm::models::ModelType::Dtmc){
storm::storage::SparseMatrix<ConstantType> submatrix = instantiatedModel.getTransitionMatrix().getSubmatrix(true, this->maybeStates, this->maybeStates, true); storm::storage::SparseMatrix<ConstantType> submatrix = instantiatedModel.getTransitionMatrix().getSubmatrix(true, this->maybeStates, this->maybeStates, true);
submatrix.convertToEquationSystem(); submatrix.convertToEquationSystem();
std::unique_ptr<storm::solver::LinearEquationSolver<ConstantType>> solver = storm::utility::solver::LinearEquationSolverFactory<ConstantType>().create(submatrix);
std::unique_ptr<storm::solver::LinearEquationSolver<ConstantType>> solver = storm::solver::GeneralLinearEquationSolverFactory<ConstantType>().create(submatrix);
std::vector<ConstantType> b; std::vector<ConstantType> b;
if(this->computeRewards){ if(this->computeRewards){
b.resize(submatrix.getRowCount()); b.resize(submatrix.getRowCount());
@ -135,10 +135,10 @@ namespace storm {
} else { } else {
b = instantiatedModel.getTransitionMatrix().getConstrainedRowSumVector(this->maybeStates, this->targetStates); 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){ } else if(this->typeOfParametricModel == storm::models::ModelType::Mdp){
storm::storage::SparseMatrix<ConstantType> submatrix = instantiatedModel.getTransitionMatrix().getSubmatrix(true, this->maybeStates, this->maybeStates, false); storm::storage::SparseMatrix<ConstantType> submatrix = instantiatedModel.getTransitionMatrix().getSubmatrix(true, this->maybeStates, this->maybeStates, false);
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ConstantType>> solver = storm::utility::solver::MinMaxLinearEquationSolverFactory<ConstantType>().create(submatrix);
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ConstantType>> solver = storm::solver::GeneralMinMaxLinearEquationSolverFactory<ConstantType>().create(submatrix);
std::vector<ConstantType> b = instantiatedModel.getTransitionMatrix().getConstrainedRowGroupSumVector(this->maybeStates, this->targetStates); std::vector<ConstantType> b = instantiatedModel.getTransitionMatrix().getConstrainedRowGroupSumVector(this->maybeStates, this->targetStates);
storm::storage::BitVector targetChoices(b.size(), false); storm::storage::BitVector targetChoices(b.size(), false);
for(std::size_t i = 0; i<b.size(); ++i){ for(std::size_t i = 0; i<b.size(); ++i){

14
src/modelchecker/region/SparseDtmcRegionModelChecker.cpp
View File

@ -155,7 +155,7 @@ namespace storm {
STORM_LOG_DEBUG("Building the resulting simplified model."); STORM_LOG_DEBUG("Building the resulting simplified model.");
//The matrix. The flexibleTransitions matrix might have empty rows where states have been eliminated. //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. //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<storm::storage::sparse::state_type> newStateIndexMap(flexibleTransitions.getNumberOfRows(), flexibleTransitions.getNumberOfRows()); //initialize with some illegal index to easily check if a transition leads to an unselected state
std::vector<storm::storage::sparse::state_type> 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; storm::storage::sparse::state_type newStateIndex=0;
for(auto const& state : subsystem){ for(auto const& state : subsystem){
newStateIndexMap[state]=newStateIndex; newStateIndexMap[state]=newStateIndex;
@ -171,7 +171,7 @@ namespace storm {
ParametricType missingProbability=storm::utility::region::getNewFunction<ParametricType, CoefficientType>(storm::utility::one<CoefficientType>()); ParametricType missingProbability=storm::utility::region::getNewFunction<ParametricType, CoefficientType>(storm::utility::one<CoefficientType>());
//go through columns: //go through columns:
for(auto& entry: flexibleTransitions.getRow(oldStateIndex)){ 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(); missingProbability-=entry.getValue();
matrixBuilder.addNextValue(newStateIndexMap[oldStateIndex],newStateIndexMap[entry.getColumn()], storm::utility::simplify(entry.getValue())); matrixBuilder.addNextValue(newStateIndexMap[oldStateIndex],newStateIndexMap[entry.getColumn()], storm::utility::simplify(entry.getValue()));
} }
@ -236,8 +236,8 @@ namespace storm {
simpleFormula = std::shared_ptr<storm::logic::OperatorFormula>(new storm::logic::ProbabilityOperatorFormula(eventuallyFormula, storm::logic::OperatorInformation(boost::none, this->getSpecifiedFormula()->getBound()))); simpleFormula = std::shared_ptr<storm::logic::OperatorFormula>(new storm::logic::ProbabilityOperatorFormula(eventuallyFormula, storm::logic::OperatorInformation(boost::none, this->getSpecifiedFormula()->getBound())));
} }
//Check if the reachability function needs to be computed //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<storm::settings::modules::RegionSettings>().getSmtMode()==storm::settings::modules::RegionSettings::SmtMode::FUNCTION) ||
(storm::settings::getModule<storm::settings::modules::RegionSettings>().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE)){
this->computeReachabilityFunction(*(this->getSimpleModel())->template as<storm::models::sparse::Dtmc<ParametricType>>()); this->computeReachabilityFunction(*(this->getSimpleModel())->template as<storm::models::sparse::Dtmc<ParametricType>>());
} }
} }
@ -428,8 +428,8 @@ namespace storm {
template<typename ParametricSparseModelType, typename ConstantType> template<typename ParametricSparseModelType, typename ConstantType>
bool SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::checkPoint(ParameterRegion<ParametricType>& region, std::map<VariableType, CoefficientType>const& point, bool favorViaFunction) { bool SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::checkPoint(ParameterRegion<ParametricType>& region, std::map<VariableType, CoefficientType>const& point, bool favorViaFunction) {
bool valueInBoundOfFormula; bool valueInBoundOfFormula;
if((storm::settings::regionSettings().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE) ||
(!storm::settings::regionSettings().doSample() && favorViaFunction)){
if((storm::settings::getModule<storm::settings::modules::RegionSettings>().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE) ||
(!storm::settings::getModule<storm::settings::modules::RegionSettings>().doSample() && favorViaFunction)){
//evaluate the reachability function //evaluate the reachability function
valueInBoundOfFormula = this->valueIsInBoundOfFormula(this->evaluateReachabilityFunction(point)); valueInBoundOfFormula = this->valueIsInBoundOfFormula(this->evaluateReachabilityFunction(point));
} }
@ -485,7 +485,7 @@ namespace storm {
template<typename ParametricSparseModelType, typename ConstantType> template<typename ParametricSparseModelType, typename ConstantType>
bool SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::checkSmt(ParameterRegion<ParametricType>& region) { bool SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::checkSmt(ParameterRegion<ParametricType>& 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<storm::settings::modules::RegionSettings>().getSmtMode()==storm::settings::modules::RegionSettings::SmtMode::FUNCTION), storm::exceptions::NotImplementedException, "Selected SMT mode has not been implemented.");
if (region.getCheckResult()==RegionCheckResult::UNKNOWN){ if (region.getCheckResult()==RegionCheckResult::UNKNOWN){
//Sampling needs to be done (on a single point) //Sampling needs to be done (on a single point)
checkPoint(region,region.getSomePoint(), true); checkPoint(region,region.getSomePoint(), true);

23
src/modelchecker/region/SparseMdpRegionModelChecker.cpp
View File

@ -13,6 +13,8 @@
#include "src/settings/SettingsManager.h" #include "src/settings/SettingsManager.h"
#include "src/settings/modules/RegionSettings.h" #include "src/settings/modules/RegionSettings.h"
#include "src/solver/OptimizationDirection.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/sparse/StateType.h"
#include "src/storage/FlexibleSparseMatrix.h" #include "src/storage/FlexibleSparseMatrix.h"
#include "src/utility/constants.h" #include "src/utility/constants.h"
@ -102,9 +104,13 @@ namespace storm {
//The states that we consider to eliminate //The states that we consider to eliminate
storm::storage::BitVector considerToEliminate(submatrix.getRowGroupCount(), true); storm::storage::BitVector considerToEliminate(submatrix.getRowGroupCount(), true);
considerToEliminate.set(initialState, false); considerToEliminate.set(initialState, false);
std::vector<uint64_t> statesToEliminate;
for (auto const& state : considerToEliminate) { 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 //state is deterministic. Check if outgoing transitions are constant
for(auto const& entry : submatrix.getRowGroup(state)){ for(auto const& entry : submatrix.getRowGroup(state)){
if(!storm::utility::isConstant(entry.getValue())){ if(!storm::utility::isConstant(entry.getValue())){
@ -115,21 +121,20 @@ namespace storm {
if(!storm::utility::isConstant(oneStepProbabilities[submatrix.getRowGroupIndices()[state]])){ if(!storm::utility::isConstant(oneStepProbabilities[submatrix.getRowGroupIndices()[state]])){
eliminateThisState=false; eliminateThisState=false;
} }
} else {
eliminateThisState = false;
} }
if(eliminateThisState){
storm::storage::FlexibleSparseMatrix<ParametricType>::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<ParametricType>(flexibleTransitions, flexibleBackwardTransitions, statesToEliminate, oneStepProbabilities);
STORM_LOG_DEBUG("Eliminated " << subsystem.size() - subsystem.getNumberOfSetBits() << " of " << subsystem.size() << " states that had constant outgoing transitions."); STORM_LOG_DEBUG("Eliminated " << subsystem.size() - subsystem.getNumberOfSetBits() << " of " << subsystem.size() << " states that had constant outgoing transitions.");
//Build the simple model //Build the simple model
STORM_LOG_DEBUG("Building the resulting simplified model."); STORM_LOG_DEBUG("Building the resulting simplified model.");
//The matrix. The flexibleTransitions matrix might have empty rows where states have been eliminated. //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. //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<storm::storage::sparse::state_type> newStateIndexMap(flexibleTransitions.getNumberOfRows(), flexibleTransitions.getNumberOfRows()); //initialize with some illegal index
std::vector<storm::storage::sparse::state_type> newStateIndexMap(flexibleTransitions.getRowCount(), flexibleTransitions.getRowCount()); //initialize with some illegal index
storm::storage::sparse::state_type newStateIndex=0; storm::storage::sparse::state_type newStateIndex=0;
for(auto const& state : subsystem){ for(auto const& state : subsystem){
newStateIndexMap[state]=newStateIndex; newStateIndexMap[state]=newStateIndex;
@ -148,7 +153,7 @@ namespace storm {
ParametricType missingProbability=storm::utility::region::getNewFunction<ParametricType, CoefficientType>(storm::utility::one<CoefficientType>()); ParametricType missingProbability=storm::utility::region::getNewFunction<ParametricType, CoefficientType>(storm::utility::one<CoefficientType>());
//go through columns: //go through columns:
for(auto& entry: flexibleTransitions.getRow(oldRow)){ 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(); missingProbability-=entry.getValue();
matrixBuilder.addNextValue(curRow,newStateIndexMap[entry.getColumn()], storm::utility::simplify(entry.getValue())); matrixBuilder.addNextValue(curRow,newStateIndexMap[entry.getColumn()], storm::utility::simplify(entry.getValue()));
} }

17
src/modelchecker/region/SparseRegionModelChecker.cpp
View File

@ -24,7 +24,6 @@
#include "src/exceptions/InvalidSettingsException.h" #include "src/exceptions/InvalidSettingsException.h"
#include "src/exceptions/NotImplementedException.h" #include "src/exceptions/NotImplementedException.h"
#include "src/exceptions/UnexpectedException.h" #include "src/exceptions/UnexpectedException.h"
#include "utility/ConversionHelper.h"
#include "modelchecker/results/CheckResult.h" #include "modelchecker/results/CheckResult.h"
#include "modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "modelchecker/results/ExplicitQuantitativeCheckResult.h"
@ -134,11 +133,11 @@ namespace storm {
//Check if the approximation and the sampling model needs to be computed //Check if the approximation and the sampling model needs to be computed
if(!this->isResultConstant()){ if(!this->isResultConstant()){
if(this->isApproximationApplicable && storm::settings::regionSettings().doApprox()){
if(this->isApproximationApplicable && storm::settings::getModule<storm::settings::modules::RegionSettings>().doApprox()){
initializeApproximationModel(*this->getSimpleModel(), this->getSimpleFormula()); 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<storm::settings::modules::RegionSettings>().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE ||
(!storm::settings::getModule<storm::settings::modules::RegionSettings>().doSample() && storm::settings::getModule<storm::settings::modules::RegionSettings>().getApproxMode()==storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST)){
initializeSamplingModel(*this->getSimpleModel(), this->getSimpleFormula()); initializeSamplingModel(*this->getSimpleModel(), this->getSimpleFormula());
} }
} else if (this->isResultConstant() && this->constantResult.get() == storm::utility::region::convertNumber<ConstantType>(-1.0)){ } else if (this->isResultConstant() && this->constantResult.get() == storm::utility::region::convertNumber<ConstantType>(-1.0)){
@ -241,10 +240,10 @@ namespace storm {
//switches for the different steps. //switches for the different steps.
bool done=false; 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<storm::settings::modules::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::getModule<storm::settings::modules::RegionSettings>().doApprox() && this->isApproximationApplicable;
bool doSampling=storm::settings::getModule<storm::settings::modules::RegionSettings>().doSample();
bool doSmt=storm::settings::getModule<storm::settings::modules::RegionSettings>().doSmt();
if(this->isResultConstant()){ if(this->isResultConstant()){
STORM_LOG_DEBUG("Checking a region although the result is constant, i.e., independent of the region. This makes sense none."); 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; bool proveAllSat;
switch (region.getCheckResult()){ switch (region.getCheckResult()){
case RegionCheckResult::UNKNOWN: case RegionCheckResult::UNKNOWN:
switch(storm::settings::regionSettings().getApproxMode()){
switch(storm::settings::getModule<storm::settings::modules::RegionSettings>().getApproxMode()){
case storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST: case storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST:
//Sample a single point to know whether we should try to prove ALLSAT or ALLVIOLATED //Sample a single point to know whether we should try to prove ALLSAT or ALLVIOLATED
checkPoint(region,region.getSomePoint(), false); checkPoint(region,region.getSomePoint(), false);

4
src/solver/Smt2SmtSolver.cpp
View File

@ -115,7 +115,7 @@ namespace storm {
writeCommand("( assert " + expressionAdapter->translateExpression(constraint) + " )", true); writeCommand("( assert " + expressionAdapter->translateExpression(constraint) + " )", true);
} }
void Smt2SmtSolver::add(storm::Variable const& guard, typename storm::ArithConstraint<storm::Polynomial> const& constraint){
void Smt2SmtSolver::add(storm::RationalFunctionVariable const& guard, typename storm::ArithConstraint<storm::Polynomial> 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."); 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!). //if some of the occurring variables are not declared yet, we will have to (including the guard!).
std::set<storm::Variable> variables = constraint.lhs().gatherVariables(); std::set<storm::Variable> variables = constraint.lhs().gatherVariables();
@ -128,7 +128,7 @@ namespace storm {
writeCommand("( assert (=> " + guardName + " " + expressionAdapter->translateExpression(constraint) + " ) )", true); 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."); 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<storm::Variable> variableSet; std::set<storm::Variable> variableSet;
variableSet.insert(variable); variableSet.insert(variable);

4
src/solver/Smt2SmtSolver.h
View File

@ -60,10 +60,10 @@ namespace storm {
void add(typename storm::ArithConstraint<storm::RawPolynomial> const& constraint); void add(typename storm::ArithConstraint<storm::RawPolynomial> const& constraint);
// adds the given carl constraint that is guarded by the given guard. The guard should have type 'bool' // 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<storm::Polynomial> const& constraint);
void add(storm::RationalFunctionVariable const& guard, typename storm::ArithConstraint<storm::Polynomial> const& constraint);
// asserts that the given variable has the given value. The variable should have type 'bool' // 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 #endif
virtual CheckResult check() override; virtual CheckResult check() override;

9
src/solver/stateelimination/PrioritizedStateEliminator.cpp
View File

@ -5,10 +5,17 @@
#include "src/utility/macros.h" #include "src/utility/macros.h"
#include "src/utility/constants.h" #include "src/utility/constants.h"
#include "StaticStatePriorityQueue.h"
namespace storm { namespace storm {
namespace solver { namespace solver {
namespace stateelimination { namespace stateelimination {
template<typename ValueType>
PrioritizedStateEliminator<ValueType>::PrioritizedStateEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, std::vector<storm::storage::sparse::state_type> const& statesToEliminate, std::vector<ValueType>& stateValues)
: PrioritizedStateEliminator(transitionMatrix, backwardTransitions, std::make_shared<StaticStatePriorityQueue>(statesToEliminate), stateValues)
{}
template<typename ValueType> template<typename ValueType>
PrioritizedStateEliminator<ValueType>::PrioritizedStateEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector<ValueType>& stateValues) : StateEliminator<ValueType>(transitionMatrix, backwardTransitions), priorityQueue(priorityQueue), stateValues(stateValues) { PrioritizedStateEliminator<ValueType>::PrioritizedStateEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector<ValueType>& stateValues) : StateEliminator<ValueType>(transitionMatrix, backwardTransitions), priorityQueue(priorityQueue), stateValues(stateValues) {
} }

3
src/solver/stateelimination/PrioritizedStateEliminator.h
View File

@ -15,7 +15,8 @@ namespace storm {
typedef typename std::shared_ptr<StatePriorityQueue> PriorityQueuePointer; typedef typename std::shared_ptr<StatePriorityQueue> PriorityQueuePointer;
PrioritizedStateEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector<ValueType>& stateValues); PrioritizedStateEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector<ValueType>& stateValues);
PrioritizedStateEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, std::vector<storm::storage::sparse::state_type> const& statesToEliminate, std::vector<ValueType>& stateValues);
// Instantiaton of virtual methods. // Instantiaton of virtual methods.
void updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) override; 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; void updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) override;

2
src/utility/region.h
View File

@ -27,7 +27,7 @@ namespace storm {
//Obtain the correct type for Variables and Coefficients out of a given Function type //Obtain the correct type for Variables and Coefficients out of a given Function type
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
template<typename FunctionType> template<typename FunctionType>
using VariableType = typename std::conditional<(std::is_same<FunctionType, storm::RationalFunction>::value), storm::Variable, std::nullptr_t>::type;
using VariableType = typename std::conditional<(std::is_same<FunctionType, storm::RationalFunction>::value), storm::RationalFunctionVariable, std::nullptr_t>::type;
template<typename FunctionType> template<typename FunctionType>
using CoefficientType = typename std::conditional<(std::is_same<FunctionType, storm::RationalFunction>::value), storm::RationalFunction::CoeffType, std::nullptr_t>::type; using CoefficientType = typename std::conditional<(std::is_same<FunctionType, storm::RationalFunction>::value), storm::RationalFunction::CoeffType, std::nullptr_t>::type;
#else #else

Write Preview
Loading…
Cancel
Save