TimQu
8 years ago
19 changed files with 284 additions and 855 deletions
-
10src/storm/modelchecker/multiobjective/pcaa.cpp
-
72src/storm/modelchecker/multiobjective/pcaa/PcaaObjective.h
-
39src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp
-
7src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h
-
26src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp
-
17src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h
-
21src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp
-
2src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h
-
4src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp
-
2src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h
-
447src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp
-
82src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.h
-
93src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessorReturnType.h
-
82src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp
-
2src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h
-
65src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp
-
14src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h
-
126src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp
-
28src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h
@ -1,72 +0,0 @@ |
|||
#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_PCAAOBJECTIVE_H_ |
|||
#define STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_PCAAOBJECTIVE_H_ |
|||
|
|||
#include <iomanip> |
|||
#include <boost/optional.hpp> |
|||
|
|||
#include "storm/logic/Formulas.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace multiobjective { |
|||
template <typename ValueType> |
|||
struct PcaaObjective { |
|||
// the original input formula |
|||
std::shared_ptr<storm::logic::Formula const> originalFormula; |
|||
|
|||
// the name of the considered reward model in the preprocessedModel |
|||
std::string rewardModelName; |
|||
|
|||
// true if all rewards for this objective are positive, false if all rewards are negative. |
|||
bool rewardsArePositive; |
|||
|
|||
// transformation from the values of the preprocessed model to the ones for the actual input model, i.e., |
|||
// x is achievable in the preprocessed model iff factor*x + offset is achievable in the original model |
|||
ValueType toOriginalValueTransformationFactor; |
|||
ValueType toOriginalValueTransformationOffset; |
|||
|
|||
// The probability/reward threshold for the preprocessed model (if originalFormula specifies one). |
|||
// This is always a lower bound. |
|||
boost::optional<ValueType> threshold; |
|||
// True iff the specified threshold is strict, i.e., > |
|||
bool thresholdIsStrict = false; |
|||
|
|||
// The time bound(s) for the formula (if given by the originalFormula) |
|||
boost::optional<storm::expressions::Expression> lowerTimeBound; |
|||
boost::optional<storm::expressions::Expression> upperTimeBound; |
|||
bool lowerTimeBoundStrict = false; |
|||
bool upperTimeBoundStrict = false; |
|||
|
|||
void printToStream(std::ostream& out) const { |
|||
out << std::setw(30) << originalFormula->toString(); |
|||
out << " \t(toOrigVal:" << std::setw(3) << toOriginalValueTransformationFactor << "*x +" << std::setw(3) << toOriginalValueTransformationOffset << ", \t"; |
|||
out << "intern threshold:"; |
|||
if(threshold){ |
|||
out << (thresholdIsStrict ? " >" : ">="); |
|||
out << std::setw(5) << (*threshold) << ","; |
|||
} else { |
|||
out << " none,"; |
|||
} |
|||
out << " \t"; |
|||
out << "intern reward model: " << std::setw(10) << rewardModelName; |
|||
out << (rewardsArePositive ? " (positive)" : " (negative)") << ", \t"; |
|||
out << "time bounds:"; |
|||
if(lowerTimeBound) { |
|||
if(upperTimeBound) { |
|||
out << (lowerTimeBoundStrict ? "(" : "[") << *lowerTimeBound << ", " << *upperTimeBound << (upperTimeBoundStrict ? ")" : "]"); |
|||
} else { |
|||
out << (lowerTimeBoundStrict ? " >" : ">=") << std::setw(5) << *lowerTimeBound; |
|||
} |
|||
} else if (upperTimeBound) { |
|||
out << (upperTimeBoundStrict ? " <" : "<=") << std::setw(5) << *upperTimeBound; |
|||
} else { |
|||
out << " none"; |
|||
} |
|||
out << ")" << std::endl; |
|||
} |
|||
}; |
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_OBJECTIVE_H_ */ |
|||
@ -1,447 +0,0 @@ |
|||
#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.h"
|
|||
|
|||
#include "storm/models/sparse/Mdp.h"
|
|||
#include "storm/models/sparse/MarkovAutomaton.h"
|
|||
#include "storm/models/sparse/StandardRewardModel.h"
|
|||
#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
|
|||
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
|
|||
#include "storm/storage/MaximalEndComponentDecomposition.h"
|
|||
#include "storm/storage/memorystructure/MemoryStructureBuilder.h"
|
|||
#include "storm/storage/memorystructure/SparseModelMemoryProduct.h"
|
|||
#include "storm/transformer/SubsystemBuilder.h"
|
|||
#include "storm/utility/macros.h"
|
|||
#include "storm/utility/vector.h"
|
|||
#include "storm/utility/graph.h"
|
|||
|
|||
#include "storm/exceptions/InvalidPropertyException.h"
|
|||
#include "storm/exceptions/UnexpectedException.h"
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace multiobjective { |
|||
|
|||
template<typename SparseModelType> |
|||
typename SparsePcaaPreprocessor<SparseModelType>::ReturnType SparsePcaaPreprocessor<SparseModelType>::preprocess(SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula) { |
|||
|
|||
ReturnType result(originalFormula, originalModel, SparseModelType(originalModel)); |
|||
result.newToOldStateIndexMapping = storm::utility::vector::buildVectorForRange(0, originalModel.getNumberOfStates()); |
|||
|
|||
//Invoke preprocessing on the individual objectives
|
|||
for (auto const& subFormula : originalFormula.getSubformulas()){ |
|||
STORM_LOG_INFO("Preprocessing objective " << *subFormula<< "."); |
|||
result.objectives.emplace_back(); |
|||
PcaaObjective<ValueType>& currentObjective = result.objectives.back(); |
|||
currentObjective.originalFormula = subFormula; |
|||
if (currentObjective.originalFormula->isOperatorFormula()) { |
|||
preprocessOperatorFormula(currentObjective.originalFormula->asOperatorFormula(), result, currentObjective); |
|||
} else { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the subformula " << *subFormula << " of " << originalFormula << " because it is not supported"); |
|||
} |
|||
} |
|||
// Set the query type. In case of a quantitative query, also set the index of the objective to be optimized.
|
|||
// Note: If there are only zero (or one) objectives left, we should not consider a pareto query!
|
|||
storm::storage::BitVector objectivesWithoutThreshold(result.objectives.size()); |
|||
for (uint_fast64_t objIndex = 0; objIndex < result.objectives.size(); ++objIndex) { |
|||
objectivesWithoutThreshold.set(objIndex, !result.objectives[objIndex].threshold); |
|||
} |
|||
uint_fast64_t numOfObjectivesWithoutThreshold = objectivesWithoutThreshold.getNumberOfSetBits(); |
|||
if (numOfObjectivesWithoutThreshold == 0) { |
|||
result.queryType = ReturnType::QueryType::Achievability; |
|||
} else if (numOfObjectivesWithoutThreshold == 1) { |
|||
result.queryType = ReturnType::QueryType::Quantitative; |
|||
result.indexOfOptimizingObjective = objectivesWithoutThreshold.getNextSetIndex(0); |
|||
} else if (numOfObjectivesWithoutThreshold == result.objectives.size()) { |
|||
result.queryType = ReturnType::QueryType::Pareto; |
|||
} else { |
|||
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The number of objectives without threshold is not valid. It should be either 0 (achievability query), 1 (quantitative query), or " << result.objectives.size() << " (Pareto Query). Got " << numOfObjectivesWithoutThreshold << " instead."); |
|||
} |
|||
|
|||
//We can remove the original reward models to save some memory
|
|||
std::set<std::string> origRewardModels = originalFormula.getReferencedRewardModels(); |
|||
for (auto const& rewModel : origRewardModels){ |
|||
result.preprocessedModel.removeRewardModel(rewModel); |
|||
} |
|||
|
|||
//Get actions to which a positive or negative reward is assigned for at least one objective
|
|||
result.actionsWithPositiveReward = storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), false); |
|||
result.actionsWithNegativeReward = storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), false); |
|||
for (uint_fast64_t objIndex = 0; objIndex < result.objectives.size(); ++objIndex) { |
|||
if (!result.objectives[objIndex].upperTimeBound) { |
|||
if (result.objectives[objIndex].rewardsArePositive) { |
|||
result.actionsWithPositiveReward |= ~storm::utility::vector::filterZero(result.preprocessedModel.getRewardModel(result.objectives[objIndex].rewardModelName).getTotalRewardVector(result.preprocessedModel.getTransitionMatrix())); |
|||
} else { |
|||
result.actionsWithNegativeReward |= ~storm::utility::vector::filterZero(result.preprocessedModel.getRewardModel(result.objectives[objIndex].rewardModelName).getTotalRewardVector(result.preprocessedModel.getTransitionMatrix())); |
|||
} |
|||
} |
|||
} |
|||
|
|||
// Analyze End components and ensure reward finiteness.
|
|||
// Note that this is only necessary if there is at least one objective with no upper time bound
|
|||
for (auto const& obj : result.objectives) { |
|||
if (!obj.upperTimeBound) { |
|||
auto backwardTransitions = result.preprocessedModel.getBackwardTransitions(); |
|||
analyzeEndComponents(result, backwardTransitions); |
|||
ensureRewardFiniteness(result, backwardTransitions); |
|||
break; |
|||
} |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
void SparsePcaaPreprocessor<SparseModelType>::updatePreprocessedModel(ReturnType& result, SparseModelType& newPreprocessedModel, std::vector<uint_fast64_t>& newToOldStateIndexMapping) { |
|||
result.preprocessedModel = std::move(newPreprocessedModel); |
|||
// the given newToOldStateIndexMapping refers to the indices of the former preprocessedModel as 'old indices'
|
|||
for (auto & preprocessedModelStateIndex : newToOldStateIndexMapping){ |
|||
preprocessedModelStateIndex = result.newToOldStateIndexMapping[preprocessedModelStateIndex]; |
|||
} |
|||
result.newToOldStateIndexMapping = std::move(newToOldStateIndexMapping); |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
void SparsePcaaPreprocessor<SparseModelType>::addMemoryToPreprocessedModel(ReturnType& result, storm::storage::MemoryStructure& memory) { |
|||
storm::storage::SparseModelMemoryProduct<ValueType> product = memory.product(result.preprocessedModel); |
|||
auto newModel = product.build(); |
|||
|
|||
// update the newToOldStateIndexMapping
|
|||
std::vector<uint_fast64_t> updatedMapping; |
|||
updatedMapping.reserve(newModel->getNumberOfStates()); |
|||
for (uint_fast64_t oldState = 0; oldState < result.preprocessedModel.getNumberOfStates(); ++oldState) { |
|||
for (uint_fast64_t memoryState = 0; memoryState < memory.getNumberOfStates(); ++memoryState) { |
|||
uint_fast64_t const& newState = product.getResultState(oldState, memoryState); |
|||
// Check if the state actually exists in the new model
|
|||
if (newState < newModel->getNumberOfStates()) { |
|||
assert(newState == updatedMapping.size()); |
|||
updatedMapping.push_back(result.newToOldStateIndexMapping[oldState]); |
|||
} |
|||
} |
|||
} |
|||
|
|||
result.preprocessedModel = std::move(dynamic_cast<SparseModelType&>(*newModel)); |
|||
result.newToOldStateIndexMapping = std::move(updatedMapping); |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
void SparsePcaaPreprocessor<SparseModelType>::preprocessOperatorFormula(storm::logic::OperatorFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective) { |
|||
|
|||
// Get a unique name for the new reward model.
|
|||
currentObjective.rewardModelName = "objective" + std::to_string(result.objectives.size()); |
|||
while(result.preprocessedModel.hasRewardModel(currentObjective.rewardModelName)){ |
|||
currentObjective.rewardModelName = "_" + currentObjective.rewardModelName; |
|||
} |
|||
|
|||
currentObjective.toOriginalValueTransformationFactor = storm::utility::one<ValueType>(); |
|||
currentObjective.toOriginalValueTransformationOffset = storm::utility::zero<ValueType>(); |
|||
currentObjective.rewardsArePositive = true; |
|||
|
|||
bool formulaMinimizes = false; |
|||
if (formula.hasBound()) { |
|||
currentObjective.threshold = formula.template getThresholdAs<ValueType>(); |
|||
currentObjective.thresholdIsStrict = storm::logic::isStrict(formula.getBound().comparisonType); |
|||
//Note that we minimize for upper bounds since we are looking for the EXISTENCE of a satisfying scheduler
|
|||
formulaMinimizes = !storm::logic::isLowerBound(formula.getBound().comparisonType); |
|||
} else if (formula.hasOptimalityType()){ |
|||
formulaMinimizes = storm::solver::minimize(formula.getOptimalityType()); |
|||
} else { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Current objective " << formula << " does not specify whether to minimize or maximize"); |
|||
} |
|||
if (formulaMinimizes) { |
|||
// We negate all the values so we can consider the maximum for this objective
|
|||
// Thus, all objectives will be maximized.
|
|||
currentObjective.rewardsArePositive = false; |
|||
currentObjective.toOriginalValueTransformationFactor = -storm::utility::one<ValueType>(); |
|||
} |
|||
|
|||
if (formula.isProbabilityOperatorFormula()){ |
|||
preprocessProbabilityOperatorFormula(formula.asProbabilityOperatorFormula(), result, currentObjective); |
|||
} else if (formula.isRewardOperatorFormula()){ |
|||
preprocessRewardOperatorFormula(formula.asRewardOperatorFormula(), result, currentObjective); |
|||
} else if (formula.isTimeOperatorFormula()){ |
|||
preprocessTimeOperatorFormula(formula.asTimeOperatorFormula(), result, currentObjective); |
|||
} else { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the objective " << formula << " because it is not supported"); |
|||
} |
|||
|
|||
// Transform the threshold for the preprocessed Model
|
|||
if (currentObjective.threshold) { |
|||
currentObjective.threshold = (currentObjective.threshold.get() - currentObjective.toOriginalValueTransformationOffset) / currentObjective.toOriginalValueTransformationFactor; |
|||
} |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
void SparsePcaaPreprocessor<SparseModelType>::preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective) { |
|||
|
|||
if (formula.getSubformula().isUntilFormula()){ |
|||
preprocessUntilFormula(formula.getSubformula().asUntilFormula(), result, currentObjective); |
|||
} else if (formula.getSubformula().isBoundedUntilFormula()){ |
|||
preprocessBoundedUntilFormula(formula.getSubformula().asBoundedUntilFormula(), result, currentObjective); |
|||
} else if (formula.getSubformula().isGloballyFormula()){ |
|||
preprocessGloballyFormula(formula.getSubformula().asGloballyFormula(), result, currentObjective); |
|||
} else if (formula.getSubformula().isEventuallyFormula()){ |
|||
preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), result, currentObjective); |
|||
} else { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); |
|||
} |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
void SparsePcaaPreprocessor<SparseModelType>::preprocessRewardOperatorFormula(storm::logic::RewardOperatorFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective) { |
|||
// Check if the reward model is uniquely specified
|
|||
STORM_LOG_THROW((formula.hasRewardModelName() && result.preprocessedModel.hasRewardModel(formula.getRewardModelName())) |
|||
|| result.preprocessedModel.hasUniqueRewardModel(), storm::exceptions::InvalidPropertyException, "The reward model is not unique and the formula " << formula << " does not specify a reward model."); |
|||
|
|||
if (formula.getSubformula().isEventuallyFormula()){ |
|||
preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), result, currentObjective, formula.getOptionalRewardModelName()); |
|||
} else if (formula.getSubformula().isCumulativeRewardFormula()) { |
|||
preprocessCumulativeRewardFormula(formula.getSubformula().asCumulativeRewardFormula(), result, currentObjective, formula.getOptionalRewardModelName()); |
|||
} else if (formula.getSubformula().isTotalRewardFormula()) { |
|||
preprocessTotalRewardFormula(result, currentObjective, formula.getOptionalRewardModelName()); |
|||
} else { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); |
|||
} |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
void SparsePcaaPreprocessor<SparseModelType>::preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective) { |
|||
// Time formulas are only supported for Markov automata
|
|||
STORM_LOG_THROW(result.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton), storm::exceptions::InvalidPropertyException, "Time operator formulas are only supported for Markov automata."); |
|||
|
|||
if (formula.getSubformula().isEventuallyFormula()){ |
|||
preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), result, currentObjective); |
|||
} else { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); |
|||
} |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
void SparsePcaaPreprocessor<SparseModelType>::preprocessUntilFormula(storm::logic::UntilFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective) { |
|||
|
|||
// Create a memory structure that stores whether a PhiState or a PsiState has already been reached
|
|||
storm::storage::MemoryStructureBuilder builder(2); |
|||
// Get a unique label that is not already present in the model
|
|||
std::string memoryLabel = "obj" + std::to_string(result.objectives.size()); |
|||
while (result.preprocessedModel.hasLabel(memoryLabel)) memoryLabel = "_" + memoryLabel; |
|||
builder.setLabel(0, memoryLabel); |
|||
auto negatedLeftSubFormula = std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getLeftSubformula().asSharedPointer()); |
|||
auto targetFormula = std::make_shared<storm::logic::BinaryBooleanStateFormula>(storm::logic::BinaryBooleanStateFormula::OperatorType::Or, negatedLeftSubFormula, formula.getRightSubformula().asSharedPointer()); |
|||
builder.setTransition(0, 0, std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, targetFormula)); |
|||
builder.setTransition(0, 1, targetFormula); |
|||
builder.setTransition(1, 1, std::make_shared<storm::logic::BooleanLiteralFormula>(true)); |
|||
storm::storage::MemoryStructure memory = builder.build(); |
|||
addMemoryToPreprocessedModel(result, memory); |
|||
|
|||
// build stateAction reward vector that gives (one*transitionProbability) reward whenever a transition leads from a memoryLabel-state to a psiState
|
|||
storm::storage::BitVector const& statesWithMemoryLabel = result.preprocessedModel.getStates(memoryLabel); |
|||
if ((statesWithMemoryLabel & result.preprocessedModel.getInitialStates()).empty() && !currentObjective.lowerTimeBound) { |
|||
// The probability is always one as the initial state is a target state.
|
|||
// For this special case, the transformation to an expected reward objective fails.
|
|||
// We could handle this with further preprocessing steps but as this case is trivial anyway, we reject the input.
|
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The Probability for the objective " << *currentObjective.originalFormula << " is always one as the rhs of the until formula is true in the initial state. Please omit this objective."); |
|||
} |
|||
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> mc(result.preprocessedModel); |
|||
storm::storage::BitVector psiStates = mc.check(formula.getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); |
|||
|
|||
std::vector<ValueType> objectiveRewards(result.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero<ValueType>()); |
|||
for (auto const& state : statesWithMemoryLabel) { |
|||
for (uint_fast64_t row = result.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]; row < result.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++row) { |
|||
objectiveRewards[row] = result.preprocessedModel.getTransitionMatrix().getConstrainedRowSum(row, psiStates); |
|||
} |
|||
} |
|||
if (!currentObjective.rewardsArePositive) { |
|||
storm::utility::vector::scaleVectorInPlace(objectiveRewards, -storm::utility::one<ValueType>()); |
|||
} |
|||
result.preprocessedModel.addRewardModel(currentObjective.rewardModelName, RewardModelType(boost::none, objectiveRewards)); |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
void SparsePcaaPreprocessor<SparseModelType>::preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective) { |
|||
STORM_LOG_THROW(!result.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) || !formula.isStepBounded(), storm::exceptions::InvalidPropertyException, "Multi-objective model checking currently does not support STEP-bounded properties for Markov automata."); |
|||
|
|||
if (formula.hasLowerBound()) { |
|||
currentObjective.lowerTimeBound = formula.getLowerBound(); |
|||
currentObjective.lowerTimeBoundStrict = formula.isLowerBoundStrict(); |
|||
} |
|||
if (formula.hasUpperBound()) { |
|||
currentObjective.upperTimeBound = formula.getUpperBound(); |
|||
currentObjective.upperTimeBoundStrict = formula.isUpperBoundStrict(); |
|||
} |
|||
preprocessUntilFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), result, currentObjective); |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
void SparsePcaaPreprocessor<SparseModelType>::preprocessGloballyFormula(storm::logic::GloballyFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective) { |
|||
// The formula will be transformed to an until formula for the complementary event.
|
|||
// If the original formula minimizes, the complementary one will maximize and vice versa.
|
|||
// Hence, the decision whether to consider positive or negative rewards flips.
|
|||
currentObjective.rewardsArePositive = !currentObjective.rewardsArePositive; |
|||
// To transform from the value of the preprocessed model back to the value of the original model, we have to add 1 to the result.
|
|||
// The transformation factor has already been set correctly.
|
|||
currentObjective.toOriginalValueTransformationOffset = storm::utility::one<ValueType>(); |
|||
|
|||
auto negatedSubformula = std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getSubformula().asSharedPointer()); |
|||
|
|||
preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), negatedSubformula), result, currentObjective); |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
void SparsePcaaPreprocessor<SparseModelType>::preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective, boost::optional<std::string> const& optionalRewardModelName) { |
|||
if (formula.isReachabilityProbabilityFormula()){ |
|||
preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asSharedPointer()), result, currentObjective); |
|||
return; |
|||
} |
|||
|
|||
// Create a memory structure that stores whether a target state has already been reached
|
|||
storm::storage::MemoryStructureBuilder builder(2); |
|||
// Get a unique label that is not already present in the model
|
|||
std::string memoryLabel = "obj" + std::to_string(result.objectives.size()); |
|||
while (result.preprocessedModel.hasLabel(memoryLabel)) memoryLabel = "_" + memoryLabel; |
|||
builder.setLabel(0, memoryLabel); |
|||
builder.setTransition(0, 0, std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getSubformula().asSharedPointer())); |
|||
builder.setTransition(0, 1, formula.getSubformula().asSharedPointer()); |
|||
builder.setTransition(1, 1, std::make_shared<storm::logic::BooleanLiteralFormula>(true)); |
|||
storm::storage::MemoryStructure memory = builder.build(); |
|||
addMemoryToPreprocessedModel(result, memory); |
|||
|
|||
// Add a reward model that only gives reward to states with the memory label
|
|||
RewardModelType objectiveRewards(boost::none); |
|||
if (formula.isReachabilityRewardFormula()) { |
|||
storm::storage::BitVector statesWithoutMemoryLabel = ~result.preprocessedModel.getStates(memoryLabel); |
|||
objectiveRewards = result.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : ""); |
|||
objectiveRewards.reduceToStateBasedRewards(result.preprocessedModel.getTransitionMatrix(), false); |
|||
if (objectiveRewards.hasStateRewards()) { |
|||
storm::utility::vector::setVectorValues(objectiveRewards.getStateRewardVector(), statesWithoutMemoryLabel, storm::utility::zero<ValueType>()); |
|||
} |
|||
if (objectiveRewards.hasStateActionRewards()) { |
|||
for (auto state : statesWithoutMemoryLabel) { |
|||
std::fill_n(objectiveRewards.getStateActionRewardVector().begin() + result.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state], result.preprocessedModel.getTransitionMatrix().getRowGroupSize(state), storm::utility::zero<ValueType>()); |
|||
} |
|||
} |
|||
} else if (formula.isReachabilityTimeFormula() && result.preprocessedModel.isOfType(storm::models::ModelType::MarkovAutomaton)) { |
|||
objectiveRewards = RewardModelType(std::vector<ValueType>(result.preprocessedModel.getNumberOfStates(), storm::utility::zero<ValueType>())); |
|||
storm::utility::vector::setVectorValues(objectiveRewards.getStateRewardVector(), dynamic_cast<storm::models::sparse::MarkovAutomaton<ValueType>*>(&result.preprocessedModel)->getMarkovianStates() & result.preprocessedModel.getStates(memoryLabel), storm::utility::one<ValueType>()); |
|||
} else { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The formula " << formula << " neither considers reachability probabilities nor reachability rewards " << (result.preprocessedModel.isOfType(storm::models::ModelType::MarkovAutomaton) ? "nor reachability time" : "") << ". This is not supported."); |
|||
} |
|||
if (!currentObjective.rewardsArePositive){ |
|||
if (objectiveRewards.hasStateRewards()) { |
|||
storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateRewardVector(), -storm::utility::one<ValueType>()); |
|||
} |
|||
if (objectiveRewards.hasStateActionRewards()) { |
|||
storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateActionRewardVector(), -storm::utility::one<ValueType>()); |
|||
} |
|||
} |
|||
result.preprocessedModel.addRewardModel(currentObjective.rewardModelName, std::move(objectiveRewards)); |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
void SparsePcaaPreprocessor<SparseModelType>::preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective, boost::optional<std::string> const& optionalRewardModelName) { |
|||
STORM_LOG_THROW(result.originalModel.isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidPropertyException, "Cumulative reward formulas are not supported for the given model type."); |
|||
currentObjective.upperTimeBound = formula.getBound(); |
|||
currentObjective.upperTimeBoundStrict = formula.isBoundStrict(); |
|||
|
|||
RewardModelType objectiveRewards = result.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : ""); |
|||
objectiveRewards.reduceToStateBasedRewards(result.preprocessedModel.getTransitionMatrix(), false); |
|||
if (!currentObjective.rewardsArePositive){ |
|||
if (objectiveRewards.hasStateRewards()) { |
|||
storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateRewardVector(), -storm::utility::one<ValueType>()); |
|||
} |
|||
if (objectiveRewards.hasStateActionRewards()) { |
|||
storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateActionRewardVector(), -storm::utility::one<ValueType>()); |
|||
} |
|||
} |
|||
result.preprocessedModel.addRewardModel(currentObjective.rewardModelName, std::move(objectiveRewards)); |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
void SparsePcaaPreprocessor<SparseModelType>::preprocessTotalRewardFormula(ReturnType& result, PcaaObjective<ValueType>& currentObjective, boost::optional<std::string> const& optionalRewardModelName) { |
|||
RewardModelType objectiveRewards = result.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : ""); |
|||
objectiveRewards.reduceToStateBasedRewards(result.preprocessedModel.getTransitionMatrix(), false); |
|||
if (!currentObjective.rewardsArePositive){ |
|||
if (objectiveRewards.hasStateRewards()) { |
|||
storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateRewardVector(), -storm::utility::one<ValueType>()); |
|||
} |
|||
if (objectiveRewards.hasStateActionRewards()) { |
|||
storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateActionRewardVector(), -storm::utility::one<ValueType>()); |
|||
} |
|||
} |
|||
result.preprocessedModel.addRewardModel(currentObjective.rewardModelName, std::move(objectiveRewards)); |
|||
} |
|||
|
|||
|
|||
template<typename SparseModelType> |
|||
void SparsePcaaPreprocessor<SparseModelType>::analyzeEndComponents(ReturnType& result, storm::storage::SparseMatrix<ValueType> const& backwardTransitions) { |
|||
|
|||
result.ecActions = storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), false); |
|||
std::vector<storm::storage::MaximalEndComponent> ecs; |
|||
auto mecDecomposition = storm::storage::MaximalEndComponentDecomposition<ValueType>(result.preprocessedModel.getTransitionMatrix(), backwardTransitions); |
|||
STORM_LOG_ASSERT(!mecDecomposition.empty(), "Empty maximal end component decomposition."); |
|||
ecs.reserve(mecDecomposition.size()); |
|||
for (auto& mec : mecDecomposition) { |
|||
for (auto const& stateActionsPair : mec) { |
|||
for (auto const& action : stateActionsPair.second) { |
|||
result.ecActions.set(action); |
|||
} |
|||
} |
|||
ecs.push_back(std::move(mec)); |
|||
} |
|||
|
|||
result.possiblyRecurrentStates = storm::storage::BitVector(result.preprocessedModel.getNumberOfStates(), false); |
|||
storm::storage::BitVector neutralActions = ~(result.actionsWithNegativeReward | result.actionsWithPositiveReward); |
|||
storm::storage::BitVector statesInCurrentECWithNeutralAction(result.preprocessedModel.getNumberOfStates(), false); |
|||
for (uint_fast64_t ecIndex = 0; ecIndex < ecs.size(); ++ecIndex) { //we will insert new ecs in the vector (thus no iterators for the loop)
|
|||
bool currentECIsNeutral = true; |
|||
for (auto const& stateActionsPair : ecs[ecIndex]) { |
|||
bool stateHasNeutralActionWithinEC = false; |
|||
for (auto const& action : stateActionsPair.second) { |
|||
stateHasNeutralActionWithinEC |= neutralActions.get(action); |
|||
} |
|||
statesInCurrentECWithNeutralAction.set(stateActionsPair.first, stateHasNeutralActionWithinEC); |
|||
currentECIsNeutral &= stateHasNeutralActionWithinEC; |
|||
} |
|||
if (currentECIsNeutral) { |
|||
result.possiblyRecurrentStates |= statesInCurrentECWithNeutralAction; |
|||
}else{ |
|||
// Check if the ec contains neutral sub ecs. This is done by adding the subECs to our list of ECs
|
|||
// A neutral subEC only consist of states that can stay in statesInCurrentECWithNeutralAction
|
|||
statesInCurrentECWithNeutralAction = storm::utility::graph::performProb0E(result.preprocessedModel.getTransitionMatrix(), result.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), backwardTransitions,statesInCurrentECWithNeutralAction, ~statesInCurrentECWithNeutralAction); |
|||
auto subECs = storm::storage::MaximalEndComponentDecomposition<ValueType>(result.preprocessedModel.getTransitionMatrix(), backwardTransitions, statesInCurrentECWithNeutralAction); |
|||
ecs.reserve(ecs.size() + subECs.size()); |
|||
for (auto& ec : subECs){ |
|||
ecs.push_back(std::move(ec)); |
|||
} |
|||
} |
|||
statesInCurrentECWithNeutralAction.clear(); |
|||
} |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
void SparsePcaaPreprocessor<SparseModelType>::ensureRewardFiniteness(ReturnType& result, storm::storage::SparseMatrix<ValueType> const& backwardTransitions) { |
|||
STORM_LOG_THROW((result.actionsWithPositiveReward & result.ecActions).empty(), storm::exceptions::InvalidPropertyException, "Infinite reward: There is one maximizing objective for which infinite reward is possible. This is not supported."); |
|||
|
|||
//Check whether the states that can be visited inf. often are reachable with prob. 1 under some scheduler
|
|||
storm::storage::BitVector statesReachingNegativeRewardsFinitelyOftenForSomeScheduler = storm::utility::graph::performProb1E(result.preprocessedModel.getTransitionMatrix(), result.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), backwardTransitions, storm::storage::BitVector(result.preprocessedModel.getNumberOfStates(), true), result.possiblyRecurrentStates); |
|||
STORM_LOG_THROW(!(statesReachingNegativeRewardsFinitelyOftenForSomeScheduler & result.preprocessedModel.getInitialStates()).empty(), storm::exceptions::InvalidPropertyException, "Infinite Rewards: For every scheduler, the induced reward for one or more of the objectives that minimize rewards is infinity."); |
|||
|
|||
if (!statesReachingNegativeRewardsFinitelyOftenForSomeScheduler.full()) { |
|||
// Remove the states that for any scheduler have one objective with infinite expected reward.
|
|||
auto subsystemBuilderResult = storm::transformer::SubsystemBuilder<SparseModelType>::transform(result.preprocessedModel, statesReachingNegativeRewardsFinitelyOftenForSomeScheduler, storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), true)); |
|||
updatePreprocessedModel(result, *subsystemBuilderResult.model, subsystemBuilderResult.newToOldStateIndexMapping); |
|||
result.ecActions = result.ecActions % subsystemBuilderResult.keptActions; |
|||
result.actionsWithPositiveReward = result.actionsWithPositiveReward % subsystemBuilderResult.keptActions; |
|||
result.actionsWithNegativeReward = result.actionsWithNegativeReward % subsystemBuilderResult.keptActions; |
|||
result.possiblyRecurrentStates = result.possiblyRecurrentStates % statesReachingNegativeRewardsFinitelyOftenForSomeScheduler; |
|||
} |
|||
} |
|||
|
|||
|
|||
|
|||
template class SparsePcaaPreprocessor<storm::models::sparse::Mdp<double>>; |
|||
template class SparsePcaaPreprocessor<storm::models::sparse::MarkovAutomaton<double>>; |
|||
|
|||
#ifdef STORM_HAVE_CARL
|
|||
template class SparsePcaaPreprocessor<storm::models::sparse::Mdp<storm::RationalNumber>>; |
|||
template class SparsePcaaPreprocessor<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>; |
|||
#endif
|
|||
} |
|||
} |
|||
} |
|||
@ -1,82 +0,0 @@ |
|||
#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAPREPROCESSOR_H_ |
|||
#define STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAPREPROCESSOR_H_ |
|||
|
|||
#include <memory> |
|||
|
|||
#include "storm/logic/Formulas.h" |
|||
#include "storm/storage/BitVector.h" |
|||
#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessorReturnType.h" |
|||
#include "storm/storage/memorystructure/MemoryStructure.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace multiobjective { |
|||
|
|||
/* |
|||
* This class invokes the necessary preprocessing for the Pareto Curve Approximation Algorithm (PCAA) |
|||
*/ |
|||
template <class SparseModelType> |
|||
class SparsePcaaPreprocessor { |
|||
public: |
|||
typedef typename SparseModelType::ValueType ValueType; |
|||
typedef typename SparseModelType::RewardModelType RewardModelType; |
|||
typedef SparsePcaaPreprocessorReturnType<SparseModelType> ReturnType; |
|||
|
|||
/*! |
|||
* Preprocesses the given model w.r.t. the given formulas. |
|||
* @param originalModel The considered model |
|||
* @param originalFormula the considered formula. The subformulas should only contain one OperatorFormula at top level, i.e., the formula is simple. |
|||
*/ |
|||
static ReturnType preprocess(SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula); |
|||
|
|||
private: |
|||
|
|||
/*! |
|||
* Updates the preprocessed model stored in the given result to the given model. |
|||
* The given newToOldStateIndexMapping should give for each state in the newPreprocessedModel |
|||
* the index of the state in the current result.preprocessedModel. |
|||
*/ |
|||
static void updatePreprocessedModel(ReturnType& result, SparseModelType& newPreprocessedModel, std::vector<uint_fast64_t>& newToOldStateIndexMapping); |
|||
|
|||
/*! |
|||
* Updates the preprocessed model stored in the given result to the product of the model and the given memory structure. |
|||
*/ |
|||
static void addMemoryToPreprocessedModel(ReturnType& result, storm::storage::MemoryStructure& memory); |
|||
|
|||
/*! |
|||
* Apply the neccessary preprocessing for the given formula. |
|||
* @param formula the current (sub)formula |
|||
* @param result the information collected so far |
|||
* @param currentObjective the currently considered objective. The given formula should be a a (sub)formula of this objective |
|||
* @param optionalRewardModelName the reward model name that is considered for the formula (if available) |
|||
*/ |
|||
static void preprocessOperatorFormula(storm::logic::OperatorFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective); |
|||
static void preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective); |
|||
static void preprocessRewardOperatorFormula(storm::logic::RewardOperatorFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective); |
|||
static void preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective); |
|||
static void preprocessUntilFormula(storm::logic::UntilFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective); |
|||
static void preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective); |
|||
static void preprocessGloballyFormula(storm::logic::GloballyFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective); |
|||
static void preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective, boost::optional<std::string> const& optionalRewardModelName = boost::none); |
|||
static void preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective, boost::optional<std::string> const& optionalRewardModelName = boost::none); |
|||
static void preprocessTotalRewardFormula(ReturnType& result, PcaaObjective<ValueType>& currentObjective, boost::optional<std::string> const& optionalRewardModelName = boost::none); // The total reward formula itself does not need to be provided as it is unique. |
|||
|
|||
/*! |
|||
* Analyzes the end components of the preprocessed model. That is: |
|||
* -get the set of actions that are part of an end component |
|||
* -Find the states that can be visited infinitely often without inducing infinite reward |
|||
*/ |
|||
static void analyzeEndComponents(ReturnType& result, storm::storage::SparseMatrix<ValueType> const& backwardTransitions); |
|||
|
|||
/*! |
|||
* Checks whether the occurring expected rewards are finite. If not, the input is rejected. |
|||
* Also removes all states for which no finite reward wrt. all objectives is possible |
|||
*/ |
|||
static void ensureRewardFiniteness(ReturnType& result, storm::storage::SparseMatrix<ValueType> const& backwardTransitions); |
|||
|
|||
}; |
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAPREPROCESSOR_H_ */ |
|||
@ -1,93 +0,0 @@ |
|||
#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAPREPROCESSORRETURNTYPE_H_ |
|||
#define STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAPREPROCESSORRETURNTYPE_H_ |
|||
|
|||
#include <vector> |
|||
#include <memory> |
|||
#include <iomanip> |
|||
#include <type_traits> |
|||
#include <boost/optional.hpp> |
|||
|
|||
#include "storm/logic/Formulas.h" |
|||
#include "storm/modelchecker/multiobjective/pcaa/PcaaObjective.h" |
|||
#include "storm/models/sparse/MarkovAutomaton.h" |
|||
#include "storm/storage/BitVector.h" |
|||
#include "storm/utility/macros.h" |
|||
#include "storm/utility/constants.h" |
|||
|
|||
#include "storm/exceptions/UnexpectedException.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace multiobjective { |
|||
|
|||
template <class SparseModelType> |
|||
struct SparsePcaaPreprocessorReturnType { |
|||
|
|||
enum class QueryType { Achievability, Quantitative, Pareto }; |
|||
|
|||
storm::logic::MultiObjectiveFormula const& originalFormula; |
|||
SparseModelType const& originalModel; |
|||
SparseModelType preprocessedModel; |
|||
QueryType queryType; |
|||
|
|||
// The (preprocessed) objectives |
|||
std::vector<PcaaObjective<typename SparseModelType::ValueType>> objectives; |
|||
|
|||
// The index of the objective that is to be maximized (or minimized) in case of a quantitative Query |
|||
boost::optional<uint_fast64_t> indexOfOptimizingObjective; |
|||
|
|||
// Maps any state of the preprocessed model to the corresponding state of the original Model |
|||
std::vector<uint_fast64_t> newToOldStateIndexMapping; |
|||
|
|||
// The actions of the preprocessed model that have positive reward assigned for at least one objective (objectives with an upper time-bound are ignored!) |
|||
storm::storage::BitVector actionsWithPositiveReward; |
|||
// The actions of the preprocessed model that have negative reward assigned for at least one objective (objectives with an upper time-bound are ignored!) |
|||
storm::storage::BitVector actionsWithNegativeReward; |
|||
// The actions of the preprocessed model that are part of an EC |
|||
storm::storage::BitVector ecActions; |
|||
|
|||
// The set of states of the preprocessed model for which there is a scheduler such that |
|||
// the state is visited infinitely often and the induced reward is finite for all objectives |
|||
storm::storage::BitVector possiblyRecurrentStates; |
|||
|
|||
SparsePcaaPreprocessorReturnType(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel, SparseModelType&& preprocessedModel) : originalFormula(originalFormula), originalModel(originalModel), preprocessedModel(preprocessedModel) { |
|||
// Intentionally left empty |
|||
} |
|||
|
|||
void printToStream(std::ostream& out) const { |
|||
out << std::endl; |
|||
out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; |
|||
out << " Multi-objective Query " << std::endl; |
|||
out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; |
|||
out << std::endl; |
|||
out << "Original Formula: " << std::endl; |
|||
out << "--------------------------------------------------------------" << std::endl; |
|||
out << "\t" << originalFormula << std::endl; |
|||
out << std::endl; |
|||
out << "Objectives:" << std::endl; |
|||
out << "--------------------------------------------------------------" << std::endl; |
|||
for (auto const& obj : objectives) { |
|||
obj.printToStream(out); |
|||
} |
|||
out << "--------------------------------------------------------------" << std::endl; |
|||
out << std::endl; |
|||
out << "Original Model Information:" << std::endl; |
|||
originalModel.printModelInformationToStream(out); |
|||
out << std::endl; |
|||
out << "Preprocessed Model Information:" << std::endl; |
|||
preprocessedModel.printModelInformationToStream(out); |
|||
out << std::endl; |
|||
out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; |
|||
} |
|||
|
|||
friend std::ostream& operator<<(std::ostream& out, SparsePcaaPreprocessorReturnType<SparseModelType> const& ret) { |
|||
ret.printToStream(out); |
|||
return out; |
|||
} |
|||
|
|||
}; |
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAPREPROCESSORRETURNTYPE_H_ */ |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue