From a3aededd3aec9932acef78d0a4c58c8d65a7bdd1 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 9 Mar 2016 13:28:50 +0100 Subject: [PATCH 1/3] public access to model ingredients: RewardModel and exitRates Former-commit-id: b8dbe8576eeb3c5a3e78b6046a7c457f326772b6 --- src/models/sparse/MarkovAutomaton.cpp | 5 +++++ src/models/sparse/MarkovAutomaton.h | 7 +++++++ src/models/sparse/Model.h | 29 ++++++++++++++------------- 3 files changed, 27 insertions(+), 14 deletions(-) diff --git a/src/models/sparse/MarkovAutomaton.cpp b/src/models/sparse/MarkovAutomaton.cpp index 56a6400d1..983bda12e 100644 --- a/src/models/sparse/MarkovAutomaton.cpp +++ b/src/models/sparse/MarkovAutomaton.cpp @@ -55,6 +55,11 @@ namespace storm { return this->exitRates; } + template + std::vector& MarkovAutomaton::getExitRates() { + return this->exitRates; + } + template ValueType const& MarkovAutomaton::getExitRate(storm::storage::sparse::state_type state) const { return this->exitRates[state]; diff --git a/src/models/sparse/MarkovAutomaton.h b/src/models/sparse/MarkovAutomaton.h index 731b845f3..0556ffa9b 100644 --- a/src/models/sparse/MarkovAutomaton.h +++ b/src/models/sparse/MarkovAutomaton.h @@ -94,6 +94,13 @@ namespace storm { */ std::vector const& getExitRates() const; + /*! + * Retrieves the vector representing the exit rates of the states. + * + * @return The exit rate vector of the model. + */ + std::vector& getExitRates(); + /*! * Retrieves the exit rate of the given state. * diff --git a/src/models/sparse/Model.h b/src/models/sparse/Model.h index dc0378348..a458bdff7 100644 --- a/src/models/sparse/Model.h +++ b/src/models/sparse/Model.h @@ -140,6 +140,21 @@ namespace storm { */ storm::storage::SparseMatrix& getTransitionMatrix(); + + /*! + * Retrieves the reward models. + * + * @return A mapping from reward model names to the reward models. + */ + std::unordered_map const& getRewardModels() const; + + /*! + * Retrieves the reward models. + * + * @return A mapping from reward model names to the reward models. + */ + std::unordered_map& getRewardModels(); + /*! * Retrieves whether the model has a reward model with the given name. * @@ -318,20 +333,6 @@ namespace storm { */ void printRewardModelsInformationToStream(std::ostream& out) const; - /*! - * Retrieves the reward models. - * - * @return A mapping from reward model names to the reward models. - */ - std::unordered_map const& getRewardModels() const; - - /*! - * Retrieves the reward models. - * - * @return A mapping from reward model names to the reward models. - */ - std::unordered_map& getRewardModels(); - private: // A matrix representing transition relation. storm::storage::SparseMatrix transitionMatrix; From 69c5ba604e388caef9644063e09a5c0a1063c2c5 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 9 Mar 2016 13:29:26 +0100 Subject: [PATCH 2/3] Helper functions for parametric stuff Former-commit-id: 288e4de3da6b1deb13fd4e758dbc2b557f375ab1 --- src/utility/constants.cpp | 19 ++++++++++++-- src/utility/constants.h | 3 +++ src/utility/parametric.cpp | 39 +++++++++++++++++++++++++++ src/utility/parametric.h | 54 ++++++++++++++++++++++++++++++++++++++ 4 files changed, 113 insertions(+), 2 deletions(-) create mode 100644 src/utility/parametric.cpp create mode 100644 src/utility/parametric.h diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp index 900482a72..2aa10d23a 100644 --- a/src/utility/constants.cpp +++ b/src/utility/constants.cpp @@ -39,6 +39,7 @@ namespace storm { bool isConstant(ValueType const& a) { return true; } + #ifdef STORM_HAVE_CARL template<> @@ -85,11 +86,11 @@ namespace storm { template ValueType simplify(ValueType value) { - // In the general case, we don't to anything here, but merely return the value. If something else is + // In the general case, we don't do anything here, but merely return the value. If something else is // supposed to happen here, the templated function can be specialized for this particular type. return value; } - + #ifdef STORM_HAVE_CARL template<> RationalFunction& simplify(RationalFunction& value); @@ -119,6 +120,17 @@ namespace storm { value.simplify(); return std::move(value); } + + template<> + double convertNumber(RationalNumber const& number){ + return carl::toDouble(number); + } + + template<> + RationalNumber convertNumber(double const& number){ + return carl::rationalize(number); + } + #endif template @@ -221,6 +233,9 @@ namespace storm { template RationalFunction& simplify(RationalFunction& value); template RationalFunction&& simplify(RationalFunction&& value); + template double convertNumber(RationalNumber const& number); + template RationalNumber convertNumber(double const& number); + template bool isOne(Interval const& value); template bool isZero(Interval const& value); template bool isConstant(Interval const& value); diff --git a/src/utility/constants.h b/src/utility/constants.h index 8f6d8149e..80222b74f 100644 --- a/src/utility/constants.h +++ b/src/utility/constants.h @@ -50,6 +50,9 @@ namespace storm { template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); + + template + TargetType convertNumber(SourceType const& number); } } diff --git a/src/utility/parametric.cpp b/src/utility/parametric.cpp new file mode 100644 index 000000000..c45882c42 --- /dev/null +++ b/src/utility/parametric.cpp @@ -0,0 +1,39 @@ +/* + * File: parametric.cpp + * Author: Tim Quatmann + * + * Created by Tim Quatmann on 08/03/16. + */ + +#include + +#include "src/utility/parametric.h" +#include "src/utility/constants.h" +#include "src/utility/macros.h" +#include "src/settings/SettingsManager.h" +#include "src/exceptions/IllegalArgumentException.h" +#include "src/exceptions/NotImplementedException.h" + +#ifdef STORM_HAVE_CARL +#include +#include +#endif + +namespace storm { + namespace utility{ + namespace parametric { + +#ifdef STORM_HAVE_CARL + template<> + typename CoefficientType::type evaluate(storm::RationalFunction const& function, std::map::type, typename CoefficientType::type> const& valuation){ + return function.evaluate(valuation); + } + + template<> + typename CoefficientType::type getConstantPart(storm::RationalFunction const& function){ + return function.constantPart(); + } +#endif + } + } +} diff --git a/src/utility/parametric.h b/src/utility/parametric.h new file mode 100644 index 000000000..2ebf1e18c --- /dev/null +++ b/src/utility/parametric.h @@ -0,0 +1,54 @@ +// +// parametric.h +// +// Created by Tim Quatmann on 08/03/16. +// +// + +#ifndef STORM_UTILITY_PARAMETRIC_H +#define STORM_UTILITY_PARAMETRIC_H + +#include "src/adapters/CarlAdapter.h" + + +namespace storm { + namespace utility { + namespace parametric { + + /*! + * Access the type of variables from a given function type + */ + template + struct VariableType { typedef void type; }; + /*! + * Acess the type of coefficients from a given function type + */ + template + struct CoefficientType { typedef void type; }; + +#ifdef STORM_HAVE_CARL + template<> + struct VariableType { typedef storm::Variable type; }; + template<> + struct CoefficientType { typedef storm::RationalNumber type; }; +#endif + + /*! + * Evaluates the given function wrt. the given valuation + */ + template + typename CoefficientType::type evaluate(FunctionType const& function, std::map::type, typename CoefficientType::type> const& valuation); + + /*! + * Retrieves the constant part of the given function. + */ + template + typename CoefficientType::type getConstantPart(FunctionType const& function); + + } + + } +} + + +#endif /* STORM_UTILITY_PARAMETRIC_H */ From 6e8602413e8524f74cbc26f940df5ddaaaa5d5a7 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 9 Mar 2016 13:29:42 +0100 Subject: [PATCH 3/3] ModelInstantiator + test Former-commit-id: f3c998006745041f98df1176aa8eeec9bd935028 --- src/models/sparse/StochasticTwoPlayerGame.cpp | 2 +- src/utility/ModelInstantiator.cpp | 161 +++++++++++ src/utility/ModelInstantiator.h | 158 +++++++++++ .../utility/ModelInstantiatorTest.cpp | 266 ++++++++++++++++++ test/functional/utility/brp16_2.pm | 146 ++++++++++ test/functional/utility/coin2_2.pm | 56 ++++ 6 files changed, 788 insertions(+), 1 deletion(-) create mode 100644 src/utility/ModelInstantiator.cpp create mode 100644 src/utility/ModelInstantiator.h create mode 100644 test/functional/utility/ModelInstantiatorTest.cpp create mode 100644 test/functional/utility/brp16_2.pm create mode 100644 test/functional/utility/coin2_2.pm diff --git a/src/models/sparse/StochasticTwoPlayerGame.cpp b/src/models/sparse/StochasticTwoPlayerGame.cpp index c8ce13bec..7a6ea02a1 100644 --- a/src/models/sparse/StochasticTwoPlayerGame.cpp +++ b/src/models/sparse/StochasticTwoPlayerGame.cpp @@ -65,7 +65,7 @@ namespace storm { // template class StochasticTwoPlayerGame; #ifdef STORM_HAVE_CARL -// template class StochasticTwoPlayerGame; + template class StochasticTwoPlayerGame; #endif } // namespace sparse diff --git a/src/utility/ModelInstantiator.cpp b/src/utility/ModelInstantiator.cpp new file mode 100644 index 000000000..cb8c62535 --- /dev/null +++ b/src/utility/ModelInstantiator.cpp @@ -0,0 +1,161 @@ +/* + * File: ModelInstantiator.cpp + * Author: Tim Quatmann + * + * Created on February 23, 2016 + */ + +#include "src/utility/ModelInstantiator.h" +#include "src/models/sparse/StandardRewardModel.h" + +namespace storm { + namespace utility { + + template + ModelInstantiator::ModelInstantiator(ParametricSparseModelType const& parametricModel){ + //Now pre-compute the information for the equation system. + initializeModelSpecificData(parametricModel); + initializeMatrixMapping(this->instantiatedModel->getTransitionMatrix(), this->functions, this->matrixMapping, parametricModel.getTransitionMatrix()); + + for(auto& rewModel : this->instantiatedModel->getRewardModels()) { + if(rewModel.second.hasStateRewards()){ + initializeVectorMapping(rewModel.second.getStateRewardVector(), this->functions, this->vectorMapping, parametricModel.getRewardModel(rewModel.first).getStateRewardVector()); + } + if(rewModel.second.hasStateActionRewards()){ + initializeVectorMapping(rewModel.second.getStateActionRewardVector(), this->functions, this->vectorMapping, parametricModel.getRewardModel(rewModel.first).getStateActionRewardVector()); + } + if(rewModel.second.hasTransitionRewards()){ + initializeMatrixMapping(rewModel.second.getTransitionRewardMatrix(), this->functions, this->matrixMapping, parametricModel.getRewardModel(rewModel.first).getTransitionRewardMatrix()); + } + } + } + + template + ModelInstantiator::~ModelInstantiator() { + //Intentionally left empty + } + + template + storm::storage::SparseMatrix ModelInstantiator::buildDummyMatrix(storm::storage::SparseMatrix const& parametricMatrix) const{ + storm::storage::SparseMatrixBuilder matrixBuilder(parametricMatrix.getRowCount(), + parametricMatrix.getColumnCount(), + parametricMatrix.getEntryCount(), + true, // no force dimensions + true, //Custom row grouping + parametricMatrix.getRowGroupCount()); + for(std::size_t rowGroup = 0; rowGroup < parametricMatrix.getRowGroupCount(); ++rowGroup){ + matrixBuilder.newRowGroup(parametricMatrix.getRowGroupIndices()[rowGroup]); + for(std::size_t row = parametricMatrix.getRowGroupIndices()[rowGroup]; row < parametricMatrix.getRowGroupIndices()[rowGroup+1]; ++row){ + ConstantType dummyValue = storm::utility::one(); + for(auto const& paramEntry : parametricMatrix.getRow(row)){ + matrixBuilder.addNextValue(row, paramEntry.getColumn(), dummyValue); + dummyValue = storm::utility::zero(); + } + } + } + return matrixBuilder.build(); + } + + template + std::unordered_map ModelInstantiator::buildDummyRewardModels(std::unordered_map const& parametricRewardModel) const { + std::unordered_map result; + for(auto const& paramRewardModel : parametricRewardModel){ + auto const& rewModel = paramRewardModel.second; + boost::optional> optionalStateRewardVector; + if(rewModel.hasStateRewards()) { + optionalStateRewardVector = std::vector(rewModel.getStateRewardVector().size()); + } + boost::optional> optionalStateActionRewardVector; + if(rewModel.hasStateActionRewards()) { + optionalStateActionRewardVector = std::vector(rewModel.getStateActionRewardVector().size()); + } + boost::optional> optionalTransitionRewardMatrix; + if(rewModel.hasTransitionRewards()) { + optionalTransitionRewardMatrix = buildDummyMatrix(rewModel.getTransitionRewardMatrix()); + } + result.insert(std::make_pair(paramRewardModel.first, + storm::models::sparse::StandardRewardModel(std::move(optionalStateRewardVector), std::move(optionalStateActionRewardVector), std::move(optionalTransitionRewardMatrix)) + )); + } + return result; + } + + template + void ModelInstantiator::initializeMatrixMapping(storm::storage::SparseMatrix& constantMatrix, + std::unordered_map& functions, + std::vector::iterator, ConstantType*>>& mapping, + storm::storage::SparseMatrix const& parametricMatrix) const{ + ConstantType dummyValue = storm::utility::one(); + auto constantEntryIt = constantMatrix.begin(); + auto parametricEntryIt = parametricMatrix.begin(); + while(parametricEntryIt != parametricMatrix.end()){ + STORM_LOG_ASSERT(parametricEntryIt->getColumn() == constantEntryIt->getColumn(), "Entries of parametric and constant matrix are not at the same position"); + if(storm::utility::isConstant(parametricEntryIt->getValue())){ + //Constant entries can be inserted directly + constantEntryIt->setValue(storm::utility::convertNumber(storm::utility::parametric::getConstantPart(parametricEntryIt->getValue()))); + } else { + //insert the new function and store that the current constantMatrix entry needs to be set to the value of this function + auto functionsIt = functions.insert(std::make_pair(parametricEntryIt->getValue(), dummyValue)).first; + mapping.emplace_back(std::make_pair(constantEntryIt, &(functionsIt->second))); + //Note that references to elements of an unordered map remain valid after calling unordered_map::insert. + } + ++constantEntryIt; + ++parametricEntryIt; + } + STORM_LOG_ASSERT(constantEntryIt == constantMatrix.end(), "Parametric matrix seems to have more or less entries then the constant matrix"); + //TODO: is this necessary? + constantMatrix.updateNonzeroEntryCount(); + } + + template + void ModelInstantiator::initializeVectorMapping(std::vector& constantVector, + std::unordered_map& functions, + std::vector::iterator, ConstantType*>>& mapping, + std::vector const& parametricVector) const{ + ConstantType dummyValue = storm::utility::one(); + auto constantEntryIt = constantVector.begin(); + auto parametricEntryIt = parametricVector.begin(); + while(parametricEntryIt != parametricVector.end()){ + if(storm::utility::isConstant(storm::utility::simplify(*parametricEntryIt))){ + //Constant entries can be inserted directly + *constantEntryIt = storm::utility::convertNumber(storm::utility::parametric::getConstantPart(*parametricEntryIt)); + } else { + //insert the new function and store that the current constantVector entry needs to be set to the value of this function + auto functionsIt = functions.insert(std::make_pair(*parametricEntryIt, dummyValue)).first; + mapping.emplace_back(std::make_pair(constantEntryIt, &(functionsIt->second))); + //Note that references to elements of an unordered map remain valid after calling unordered_map::insert. + } + ++constantEntryIt; + ++parametricEntryIt; + } + STORM_LOG_ASSERT(constantEntryIt == constantVector.end(), "Parametric vector seems to have more or less entries then the constant vector"); + } + + template + ConstantSparseModelType const& ModelInstantiator::instantiate(std::mapconst& valuation){ + //Write results into the placeholders + for(auto& functionResult : this->functions){ + functionResult.second=storm::utility::convertNumber( + storm::utility::parametric::evaluate(functionResult.first, valuation)); + } + + //Write the instantiated values to the matrices and vectors according to the stored mappings + for(auto& entryValuePair : this->matrixMapping){ + entryValuePair.first->setValue(*(entryValuePair.second)); + } + for(auto& entryValuePair : this->vectorMapping){ + *(entryValuePair.first)=*(entryValuePair.second); + } + + return *this->instantiatedModel; + } + +#ifdef STORM_HAVE_CARL + template class ModelInstantiator, storm::models::sparse::Dtmc>; + template class ModelInstantiator, storm::models::sparse::Mdp>; + template class ModelInstantiator, storm::models::sparse::Ctmc>; + template class ModelInstantiator, storm::models::sparse::MarkovAutomaton>; + template class ModelInstantiator, storm::models::sparse::StochasticTwoPlayerGame>; +#endif + } //namespace utility +} //namespace storm \ No newline at end of file diff --git a/src/utility/ModelInstantiator.h b/src/utility/ModelInstantiator.h new file mode 100644 index 000000000..939e71e2d --- /dev/null +++ b/src/utility/ModelInstantiator.h @@ -0,0 +1,158 @@ +/* + * File: ModelInstantiator.h + * Author: Tim Quatmann + * + * Created on February 23, 2016 + */ + +#ifndef STORM_UTILITY_MODELINSTANTIATOR_H +#define STORM_UTILITY_MODELINSTANTIATOR_H + +#include +#include +#include + +#include "src/models/sparse/Dtmc.h" +#include "src/models/sparse/Mdp.h" +#include "src/models/sparse/Ctmc.h" +#include "src/models/sparse/MarkovAutomaton.h" +#include "src/models/sparse/StochasticTwoPlayerGame.h" +#include "src/utility/parametric.h" +#include "src/utility/constants.h" + +namespace storm { + namespace utility{ + + + /*! + * This class allows efficient instantiation of the given parametric model. + * The key to efficiency is to evaluate every distinct transition- (or reward-) function only once + * instead of evaluating the same function for each occurrence in the model. + */ + template + class ModelInstantiator { + public: + typedef typename ParametricSparseModelType::ValueType ParametricType; + typedef typename storm::utility::parametric::VariableType::type VariableType; + typedef typename storm::utility::parametric::CoefficientType::type CoefficientType; + typedef typename ConstantSparseModelType::ValueType ConstantType; + + /*! + * Constructs a ModelInstantiator + * @param parametricModel The model that is to be instantiated + */ + ModelInstantiator(ParametricSparseModelType const& parametricModel); + + /*! + * Destructs the ModelInstantiator + */ + virtual ~ModelInstantiator(); + + /*! + * Evaluates the occurring parametric functions and retrieves the instantiated model + * @param valuation Maps each occurring variables to the value with which it should be substituted + * @return The instantiated model + */ + ConstantSparseModelType const& instantiate(std::mapconst& valuation); + + + private: + /*! + * Initializes the instantiatedModel with dummy data by considering the model-specific ingredients. + * Also initializes other model-specific data, e.g., the exitRate vector of a markov automaton + */ + template + typename std::enable_if< + std::is_same>::value || + std::is_same>::value || + std::is_same>::value + >::type + initializeModelSpecificData(PMT const& parametricModel) { + auto stateLabelingCopy = parametricModel.getStateLabeling(); + auto choiceLabelingCopy = parametricModel.getOptionalChoiceLabeling(); + this->instantiatedModel = std::make_shared(buildDummyMatrix(parametricModel.getTransitionMatrix()), std::move(stateLabelingCopy), buildDummyRewardModels(parametricModel.getRewardModels()), std::move(choiceLabelingCopy)); + } + + template + typename std::enable_if< + std::is_same>::value + >::type + initializeModelSpecificData(PMT const& parametricModel) { + auto stateLabelingCopy = parametricModel.getStateLabeling(); + auto markovianStatesCopy = parametricModel.getMarkovianStates(); + auto choiceLabelingCopy = parametricModel.getOptionalChoiceLabeling(); + std::vector exitRates(parametricModel.getExitRates().size(), storm::utility::one()); + this->instantiatedModel = std::make_shared(buildDummyMatrix(parametricModel.getTransitionMatrix()), std::move(stateLabelingCopy), std::move(markovianStatesCopy), std::move(exitRates), buildDummyRewardModels(parametricModel.getRewardModels()), std::move(choiceLabelingCopy)); + + initializeVectorMapping(this->instantiatedModel->getExitRates(), this->functions, this->vectorMapping, parametricModel.getExitRates()); + } + + template + typename std::enable_if< + std::is_same>::value + >::type + initializeModelSpecificData(PMT const& parametricModel) { + auto player1MatrixCopy = parametricModel.getPlayer1Matrix(); + auto stateLabelingCopy = parametricModel.getStateLabeling(); + boost::optional> player1ChoiceLabeling, player2ChoiceLabeling; + if(parametricModel.hasPlayer1ChoiceLabeling()) player1ChoiceLabeling = parametricModel.getPlayer1ChoiceLabeling(); + if(parametricModel.hasPlayer2ChoiceLabeling()) player2ChoiceLabeling = parametricModel.getPlayer2ChoiceLabeling(); + this->instantiatedModel = std::make_shared(std::move(player1MatrixCopy), buildDummyMatrix(parametricModel.getTransitionMatrix()), std::move(stateLabelingCopy), buildDummyRewardModels(parametricModel.getRewardModels()), std::move(player1ChoiceLabeling), std::move(player2ChoiceLabeling)); + } + + /*! + * Creates a matrix that has entries at the same position as the given matrix. + * The returned matrix is a stochastic matrix, i.e., the rows sum up to one. + */ + storm::storage::SparseMatrix buildDummyMatrix(storm::storage::SparseMatrix const& parametricMatrix) const; + + /*! + * Creates a copy of the given reward models with the same names and with state(action)rewards / transitionrewards having the same entry-count and entry-positions. + */ + std::unordered_map buildDummyRewardModels(std::unordered_map const& parametricRewardModel) const; + + /*! + * Connects the occurring functions with the corresponding matrix entries + * + * @note constantMatrix and parametricMatrix should have entries at the same positions + * + * @param constantMatrix The matrix to which the evaluation results are written + * @param functions Occurring functions are inserted in this map + * @param mapping The connections of functions to matrix entries are push_backed into this + * @param parametricMatrix the source matrix with the functions to consider. + */ + void initializeMatrixMapping(storm::storage::SparseMatrix& constantMatrix, + std::unordered_map& functions, + std::vector::iterator, ConstantType*>>& mapping, + storm::storage::SparseMatrix const& parametricMatrix) const; + + /*! + * Connects the occurring functions with the corresponding vector entries + * + * @note constantVector and parametricVector should have the same size + * + * @param constantVector The vector to which the evaluation results are written + * @param functions Occurring functions with their placeholders are inserted in this map + * @param mapping The connections of functions to vector entries are push_backed into this + * @param parametricVector the source vector with the functions to consider. + */ + void initializeVectorMapping(std::vector& constantVector, + std::unordered_map& functions, + std::vector::iterator, ConstantType*>>& mapping, + std::vector const& parametricVector) const; + + /// The resulting model + std::shared_ptr instantiatedModel; + /// the occurring functions together with the corresponding placeholders for their evaluated result + std::unordered_map functions; + /// Connection of matrix entries with placeholders + std::vector::iterator, ConstantType*>> matrixMapping; + /// Connection of Vector entries with placeholders + std::vector::iterator, ConstantType*>> vectorMapping; + + + }; + }//Namespace utility +} //namespace storm +#endif /* STORM_UTILITY_MODELINSTANTIATOR_H */ + diff --git a/test/functional/utility/ModelInstantiatorTest.cpp b/test/functional/utility/ModelInstantiatorTest.cpp new file mode 100644 index 000000000..af8f5b8d2 --- /dev/null +++ b/test/functional/utility/ModelInstantiatorTest.cpp @@ -0,0 +1,266 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#ifdef STORM_HAVE_CARL + +#include "src/adapters/CarlAdapter.h" +#include +#include + + +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" + +#include "utility/storm.h" +#include "utility/ModelInstantiator.h" +#include "src/models/sparse/Model.h" +#include "src/models/sparse/Dtmc.h" +#include "src/models/sparse/Mdp.h" + +TEST(ModelInstantiatorTest, Brp_Prob) { + carl::VariablePool::getInstance().clear(); + + std::string const& programFile = STORM_CPP_TESTS_BASE_PATH "/functional/utility/brp16_2.pm"; + std::string const& formulaAsString = "P=? [F s=5 ]"; + std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + // Program and formula + storm::prism::Program program = storm::parseProgram(programFile); + program.checkValidity(); + std::vector> formulas = storm::parseFormulasForProgram(formulaAsString, program); + ASSERT_TRUE(formulas.size()==1); + // Parametric model + typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); + options.addConstantDefinitionsFromString(program, constantsAsString); + options.preserveFormula(*formulas[0]); + std::shared_ptr> dtmc = storm::builder::ExplicitPrismModelBuilder().translateProgram(program, options)->as>(); + + storm::utility::ModelInstantiator, storm::models::sparse::Dtmc> modelInstantiator(*dtmc); + EXPECT_FALSE(dtmc->hasRewardModel()); + + { + std::map valuation; + storm::Variable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL"); + ASSERT_NE(pL, carl::Variable::NO_VARIABLE); + storm::Variable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK"); + ASSERT_NE(pK, carl::Variable::NO_VARIABLE); + valuation.insert(std::make_pair(pL,carl::rationalize(0.8))); + valuation.insert(std::make_pair(pK,carl::rationalize(0.9))); + + storm::models::sparse::Dtmc const& instantiated(modelInstantiator.instantiate(valuation)); + + ASSERT_EQ(dtmc->getTransitionMatrix().getRowGroupIndices(), instantiated.getTransitionMatrix().getRowGroupIndices()); + for(std::size_t rowGroup = 0; rowGroup < dtmc->getTransitionMatrix().getRowGroupCount(); ++rowGroup){ + for(std::size_t row = dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup]; row < dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup+1]; ++row){ + auto instantiatedEntry = instantiated.getTransitionMatrix().getRow(row).begin(); + for(auto const& paramEntry : dtmc->getTransitionMatrix().getRow(row)){ + EXPECT_EQ(paramEntry.getColumn(), instantiatedEntry->getColumn()); + double evaluatedValue = carl::toDouble(paramEntry.getValue().evaluate(valuation)); + EXPECT_EQ(evaluatedValue, instantiatedEntry->getValue()); + ++instantiatedEntry; + } + EXPECT_EQ(instantiated.getTransitionMatrix().getRow(row).end(),instantiatedEntry); + } + } + EXPECT_EQ(dtmc->getStateLabeling(), instantiated.getStateLabeling()); + EXPECT_EQ(dtmc->getOptionalChoiceLabeling(), instantiated.getOptionalChoiceLabeling()); + + storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(instantiated); + std::unique_ptr chkResult = modelchecker.check(*formulas[0]); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeChkResult = chkResult->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(0.2989278941, quantitativeChkResult[*instantiated.getInitialStates().begin()], storm::settings::generalSettings().getPrecision()); + } + + { + std::map valuation; + storm::Variable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL"); + ASSERT_NE(pL, carl::Variable::NO_VARIABLE); + storm::Variable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK"); + ASSERT_NE(pK, carl::Variable::NO_VARIABLE); + valuation.insert(std::make_pair(pL,carl::rationalize(1))); + valuation.insert(std::make_pair(pK,carl::rationalize(1))); + + storm::models::sparse::Dtmc const& instantiated(modelInstantiator.instantiate(valuation)); + + ASSERT_EQ(dtmc->getTransitionMatrix().getRowGroupIndices(), instantiated.getTransitionMatrix().getRowGroupIndices()); + for(std::size_t rowGroup = 0; rowGroup < dtmc->getTransitionMatrix().getRowGroupCount(); ++rowGroup){ + for(std::size_t row = dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup]; row < dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup+1]; ++row){ + auto instantiatedEntry = instantiated.getTransitionMatrix().getRow(row).begin(); + for(auto const& paramEntry : dtmc->getTransitionMatrix().getRow(row)){ + EXPECT_EQ(paramEntry.getColumn(), instantiatedEntry->getColumn()); + double evaluatedValue = carl::toDouble(paramEntry.getValue().evaluate(valuation)); + EXPECT_EQ(evaluatedValue, instantiatedEntry->getValue()); + ++instantiatedEntry; + } + EXPECT_EQ(instantiated.getTransitionMatrix().getRow(row).end(),instantiatedEntry); + } + } + EXPECT_EQ(dtmc->getStateLabeling(), instantiated.getStateLabeling()); + EXPECT_EQ(dtmc->getOptionalChoiceLabeling(), instantiated.getOptionalChoiceLabeling()); + + storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(instantiated); + std::unique_ptr chkResult = modelchecker.check(*formulas[0]); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeChkResult = chkResult->asExplicitQuantitativeCheckResult(); + EXPECT_EQ(0.0 , quantitativeChkResult[*instantiated.getInitialStates().begin()]); + } + + { + std::map valuation; + storm::Variable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL"); + ASSERT_NE(pL, carl::Variable::NO_VARIABLE); + storm::Variable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK"); + ASSERT_NE(pK, carl::Variable::NO_VARIABLE); + valuation.insert(std::make_pair(pL,carl::rationalize(1))); + valuation.insert(std::make_pair(pK,carl::rationalize(0.9))); + + storm::models::sparse::Dtmc const& instantiated(modelInstantiator.instantiate(valuation)); + + ASSERT_EQ(dtmc->getTransitionMatrix().getRowGroupIndices(), instantiated.getTransitionMatrix().getRowGroupIndices()); + for(std::size_t rowGroup = 0; rowGroup < dtmc->getTransitionMatrix().getRowGroupCount(); ++rowGroup){ + for(std::size_t row = dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup]; row < dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup+1]; ++row){ + auto instantiatedEntry = instantiated.getTransitionMatrix().getRow(row).begin(); + for(auto const& paramEntry : dtmc->getTransitionMatrix().getRow(row)){ + EXPECT_EQ(paramEntry.getColumn(), instantiatedEntry->getColumn()); + double evaluatedValue = carl::toDouble(paramEntry.getValue().evaluate(valuation)); + EXPECT_EQ(evaluatedValue, instantiatedEntry->getValue()); + ++instantiatedEntry; + } + EXPECT_EQ(instantiated.getTransitionMatrix().getRow(row).end(),instantiatedEntry); + } + } + EXPECT_EQ(dtmc->getStateLabeling(), instantiated.getStateLabeling()); + EXPECT_EQ(dtmc->getOptionalChoiceLabeling(), instantiated.getOptionalChoiceLabeling()); + + storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(instantiated); + std::unique_ptr chkResult = modelchecker.check(*formulas[0]); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeChkResult = chkResult->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(0.01588055832, quantitativeChkResult[*instantiated.getInitialStates().begin()], storm::settings::generalSettings().getPrecision()); + } +} + +TEST(ModelInstantiatorTest, Brp_Rew) { + carl::VariablePool::getInstance().clear(); + + std::string const& programFile = STORM_CPP_TESTS_BASE_PATH "/functional/utility/brp16_2.pm"; + std::string const& formulaAsString = "R=? [F ((s=5) | (s=0&srep=3)) ]"; + std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + // Program and formula + storm::prism::Program program = storm::parseProgram(programFile); + program.checkValidity(); + std::vector> formulas = storm::parseFormulasForProgram(formulaAsString, program); + ASSERT_TRUE(formulas.size()==1); + // Parametric model + typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); + options.addConstantDefinitionsFromString(program, constantsAsString); + options.preserveFormula(*formulas[0]); + std::shared_ptr> dtmc = storm::builder::ExplicitPrismModelBuilder().translateProgram(program, options)->as>(); + + storm::utility::ModelInstantiator, storm::models::sparse::Dtmc> modelInstantiator(*dtmc); + + { + std::map valuation; + storm::Variable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL"); + ASSERT_NE(pL, carl::Variable::NO_VARIABLE); + storm::Variable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK"); + ASSERT_NE(pK, carl::Variable::NO_VARIABLE); + storm::Variable const& TOMsg = carl::VariablePool::getInstance().findVariableWithName("TOMsg"); + ASSERT_NE(pK, carl::Variable::NO_VARIABLE); + storm::Variable const& TOAck = carl::VariablePool::getInstance().findVariableWithName("TOAck"); + ASSERT_NE(pK, carl::Variable::NO_VARIABLE); + valuation.insert(std::make_pair(pL,carl::rationalize(0.9))); + valuation.insert(std::make_pair(pK,carl::rationalize(0.3))); + valuation.insert(std::make_pair(TOMsg,carl::rationalize(0.3))); + valuation.insert(std::make_pair(TOAck,carl::rationalize(0.5))); + + storm::models::sparse::Dtmc const& instantiated(modelInstantiator.instantiate(valuation)); + + ASSERT_EQ(dtmc->getTransitionMatrix().getRowGroupIndices(), instantiated.getTransitionMatrix().getRowGroupIndices()); + for(std::size_t rowGroup = 0; rowGroup < dtmc->getTransitionMatrix().getRowGroupCount(); ++rowGroup){ + for(std::size_t row = dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup]; row < dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup+1]; ++row){ + auto instantiatedEntry = instantiated.getTransitionMatrix().getRow(row).begin(); + for(auto const& paramEntry : dtmc->getTransitionMatrix().getRow(row)){ + EXPECT_EQ(paramEntry.getColumn(), instantiatedEntry->getColumn()); + double evaluatedValue = carl::toDouble(paramEntry.getValue().evaluate(valuation)); + EXPECT_EQ(evaluatedValue, instantiatedEntry->getValue()); + ++instantiatedEntry; + } + EXPECT_EQ(instantiated.getTransitionMatrix().getRow(row).end(),instantiatedEntry); + } + } + ASSERT_TRUE(instantiated.hasUniqueRewardModel()); + EXPECT_FALSE(instantiated.getUniqueRewardModel()->second.hasStateRewards()); + EXPECT_FALSE(instantiated.getUniqueRewardModel()->second.hasTransitionRewards()); + EXPECT_TRUE(instantiated.getUniqueRewardModel()->second.hasStateActionRewards()); + ASSERT_TRUE(dtmc->getUniqueRewardModel()->second.hasStateActionRewards()); + std::size_t stateActionEntries = dtmc->getUniqueRewardModel()->second.getStateActionRewardVector().size(); + ASSERT_EQ(stateActionEntries, instantiated.getUniqueRewardModel()->second.getStateActionRewardVector().size()); + for(std::size_t i =0; igetUniqueRewardModel()->second.getStateActionRewardVector()[i].evaluate(valuation)); + EXPECT_EQ(evaluatedValue, instantiated.getUniqueRewardModel()->second.getStateActionRewardVector()[i]); + } + EXPECT_EQ(dtmc->getStateLabeling(), instantiated.getStateLabeling()); + EXPECT_EQ(dtmc->getOptionalChoiceLabeling(), instantiated.getOptionalChoiceLabeling()); + + storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(instantiated); + std::unique_ptr chkResult = modelchecker.check(*formulas[0]); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeChkResult = chkResult->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(1.308324495, quantitativeChkResult[*instantiated.getInitialStates().begin()], storm::settings::generalSettings().getPrecision()); + } + +} + + +TEST(ModelInstantiatorTest, consensus) { + carl::VariablePool::getInstance().clear(); + + std::string const& programFile = STORM_CPP_TESTS_BASE_PATH "/functional/utility/coin2_2.pm"; + std::string const& formulaAsString = "Pmin=? [F \"finished\"&\"all_coins_equal_1\" ]"; + std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + // Program and formula + storm::prism::Program program = storm::parseProgram(programFile); + program.checkValidity(); + std::vector> formulas = storm::parseFormulasForProgram(formulaAsString, program); + ASSERT_TRUE(formulas.size()==1); + // Parametric model + typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); + options.addConstantDefinitionsFromString(program, constantsAsString); + options.preserveFormula(*formulas[0]); + std::shared_ptr> mdp = storm::builder::ExplicitPrismModelBuilder().translateProgram(program, options)->as>(); + + storm::utility::ModelInstantiator, storm::models::sparse::Mdp> modelInstantiator(*mdp); + + std::map valuation; + storm::Variable const& p1 = carl::VariablePool::getInstance().findVariableWithName("p1"); + ASSERT_NE(p1, carl::Variable::NO_VARIABLE); + storm::Variable const& p2 = carl::VariablePool::getInstance().findVariableWithName("p2"); + ASSERT_NE(p2, carl::Variable::NO_VARIABLE); + valuation.insert(std::make_pair(p1,carl::rationalize(0.51))); + valuation.insert(std::make_pair(p2,carl::rationalize(0.49))); + storm::models::sparse::Mdp const& instantiated(modelInstantiator.instantiate(valuation)); + + ASSERT_EQ(mdp->getTransitionMatrix().getRowGroupIndices(), instantiated.getTransitionMatrix().getRowGroupIndices()); + for(std::size_t rowGroup = 0; rowGroup < mdp->getTransitionMatrix().getRowGroupCount(); ++rowGroup){ + for(std::size_t row = mdp->getTransitionMatrix().getRowGroupIndices()[rowGroup]; row < mdp->getTransitionMatrix().getRowGroupIndices()[rowGroup+1]; ++row){ + auto instantiatedEntry = instantiated.getTransitionMatrix().getRow(row).begin(); + for(auto const& paramEntry : mdp->getTransitionMatrix().getRow(row)){ + EXPECT_EQ(paramEntry.getColumn(), instantiatedEntry->getColumn()); + double evaluatedValue = carl::toDouble(paramEntry.getValue().evaluate(valuation)); + EXPECT_EQ(evaluatedValue, instantiatedEntry->getValue()); + ++instantiatedEntry; + } + EXPECT_EQ(instantiated.getTransitionMatrix().getRow(row).end(),instantiatedEntry); + } + } + EXPECT_EQ(mdp->getStateLabeling(), instantiated.getStateLabeling()); + EXPECT_EQ(mdp->getOptionalChoiceLabeling(), instantiated.getOptionalChoiceLabeling()); + + storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(instantiated); + std::unique_ptr chkResult = modelchecker.check(*formulas[0]); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeChkResult = chkResult->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(0.3526577219, quantitativeChkResult[*instantiated.getInitialStates().begin()], storm::settings::generalSettings().getPrecision()); + +} + +#endif \ No newline at end of file diff --git a/test/functional/utility/brp16_2.pm b/test/functional/utility/brp16_2.pm new file mode 100644 index 000000000..d756a90ec --- /dev/null +++ b/test/functional/utility/brp16_2.pm @@ -0,0 +1,146 @@ +// bounded retransmission protocol [D'AJJL01] +// gxn/dxp 23/05/2001 + +dtmc + +// number of chunks +const int N = 16; +// maximum number of retransmissions +const int MAX = 2; + +// reliability of channels +const double pL; +const double pK; + +// timeouts +const double TOMsg; +const double TOAck; + +module sender + + s : [0..6]; + // 0 idle + // 1 next_frame + // 2 wait_ack + // 3 retransmit + // 4 success + // 5 error + // 6 wait sync + srep : [0..3]; + // 0 bottom + // 1 not ok (nok) + // 2 do not know (dk) + // 3 ok (ok) + nrtr : [0..MAX]; + i : [0..N]; + bs : bool; + s_ab : bool; + fs : bool; + ls : bool; + + // idle + [NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0); + // next_frame + [aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0); + // wait_ack + [aB] (s=2) -> (s'=4) & (s_ab'=!s_ab); + [TO_Msg] (s=2) -> (s'=3); + [TO_Ack] (s=2) -> (s'=3); + // retransmit + [aF] (s=3) & (nrtr (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); + [] (s=3) & (nrtr=MAX) & (i (s'=5) & (srep'=1); + [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); + // success + [] (s=4) & (i (s'=1) & (i'=i+1); + [] (s=4) & (i=N) -> (s'=0) & (srep'=3); + // error + [SyncWait] (s=5) -> (s'=6); + // wait sync + [SyncWait] (s=6) -> (s'=0) & (s_ab'=false); + +endmodule + +module receiver + + r : [0..5]; + // 0 new_file + // 1 fst_safe + // 2 frame_received + // 3 frame_reported + // 4 idle + // 5 resync + rrep : [0..4]; + // 0 bottom + // 1 fst + // 2 inc + // 3 ok + // 4 nok + fr : bool; + lr : bool; + br : bool; + r_ab : bool; + recv : bool; + + + // new_file + [SyncWait] (r=0) -> (r'=0); + [aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); + // fst_safe_frame + [] (r=1) -> (r'=2) & (r_ab'=br); + // frame_received + [] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1); + [] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2); + [] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3); + [aA] (r=2) & !(r_ab=br) -> (r'=4); + // frame_reported + [aA] (r=3) -> (r'=4) & (r_ab'=!r_ab); + // idle + [aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); + [SyncWait] (r=4) & (ls=true) -> (r'=5); + [SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4); + // resync + [SyncWait] (r=5) -> (r'=0) & (rrep'=0); + +endmodule + +// prevents more than one file being sent +module tester + + T : bool; + + [NewFile] (T=false) -> (T'=true); + +endmodule + +module channelK + + k : [0..2]; + + // idle + [aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2); + // sending + [aG] (k=1) -> (k'=0); + // lost + [TO_Msg] (k=2) -> (k'=0); + +endmodule + +module channelL + + l : [0..2]; + + // idle + [aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2); + // sending + [aB] (l=1) -> (l'=0); + // lost + [TO_Ack] (l=2) -> (l'=0); + +endmodule + +rewards + [TO_Msg] true : TOMsg; + [TO_Ack] true : TOAck; +endrewards + + diff --git a/test/functional/utility/coin2_2.pm b/test/functional/utility/coin2_2.pm new file mode 100644 index 000000000..3f5358cdd --- /dev/null +++ b/test/functional/utility/coin2_2.pm @@ -0,0 +1,56 @@ +//Randomised Consensus Protocol + +mdp +const double p1; // in [0.2 , 0.8] +const double p2; // in [0.2 , 0.8] + + +const int N=2; +const int K=2; +const int range = 2*(K+1)*N; +const int counter_init = (K+1)*N; +const int left = N; +const int right = 2*(K+1)*N - N; + +// shared coin +global counter : [0..range] init counter_init; + +module process1 + + // program counter + pc1 : [0..3]; + // 0 - flip + // 1 - write + // 2 - check + // 3 - finished + + // local coin + coin1 : [0..1]; + + // flip coin + [] (pc1=0) -> p1 : (coin1'=0) & (pc1'=1) + 1 - p1 : (coin1'=1) & (pc1'=1); + // write tails -1 (reset coin to add regularity) + [] (pc1=1) & (coin1=0) & (counter>0) -> (counter'=counter-1) & (pc1'=2) & (coin1'=0); + // write heads +1 (reset coin to add regularity) + [] (pc1=1) & (coin1=1) & (counter (counter'=counter+1) & (pc1'=2) & (coin1'=0); + // check + // decide tails + [] (pc1=2) & (counter<=left) -> (pc1'=3) & (coin1'=0); + // decide heads + [] (pc1=2) & (counter>=right) -> (pc1'=3) & (coin1'=1); + // flip again + [] (pc1=2) & (counter>left) & (counter (pc1'=0); + // loop (all loop together when done) + [done] (pc1=3) -> (pc1'=3); + +endmodule + +module process2 = process1[pc1=pc2,coin1=coin2,p1=p2] endmodule +label "finished" = pc1=3 &pc2=3 ; +label "all_coins_equal_1" = coin1=1 &coin2=1 ; +rewards "steps" + true : 1; +endrewards + + +