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

fixed selection of states to eliminate, added support for model simplification for step bounded properties

tempestpy_adaptions
TimQu 8 years ago
parent
732bbc85d2
commit
a4e4aba487
3 changed files with 37 additions and 10 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/storm/modelchecker/region/ApproximationModel.cpp
  2. 43
      src/storm/transformer/SparseParametricDtmcSimplifier.cpp
  3. 2
      src/storm/transformer/SparseParametricModelSimplifier.cpp

2
src/storm/modelchecker/region/ApproximationModel.cpp
View File

@ -212,7 +212,7 @@ namespace storm {
auto vectorIt = this->vectorData.vector.begin();
for(auto oldState : this->maybeStates){
if(storm::utility::isConstant(parametricModel.getUniqueRewardModel().getStateActionRewardVector()[oldState])){
ConstantType reward = storm::utility::region::convertNumber<ConstantType>(storm::utility::region::getConstantPart(parametricModel.getUniqueRewardModel().getStateRewardVector()[oldState]));
ConstantType reward = storm::utility::region::convertNumber<ConstantType>(storm::utility::region::getConstantPart(parametricModel.getUniqueRewardModel().getStateActionRewardVector()[oldState]));
//Add one of these entries for every row in the row group of oldState
for(auto matrixRow=this->matrixData.matrix.getRowGroupIndices()[oldState]; matrixRow<this->matrixData.matrix.getRowGroupIndices()[oldState+1]; ++matrixRow){
*vectorIt = reward;

43
src/storm/transformer/SparseParametricDtmcSimplifier.cpp
View File

@ -56,7 +56,13 @@ namespace storm {
bool SparseParametricDtmcSimplifier<SparseModelType>::simplifyForBoundedUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) {
STORM_LOG_THROW(!formula.getSubformula().asBoundedUntilFormula().hasLowerBound(), storm::exceptions::NotSupportedException, "Lower step bounds are not supported.");
STORM_LOG_THROW(formula.getSubformula().asBoundedUntilFormula().hasUpperBound(), storm::exceptions::UnexpectedException, "Expected a bounded until formula with an upper bound.");
STORM_LOG_THROW(formula.getSubformula().asBoundedUntilFormula().hasIntegerUpperBound(), storm::exceptions::UnexpectedException, "Expected a bounded until formula with an integral upper bound.");
STORM_LOG_THROW(formula.getSubformula().asBoundedUntilFormula().isStepBounded(), storm::exceptions::UnexpectedException, "Expected a bounded until formula with step bounds.");
uint_fast64_t upperStepBound = formula.getSubformula().asBoundedUntilFormula().getUpperBound().evaluateAsInt();
if (formula.getSubformula().asBoundedUntilFormula().isUpperBoundStrict()) {
STORM_LOG_THROW(upperStepBound > 0, storm::exceptions::UnexpectedException, "Expected a strict upper bound that is greater than zero.");
--upperStepBound;
}
// Get the prob0, target, and the maybeStates
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->originalModel);
@ -66,12 +72,11 @@ namespace storm {
}
storm::storage::BitVector phiStates = std::move(propositionalChecker.check(formula.getSubformula().asBoundedUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
storm::storage::BitVector psiStates = std::move(propositionalChecker.check(formula.getSubformula().asBoundedUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
storm::storage::BitVector probGreater0States = storm::utility::graph::performProbGreater0(this->originalModel.getBackwardTransitions(), phiStates, psiStates, true, formula.getSubformula().asBoundedUntilFormula().getUpperBound().evaluateAsInt());
storm::storage::BitVector probGreater0States = storm::utility::graph::performProbGreater0(this->originalModel.getBackwardTransitions(), phiStates, psiStates, true, upperStepBound);
storm::storage::BitVector prob0States = ~probGreater0States;
// Only consider the maybestates that are reachable from one initial probGreater0 state within the given amount of steps and without hopping over a target state
storm::storage::BitVector reachableGreater0States = storm::utility::graph::getReachableStates(this->originalModel.getTransitionMatrix(), this->originalModel.getInitialStates() & probGreater0States, probGreater0States, psiStates, true, formula.getSubformula().asBoundedUntilFormula().getUpperBound().evaluateAsInt());
storm::storage::BitVector reachableGreater0States = storm::utility::graph::getReachableStates(this->originalModel.getTransitionMatrix(), this->originalModel.getInitialStates() & probGreater0States, probGreater0States, psiStates, true, upperStepBound);
storm::storage::BitVector maybeStates = reachableGreater0States & ~psiStates;
// obtain the resulting subsystem
@ -82,8 +87,8 @@ namespace storm {
// obtain the simplified formula for the simplified model
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula const> ("target");
auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula const>(storm::logic::Formula::getTrueFormula(), labelFormula, boost::none, storm::logic::);
this->simplifiedFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula const>(eventuallyFormula, formula.getOperatorInformation());
auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula const>(storm::logic::Formula::getTrueFormula(), labelFormula, boost::none, storm::logic::TimeBound(formula.getSubformula().asBoundedUntilFormula().isUpperBoundStrict(), formula.getSubformula().asBoundedUntilFormula().getUpperBound()), storm::logic::TimeBoundType::Steps);
this->simplifiedFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula const>(boundedUntilFormula, formula.getOperatorInformation());
return true;
}
@ -128,8 +133,30 @@ namespace storm {
template<typename SparseModelType>
bool SparseParametricDtmcSimplifier<SparseModelType>::simplifyForCumulativeRewards(storm::logic::RewardOperatorFormula const& formula) {
// If this method was not overriden by any subclass, simplification is not possible
return false;
STORM_LOG_THROW(formula.getSubformula().asCumulativeRewardFormula().isStepBounded(), storm::exceptions::UnexpectedException, "Expected a cumulative reward formula with step bounds.");
typename SparseModelType::RewardModelType const& originalRewardModel = formula.hasRewardModelName() ? this->originalModel.getRewardModel(formula.getRewardModelName()) : this->originalModel.getUniqueRewardModel();
uint_fast64_t stepBound = formula.getSubformula().asCumulativeRewardFormula().getBound().evaluateAsInt();
if (formula.getSubformula().asCumulativeRewardFormula().isBoundStrict()) {
STORM_LOG_THROW(stepBound > 0, storm::exceptions::UnexpectedException, "Expected a strict upper bound that is greater than zero.");
--stepBound;
}
// Get the states with non-zero reward
storm::storage::BitVector maybeStates = storm::utility::graph::performProbGreater0(this->originalModel.getBackwardTransitions(), storm::storage::BitVector(this->originalModel.getNumberOfStates(), true), ~originalRewardModel.getStatesWithZeroReward(this->originalModel.getTransitionMatrix()), true, stepBound);
storm::storage::BitVector zeroRewardStates = ~maybeStates;
storm::storage::BitVector noStates(this->originalModel.getNumberOfStates(), false);
// obtain the resulting subsystem
std::vector<std::string> rewardModelNameAsVector(1, formula.hasRewardModelName() ? formula.getRewardModelName() : this->originalModel.getRewardModels().begin()->first);
storm::transformer::GoalStateMerger<SparseModelType> goalStateMerger(this->originalModel);
this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, noStates, zeroRewardStates, rewardModelNameAsVector);
// obtain the simplified formula for the simplified model
this->simplifiedFormula = formula.asSharedPointer();
return true;
}
template class SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>;

2
src/storm/transformer/SparseParametricModelSimplifier.cpp
View File

@ -126,7 +126,7 @@ namespace storm {
if (sparseMatrix.getRowGroupSize(state) == 1 && storm::utility::isConstant(stateValues[state])) {
bool hasOnlyConstEntries = true;
for (auto const& entry : sparseMatrix.getRowGroup(state)) {
if(!storm::utility::isConstant(entry.getColumn())) {
if(!storm::utility::isConstant(entry.getValue())) {
hasOnlyConstEntries = false;
break;
}

Write Preview
Loading…
Cancel
Save