preparing labels for JANI models (game-based abstraction)

src/storm/abstraction/AbstractionInformation.cpp

@@ -492,9 +492,11 @@ namespace storm {
         }
         
         template <storm::dd::DdType DdType>
-        std::pair<std::pair<storm::expressions::Variable, storm::expressions::Variable>, uint64_t> AbstractionInformation<DdType>::addLocationVariables(uint64_t highestLocationIndex) {
+        std::pair<std::pair<storm::expressions::Variable, storm::expressions::Variable>, uint64_t> AbstractionInformation<DdType>::addLocationVariables(storm::expressions::Variable const& locationExpressionVariable, uint64_t highestLocationIndex) {
             auto newMetaVariable = ddManager->addMetaVariable("loc_" + std::to_string(locationVariablePairs.size()), 0, highestLocationIndex);
             
+            locationExpressionVariables.insert(locationExpressionVariable);
+            locationExpressionToDdVariableMap.emplace(locationExpressionVariable, newMetaVariable);
             locationVariablePairs.emplace_back(newMetaVariable);
             allSourceLocationVariables.insert(newMetaVariable.first);
             sourceVariables.insert(newMetaVariable.first);
@@ -524,6 +526,21 @@ namespace storm {
             return allSuccessorLocationVariables;
         }
         
+        template <storm::dd::DdType DdType>
+        storm::expressions::Variable const& AbstractionInformation<DdType>::getDdLocationVariable(storm::expressions::Variable const& locationExpressionVariable, bool source) {
+            auto const& metaVariablePair = locationExpressionToDdVariableMap.at(locationExpressionVariable);
+            if (source) {
+                return metaVariablePair.first;
+            } else {
+                return metaVariablePair.second;
+            }
+        }
+        
+        template <storm::dd::DdType DdType>
+        std::set<storm::expressions::Variable> const& AbstractionInformation<DdType>::getLocationExpressionVariables() const {
+            return locationExpressionVariables;
+        }
+        
         template <storm::dd::DdType DdType>
         storm::dd::Bdd<DdType> AbstractionInformation<DdType>::encodeLocation(storm::expressions::Variable const& locationVariable, uint64_t locationIndex) const {
             return this->getDdManager().getEncoding(locationVariable, locationIndex);

src/storm/abstraction/AbstractionInformation.h

@@ -462,7 +462,7 @@ namespace storm {
             /*!
              * Adds a location variable of appropriate range and returns the pair of meta variables.
              */
-            std::pair<std::pair<storm::expressions::Variable, storm::expressions::Variable>, uint64_t> addLocationVariables(uint64_t highestLocationIndex);
+            std::pair<std::pair<storm::expressions::Variable, storm::expressions::Variable>, uint64_t> addLocationVariables(storm::expressions::Variable const& locationExpressionVariable, uint64_t highestLocationIndex);
             
             /*!
              * Retrieves the location variable with the given index as either source or successor.
@@ -479,6 +479,16 @@ namespace storm {
              */
             std::set<storm::expressions::Variable> const& getSuccessorLocationVariables() const;
             
+            /*!
+             * Retrieves the DD variable for the given location expression variable.
+             */
+            storm::expressions::Variable const& getDdLocationVariable(storm::expressions::Variable const& locationExpressionVariable, bool source);
+            
+            /*!
+             * Retrieves the source location variables.
+             */
+            std::set<storm::expressions::Variable> const& getLocationExpressionVariables() const;
+            
             /*!
              * Encodes the given location index as either source or successor.
              */
@@ -612,6 +622,12 @@ namespace storm {
             /// The location variable pairs (source/successor).
             std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> locationVariablePairs;
             
+            /// A mapping from location expression variables to their source/successor counterparts.
+            std::map<storm::expressions::Variable, std::pair<storm::expressions::Variable, storm::expressions::Variable>> locationExpressionToDdVariableMap;
+            
+            /// The set of all location expression variables.
+            std::set<storm::expressions::Variable> locationExpressionVariables;
+            
             // All source location variables.
             std::set<storm::expressions::Variable> allSourceLocationVariables;
             

src/storm/abstraction/ExpressionTranslator.cpp

@@ -16,7 +16,7 @@ namespace storm {
         using namespace storm::expressions;
         
         template <storm::dd::DdType DdType>
-        ExpressionTranslator<DdType>::ExpressionTranslator(AbstractionInformation<DdType>& abstractionInformation, std::unique_ptr<storm::solver::SmtSolver>&& smtSolver) : abstractionInformation(abstractionInformation), equivalenceChecker(std::move(smtSolver)), locationVariables(abstractionInformation.getSourceLocationVariables()), abstractedVariables(abstractionInformation.getAbstractedVariables()) {
+        ExpressionTranslator<DdType>::ExpressionTranslator(AbstractionInformation<DdType>& abstractionInformation, std::unique_ptr<storm::solver::SmtSolver>&& smtSolver) : abstractionInformation(abstractionInformation), equivalenceChecker(std::move(smtSolver)), locationVariables(abstractionInformation.getLocationExpressionVariables()), abstractedVariables(abstractionInformation.getAbstractedVariables()) {
             // Intentionally left empty.
         }
 
@@ -127,7 +127,7 @@ namespace storm {
                 
                 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Expressions of this kind are currently not supported by the abstraction expression translator.");
             } else {
-                return abstractionInformation.get().getDdManager().template getIdentity<double>(expression.getVariable());
+                return abstractionInformation.get().getDdManager().template getIdentity<double>(abstractionInformation.get().getDdLocationVariable(expression.getVariable(), true));
             }
         }
         

src/storm/abstraction/jani/AutomatonAbstractor.cpp

@@ -33,7 +33,7 @@ namespace storm {
                 }
                 
                 if (automaton.getNumberOfLocations() > 1) {
-                    locationVariables = abstractionInformation.addLocationVariables(automaton.getNumberOfLocations() - 1).first;
+                    locationVariables = abstractionInformation.addLocationVariables(automaton.getLocationExpressionVariable(), automaton.getNumberOfLocations() - 1).first;
                 }
             }
             

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -8,6 +8,7 @@
 #include "storm/models/symbolic/Mdp.h"
 
 #include "storm/storage/expressions/ExpressionManager.h"
+#include "storm/storage/expressions/VariableSetAbstractor.h"
 
 #include "storm/storage/dd/DdManager.h"
 
@@ -445,10 +446,26 @@ namespace storm {
         template<storm::dd::DdType Type, typename ModelType>
         std::vector<storm::expressions::Expression> GameBasedMdpModelChecker<Type, ModelType>::getInitialPredicates(storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) {
             std::vector<storm::expressions::Expression> initialPredicates;
+            if (preprocessedModel.isJaniModel()) {
+                storm::expressions::VariableSetAbstractor abstractor(preprocessedModel.asJaniModel().getAllLocationExpressionVariables());
+
+                storm::expressions::Expression abstractedExpression = abstractor.abstract(targetStateExpression);
+                if (abstractedExpression.isInitialized() && !abstractedExpression.isTrue() && !abstractedExpression.isFalse()) {
+                    initialPredicates.push_back(abstractedExpression);
+                }
+                
+                abstractedExpression = abstractor.abstract(constraintExpression);
+                if (abstractedExpression.isInitialized() && !abstractedExpression.isTrue() && !abstractedExpression.isFalse()) {
+                    initialPredicates.push_back(abstractedExpression);
+                }
+            } else {
+                if (!targetStateExpression.isTrue() && !targetStateExpression.isFalse()) {
                     initialPredicates.push_back(targetStateExpression);
+                }
                 if (!constraintExpression.isTrue() && !constraintExpression.isFalse()) {
                     initialPredicates.push_back(constraintExpression);
                 }
+            }
             return initialPredicates;
         }
         

src/storm/storage/expressions/VariableSetAbstractor.cpp

@@ -0,0 +1,225 @@
+#include "storm/storage/expressions/VariableSetAbstractor.h"
+
+#include "storm/storage/expressions/Expressions.h"
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/InvalidArgumentException.h"
+
+namespace storm {
+    namespace expressions {
+        
+        VariableSetAbstractor::VariableSetAbstractor(std::set<storm::expressions::Variable> const& variablesToAbstract) : variablesToAbstract(variablesToAbstract) {
+            // Intentionally left empty.
+        }
+        
+        storm::expressions::Expression VariableSetAbstractor::abstract(storm::expressions::Expression const& expression) {
+            std::set<storm::expressions::Variable> containedVariables = expression.getVariables();
+            bool onlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), containedVariables.begin(), containedVariables.end());
+            
+            if (onlyAbstractedVariables) {
+                return storm::expressions::Expression();
+            }
+            
+            std::set<storm::expressions::Variable> tmp;
+            std::set_intersection(containedVariables.begin(), containedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin()));
+            bool hasAbstractedVariables = !tmp.empty();
+            
+            if (hasAbstractedVariables) {
+                return boost::any_cast<storm::expressions::Expression>(expression.accept(*this, boost::none));
+            } else {
+                return expression;
+            }
+        }
+        
+        boost::any VariableSetAbstractor::visit(IfThenElseExpression const& expression, boost::any const& data) {
+            std::set<storm::expressions::Variable> conditionVariables;
+            expression.getCondition()->gatherVariables(conditionVariables);
+            bool conditionOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), conditionVariables.begin(), conditionVariables.end());
+            
+            std::set<storm::expressions::Variable> tmp;
+            std::set_intersection(conditionVariables.begin(), conditionVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin()));
+            bool conditionHasAbstractedVariables = !tmp.empty();
+            
+            std::set<storm::expressions::Variable> thenVariables;
+            expression.getThenExpression()->gatherVariables(thenVariables);
+            bool thenOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), thenVariables.begin(), thenVariables.end());
+
+            tmp.clear();
+            std::set_intersection(thenVariables.begin(), thenVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin()));
+            bool thenHasAbstractedVariables = !tmp.empty();
+
+            std::set<storm::expressions::Variable> elseVariables;
+            expression.getElseExpression()->gatherVariables(elseVariables);
+            bool elseOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), elseVariables.begin(), elseVariables.end());
+
+            tmp.clear();
+            std::set_intersection(elseVariables.begin(), elseVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin()));
+            bool elseHasAbstractedVariables = !tmp.empty();
+
+            if (conditionHasAbstractedVariables || thenHasAbstractedVariables || elseHasAbstractedVariables) {
+                if (conditionOnlyAbstractedVariables && thenOnlyAbstractedVariables && elseOnlyAbstractedVariables) {
+                    return boost::any();
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot abstract from variable set in expression as it mixes variables of different types.");
+                }
+            } else {
+                return expression.toExpression();
+            }
+        }
+        
+        boost::any VariableSetAbstractor::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) {
+            std::set<storm::expressions::Variable> leftContainedVariables;
+            expression.getFirstOperand()->gatherVariables(leftContainedVariables);
+            bool leftOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), leftContainedVariables.begin(), leftContainedVariables.end());
+            
+            std::set<storm::expressions::Variable> tmp;
+            std::set_intersection(leftContainedVariables.begin(), leftContainedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin()));
+            bool leftHasAbstractedVariables = !tmp.empty();
+            
+            std::set<storm::expressions::Variable> rightContainedVariables;
+            expression.getSecondOperand()->gatherVariables(rightContainedVariables);
+            bool rightOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), rightContainedVariables.begin(), rightContainedVariables.end());
+            
+            tmp.clear();
+            std::set_intersection(rightContainedVariables.begin(), rightContainedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin()));
+            bool rightHasAbstractedVariables = !tmp.empty();
+            
+            if (leftOnlyAbstractedVariables && rightOnlyAbstractedVariables) {
+                return boost::any();
+            } else if (!leftHasAbstractedVariables && !rightHasAbstractedVariables) {
+                return expression;
+            } else {
+                if (leftHasAbstractedVariables && !rightHasAbstractedVariables) {
+                    return expression.getFirstOperand()->toExpression();
+                } else  if (rightHasAbstractedVariables && !leftHasAbstractedVariables) {
+                    return expression.getSecondOperand()->toExpression();
+                } else {
+                    storm::expressions::Expression leftResult = boost::any_cast<storm::expressions::Expression>(expression.getFirstOperand()->accept(*this, data));
+                    storm::expressions::Expression rightResult = boost::any_cast<storm::expressions::Expression>(expression.getFirstOperand()->accept(*this, data));
+                    
+                    switch (expression.getOperatorType()) {
+                        case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::And: return leftResult && rightResult;
+                        case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Or: return leftResult || rightResult;
+                        case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Xor: return leftResult ^ rightResult;
+                        case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Implies: return storm::expressions::implies(leftResult, rightResult);
+                        case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Iff: return storm::expressions::iff(leftResult, rightResult);
+                    }
+                }
+            }
+        }
+        
+        boost::any VariableSetAbstractor::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) {
+            std::set<storm::expressions::Variable> leftContainedVariables;
+            expression.getFirstOperand()->gatherVariables(leftContainedVariables);
+            bool leftOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), leftContainedVariables.begin(), leftContainedVariables.end());
+            
+            std::set<storm::expressions::Variable> tmp;
+            std::set_intersection(leftContainedVariables.begin(), leftContainedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin()));
+            bool leftHasAbstractedVariables = !tmp.empty();
+            
+            std::set<storm::expressions::Variable> rightContainedVariables;
+            expression.getSecondOperand()->gatherVariables(rightContainedVariables);
+            bool rightOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), rightContainedVariables.begin(), rightContainedVariables.end());
+            
+            tmp.clear();
+            std::set_intersection(rightContainedVariables.begin(), rightContainedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin()));
+            bool rightHasAbstractedVariables = !tmp.empty();
+            
+            if (leftOnlyAbstractedVariables && rightOnlyAbstractedVariables) {
+                return boost::any();
+            } else if (!leftHasAbstractedVariables && !rightHasAbstractedVariables) {
+                return expression;
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot abstract from variable set in expression as it mixes variables of different types.");
+            }
+        }
+        
+        boost::any VariableSetAbstractor::visit(BinaryRelationExpression const& expression, boost::any const& data) {
+            std::set<storm::expressions::Variable> leftContainedVariables;
+            expression.getFirstOperand()->gatherVariables(leftContainedVariables);
+            bool leftOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), leftContainedVariables.begin(), leftContainedVariables.end());
+            
+            std::set<storm::expressions::Variable> tmp;
+            std::set_intersection(leftContainedVariables.begin(), leftContainedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin()));
+            bool leftHasAbstractedVariables = !tmp.empty();
+
+            std::set<storm::expressions::Variable> rightContainedVariables;
+            expression.getSecondOperand()->gatherVariables(rightContainedVariables);
+            bool rightOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), rightContainedVariables.begin(), rightContainedVariables.end());
+            
+            tmp.clear();
+            std::set_intersection(rightContainedVariables.begin(), rightContainedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin()));
+            bool rightHasAbstractedVariables = !tmp.empty();
+
+            if (leftOnlyAbstractedVariables && rightOnlyAbstractedVariables) {
+                return boost::any();
+            } else if (!leftHasAbstractedVariables && !rightHasAbstractedVariables) {
+                return expression;
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot abstract from variable set in expression as it mixes variables of different types.");
+            }
+        }
+        
+        boost::any VariableSetAbstractor::visit(VariableExpression const& expression, boost::any const& data) {
+            if (variablesToAbstract.find(expression.getVariable()) != variablesToAbstract.end()) {
+                return boost::any();
+            } else {
+                return expression.toExpression();
+            }
+        }
+        
+        boost::any VariableSetAbstractor::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) {
+            std::set<storm::expressions::Variable> containedVariables;
+            expression.gatherVariables(containedVariables);
+            bool onlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), containedVariables.begin(), containedVariables.end());
+            
+            if (onlyAbstractedVariables) {
+                return boost::any();
+            }
+            
+            std::set<storm::expressions::Variable> tmp;
+            std::set_intersection(containedVariables.begin(), containedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin()));
+            bool hasAbstractedVariables = !tmp.empty();
+            if (hasAbstractedVariables) {
+                storm::expressions::Expression subexpression = boost::any_cast<storm::expressions::Expression>(expression.getOperand()->accept(*this, data));
+                switch (expression.getOperatorType()) {
+                    case storm::expressions::UnaryBooleanFunctionExpression::OperatorType::Not: return !subexpression;
+                }
+            } else {
+                return expression.toExpression();
+            }
+        }
+        
+        boost::any VariableSetAbstractor::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) {
+            std::set<storm::expressions::Variable> containedVariables;
+            expression.gatherVariables(containedVariables);
+            bool onlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), containedVariables.begin(), containedVariables.end());
+            
+            if (onlyAbstractedVariables) {
+                return boost::any();
+            }
+            
+            std::set<storm::expressions::Variable> tmp;
+            std::set_intersection(containedVariables.begin(), containedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin()));
+            bool hasAbstractedVariables = !tmp.empty();
+            if (hasAbstractedVariables) {
+                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot abstract from variable set in expression as it mixes variables of different types.");
+            } else {
+                return expression.toExpression();
+            }
+        }
+        
+        boost::any VariableSetAbstractor::visit(BooleanLiteralExpression const& expression, boost::any const& data) {
+            return expression.toExpression();
+        }
+        
+        boost::any VariableSetAbstractor::visit(IntegerLiteralExpression const& expression, boost::any const& data) {
+            return expression.toExpression();
+        }
+        
+        boost::any VariableSetAbstractor::visit(RationalLiteralExpression const& expression, boost::any const& data) {
+            return expression.toExpression();
+        }
+        
+    }
+}

