First try

src/storm-pars-cli/storm-pars.cpp

@@ -3,6 +3,8 @@
 #include "storm-pars/settings/ParsSettings.h"
 #include "storm-pars/settings/modules/ParametricSettings.h"
 #include "storm-pars/settings/modules/RegionSettings.h"
+#include "storm-pars/analysis/Lattice.h"
+#include "storm-pars/analysis/Transformer.h"
 
 #include "storm/settings/SettingsManager.h"
 #include "storm/api/storm.h"
@@ -455,7 +457,9 @@ namespace storm {
             }
             
             STORM_LOG_THROW(model || input.properties.empty(), storm::exceptions::InvalidSettingsException, "No input model.");
-            
+
+            // TODO: Shift this to after preprocessing?
+
             if (model) {
                 auto preprocessingResult = storm::pars::preprocessModel<DdType, ValueType>(model, input);
                 if (preprocessingResult.second) {
@@ -463,7 +467,40 @@ namespace storm {
                     model->printModelInformationToStream(std::cout);
                 }
             }
-            
+
+
+            if (parSettings.isMonotonicityAnalysisSet()) {
+                // Do something more fancy.
+                std::cout << "Hello, Jip" << std::endl;
+                std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
+
+                storm::storage::SparseMatrix<ValueType> matrix = sparseModel.get()->getTransitionMatrix();
+
+                storm::storage::BitVector initialStates = sparseModel.get()->getInitialStates();
+
+                std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(input.properties);
+
+                STORM_LOG_THROW((*(formulas[0])).isProbabilityOperatorFormula() && (*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula(), storm::exceptions::NotSupportedException, "Expecting until formula");
+                // Check that formulas[0] is actually a ProbabilityOperator ...
+                // Check that formulas[0]->asProbabilityOperator().subformula() is an EventuallyFormula..
+                // Compute phiStates, psiStates via formulas[0]....subformula().as..().subformula
+                storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<ValueType>> propositionalChecker(*sparseModel);
+                storm::storage::BitVector phiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
+                storm::storage::BitVector psiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); //right
+                // get the maybeStates
+                std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(sparseModel.get()->getBackwardTransitions(), phiStates, psiStates);
+
+                model.get()->printModelInformationToStream(std::cout);
+
+                storm::storage::BitVector topStates = statesWithProbability01.second;
+                storm::storage::BitVector bottomStates = statesWithProbability01.first;
+                storm::analysis::Lattice* lattice = storm::analysis::Transformer::toLattice(matrix, initialStates, topStates, bottomStates, sparseModel.get()->getNumberOfStates());
+                lattice->toString(std::cout);
+                return;
+            }
+
+
+
             std::vector<storm::storage::ParameterRegion<ValueType>> regions = parseRegions<ValueType>(model);
             std::string samplesAsString = parSettings.getSamples();
             SampleInformation<ValueType> samples;

src/storm-pars/analysis/Lattice.cpp

@@ -0,0 +1,171 @@
+//
+// Created by Jip Spel on 24.07.18.
+//
+
+#include <iostream>
+#include "Lattice.h"
+namespace storm {
+    namespace analysis {
+        Lattice::Lattice(Node *topNode, Node *bottomNode, uint_fast64_t numberOfStates) {
+            Node *top = new Node();
+            top->states = topNode->states;
+            Node *bottom = new Node();
+            bottom->states = bottomNode->states;
+            top->below.push_back(bottom);
+            bottom->above.push_back(top);
+            nodes = std::vector<Node *>({top, bottom});
+//            addedStates.insert(addedStates.end(), top->states.begin(), top->states.end());
+//            addedStates.insert(addedStates.end(), bottom->states.begin(), bottom->states.end());
+            this->numberOfStates = numberOfStates;
+        }
+
+        void Lattice::addBetween(uint_fast64_t state, Node *above, Node *below) {
+            Node *newNode = new Node();
+            newNode->states = storm::storage::BitVector(numberOfStates);
+            newNode->states.set(state);
+            newNode->above = std::vector<Node *>({above});
+            newNode->below = std::vector<Node *>({below});
+            remove(&(below->above), above);
+            remove(&(above->below), below);
+            (below->above).push_back(newNode);
+            above->below.push_back(newNode);
+            nodes.push_back(newNode);
+//            addedStates.push_back(state);
+        }
+
+        void Lattice::addToNode(uint_fast64_t state, Node *node) {
+            node->states.set(state);
+//            addedStates.push_back(state);
+        }
+
+        int Lattice::compare(uint_fast64_t state1, uint_fast64_t state2) {
+            Node *node1 = getNode(state1);
+            Node *node2 = getNode(state2);
+
+            if (node1 == node2) {
+                return 0;
+            }
+
+            if (above(node1, node2)) {
+                return 1;
+            }
+
+            if (below(node1, node2)) {
+                return 2;
+            }
+
+            return -1;
+        }
+
+        Lattice::Node *Lattice::getNode(uint_fast64_t stateNumber) {
+            Node *node;
+            for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) {
+                storm::storage::BitVector states = (*itr)->states;
+
+                if (states[stateNumber]) return (*itr);
+            }
+            return node;
+        }
+
+        void Lattice::toString(std::ostream &out) {
+            for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) {
+                Node *node = *itr;
+                out << "Node: {";
+                uint_fast64_t index = node->states.getNextSetIndex(0);
+                while (index < numberOfStates) {
+                    out << index;
+                    index = node->states.getNextSetIndex(index+1);
+                    if (index < numberOfStates) {
+                        out << ", ";
+                    }
+                }
+                out << "}" << std::endl;
+                out << "  Address: " << node << std::endl;
+                out << "    Above: {";
+                for (auto itr2 = node->above.begin(); itr2 != node->above.end(); ++itr2) {
+                    Node *above = *itr2;
+                    out << "{";
+                    index = above->states.getNextSetIndex(0);
+                    while (index < numberOfStates) {
+                        out << index;
+                        index = above->states.getNextSetIndex(index+1);
+                        if (index < numberOfStates) {
+                            out << ", ";
+                        }
+                    }
+
+                    out << "}";
+                    if (itr2 + 1 != node->above.end()) {
+                        out << ", ";
+                    }
+                }
+                out << "}" << std::endl;
+
+                out << "    Below: {";
+                for (auto itr2 = node->below.begin(); itr2 != node->below.end(); ++itr2) {
+                    Node *below = *itr2;
+                    out << "{";
+                    index = below->states.getNextSetIndex(0);
+                    while (index < numberOfStates) {
+                        out << index;
+                        index = below->states.getNextSetIndex(index+1);
+                        if (index < numberOfStates) {
+                            out << ", ";
+                        }
+                    }
+
+                    out << "}";
+                    if (itr2 + 1 != node->below.end()) {
+                        out << ", ";
+                    }
+                }
+                out << "}" << std::endl;
+            }
+        }
+
+        bool Lattice::above(Node *node1, Node *node2) {
+            if (node1->below.empty()) {
+                return false;
+            }
+
+            if (std::find(node1->below.begin(), node1->below.end(), node2) != node1->below.end()) {
+                return true;
+            }
+
+            bool result = false;
+            for (auto itr = node1->below.begin(); node1->below.end() != itr; ++itr) {
+                result |= above(*itr, node2);
+            }
+            return result;
+        }
+
+        bool Lattice::below(Node *node1, Node *node2) {
+            if (node1->above.empty()) {
+                return false;
+            }
+
+            if (std::find(node1->above.begin(), node1->above.end(), node2) != node1->above.end()) {
+                return true;
+            }
+
+            bool result = false;
+            for (auto itr = node1->above.begin(); node1->above.end() != itr; ++itr) {
+                result |= below(*itr, node2);
+            }
+            return result;
+        }
+
+        void Lattice::remove(std::vector<Node *> *nodes, Node *node) {
+            auto index = std::find(nodes->begin(), nodes->end(), node);
+            if (index != nodes->end()) {
+                nodes->erase(index);
+            }
+        };
+
+        void Lattice::setStates(std::vector<uint_fast64_t> states, Node *node) {
+            for (auto itr = states.begin(); itr < states.end(); ++itr) {
+                node->states.set(*itr);
+            }
+        }
+    }
+}

