Fixed an issue with JANI models concerning properties using transient variable expressions.

CHANGELOG.md

@@ -13,6 +13,9 @@ Version 1.6.x
 - Added support for generating optimal schedulers for globally formulae
 - Simulator supports exact arithmetic
 - Added switch `--no-simplify` to disable simplification of PRISM programs (which sometimes costs a bit of time on extremely large inputs)
+- Fixed issues with JANI inputs concerning 
+    - transient variable expressions in properties and
+    - integer variables with either only an upper or only a lower bound.
 - `storm-pomdp`: States can be labelled with values for observable predicates
 - `storm-pomdp`: (Only API) Track state estimates
 - `storm-pomdp`: (Only API) Reduce computation of state estimates to computation on unrolled MDP

src/storm/generator/JaniNextStateGenerator.cpp

@@ -457,7 +457,7 @@ namespace storm {
         }
         
         template<typename ValueType, typename StateType>
-        TransientVariableValuation<ValueType> JaniNextStateGenerator<ValueType, StateType>::getTransientVariableValuationAtLocations(std::vector<uint64_t> const& locations) const {
+        TransientVariableValuation<ValueType> JaniNextStateGenerator<ValueType, StateType>::getTransientVariableValuationAtLocations(std::vector<uint64_t> const& locations, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator) const {
             uint64_t automatonIndex = 0;
             TransientVariableValuation<ValueType> transientVariableValuation;
             for (auto const& automatonRef : this->parallelAutomata) {
@@ -465,12 +465,19 @@ namespace storm {
                 uint64_t currentLocationIndex = locations[automatonIndex];
                 storm::jani::Location const& location = automaton.getLocation(currentLocationIndex);
                 STORM_LOG_ASSERT(!location.getAssignments().hasMultipleLevels(true), "Indexed assignments at locations are not supported in the jani standard.");
-                applyTransientUpdate(transientVariableValuation, location.getAssignments().getTransientAssignments(), *this->evaluator);
+                applyTransientUpdate(transientVariableValuation, location.getAssignments().getTransientAssignments(), evaluator);
                 ++automatonIndex;
             }
             return transientVariableValuation;
         }
         
+        template<typename ValueType, typename StateType>
+        void JaniNextStateGenerator<ValueType, StateType>::unpackTransientVariableValuesIntoEvaluator(CompressedState const& state, storm::expressions::ExpressionEvaluator<ValueType>& evaluator) const {
+            transientVariableInformation.setDefaultValuesInEvaluator(evaluator);
+            auto transientVariableValuation = getTransientVariableValuationAtLocations(getLocations(state), evaluator);
+            transientVariableValuation.setInEvaluator(evaluator, this->getOptions().isExplorationChecksSet());
+        }
+        
         template<typename ValueType, typename StateType>
         storm::storage::sparse::StateValuationsBuilder JaniNextStateGenerator<ValueType, StateType>::initializeStateValuationsBuilder() const {
             auto result = NextStateGenerator<ValueType, StateType>::initializeStateValuationsBuilder();
@@ -500,7 +507,7 @@ namespace storm {
             extractVariableValues(*this->state, this->variableInformation, integerValues, booleanValues, integerValues);
             
             // Add values for transient variables
-            auto transientVariableValuation = getTransientVariableValuationAtLocations(getLocations(*this->state));
+            auto transientVariableValuation = getTransientVariableValuationAtLocations(getLocations(*this->state), *this->evaluator);
             {
                 auto varIt = transientVariableValuation.booleanValues.begin();
                 auto varIte = transientVariableValuation.booleanValues.end();
@@ -551,7 +558,7 @@ namespace storm {
             
             // First, construct the state rewards, as we may return early if there are no choices later and we already
             // need the state rewards then.
-            auto transientVariableValuation = getTransientVariableValuationAtLocations(locations);
+            auto transientVariableValuation = getTransientVariableValuationAtLocations(locations, *this->evaluator);
             transientVariableValuation.setInEvaluator(*this->evaluator, this->getOptions().isExplorationChecksSet());
             result.addStateRewards(evaluateRewardExpressions());
             this->transientVariableInformation.setDefaultValuesInEvaluator(*this->evaluator);
@@ -1096,26 +1103,17 @@ namespace storm {
         
         template<typename ValueType, typename StateType>
         storm::models::sparse::StateLabeling JaniNextStateGenerator<ValueType, StateType>::label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices) {
+            
             // As in JANI we can use transient boolean variable assignments in locations to identify states, we need to
             // create a list of boolean transient variables and the expressions that define them.
-            std::unordered_map<storm::expressions::Variable, storm::expressions::Expression> transientVariableToExpressionMap;
-            bool translateArrays = !this->arrayEliminatorData.replacements.empty();
+            std::vector<std::pair<std::string, storm::expressions::Expression>> transientVariableExpressions;
             for (auto const& variable : model.getGlobalVariables().getTransientVariables()) {
                 if (variable.isBooleanVariable()) {
                     if (this->options.isBuildAllLabelsSet() || this->options.getLabelNames().find(variable.getName()) != this->options.getLabelNames().end()) {
-                        storm::expressions::Expression labelExpression = model.getLabelExpression(variable.asBooleanVariable(), this->parallelAutomata);
-                        if (translateArrays) {
-                            labelExpression = this->arrayEliminatorData.transformExpression(labelExpression);
+                        transientVariableExpressions.emplace_back(variable.getName(), variable.getExpressionVariable().getExpression());
                     }
-                        transientVariableToExpressionMap[variable.getExpressionVariable()] = std::move(labelExpression);
                 }
             }
-            }
-            
-            std::vector<std::pair<std::string, storm::expressions::Expression>> transientVariableExpressions;
-            for (auto const& element : transientVariableToExpressionMap) {
-                transientVariableExpressions.push_back(std::make_pair(element.first.getName(), element.second));
-            }
             return NextStateGenerator<ValueType, StateType>::label(stateStorage, initialStateIndices, deadlockStateIndices, transientVariableExpressions);
         }
         

src/storm/generator/JaniNextStateGenerator.h

@@ -65,6 +65,15 @@ namespace storm {
             
             virtual std::shared_ptr<storm::storage::sparse::ChoiceOrigins> generateChoiceOrigins(std::vector<boost::any>& dataForChoiceOrigins) const override;
             
+            /*!
+             * Sets the values of all transient variables in the current state to the given evaluator.
+             * @pre The values of non-transient variables have been set in the provided evaluator
+             * @param state The current state
+             * @param evaluator the evaluator to which the values will be set
+             * @post The values of all transient variables are set in the given evaluator (including the transient variables without an explicit assignment in the current locations).
+             */
+            virtual void unpackTransientVariableValuesIntoEvaluator(CompressedState const& state, storm::expressions::ExpressionEvaluator<ValueType>& evaluator) const override;
+            
         private:
             /*!
              * Retrieves the location index from the given state.
@@ -119,7 +128,13 @@ namespace storm {
              */
             virtual storm::storage::BitVector evaluateObservationLabels(CompressedState const& state) const override;
 
-            TransientVariableValuation<ValueType> getTransientVariableValuationAtLocations(std::vector<uint64_t> const& locations) const;
+            /*!
+             * Computes the values of the transient variables assigned in the given locations.
+             * @note Only the the transient variables with an explicit assignment in the provided locations are contained in the returned struct.
+             * @pre The values of non-transient variables have been set in the provided evaluator
+             * @return a struct containing the values of the transient variables within the given locations
+             */
+            TransientVariableValuation<ValueType> getTransientVariableValuationAtLocations(std::vector<uint64_t> const& locations, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator) const;
             
             /*!
              * Retrieves all choices possible from the given state.

src/storm/generator/NextStateGenerator.cpp

@@ -169,6 +169,7 @@ namespace storm {
             auto const& states = stateStorage.stateToId;
             for (auto const& stateIndexPair : states) {
                 unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, *this->evaluator);
+                unpackTransientVariableValuesIntoEvaluator(stateIndexPair.first, *this->evaluator);
                 
                 for (auto const& label : labelsAndExpressions) {
                     // Add label to state, if the corresponding expression is true.
@@ -209,6 +210,12 @@ namespace storm {
             return result;
         }
         
+        template<typename ValueType, typename StateType>
+        void NextStateGenerator<ValueType, StateType>::unpackTransientVariableValuesIntoEvaluator(CompressedState const&, storm::expressions::ExpressionEvaluator<ValueType>&) const {
+            // Intentionally left empty.
+            // This method should be overwritten in case there are transient variables (e.g. JANI).
+        }
+
         template<typename ValueType, typename StateType>
         void NextStateGenerator<ValueType, StateType>::postprocess(StateBehavior<ValueType, StateType>& result) {
             // If the model we build is a Markov Automaton, we postprocess the choices to sum all Markovian choices

src/storm/generator/NextStateGenerator.h

@@ -95,6 +95,15 @@ namespace storm {
              */
             storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices, std::vector<std::pair<std::string, storm::expressions::Expression>> labelsAndExpressions);
 
+            /*!
+             * Sets the values of all transient variables in the current state to the given evaluator.
+             * @pre The values of non-transient variables have been set in the provided evaluator
+             * @param state The current state
+             * @param evaluator the evaluator to which the values will be set
+             * @post The values of all transient variables are set in the given evaluator (including the transient variables without an explicit assignment in the current locations).
+             */
+            virtual void unpackTransientVariableValuesIntoEvaluator(CompressedState const& state, storm::expressions::ExpressionEvaluator<ValueType>& evaluator) const;
+            
             virtual storm::storage::BitVector evaluateObservationLabels(CompressedState const& state) const =0;
 
             virtual storm::storage::sparse::StateValuationsBuilder initializeObservationValuationsBuilder() const;