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

minor fixes

tempestpy_adaptions
TimQu 8 years ago
parent
38fa454ace
commit
1e1b037cb2
7 changed files with 20 additions and 35 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. 3
      src/storm/modelchecker/parametric/ParameterLifting.cpp
  2. 2
      src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp
  3. 2
      src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp
  4. 4
      src/storm/transformer/SparseParametricMdpSimplifier.cpp
  5. 25
      src/storm/transformer/SparseParametricModelSimplifier.cpp
  6. 15
      src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp
  7. 4
      src/test/modelchecker/SparseMdpParameterLiftingTest.cpp

3
src/storm/modelchecker/parametric/ParameterLifting.cpp
View File

@ -31,13 +31,14 @@ namespace storm {
template <typename SparseModelType, typename ConstantType>
void ParameterLifting<SparseModelType, ConstantType>::specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::NotSupportedException, "Parameter lifting requires a property where only the value in the initial states is relevant.");
STORM_LOG_THROW(checkTask.isBoundSet(), storm::exceptions::NotSupportedException, "Parameter lifting requires a bounded property.");
STORM_LOG_THROW(parameterLiftingChecker->canHandle(checkTask), storm::exceptions::NotSupportedException, "Parameter lifting is not supported for this property.");
simplifyParametricModel(checkTask);
initializeUnderlyingCheckers();
currentCheckTask = std::make_unique<storm::modelchecker::CheckTask<storm::logic::Formula, typename SparseModelType::ValueType>>(checkTask.substituteFormula(*currentFormula));
STORM_LOG_THROW(parameterLiftingChecker->canHandle(*currentCheckTask), storm::exceptions::NotSupportedException, "Parameter lifting is not supported for this property.");
instantiationChecker->specifyFormula(*currentCheckTask);
parameterLiftingChecker->specifyFormula(*currentCheckTask);
}

2
src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp
View File

@ -27,7 +27,7 @@ namespace storm {
template <typename SparseModelType, typename ConstantType>
bool SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const {
return checkTask.getFormula().isInFragment(storm::logic::reachability().setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true));
return checkTask.getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true));
}
template <typename SparseModelType, typename ConstantType>

2
src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp
View File

@ -55,7 +55,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Checking with hint is only implemented for probability or reward operator formulas");
}
std::unique_ptr<storm::modelchecker::CheckResult> qualitativeResult = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
storm::storage::Scheduler& scheduler = qualitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getScheduler();
storm::storage::Scheduler& scheduler = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getScheduler();
this->currentCheckTask->setHint(ExplicitModelCheckerHint<ConstantType>(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()),
std::move(dynamic_cast<storm::storage::TotalScheduler const&>(scheduler))));
return qualitativeResult;

4
src/storm/transformer/SparseParametricMdpSimplifier.cpp
View File

@ -150,7 +150,9 @@ namespace storm {
this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel, rewardModelNameAsVector.front());
// Eliminate the end components in which no reward is collected (only required if rewards are minimized)
this->simplifiedModel = this->eliminateNeutralEndComponents(*this->simplifiedModel, this->simplifiedModel->getStates("target") | this->simplifiedModel->getStates("sink"), rewardModelNameAsVector.front());
if (minimizing) {
this->simplifiedModel = this->eliminateNeutralEndComponents(*this->simplifiedModel, this->simplifiedModel->getStates("target") | this->simplifiedModel->getStates("sink"), rewardModelNameAsVector.front());
}
return true;
}

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