src/storm/storage/expressions/VariableSetAbstractor.h

@@ -0,0 +1,35 @@
+#pragma once
+
+#include <set>
+
+#include "storm/storage/expressions/ExpressionVisitor.h"
+
+namespace storm {
+    namespace expressions {
+        
+        class Variable;
+        class Expression;
+        
+        class VariableSetAbstractor : public ExpressionVisitor {
+        public:
+            VariableSetAbstractor(std::set<storm::expressions::Variable> const& variablesToAbstract);
+            
+            storm::expressions::Expression abstract(storm::expressions::Expression const& expression);
+            
+            virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(BinaryRelationExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(VariableExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(BooleanLiteralExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(IntegerLiteralExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override;
+            
+        private:
+            std::set<storm::expressions::Variable> variablesToAbstract;
+        };
+        
+    }
+}

src/storm/storage/jani/Model.cpp

@@ -630,7 +630,7 @@ namespace storm {
             return globalVariables;
         }
         
-        std::set<storm::expressions::Variable> Model::getAllExpressionVariables() const {
+        std::set<storm::expressions::Variable> Model::getAllExpressionVariables(bool includeLocationExpressionVariables) const {
             std::set<storm::expressions::Variable> result;
             
             for (auto const& constant : constants) {
@@ -642,11 +642,22 @@ namespace storm {
             for (auto const& automaton : automata) {
                 auto const& automatonVariables = automaton.getAllExpressionVariables();
                 result.insert(automatonVariables.begin(), automatonVariables.end());
+                if (includeLocationExpressionVariables) {
+                    result.insert(automaton.getLocationExpressionVariable());
+                }
             }
             
             return result;
         }
         
+        std::set<storm::expressions::Variable> Model::getAllLocationExpressionVariables() const {
+            std::set<storm::expressions::Variable> result;
+            for (auto const& automaton : automata) {
+                result.insert(automaton.getLocationExpressionVariable());
+            }
+            return result;
+        }
+        
         bool Model::hasGlobalVariable(std::string const& name) const {
             return globalVariables.hasVariable(name);
         }
@@ -969,6 +980,14 @@ namespace storm {
             STORM_LOG_ASSERT(composition != nullptr, "Composition is not set");
         }
 
+        storm::expressions::Expression Model::getLabelExpression(BooleanVariable const& transientVariable) const {
+            std::vector<std::reference_wrapper<Automaton const>> allAutomata;
+            for (auto const& automaton : automata) {
+                allAutomata.emplace_back(automaton);
+            }
+            return getLabelExpression(transientVariable, allAutomata);
+        }
+        
         storm::expressions::Expression Model::getLabelExpression(BooleanVariable const& transientVariable, std::vector<std::reference_wrapper<Automaton const>> const& automata) const {
             STORM_LOG_THROW(transientVariable.isTransient(), storm::exceptions::InvalidArgumentException, "Expected transient variable.");
             

src/storm/storage/jani/Model.h

@@ -183,11 +183,19 @@ namespace storm {
             VariableSet const& getGlobalVariables() const;
             
             /*!
-             * Retrieves all expression variables used by this model.
+             * Retrieves all expression variables used by this model. Note that this does not include the location
+             * expression variables by default.
              *
              * @return The set of expression variables used by this model.
              */
-            std::set<storm::expressions::Variable> getAllExpressionVariables() const;
+            std::set<storm::expressions::Variable> getAllExpressionVariables(bool includeLocationExpressionVariables = false) const;
+
+            /*!
+             * Retrieves all location expression variables used by this model.
+             *
+             * @return The set of expression variables used by this model.
+             */
+            std::set<storm::expressions::Variable> getAllLocationExpressionVariables() const;
 
             /*!
              * Retrieves whether this model has a global variable with the given name.
@@ -381,6 +389,12 @@ namespace storm {
              */
             storm::expressions::Expression getLabelExpression(BooleanVariable const& transientVariable, std::vector<std::reference_wrapper<Automaton const>> const& automata) const;
 
+            /*!
+             * Creates the expression that characterizes all states in which the provided transient boolean variable is
+             * true. The provided location variables are used to encode the location of the automata.
+             */
+            storm::expressions::Expression getLabelExpression(BooleanVariable const& transientVariable) const;
+
             /*!
              * Checks that undefined constants (parameters) of the model preserve the graph of the underlying model.
              * That is, undefined constants may only appear in the probability expressions of edge destinations as well