src/storm-pars/analysis/Lattice.h

@@ -0,0 +1,94 @@
+//
+// Created by Jip Spel on 24.07.18.
+//
+
+#ifndef LATTICE_LATTICE_H
+#define LATTICE_LATTICE_H
+
+#include <iostream>
+#include <vector>
+
+#include "storm/storage/BitVector.h"
+
+namespace storm {
+            namespace analysis {
+                class Lattice {
+
+                public:
+                    struct Node {
+                        storm::storage::BitVector states;
+                        std::vector<Node *> above;
+                        std::vector<Node *> below;
+                    };
+
+                    /*!
+                     * Constructs a lattice with the given top node and bottom node.
+                     *
+                     * @param topNode The top node of the resulting lattice.
+                     * @param bottomNode The bottom node of the resulting lattice.
+                     */
+                    Lattice(Node *topNode, Node *bottomNode, uint_fast64_t numberOfStates);
+
+                    /*!
+                     * Adds a node with the given state below node1 and above node2.
+                     * @param state The given state.
+                     * @param node1 The pointer to the node below which a new node is added.
+                     * @param node2 The pointer to the node above which a new node is added.
+                     */
+                    void addBetween(uint_fast64_t state, Node *node1, Node *node2);
+
+                    /*!
+                     * Adds state to the states of the given node.
+                     * @param state The state which is added.
+                     * @param node The pointer to the node to which state is added.
+                     */
+                    void addToNode(uint_fast64_t state, Node *node);
+
+                    /*!
+                     * Compares the level of the nodes of the states.
+                     * Behaviour unknown when one or more of the states doesnot occur at any Node in the Lattice.
+                     * @param state1 The first state.
+                     * @param state2 The second state.
+                     * @return 0 if the nodes are on the same level;
+                     * 1 if the node of the first state is closer to top then the node of the second state;
+                     * 2 if the node of the second state is closer to top then the node of the first state;
+                     * -1 if it is unclear from the structure of the lattice how the nodes relate.
+                     */
+                    int compare(uint_fast64_t state1, uint_fast64_t state2);
+
+                    /*!
+                     * Retrieves the pointer to a Node at which the state occurs.
+                     * Behaviour unknown when state does not exists at any Node in the Lattice.
+                     *
+                     * @param state The number of the state.
+                     *
+                     * @return The pointer to the node of the state.
+                     */
+                    Node *getNode(uint_fast64_t state);
+
+                    /*!
+                     * Prints a string representation of the lattice to std::cout.
+                     *
+                     * @param out The stream to output to.
+                     */
+                    void toString(std::ostream &out);
+
+//                    std::vector<uint_fast64_t> addedStates;
+
+                private:
+                    std::vector<Node *> nodes;
+
+                    uint_fast64_t numberOfStates;
+
+                    bool above(Node *, Node *);
+
+                    bool below(Node *, Node *);
+
+                    void remove(std::vector<Node *> *nodes, Node *node);
+
+                    void setStates(std::vector<uint_fast64_t>  states, Node *node);
+
+                };
+            }
+}
+#endif //LATTICE_LATTICE_H

