extend the next state generator to support prism program simulation

src/storm/generator/CompressedState.cpp

@@ -126,8 +126,34 @@ namespace storm {
             }
         }
 
+        template<typename ValueType>
+        storm::json<ValueType> unpackStateIntoJson(CompressedState const& state, VariableInformation const& variableInformation, bool onlyObservable) {
+            storm::json<ValueType> result;
+            for (auto const& locationVariable : variableInformation.locationVariables) {
+                if (onlyObservable && !locationVariable.observable)  {
+                    continue;
+                }
+                if (locationVariable.bitWidth != 0) {
+                    result[locationVariable.variable.getName()] = state.getAsInt(locationVariable.bitOffset, locationVariable.bitWidth);
+                } else {
+                    result[locationVariable.variable.getName()] = 0;
+                }
+            }
+            for (auto const& booleanVariable : variableInformation.booleanVariables) {
+                if (onlyObservable && !booleanVariable.observable)  {
+                    continue;
+                }
+                result[booleanVariable.getName()] = state.get(booleanVariable.bitOffset);
+            }
+            for (auto const& integerVariable : variableInformation.integerVariables) {
+                if (onlyObservable && !integerVariable.observable)  {
+                    continue;
+                }
+                result[integerVariable.getName()] = state.getAsInt(integerVariable.bitOffset, integerVariable.bitWidth) + integerVariable.lowerBound;
+            }
+            return result;
+        }
 
-        template void unpackStateIntoEvaluator<double>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<double>& evaluator);
         storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager);
 
         CompressedState createOutOfBoundsState(VariableInformation const& varInfo, bool roundTo64Bit) {
@@ -164,7 +190,11 @@ namespace storm {
             return result;
         }
 
+        template storm::json<double> unpackStateIntoJson<double>(CompressedState const& state, VariableInformation const& variableInformation, bool onlyObservable);
+        template void unpackStateIntoEvaluator<double>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<double>& evaluator);
 #ifdef STORM_HAVE_CARL
+        template storm::json<storm::RationalNumber> unpackStateIntoJson<storm::RationalNumber>(CompressedState const& state, VariableInformation const& variableInformation, bool onlyObservable);
+        template storm::json<storm::RationalFunction> unpackStateIntoJson<storm::RationalFunction>(CompressedState const& state, VariableInformation const& variableInformation, bool onlyObservable);
         template void unpackStateIntoEvaluator<storm::RationalNumber>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<storm::RationalNumber>& evaluator);
         template void unpackStateIntoEvaluator<storm::RationalFunction>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<storm::RationalFunction>& evaluator);
 #endif

src/storm/generator/CompressedState.h

@@ -2,6 +2,7 @@
 #define STORM_GENERATOR_COMPRESSEDSTATE_H_
 
 #include "storm/storage/BitVector.h"
+#include "storm/adapters/JsonAdapter.h"
 #include <map>
 #include <unordered_map>
 
@@ -41,6 +42,17 @@ namespace storm {
          */
         storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager);
 