@ -111,6 +111,8 @@ namespace storm {
std::vector<typename SparseModelType::ValueType> actionRewards;
if(rewardModelName) {
actionRewards = model.getRewardModel(*rewardModelName).getTotalRewardVector(sparseMatrix);
} else {
actionRewards = std::vector<typename SparseModelType::ValueType>(model.getTransitionMatrix().getRowCount(), storm::utility::zero<typename SparseModelType::ValueType>());
}
// Find the states that are to be eliminated
@ -134,27 +136,10 @@ namespace storm {
}
}
// only keep the relevant reward values and translate them to state-based rewards
std::vector<typename SparseModelType::ValueType> rewardsOfEliminatedStates;
if(rewardModelName) {
rewardsOfEliminatedStates.reserve(model.getNumberOfStates());
for(uint_fast64_t state = 0; state < model.getNumberOfStates(); ++state) {
if(keptStates.get(state)) {
// The current state will not be eliminated. Hence we do not need to consider its reward during elimination
rewardsOfEliminatedStates.push_back(storm::utility::zero<typename SparseModelType::ValueType>());
} else {
// We need to keep track of the reward of this state during elimination
rewardsOfEliminatedStates.push_back(std::move(actionRewards[sparseMatrix.getRowGroupIndices()[state]]));
}
}
} else {
rewardsOfEliminatedStates.resize(model.getNumberOfStates(), storm::utility::zero<typename SparseModelType::ValueType>());
}
// invoke elimination and obtain resulting transition matrix
storm::storage::FlexibleSparseMatrix<typename SparseModelType::ValueType> flexibleMatrix(sparseMatrix);
storm::storage::FlexibleSparseMatrix<typename SparseModelType::ValueType> flexibleBackwardTransitions(sparseMatrix.transpose(true), true);
storm::solver::stateelimination::PrioritizedStateEliminator<typename SparseModelType::ValueType> stateEliminator(flexibleMatrix, flexibleBackwardTransitions, statesToEliminate, rewardsOfEliminatedStates);
storm::storage::FlexibleSparseMatrix<typename SparseModelType::ValueType> flexibleBackwardTransitions(sparseMatrix.transpose(), true);
storm::solver::stateelimination::PrioritizedStateEliminator<typename SparseModelType::ValueType> stateEliminator(flexibleMatrix, flexibleBackwardTransitions, statesToEliminate, actionRewards);
stateEliminator.eliminateAll();
storm::storage::SparseMatrix<typename SparseModelType::ValueType> newTransitionMatrix = flexibleMatrix.createSparseMatrix(keptRows, keptStates);
@ -162,8 +147,6 @@ namespace storm {
std::unordered_map<std::string, typename SparseModelType::RewardModelType> rewardModels;
if(rewardModelName) {
actionRewards = storm::utility::vector::filterVector(actionRewards, keptRows);
rewardsOfEliminatedStates = storm::utility::vector::filterVector(rewardsOfEliminatedStates, keptStates);
storm::utility::vector::addVectorToGroupedVector(actionRewards, rewardsOfEliminatedStates, newTransitionMatrix.getRowGroupIndices());
rewardModels.insert(std::make_pair(*rewardModelName, typename SparseModelType::RewardModelType(boost::none, std::move(actionRewards))));
}

15
src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp
View File

@ -26,8 +26,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Prob) {
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(*formulas[0]);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters);
@ -57,7 +56,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew) {
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(*formulas[0]);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
@ -89,7 +88,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Infty) {
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(*formulas[0]);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("", modelParameters);
@ -115,7 +114,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_4Par) {
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(*formulas[0]);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters);
@ -146,7 +145,7 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob) {
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(*formulas[0]);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2", modelParameters);
@ -180,7 +179,7 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_1Par) {
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(*formulas[0]);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.9<=PF<=0.99", modelParameters);
@ -211,7 +210,7 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_Const) {
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(*formulas[0]);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("", modelParameters);

4
src/test/modelchecker/SparseMdpParameterLiftingTest.cpp
View File

@ -25,7 +25,7 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob) {
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(*formulas[0]);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
auto allSatRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters);
auto exBothRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters);
@ -55,7 +55,7 @@ TEST(SparseMdpParameterLiftingTest, coin_Prob) {
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(*formulas[0]);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.3<=p1<=0.45,0.2<=p2<=0.54", modelParameters);

Write Preview
Loading…
Cancel
Save