Merge branch 'future' into variance_properties

Former-commit-id: 13fe1e8531

src/models/sparse/MarkovAutomaton.cpp

@@ -55,6 +55,11 @@ namespace storm {
                 return this->exitRates;
             }
             
+            template <typename ValueType, typename RewardModelType>
+            std::vector<ValueType>& MarkovAutomaton<ValueType, RewardModelType>::getExitRates() {
+                return this->exitRates;
+            }
+            
             template <typename ValueType, typename RewardModelType>
             ValueType const& MarkovAutomaton<ValueType, RewardModelType>::getExitRate(storm::storage::sparse::state_type state) const {
                 return this->exitRates[state];

src/models/sparse/MarkovAutomaton.h

@@ -94,6 +94,13 @@ namespace storm {
                  */
                 std::vector<ValueType> const& getExitRates() const;
                 
+                /*!
+                 * Retrieves the vector representing the exit rates of the states.
+                 *
+                 * @return The exit rate vector of the model.
+                 */
+                std::vector<ValueType>& getExitRates();
+                
                 /*!
                  * Retrieves the exit rate of the given state.
                  *

src/models/sparse/Model.h

@@ -140,6 +140,21 @@ namespace storm {
                  */
                 storm::storage::SparseMatrix<ValueType>& getTransitionMatrix();
 
+                
+                /*!
+                 * Retrieves the reward models.
+                 *
+                 * @return A mapping from reward model names to the reward models.
+                 */
+                std::unordered_map<std::string, RewardModelType> const& getRewardModels() const;
+                
+                /*!
+                 * Retrieves the reward models.
+                 *
+                 * @return A mapping from reward model names to the reward models.
+                 */
+                std::unordered_map<std::string, RewardModelType>& 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<std::string, RewardModelType> const& getRewardModels() const;
-                
-                /*!
-                 * Retrieves the reward models.
-                 *
-                 * @return A mapping from reward model names to the reward models.
-                 */
-                std::unordered_map<std::string, RewardModelType>& getRewardModels();
-                
             private:
                 //  A matrix representing transition relation.
                 storm::storage::SparseMatrix<ValueType> transitionMatrix;

src/models/sparse/StochasticTwoPlayerGame.cpp

@@ -65,7 +65,7 @@ namespace storm {
 //            template class StochasticTwoPlayerGame<float>;
             
 #ifdef STORM_HAVE_CARL
-//            template class StochasticTwoPlayerGame<storm::RationalFunction>;
+            template class StochasticTwoPlayerGame<storm::RationalFunction>;
 #endif
             
         } // namespace sparse

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<typename ParametricSparseModelType, typename ConstantSparseModelType>
+            ModelInstantiator<ParametricSparseModelType, ConstantSparseModelType>::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<typename ParametricSparseModelType, typename ConstantType>
+            ModelInstantiator<ParametricSparseModelType, ConstantType>::~ModelInstantiator() {
+                //Intentionally left empty
+            }
+            
+            template<typename ParametricSparseModelType, typename ConstantSparseModelType>
+            storm::storage::SparseMatrix<typename ConstantSparseModelType::ValueType> ModelInstantiator<ParametricSparseModelType, ConstantSparseModelType>::buildDummyMatrix(storm::storage::SparseMatrix<ParametricType> const& parametricMatrix) const{
+                storm::storage::SparseMatrixBuilder<ConstantType> 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<ConstantType>();
+                        for(auto const& paramEntry : parametricMatrix.getRow(row)){
+                            matrixBuilder.addNextValue(row, paramEntry.getColumn(), dummyValue);
+                            dummyValue = storm::utility::zero<ConstantType>();
+                        }
+                    }
+                }
+                return matrixBuilder.build();
+            }
+            
+            template<typename ParametricSparseModelType, typename ConstantSparseModelType>
+            std::unordered_map<std::string, typename ConstantSparseModelType::RewardModelType> ModelInstantiator<ParametricSparseModelType, ConstantSparseModelType>::buildDummyRewardModels(std::unordered_map<std::string, typename ParametricSparseModelType::RewardModelType> const& parametricRewardModel) const {
+                std::unordered_map<std::string, typename ConstantSparseModelType::RewardModelType> result;
+                for(auto const& paramRewardModel : parametricRewardModel){
+                    auto const& rewModel = paramRewardModel.second;
+                    boost::optional<std::vector<ConstantType>> optionalStateRewardVector;
+                    if(rewModel.hasStateRewards()) {
+                        optionalStateRewardVector = std::vector<ConstantType>(rewModel.getStateRewardVector().size());
+                    }
+                    boost::optional<std::vector<ConstantType>> optionalStateActionRewardVector;
+                    if(rewModel.hasStateActionRewards()) {
+                        optionalStateActionRewardVector = std::vector<ConstantType>(rewModel.getStateActionRewardVector().size());
+                    }
+                    boost::optional<storm::storage::SparseMatrix<ConstantType>> optionalTransitionRewardMatrix;
+                    if(rewModel.hasTransitionRewards()) {
+                        optionalTransitionRewardMatrix = buildDummyMatrix(rewModel.getTransitionRewardMatrix());
+                    }
+                    result.insert(std::make_pair(paramRewardModel.first, 
+                                                 storm::models::sparse::StandardRewardModel<ConstantType>(std::move(optionalStateRewardVector), std::move(optionalStateActionRewardVector), std::move(optionalTransitionRewardMatrix))
+                                                ));
+                }
+                return result;
+            }
+            
+            template<typename ParametricSparseModelType, typename ConstantSparseModelType>
+            void ModelInstantiator<ParametricSparseModelType, ConstantSparseModelType>::initializeMatrixMapping(storm::storage::SparseMatrix<ConstantType>& constantMatrix,
+                                             std::unordered_map<ParametricType, ConstantType>& functions,
+                                             std::vector<std::pair<typename storm::storage::SparseMatrix<ConstantType>::iterator, ConstantType*>>& mapping,
+                                             storm::storage::SparseMatrix<ParametricType> const& parametricMatrix) const{
+                ConstantType dummyValue = storm::utility::one<ConstantType>();
+                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<ConstantType>(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<typename ParametricSparseModelType, typename ConstantSparseModelType>
+            void ModelInstantiator<ParametricSparseModelType, ConstantSparseModelType>::initializeVectorMapping(std::vector<ConstantType>& constantVector,
+                                             std::unordered_map<ParametricType, ConstantType>& functions,
+                                             std::vector<std::pair<typename std::vector<ConstantType>::iterator, ConstantType*>>& mapping,
+                                             std::vector<ParametricType> const& parametricVector) const{
+                ConstantType dummyValue = storm::utility::one<ConstantType>();
+                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<ConstantType>(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<typename ParametricSparseModelType, typename ConstantSparseModelType>
+            ConstantSparseModelType const& ModelInstantiator<ParametricSparseModelType, ConstantSparseModelType>::instantiate(std::map<VariableType, CoefficientType>const& valuation){
+                //Write results into the placeholders
+                for(auto& functionResult : this->functions){
+                    functionResult.second=storm::utility::convertNumber<ConstantType>(
+                            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<storm::RationalFunction>, storm::models::sparse::Dtmc<double>>;
+            template class ModelInstantiator<storm::models::sparse::Mdp<storm::RationalFunction>, storm::models::sparse::Mdp<double>>;
+            template class ModelInstantiator<storm::models::sparse::Ctmc<storm::RationalFunction>, storm::models::sparse::Ctmc<double>>;
+            template class ModelInstantiator<storm::models::sparse::MarkovAutomaton<storm::RationalFunction>, storm::models::sparse::MarkovAutomaton<double>>;
+            template class ModelInstantiator<storm::models::sparse::StochasticTwoPlayerGame<storm::RationalFunction>, storm::models::sparse::StochasticTwoPlayerGame<double>>;
+#endif
+    } //namespace utility
+} //namespace storm

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 <unordered_map>
+#include <memory>
+#include <type_traits>
+
+#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<typename ParametricSparseModelType, typename ConstantSparseModelType>
+            class ModelInstantiator {
+            public:
+                typedef typename ParametricSparseModelType::ValueType ParametricType;
+                typedef typename storm::utility::parametric::VariableType<ParametricType>::type VariableType;
+                typedef typename storm::utility::parametric::CoefficientType<ParametricType>::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::map<VariableType, CoefficientType>const& 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 PMT = ParametricSparseModelType>
+                typename std::enable_if<
+                            std::is_same<PMT,storm::models::sparse::Dtmc<typename ParametricSparseModelType::ValueType>>::value ||
+                            std::is_same<PMT,storm::models::sparse::Mdp<typename ParametricSparseModelType::ValueType>>::value ||
+                            std::is_same<PMT,storm::models::sparse::Ctmc<typename ParametricSparseModelType::ValueType>>::value
+                >::type
+                initializeModelSpecificData(PMT const& parametricModel) {
+                    auto stateLabelingCopy = parametricModel.getStateLabeling();
+                    auto choiceLabelingCopy = parametricModel.getOptionalChoiceLabeling();
+                    this->instantiatedModel = std::make_shared<ConstantSparseModelType>(buildDummyMatrix(parametricModel.getTransitionMatrix()), std::move(stateLabelingCopy), buildDummyRewardModels(parametricModel.getRewardModels()), std::move(choiceLabelingCopy));
+                }
+                
+                template<typename PMT = ParametricSparseModelType>
+                typename std::enable_if<
+                            std::is_same<PMT,storm::models::sparse::MarkovAutomaton<typename ParametricSparseModelType::ValueType>>::value
+                >::type
+                initializeModelSpecificData(PMT const& parametricModel) {
+                    auto stateLabelingCopy = parametricModel.getStateLabeling();
+                    auto markovianStatesCopy = parametricModel.getMarkovianStates();
+                    auto choiceLabelingCopy = parametricModel.getOptionalChoiceLabeling();
+                    std::vector<ConstantType> exitRates(parametricModel.getExitRates().size(), storm::utility::one<ConstantType>());
+                    this->instantiatedModel = std::make_shared<ConstantSparseModelType>(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 PMT = ParametricSparseModelType>
+                typename std::enable_if<
+                            std::is_same<PMT,storm::models::sparse::StochasticTwoPlayerGame<typename ParametricSparseModelType::ValueType>>::value
+                >::type
+                initializeModelSpecificData(PMT const& parametricModel) {
+                    auto player1MatrixCopy = parametricModel.getPlayer1Matrix();
+                    auto stateLabelingCopy = parametricModel.getStateLabeling();
+                    boost::optional<std::vector<typename storm::models::sparse::LabelSet>> player1ChoiceLabeling, player2ChoiceLabeling;
+                    if(parametricModel.hasPlayer1ChoiceLabeling()) player1ChoiceLabeling = parametricModel.getPlayer1ChoiceLabeling();
+                    if(parametricModel.hasPlayer2ChoiceLabeling()) player2ChoiceLabeling = parametricModel.getPlayer2ChoiceLabeling();
+                    this->instantiatedModel = std::make_shared<ConstantSparseModelType>(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<ConstantType> buildDummyMatrix(storm::storage::SparseMatrix<ParametricType> 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<std::string, typename ConstantSparseModelType::RewardModelType> buildDummyRewardModels(std::unordered_map<std::string, typename ParametricSparseModelType::RewardModelType> 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<ConstantType>& constantMatrix,
+                                             std::unordered_map<ParametricType, ConstantType>& functions,
+                                             std::vector<std::pair<typename storm::storage::SparseMatrix<ConstantType>::iterator, ConstantType*>>& mapping,
+                                             storm::storage::SparseMatrix<ParametricType> 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<ConstantType>& constantVector,
+                                             std::unordered_map<ParametricType, ConstantType>& functions,
+                                             std::vector<std::pair<typename std::vector<ConstantType>::iterator, ConstantType*>>& mapping,
+                                             std::vector<ParametricType> const& parametricVector) const;
+                
+                /// The resulting model
+                std::shared_ptr<ConstantSparseModelType> instantiatedModel;
+                /// the occurring functions together with the corresponding placeholders for their evaluated result
+                std::unordered_map<ParametricType, ConstantType> functions; 
+                /// Connection of matrix entries with placeholders
+                std::vector<std::pair<typename storm::storage::SparseMatrix<ConstantType>::iterator, ConstantType*>> matrixMapping; 
+                /// Connection of Vector entries with placeholders
+                std::vector<std::pair<typename std::vector<ConstantType>::iterator, ConstantType*>> vectorMapping; 
+                
+                
+            };
+    }//Namespace utility
+} //namespace storm
+#endif	/* STORM_UTILITY_MODELINSTANTIATOR_H */
+

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<typename ValueType>
 		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<RationalNumber>(number);
+        }
+
 #endif
         
         template<typename IndexType, typename ValueType>
@@ -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);

src/utility/constants.h

@@ -50,6 +50,9 @@ namespace storm {
 
         template<typename IndexType, typename ValueType>
         storm::storage::MatrixEntry<IndexType, ValueType>&& simplify(storm::storage::MatrixEntry<IndexType, ValueType>&& matrixEntry);
+        
+        template<typename TargetType, typename SourceType>
+        TargetType convertNumber(SourceType const& number);
     }
 }
 

src/utility/parametric.cpp

@@ -0,0 +1,39 @@
+/* 
+ * File:   parametric.cpp
+ * Author: Tim Quatmann
+ * 
+ * Created by Tim Quatmann on 08/03/16.
+ */
+
+#include <string>
+
+#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<carl/numbers/numbers.h>
+#include<carl/core/VariablePool.h>
+#endif
+
+namespace storm {
+    namespace utility{
+        namespace parametric {
+            
+#ifdef STORM_HAVE_CARL
+            template<>
+            typename CoefficientType<storm::RationalFunction>::type evaluate<storm::RationalFunction>(storm::RationalFunction const& function, std::map<typename VariableType<storm::RationalFunction>::type, typename CoefficientType<storm::RationalFunction>::type> const& valuation){
+                return function.evaluate(valuation);
+            }
+            
+            template<>
+            typename CoefficientType<storm::RationalFunction>::type getConstantPart<storm::RationalFunction>(storm::RationalFunction const& function){
+                return function.constantPart();
+            }
+#endif
+        }
+    }
+}

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<typename FunctionType>
+            struct VariableType { typedef void type; };
+            /*!
+             * Acess the type of coefficients from a given function type
+             */
+            template<typename FunctionType>
+            struct CoefficientType { typedef void type; };
+            
+#ifdef STORM_HAVE_CARL
+            template<>
+            struct VariableType<storm::RationalFunction> { typedef storm::Variable type; };
+            template<>
+            struct CoefficientType<storm::RationalFunction> { typedef storm::RationalNumber type; };
+#endif
+            
+            /*!
+             * Evaluates the given function wrt. the given valuation
+             */
+            template<typename FunctionType>
+            typename CoefficientType<FunctionType>::type evaluate(FunctionType const& function, std::map<typename VariableType<FunctionType>::type, typename CoefficientType<FunctionType>::type> const& valuation);
+            
+            /*!
+             * Retrieves the constant part of the given function.
+             */
+            template<typename FunctionType>
+            typename CoefficientType<FunctionType>::type getConstantPart(FunctionType const& function);
+
+        }
+        
+    }
+}
+
+
+#endif /* STORM_UTILITY_PARAMETRIC_H */

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<carl/numbers/numbers.h>
+#include<carl/core/VariablePool.h>
+
+
+#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<std::shared_ptr<storm::logic::Formula>> formulas = storm::parseFormulasForProgram(formulaAsString, program);
+    ASSERT_TRUE(formulas.size()==1);
+    // Parametric model
+    typename storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options options = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options(*formulas[0]);
+    options.addConstantDefinitionsFromString(program, constantsAsString); 
+    options.preserveFormula(*formulas[0]);
+    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>().translateProgram(program, options)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
+    
+    storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::models::sparse::Dtmc<double>> modelInstantiator(*dtmc);
+    EXPECT_FALSE(dtmc->hasRewardModel());
+    
+    {
+        std::map<storm::Variable, storm::RationalNumber> 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<storm::RationalNumber>(0.8)));
+        valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(0.9)));
+
+        storm::models::sparse::Dtmc<double> 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<storm::models::sparse::Dtmc<double>> modelchecker(instantiated);
+        std::unique_ptr<storm::modelchecker::CheckResult> chkResult = modelchecker.check(*formulas[0]);
+        storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeChkResult = chkResult->asExplicitQuantitativeCheckResult<double>();
+        EXPECT_NEAR(0.2989278941, quantitativeChkResult[*instantiated.getInitialStates().begin()], storm::settings::generalSettings().getPrecision());
+    }
+    
+    {
+        std::map<storm::Variable, storm::RationalNumber> 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<storm::RationalNumber>(1)));
+        valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(1)));
+
+        storm::models::sparse::Dtmc<double> 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<storm::models::sparse::Dtmc<double>> modelchecker(instantiated);
+        std::unique_ptr<storm::modelchecker::CheckResult> chkResult = modelchecker.check(*formulas[0]);
+        storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeChkResult = chkResult->asExplicitQuantitativeCheckResult<double>();
+        EXPECT_EQ(0.0 , quantitativeChkResult[*instantiated.getInitialStates().begin()]);
+    }
+    
+    {
+        std::map<storm::Variable, storm::RationalNumber> 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<storm::RationalNumber>(1)));
+        valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(0.9)));
+
+        storm::models::sparse::Dtmc<double> 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<storm::models::sparse::Dtmc<double>> modelchecker(instantiated);
+        std::unique_ptr<storm::modelchecker::CheckResult> chkResult = modelchecker.check(*formulas[0]);
+        storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeChkResult = chkResult->asExplicitQuantitativeCheckResult<double>();
+        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<std::shared_ptr<storm::logic::Formula>> formulas = storm::parseFormulasForProgram(formulaAsString, program);
+    ASSERT_TRUE(formulas.size()==1);
+    // Parametric model
+    typename storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options options = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options(*formulas[0]);
+    options.addConstantDefinitionsFromString(program, constantsAsString); 
+    options.preserveFormula(*formulas[0]);
+    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>().translateProgram(program, options)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
+
+    storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::models::sparse::Dtmc<double>> modelInstantiator(*dtmc);
+    
+    {
+        std::map<storm::Variable, storm::RationalNumber> 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<storm::RationalNumber>(0.9)));
+        valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(0.3)));
+        valuation.insert(std::make_pair(TOMsg,carl::rationalize<storm::RationalNumber>(0.3)));
+        valuation.insert(std::make_pair(TOAck,carl::rationalize<storm::RationalNumber>(0.5)));
+
+        storm::models::sparse::Dtmc<double> 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; i<stateActionEntries; ++i){
+            double evaluatedValue = carl::toDouble(dtmc->getUniqueRewardModel()->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<storm::models::sparse::Dtmc<double>> modelchecker(instantiated);
+        std::unique_ptr<storm::modelchecker::CheckResult> chkResult = modelchecker.check(*formulas[0]);
+        storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeChkResult = chkResult->asExplicitQuantitativeCheckResult<double>();
+        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<std::shared_ptr<storm::logic::Formula>> formulas = storm::parseFormulasForProgram(formulaAsString, program);
+    ASSERT_TRUE(formulas.size()==1);
+    // Parametric model
+    typename storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options options = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options(*formulas[0]);
+    options.addConstantDefinitionsFromString(program, constantsAsString); 
+    options.preserveFormula(*formulas[0]);
+    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> mdp = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>().translateProgram(program, options)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
+
+    storm::utility::ModelInstantiator<storm::models::sparse::Mdp<storm::RationalFunction>, storm::models::sparse::Mdp<double>> modelInstantiator(*mdp);
+    
+    std::map<storm::Variable, storm::RationalNumber> 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<storm::RationalNumber>(0.51)));
+    valuation.insert(std::make_pair(p2,carl::rationalize<storm::RationalNumber>(0.49)));
+    storm::models::sparse::Mdp<double> 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<storm::models::sparse::Mdp<double>> modelchecker(instantiated);
+    std::unique_ptr<storm::modelchecker::CheckResult> chkResult = modelchecker.check(*formulas[0]);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeChkResult = chkResult->asExplicitQuantitativeCheckResult<double>();
+    EXPECT_NEAR(0.3526577219, quantitativeChkResult[*instantiated.getInitialStates().begin()], storm::settings::generalSettings().getPrecision());
+    
+}
+
+#endif

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<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1);
+    [] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1);
+    [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2);
+    // success
+    [] (s=4) & (i<N) -> (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
+
+

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<range) -> (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<right) -> (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
+
+
+