src/storm-pars/analysis/Transformer.cpp

@@ -0,0 +1,249 @@
+//
+// Created by Jip Spel on 26.07.18.
+//
+
+#include "Transformer.h"
+namespace storm {
+    namespace analysis {
+        Lattice *Transformer::toLattice(storm::storage::SparseMatrix<storm::RationalFunction> matrix,
+                                        storm::storage::BitVector const &initialStates,
+                                        storm::storage::BitVector topStates,
+                                        storm::storage::BitVector bottomStates, uint_fast64_t numberOfStates) {
+            // Transform the transition matrix into a vector containing the states with the state to which the transition goes.
+            std::vector<State*> stateVector = toStateVector(matrix, initialStates);
+
+            // Start creating the Lattice.
+            Lattice::Node top = {topStates};
+            Lattice::Node bottom = {bottomStates};
+            Lattice *lattice = new Lattice(&top, &bottom, numberOfStates);
+            storm::storage::BitVector oldStates(numberOfStates);
+            // Create a copy of the states already present in the lattice.
+            storm::storage::BitVector seenStates = topStates|=bottomStates;
+
+            matrix.printAsMatlabMatrix(std::cout);
+
+            while (oldStates != seenStates) {
+                // As long as new states are discovered, continue.
+                oldStates = storm::storage::BitVector(seenStates);
+
+                for (auto itr = stateVector.begin(); itr != stateVector.end(); ++itr) {
+                    // Iterate over all states
+                    State *currentState = *itr;
+
+                    if (!seenStates[currentState->stateNumber]
+                        && seenStates[currentState->successor1]
+                        && seenStates[currentState->successor2]) {
+
+                        // Check if the current state number has not been added, but its successors have been added.
+                        if (currentState->successor1 == currentState->successor2) {
+                            // If there is only one successor, the state should be added to the same Node as its successor
+                            lattice->addToNode(currentState->stateNumber, lattice->getNode(currentState->successor1));
+                            // Add stateNumber to the set with seen states.
+                            seenStates.set(currentState->stateNumber);
+                        } else {
+                            // Otherwise, check how the two states compare, and add if the comparison is possible.
+                            uint_fast64_t successor1 = currentState->successor1;
+                            uint_fast64_t successor2 = currentState->successor2;
+                            int compareResult = lattice->compare(successor1, successor2);
+                            if (compareResult == 1) {
+                                //TODO dit in een aparte methode doen
+                                Lattice::Node *above = lattice->getNode(successor1);
+                                Lattice::Node *below = lattice->getNode(successor2);
+                                std::vector<Lattice::Node *> states1 = above->below;
+                                std::vector<Lattice::Node *> states2 = below->above;
+                                bool added = false;
+                                for (auto itr1 = states1.begin(); itr1 < states1.end(); ++itr1) {
+                                    for (auto itr2 = states2.begin(); itr2 < states2.end(); ++itr2) {
+                                        if ((*itr1)->states == (*itr2)->states) {
+                                            storm::RationalFunction prob1 = getProbability(currentState->stateNumber, successor1, matrix);
+                                            storm::RationalFunction prob2 = getProbability(currentState->stateNumber, successor2, matrix);
+                                            if (prob1 != storm::RationalFunction(1)
+                                                && prob2 != storm::RationalFunction(1)
+                                                && getProbability((*itr1)->states, above->states, matrix) == prob1
+                                                && getProbability((*itr1)->states, below->states, matrix) == prob2) {
+
+                                                std::cout << "Van: " << currentState-> stateNumber << " naar: " << successor1 << std::endl;
+                                                std::cout << prob1 << std::endl;
+                                                std::cout << "Van: " << currentState-> stateNumber << " naar: " << successor2 << std::endl;
+                                                std::cout << prob2 << std::endl;
+
+                                                lattice->addToNode(currentState->stateNumber, (*itr1));
+                                                seenStates.set(currentState->stateNumber);
+                                                added = true;
+                                            }
+                                        }
+
+                                    }
+                                }
+
+                                if (!added) {
+                                    // successor 1 is closer to top than successor 2
+                                    lattice->addBetween(currentState->stateNumber, lattice->getNode(successor1),
+                                                        lattice->getNode(successor2));
+                                    // Add stateNumber to the set with seen states.
+                                    seenStates.set(currentState->stateNumber);
+                                }
+                            } else if (compareResult == 2) {
+                                //TODO dit in een aparte methode doen
+                                // als er in de below van successor 2 en de above van succesor 1 een overlap is met een state, dan moet je kijken naar de kans
+                                Lattice::Node *above = lattice->getNode(successor2);
+                                Lattice::Node *below = lattice->getNode(successor1);
+                                std::vector<Lattice::Node *> states1 = above->below;
+                                std::vector<Lattice::Node *> states2 = below->above;
+                                bool added = false;
+                                for (auto itr1 = states1.begin(); itr1 < states1.end(); ++itr1) {
+                                    for (auto itr2 = states2.begin(); itr2 < states2.end(); ++itr2) {
+                                        if ((*itr1)->states == (*itr2)->states) {
+                                            storm::RationalFunction prob1 = getProbability(currentState->stateNumber, successor2, matrix);
+                                            storm::RationalFunction prob2 = getProbability(currentState->stateNumber, successor1, matrix);
+                                            if (prob1 != storm::RationalFunction(1)
+                                                && prob2 != storm::RationalFunction(1)
+                                                && getProbability((*itr1)->states, above->states, matrix) == prob1
+                                                && getProbability((*itr1)->states, below->states, matrix) == prob2) {
+
+                                                std::cout << "Van: " << currentState-> stateNumber << " naar: " << successor2 << std::endl;
+                                                std::cout << prob1 << std::endl;
+                                                std::cout << "Van: " << currentState-> stateNumber << " naar: " << successor1 << std::endl;
+                                                std::cout << prob2 << std::endl;
+
+                                                lattice->addToNode(currentState->stateNumber, (*itr1));
+                                                seenStates.set(currentState->stateNumber);
+                                                added = true;
+                                            }
+                                        }
+                                    }
+                                }
+
+                                if (!added) {
+                                    // successor 2 is closer to top than successor 1
+                                    lattice->addBetween(currentState->stateNumber, lattice->getNode(successor2),
+                                                        lattice->getNode(successor1));
+                                    // Add stateNumber to the set with seen states.
+                                    seenStates.set(currentState->stateNumber);
+                                }
+
+
+
+
+                            } else if (compareResult == 0) {
+                                // the successors are at the same level
+                                lattice->addToNode(currentState->stateNumber, lattice->getNode(successor1));
+                                // Add stateNumber to the set with seen states.
+                                seenStates.set(currentState->stateNumber);
+                            } else {
+                                // TODO: what to do?
+                                STORM_LOG_DEBUG("Failed to add" << currentState->stateNumber << "\n");
+                            }
+
+                        }
+                    }
+                }
+
+            }
+
+            return lattice;
+        }
+
+        std::vector<Transformer::State *>
+        Transformer::toStateVector(storm::storage::SparseMatrix<storm::RationalFunction> transitionMatrix,
+                                   storm::storage::BitVector const &initialStates) {
+            std::vector < State *> states = std::vector<State *>({});
+            std::vector <uint_fast64_t> stack(initialStates.begin(), initialStates.end());
+            std::vector <uint_fast64_t> seenStates(initialStates.begin(), initialStates.end());
+            uint_fast64_t currentState;
+
+            while (!stack.empty()) {
+                currentState = stack.back();
+                stack.pop_back();
+                std::vector <uint_fast64_t> successorStates(0, 2);
+
+                // Assume there are at most 2 successors
+                for (auto const &successor : transitionMatrix.getRowGroup(currentState)) {
+                    if (!storm::utility::isZero(successor.getValue())) {
+                        // Only explore the state if the transition was actually there.
+                        uint_fast64_t successorNumber = successor.getColumn();
+                        if (std::find(seenStates.begin(), seenStates.end(), successorNumber) == seenStates.end()) {
+                            stack.push_back(successorNumber);
+                            seenStates.push_back(successorNumber);
+                        }
+                        successorStates.push_back(successorNumber);
+                    }
+                }
+
+                State *state = new State();
+                state->stateNumber = currentState;
+                state->successor1 = successorStates.back();
+                successorStates.pop_back();
+                if (!successorStates.empty()) {
+                    state->successor2 = successorStates.back();
+                    successorStates.pop_back();
+                } else {
+                    state->successor2 = state->successor1;
+                }
+                states.push_back(state);
+            }
+            return states;
+        }
+
+        void Transformer::print(storm::storage::BitVector vector, std::string message) {
+            uint_fast64_t index = vector.getNextSetIndex(0);
+            std::cout << message <<": {";
+            while (index < vector.size()) {
+                std::cout << index;
+                index = vector.getNextSetIndex(index+1);
+                if (index < vector.size()) {
+                    std::cout << ", ";
+                }
+            }
+            std::cout << "}" << std::endl;
+        }
+
+        std::vector<uint_fast64_t> Transformer::getNumbers(storm::storage::BitVector vector) {
+            std::vector<uint_fast64_t> result = std::vector<uint_fast64_t>({});
+            uint_fast64_t index = vector.getNextSetIndex(0);
+            while (index < vector.size()) {
+                result.push_back(index);
+                index = vector.getNextSetIndex(index+1);
+
+            }
+            return result;
+        }
+
+        storm::RationalFunction Transformer::getProbability(storm::storage::BitVector state, storm::storage::BitVector successor, storm::storage::SparseMatrix<storm::RationalFunction>  matrix) {
+            std::vector<uint_fast64_t> successorNumbers = getNumbers(successor);
+            storm::RationalFunction result = storm::RationalFunction(1);
+            for (auto itr = successorNumbers.begin(); itr < successorNumbers.end() && result == storm::RationalFunction(1); ++itr) {
+                result = getProbability(state, (*itr), matrix);
+            }
+            return result;
+        }
+
+        storm::RationalFunction Transformer::getProbability(storm::storage::BitVector state, uint_fast64_t successor, storm::storage::SparseMatrix<storm::RationalFunction>  matrix) {
+            std::vector<uint_fast64_t> stateNumbers = getNumbers(state);
+            storm::RationalFunction result = storm::RationalFunction(1);
+            for (auto itr = stateNumbers.begin(); itr < stateNumbers.end() && result == storm::RationalFunction(1); ++itr) {
+                result = getProbability((*itr), successor, matrix);
+            }
+            return result;
+        }
+
+        storm::RationalFunction Transformer::getProbability(uint_fast64_t state, uint_fast64_t successor, storm::storage::SparseMatrix<storm::RationalFunction>  matrix) {
+            storm::RationalFunction result = storm::RationalFunction(1);
+            // Iterate over all row groups.
+            auto row = matrix.getRow(state);
+
+            for (auto itr = row.begin(); itr < row.end() && result == storm::RationalFunction(1); ++itr) {
+                if ((*itr).getColumn() == successor) {
+                    std::cout << "Tralala" << std::endl;
+                    // TODO: nog checken dat ie wel met state te doen heeft
+                    result = (*itr).getValue();
+                    std::cout << "Van: " << state << " naar: " << successor << std::endl;
+                    std::cout << result << std::endl;
+                }
+
+            }
+
+            return result;
+        }
+    }
+}