+        /**
+         *
+         * @tparam ValueType  (The ValueType does not matter for the string representation.)
+         * @param state The state to export
+         * @param variableInformation Variable information to extract from the state
+         * @param onlyObservable Should we only export the observable information
+         * @return
+         */
+        template<typename ValueType>
+        storm::json<ValueType> unpackStateIntoJson(CompressedState const& state, VariableInformation const& variableInformation, bool onlyObservable);
+
         /*!
          * Appends the values of the given variables in the given state to the corresponding result vectors.
          * locationValues are inserted before integerValues (relevant if both, locationValues and integerValues actually refer to the same vector)

src/storm/generator/NextStateGenerator.cpp

@@ -257,12 +257,25 @@ namespace storm {
                 }
             }
         }
-        
+
         template<typename ValueType, typename StateType>
         std::string NextStateGenerator<ValueType, StateType>::stateToString(CompressedState const& state) const {
             return toString(state, variableInformation);
         }
-        
+
+        template<typename ValueType, typename StateType>
+        storm::json<ValueType> NextStateGenerator<ValueType, StateType>::currentStateToJson(bool onlyObservable) const {
+            storm::json<ValueType> result = unpackStateIntoJson<ValueType>(*state, variableInformation, onlyObservable);
+            extendStateInformation(result,onlyObservable);
+            return result;
+        }
+
+        template<typename ValueType, typename StateType>
+        void NextStateGenerator<ValueType, StateType>::extendStateInformation(storm::json<ValueType>&, bool) const {
+            // Intentionally left empty.
+        }
+
+
         template<typename ValueType, typename StateType>
         std::shared_ptr<storm::storage::sparse::ChoiceOrigins> NextStateGenerator<ValueType, StateType>::generateChoiceOrigins(std::vector<boost::any>& dataForChoiceOrigins) const {
             STORM_LOG_ERROR_COND(!options.isBuildChoiceOriginsSet(), "Generating choice origins is not supported for the considered model format.");

src/storm/generator/NextStateGenerator.h

@@ -72,6 +72,8 @@ namespace storm {
             
             std::string stateToString(CompressedState const& state) const;
 
+            storm::json<ValueType> currentStateToJson(bool onlyObservable = false) const;
+
             uint32_t observabilityClass(CompressedState const& state) const;
 
             virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) = 0;
@@ -106,6 +108,8 @@ namespace storm {
             
             virtual storm::storage::BitVector evaluateObservationLabels(CompressedState const& state) const =0;
 
+            virtual void extendStateInformation(storm::json<ValueType>& stateInfo, bool onlyObservable = false) const;
+
             virtual storm::storage::sparse::StateValuationsBuilder initializeObservationValuationsBuilder() const;
 
             void postprocess(StateBehavior<ValueType, StateType>& result);

src/storm/generator/PrismNextStateGenerator.cpp

@@ -727,15 +727,26 @@ namespace storm {
         template<typename ValueType, typename StateType>
         storm::storage::BitVector PrismNextStateGenerator<ValueType, StateType>::evaluateObservationLabels(CompressedState const& state) const {
             // TODO consider to avoid reloading by computing these bitvectors in an earlier build stage
-            unpackStateIntoEvaluator(state, this->variableInformation, *this->evaluator);
-
             storm::storage::BitVector result(program.getNumberOfObservationLabels() * 64);
+
+            if (program.getNumberOfObservationLabels() == 0) {
+                return result;
+            }
+            unpackStateIntoEvaluator(state, this->variableInformation, *this->evaluator);
             for (uint64_t i = 0; i < program.getNumberOfObservationLabels(); ++i) {
                 result.setFromInt(64*i,64,this->evaluator->asInt(program.getObservationLabels()[i].getStatePredicateExpression()));
             }
             return result;
         }
 
+        template<typename ValueType, typename StateType>
+        void PrismNextStateGenerator<ValueType, StateType>::extendStateInformation(storm::json<ValueType>& result, bool onlyObservable) const {
+
+            for (uint64_t i = 0; i < program.getNumberOfObservationLabels(); ++i) {
+                result[program.getObservationLabels()[i].getName()] = this->evaluator->asInt(program.getObservationLabels()[i].getStatePredicateExpression());
+            }
+        }
+
 
         template<typename ValueType, typename StateType>
         std::size_t PrismNextStateGenerator<ValueType, StateType>::getNumberOfRewardModels() const {

src/storm/generator/PrismNextStateGenerator.h

@@ -101,6 +101,10 @@ namespace storm {
              */
             void addLabeledChoices(std::vector<Choice<ValueType>>& choices, CompressedState const& state, StateToIdCallback stateToIdCallback, CommandFilter const& commandFilter = CommandFilter::All);
 
+            /*
+             * Extend the Json struct with additional information about the state.
+             */
+            virtual void extendStateInformation(storm::json<ValueType>& stateInfo, bool onlyObservable = false) const override;
 
             /*!
              * Evaluate observation labels

src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.h

@@ -46,7 +46,6 @@ namespace storm {
                 virtual std::vector<ValueType> getOverApproximationOfInitialStateResults() const override;
                 
             private:
-                
                 struct EpochCheckingData {
                 
                     std::vector<ValueType> bMinMax;
@@ -73,8 +72,6 @@ namespace storm {
                 
                 boost::optional<std::vector<ValueType>> underApproxResult;
                 boost::optional<std::vector<ValueType>> overApproxResult;
-
-                
             };
             
         }

src/storm/simulator/PrismProgramSimulator.cpp

@@ -38,7 +38,8 @@ namespace storm {
         bool DiscreteTimePrismProgramSimulator<ValueType>::explore() {
             // Load the current state into the next state generator.
             stateGenerator->load(currentState);
-            // TODO: This low-level code currently expands all actions, while this may not be necessary.
+            // TODO: This low-level code currently expands all actions, while this is not necessary.
+            // However, using the next state generator ensures compatibliity with the model generator.
             behavior = stateGenerator->expand(stateToIdCallback);
             if (behavior.getStateRewards().size() > 0) {
                 STORM_LOG_ASSERT(behavior.getStateRewards().size() == lastActionRewards.size(), "Reward vectors should have same length.");
@@ -47,7 +48,27 @@ namespace storm {
         }
 
         template<typename ValueType>
-        std::vector<generator::Choice<ValueType, uint32_t>> const& DiscreteTimePrismProgramSimulator<ValueType>::getChoices() {
+        bool DiscreteTimePrismProgramSimulator<ValueType>::isSinkState() const {
+            if(behavior.empty()) {
+                return true;
+            }
+            std::set<uint32_t> successorIds;
+            for (Choice<ValueType,uint32_t> const& choice : behavior.getChoices()) {
+                for (auto it = choice.begin(); it != choice.end(); ++it) {
+                    successorIds.insert(it->first);
+                    if (successorIds.size() > 1) {
+                        return false;
+                    }
+                }
+            }
+            if (idToState.at(*(successorIds.begin())) == currentState) {
+                return true;
+            }
+            return false;
+        }
+
+        template<typename ValueType>
+        std::vector<generator::Choice<ValueType, uint32_t>> const& DiscreteTimePrismProgramSimulator<ValueType>::getChoices() const {
             return behavior.getChoices();
         }
 
@@ -71,6 +92,16 @@ namespace storm {
             return stateGenerator->stateToString(currentState);
         }
 
+        template<typename ValueType>
+        storm::json<ValueType> DiscreteTimePrismProgramSimulator<ValueType>::getStateAsJson() const {
+            return stateGenerator->currentStateToJson(false);
+        }
+
+        template<typename ValueType>
+        storm::json<ValueType> DiscreteTimePrismProgramSimulator<ValueType>::getObservationAsJson() const {
+            return stateGenerator->currentStateToJson(true);
+        }
+
         template<typename ValueType>
         bool DiscreteTimePrismProgramSimulator<ValueType>::resetToInitial() {
             auto indices = stateGenerator->getInitialStates(stateToIdCallback);

src/storm/simulator/PrismProgramSimulator.h

@@ -5,7 +5,6 @@
 #include "storm/generator/PrismNextStateGenerator.h"
 #include "storm/utility/random.h"
 
-
 namespace storm {
     namespace simulator {
 
@@ -41,7 +40,10 @@ namespace storm {
              *
              * @return A list of choices that encode the possibilities in the current state.
              */