src/storm-pars/analysis/Transformer.h

@@ -0,0 +1,55 @@
+//
+// Created by Jip Spel on 26.07.18.
+//
+
+#ifndef LATTICE_BUILDER_H
+#define LATTICE_BUILDER_H
+
+#include "storm/storage/BitVector.h"
+#include "storm/storage/SparseMatrix.h"
+#include "Lattice.h"
+namespace storm {
+    namespace analysis {
+        class Transformer {
+        public:
+            struct State {
+                uint_fast64_t stateNumber;
+                uint_fast64_t successor1;
+                uint_fast64_t successor2;
+            };
+
+            /*!
+             * Returns the pointer to the Lattice constructed from the given transitionMatrix,
+             * BitVector of initialStates, vector with the top states and vector with the bottom states.
+             * Assumes that every state has at least one and at most two outgoing transitions.
+             *
+             * @param matrix The transition matrix.
+             * @param initialStates The BitVector containing the initialStates.
+             * @param topStates Vector containing the numbers of the top states.
+             * @param bottomStates Vector containing the numbers of the bottom states.
+             *
+             * @return The lattice ordering of the states.
+             */
+            static Lattice *toLattice(storm::storage::SparseMatrix<storm::RationalFunction> matrix,
+                                      storm::storage::BitVector const &initialStates,
+                                      storm::storage::BitVector topStates,
+                                      storm::storage::BitVector bottomStates, uint_fast64_t numberOfStates);
+
+        private:
+            static std::vector<Transformer::State *>
+            toStateVector(storm::storage::SparseMatrix<storm::RationalFunction> transitionMatrix,
+                          storm::storage::BitVector const &initialStates);
+
+            static void print(storm::storage::BitVector vector, std::string message);
+
+            static std::vector<uint_fast64_t> getNumbers(storm::storage::BitVector vector);
+
+            static storm::RationalFunction getProbability(storm::storage::BitVector state, storm::storage::BitVector successor, storm::storage::SparseMatrix<storm::RationalFunction> matrix);
+
+            static storm::RationalFunction getProbability(storm::storage::BitVector state, uint_fast64_t successor, storm::storage::SparseMatrix<storm::RationalFunction> matrix);
+
+            static storm::RationalFunction getProbability(uint_fast64_t state, uint_fast64_t successor, storm::storage::SparseMatrix<storm::RationalFunction> matrix);
+            };
+    }
+}
+#endif //LATTICE_BUILDER_H

src/storm-pars/settings/modules/ParametricSettings.cpp

@@ -65,7 +65,11 @@ namespace storm {
             bool ParametricSettings::isSampleExactSet() const {
                 return this->getOption(sampleExactOptionName).getHasOptionBeenSet();
             }
-            
+
+            bool ParametricSettings::isMonotonicityAnalysisSet() const {
+                // TODO: Make this dependent on the input.
+                return true;
+            }
         } // namespace modules
     } // namespace settings
 } // namespace storm

src/storm-pars/settings/modules/ParametricSettings.h

@@ -63,6 +63,8 @@ namespace storm {
                  * Retrieves whether samples are to be computed exactly.
                  */
                 bool isSampleExactSet() const;
+
+                bool isMonotonicityAnalysisSet() const;
                 
                 const static std::string moduleName;