-            std::vector<generator::Choice<ValueType, uint32_t>> const& getChoices();
+            std::vector<generator::Choice<ValueType, uint32_t>> const& getChoices() const;
+
+            bool isSinkState() const;
+
             /**
              * Make a step and randomly select the successor. The action is given as an argument, the index reflects the index of the getChoices vector that can be accessed.
              *
@@ -57,6 +59,10 @@ namespace storm {
             generator::CompressedState const& getCurrentState() const;
             expressions::SimpleValuation getCurrentStateAsValuation() const;
 
+            storm::json<ValueType> getStateAsJson() const;
+
+            storm::json<ValueType> getObservationAsJson() const;
+
             std::string getCurrentStateString() const;
             /**
              * Reset to the (unique) initial state.
@@ -78,7 +84,7 @@ namespace storm {
             generator::CompressedState currentState;
             /// Generator for the next states
             std::shared_ptr<storm::generator::PrismNextStateGenerator<ValueType, uint32_t>> stateGenerator;
-            bool explored = false;
+            /// Obtained behavior of a state
             generator::StateBehavior<ValueType> behavior;
             /// Helper for last action reward construction
             std::vector<ValueType> zeroRewards;

src/storm/storage/expressions/ExpressionStringFormat.h

@@ -0,0 +1,9 @@
+#pragma once
+
+namespace storm {
+    namespace expressions {
+        struct ExpressionStringFormat {
+            bool alternativeIff = false;
+        };
+    }
+}

src/storm/storage/prism/OverlappingGuardAnalyser.cpp

@@ -0,0 +1,58 @@
+#include "storm/storage/prism/OverlappingGuardAnalyser.h"
+#include "storm/storage/prism/Program.h"
+#include "storm/solver/SmtSolver.h"
+
+
+namespace storm {
+    namespace prism {
+        OverlappingGuardAnalyser::OverlappingGuardAnalyser(Program const& program, std::shared_ptr<storm::utility::solver::SmtSolverFactory>& smtSolverFactory) :
+                program(program), smtSolver(smtSolverFactory->create(program.getManager())), initializedWithStateConstraints(false) {
+            // Intentionally left empty.
+        }
+
+
+        bool OverlappingGuardAnalyser::hasModuleWithInnerActionOverlap() {
+            if(!initializedWithStateConstraints) {
+                for(auto const& integerVariable : program.getGlobalIntegerVariables()) {
+                    smtSolver->add(integerVariable.getExpressionVariable().getExpression() >= integerVariable.getLowerBoundExpression());
+                    smtSolver->add(integerVariable.getExpressionVariable().getExpression() <= integerVariable.getUpperBoundExpression());
+                }
+                for (auto const& module : program.getModules()) {
+                    for(auto const& integerVariable : module.getIntegerVariables()) {
+                        smtSolver->add(integerVariable.getExpressionVariable().getExpression() >= integerVariable.getLowerBoundExpression());
+                        smtSolver->add(integerVariable.getExpressionVariable().getExpression() <= integerVariable.getUpperBoundExpression());
+                    }
+                }
+            }
+
+            for(auto const& module : program.getModules()) {
+                for (auto const& actionIndex : module.getSynchronizingActionIndices()) {
+                    auto const& commandIndices = module.getCommandIndicesByActionIndex(actionIndex);
+                    if (commandIndices.size() == 1) {
+                        continue;
+                    } else {
+                        for (uint64_t commandIndexA : commandIndices) {
+                            for (uint64_t commandIndexB : commandIndices) {
+                                if (commandIndexA == commandIndexB) {
+                                    continue;
+                                }
+                                smtSolver->push();
+                                smtSolver->add(module.getCommand(commandIndexA).getGuardExpression());
+                                smtSolver->add(module.getCommand(commandIndexB).getGuardExpression());
+                                auto smtCheckResult = smtSolver->check();
+                                smtSolver->pop();
+                                if (smtCheckResult == storm::solver::SmtSolver::CheckResult::Sat) {
+                                    return true;
+                                }
+                            }
+                        }
+                    }
+
+
+                }
+            }
+            return false;
+        }
+
+    }
+}

src/storm/storage/prism/OverlappingGuardAnalyser.h

@@ -0,0 +1,32 @@
+#pragma once
+#include <cstdint>
+#include <memory>
+
+namespace storm {
+    namespace utility {
+        namespace solver {
+            class SmtSolverFactory;
+        }
+    }
+
+    namespace solver {
+        class SmtSolver;
+    }
+
+    namespace prism {
+        class Program;
+        class Module;
+
+        class OverlappingGuardAnalyser {
+        public:
+            OverlappingGuardAnalyser(Program const& program, std::shared_ptr<storm::utility::solver::SmtSolverFactory>& smtSolverFactory);
+            bool hasModuleWithInnerActionOverlap();
+
+        private:
+            Program const& program;
+            std::unique_ptr<storm::solver::SmtSolver> smtSolver;
+            bool initializedWithStateConstraints;
+        };
+    }
+}
+

src/storm/utility/random.h

@@ -1,3 +1,5 @@
+#pragma once
+
 #include <random>
 #include "storm/adapters/RationalNumberAdapter.h"