From 000a8c2d77d12951c37b6292be2bb4e9ae696f24 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 14 Jun 2016 16:59:41 +0200 Subject: [PATCH] more work on JANI next-state generator Former-commit-id: d94ab2b81e93ca786a30f529ddb74b36dc0c0862 --- src/generator/JaniNextStateGenerator.cpp | 261 ++++++++++++------ src/generator/JaniNextStateGenerator.h | 134 +++++---- src/generator/PrismNextStateGenerator.cpp | 59 +++- src/generator/VariableInformation.cpp | 73 +++-- src/generator/VariableInformation.h | 35 +-- src/storage/jani/Automaton.cpp | 7 + src/storage/jani/Automaton.h | 5 + src/storage/jani/BoundedIntegerVariable.cpp | 4 + src/storage/jani/BoundedIntegerVariable.h | 5 + .../jani/CompositionInformationVisitor.cpp | 92 ++++++ .../jani/CompositionInformationVisitor.h | 60 ++++ src/storage/jani/CompositionVisitor.h | 1 + src/storage/jani/Compositions.h | 3 + src/storage/jani/EdgeDestination.cpp | 14 +- src/storage/jani/EdgeDestination.h | 6 + src/storage/jani/Model.cpp | 13 + src/storage/jani/Model.h | 5 + src/storage/prism/IntegerVariable.cpp | 4 + src/storage/prism/IntegerVariable.h | 7 + src/storage/prism/Module.cpp | 19 ++ src/storage/prism/Module.h | 16 ++ src/storage/prism/Program.cpp | 34 +++ src/storage/prism/Program.h | 14 + src/storage/prism/Update.cpp | 8 +- 24 files changed, 663 insertions(+), 216 deletions(-) create mode 100644 src/storage/jani/CompositionInformationVisitor.cpp create mode 100644 src/storage/jani/CompositionInformationVisitor.h create mode 100644 src/storage/jani/Compositions.h diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index fc213467a..eea91cb0b 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -1,89 +1,172 @@ -//#include "src/generator/JaniNextStateGenerator.h" -// -//#include "src/models/sparse/StateLabeling.h" -// -//#include "src/storage/expressions/SimpleValuation.h" -// -//#include "src/utility/constants.h" -//#include "src/utility/macros.h" -//#include "src/exceptions/InvalidSettingsException.h" -//#include "src/exceptions/WrongFormatException.h" -// -//namespace storm { -// namespace generator { -// -// template -// JaniNextStateGenerator::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options) : NextStateGenerator(options), model(model.substituteConstants()), variableInformation(this->model), evaluator(this->model.getManager()), state(nullptr), comparator() { -// STORM_LOG_THROW(!this->model.hasDefaultComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions."); -// STORM_LOG_THROW(!this->options.isBuildAllRewardModelsSet() && this->options.getRewardModelNames().empty(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support building reward models."); -// -// // If there are terminal states we need to handle, we now need to translate all labels to expressions. -// if (this->options.hasTerminalStates()) { -// for (auto const& expressionOrLabelAndBool : this->options.getTerminalStates()) { -// if (expressionOrLabelAndBool.first.isExpression()) { -// terminalStates.push_back(std::make_pair(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second)); -// } else { -// STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Cannot make label terminal for JANI models."); -// } -// } -// } -// } -// -// template -// uint64_t JaniNextStateGenerator::getStateSize() const { -// return variableInformation.getTotalBitOffset(true); -// } -// -// template -// ModelType JaniNextStateGenerator::getModelType() const { -// switch (model.getModelType()) { -// case storm::jani::ModelType::DTMC: return ModelType::DTMC; -// case storm::jani::ModelType::CTMC: return ModelType::CTMC; -// case storm::jani::ModelType::MDP: return ModelType::MDP; -// case storm::jani::ModelType::MA: return ModelType::MA; -// default: -// STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Invalid model type."); -// } -// } -// -// template -// bool JaniNextStateGenerator::isDeterministicModel() const { -// return model.isDeterministicModel(); -// } -// -// template -// std::vector JaniNextStateGenerator::getInitialStates(StateToIdCallback const& stateToIdCallback) { -// // FIXME: This only works for models with exactly one initial state. We should make this more general. -// CompressedState initialState(variableInformation.getTotalBitOffset()); -// -// // We need to initialize the values of the variables to their initial value. -// for (auto const& booleanVariable : variableInformation.booleanVariables) { -// initialState.set(booleanVariable.bitOffset, booleanVariable.initialValue); -// } -// for (auto const& integerVariable : variableInformation.integerVariables) { -// initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast(integerVariable.initialValue - integerVariable.lowerBound)); -// } -// -// // Register initial state and return it. -// StateType id = stateToIdCallback(initialState); -// return {id}; -// } -// -// template -// void JaniNextStateGenerator::load(CompressedState const& state) { -// // Since almost all subsequent operations are based on the evaluator, we load the state into it now. -// unpackStateIntoEvaluator(state, variableInformation, evaluator); -// -// // Also, we need to store a pointer to the state itself, because we need to be able to access it when expanding it. -// this->state = &state; -// } -// -// template -// bool JaniNextStateGenerator::satisfies(storm::expressions::Expression const& expression) const { -// if (expression.isTrue()) { -// return true; -// } -// return evaluator.asBool(expression); -// } -// } -//} \ No newline at end of file +#include "src/generator/JaniNextStateGenerator.h" + +#include "src/models/sparse/StateLabeling.h" + +#include "src/storage/expressions/SimpleValuation.h" + +#include "src/solver/SmtSolver.h" + +#include "src/utility/constants.h" +#include "src/utility/macros.h" +#include "src/utility/solver.h" +#include "src/exceptions/InvalidSettingsException.h" +#include "src/exceptions/WrongFormatException.h" + +namespace storm { + namespace generator { + + template + JaniNextStateGenerator::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options) : JaniNextStateGenerator(model.substituteConstants(), options, false) { + // Intentionally left empty. + } + + template + JaniNextStateGenerator::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator(model.getExpressionManager(), VariableInformation(model), options), model(model) { + STORM_LOG_THROW(!this->model.hasDefaultComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions."); + STORM_LOG_THROW(!this->options.isBuildAllRewardModelsSet() && this->options.getRewardModelNames().empty(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support building reward models."); + + // If there are terminal states we need to handle, we now need to translate all labels to expressions. + if (this->options.hasTerminalStates()) { + for (auto const& expressionOrLabelAndBool : this->options.getTerminalStates()) { + if (expressionOrLabelAndBool.first.isExpression()) { + this->terminalStates.push_back(std::make_pair(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second)); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Cannot make label terminal for JANI models."); + } + } + } + } + + template + ModelType JaniNextStateGenerator::getModelType() const { + switch (model.getModelType()) { + case storm::jani::ModelType::DTMC: return ModelType::DTMC; + case storm::jani::ModelType::CTMC: return ModelType::CTMC; + case storm::jani::ModelType::MDP: return ModelType::MDP; + case storm::jani::ModelType::MA: return ModelType::MA; + default: + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Invalid model type."); + } + } + + template + bool JaniNextStateGenerator::isDeterministicModel() const { + return model.isDeterministicModel(); + } + + template + std::vector JaniNextStateGenerator::getInitialStates(StateToIdCallback const& stateToIdCallback) { + // Prepare an SMT solver to enumerate all initial states. + storm::utility::solver::SmtSolverFactory factory; + std::unique_ptr solver = factory.create(model.getExpressionManager()); + + std::vector rangeExpressions = model.getAllRangeExpressions(); + for (auto const& expression : rangeExpressions) { + solver->add(expression); + } + solver->add(model.getInitialStatesExpression(true)); + + // Proceed ss long as the solver can still enumerate initial states. + std::vector initialStateIndices; + while (solver->check() == storm::solver::SmtSolver::CheckResult::Sat) { + // Create fresh state. + CompressedState initialState(this->variableInformation.getTotalBitOffset()); + + // Read variable assignment from the solution of the solver. Also, create an expression we can use to + // prevent the variable assignment from being enumerated again. + storm::expressions::Expression blockingExpression; + std::shared_ptr model = solver->getModel(); + for (auto const& booleanVariable : this->variableInformation.booleanVariables) { + bool variableValue = model->getBooleanValue(booleanVariable.variable); + storm::expressions::Expression localBlockingExpression = variableValue ? !booleanVariable.variable : booleanVariable.variable; + blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; + initialState.set(booleanVariable.bitOffset, variableValue); + } + for (auto const& integerVariable : this->variableInformation.integerVariables) { + int_fast64_t variableValue = model->getIntegerValue(integerVariable.variable); + storm::expressions::Expression localBlockingExpression = integerVariable.variable != model->getManager().integer(variableValue); + blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; + initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast(variableValue - integerVariable.lowerBound)); + } + + // Register initial state and return it. + StateType id = stateToIdCallback(initialState); + initialStateIndices.push_back(id); + + // Block the current initial state to search for the next one. + solver->add(blockingExpression); + } + + return initialStateIndices; + } + + template + CompressedState JaniNextStateGenerator::applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& destination) { + CompressedState newState(state); + + auto assignmentIt = destination.getAssignments().begin(); + auto assignmentIte = destination.getAssignments().end(); + + // Iterate over all boolean assignments and carry them out. + auto boolIt = this->variableInformation.booleanVariables.begin(); + for (; assignmentIt != assignmentIte && assignmentIt->getAssignedExpression().hasBooleanType(); ++assignmentIt) { + while (assignmentIt->getExpressionVariable() != boolIt->variable) { + ++boolIt; + } + newState.set(boolIt->bitOffset, this->evaluator.asBool(assignmentIt->getExpressionVariable())); + } + + // Iterate over all integer assignments and carry them out. + auto integerIt = this->variableInformation.integerVariables.begin(); + for (; assignmentIt != assignmentIte && assignmentIt->getAssignedExpression().hasIntegerType(); ++assignmentIt) { + while (assignmentIt->getExpressionVariable() != integerIt->variable) { + ++integerIt; + } + int_fast64_t assignedValue = this->evaluator.asInt(assignmentIt->getAssignedExpression()); + STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getExpressionVariable().getName() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'."); + newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound); + STORM_LOG_ASSERT(static_cast(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ")."); + } + + // Check that we processed all assignments. + STORM_LOG_ASSERT(assignmentIt == assignmentIte, "Not all assignments were consumed."); + + return newState; + } + + template + StateBehavior JaniNextStateGenerator::expand(StateToIdCallback const& stateToIdCallback) { + + } + + template + std::vector> JaniNextStateGenerator::getSilentActionChoices(CompressedState const& state, StateToIdCallback stateToIdCallback) { + + } + + template + std::vector> JaniNextStateGenerator::getNonsilentActionChoices(CompressedState const& state, StateToIdCallback stateToIdCallback) { + + } + + template + std::size_t JaniNextStateGenerator::getNumberOfRewardModels() const { + return 0; + } + + template + RewardModelInformation JaniNextStateGenerator::getRewardModelInformation(uint64_t const& index) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Cannot retrieve reward model information."); + return RewardModelInformation("", false, false, false); + } + + template + storm::models::sparse::StateLabeling JaniNextStateGenerator::label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices) { + return NextStateGenerator::label(states, initialStateIndices, {}); + } + + template class JaniNextStateGenerator; + template class JaniNextStateGenerator; + + } +} \ No newline at end of file diff --git a/src/generator/JaniNextStateGenerator.h b/src/generator/JaniNextStateGenerator.h index b93f5a9db..24d62d456 100644 --- a/src/generator/JaniNextStateGenerator.h +++ b/src/generator/JaniNextStateGenerator.h @@ -1,68 +1,66 @@ -//#pragma once -// -//#include "src/generator/NextStateGenerator.h" -//#include "src/generator/VariableInformation.h" -// -//#include "src/storage/jani/Model.h" -//#include "src/storage/expressions/ExpressionEvaluator.h" -// -//#include "src/utility/ConstantsComparator.h" -// -//namespace storm { -// namespace generator { -// -// template -// class JaniNextStateGenerator : public NextStateGenerator { -// public: -// typedef typename NextStateGenerator::StateToIdCallback StateToIdCallback; -// -// JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options = NextStateGeneratorOptions()); -// -// virtual uint64_t getStateSize() const override; -// virtual ModelType getModelType() const override; -// virtual bool isDeterministicModel() const override; -// virtual std::vector getInitialStates(StateToIdCallback const& stateToIdCallback) override; -// -// virtual void load(CompressedState const& state) override; -// virtual StateBehavior expand(StateToIdCallback const& stateToIdCallback) override; -// virtual bool satisfies(storm::expressions::Expression const& expression) const override; -// -// virtual std::size_t getNumberOfRewardModels() const override; -// virtual RewardModelInformation getRewardModelInformation(uint64_t const& index) const override; -// -// virtual storm::expressions::SimpleValuation toValuation(CompressedState const& state) const override; -// -// virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices = {}) override; -// -// private: -// /*! -// * Applies an update to the state currently loaded into the evaluator and applies the resulting values to -// * the given compressed state. -// * @params state The state to which to apply the new values. -// * @params update The update to apply. -// * @return The resulting state. -// */ -// CompressedState applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& update); -// -// /*! -// * Retrieves all choices labeled with the silent action possible from the given state. -// * -// * @param state The state for which to retrieve the silent choices. -// * @return The silent action choices of the state. -// */ -// std::vector> getSilentActionChoices(CompressedState const& state, StateToIdCallback stateToIdCallback); -// -// /*! -// * Retrieves all choices labeled with some non-silent action possible from the given state. -// * -// * @param state The state for which to retrieve the non-silent choices. -// * @return The non-silent action choices of the state. -// */ -// std::vector> getNonsilentActionChoices(CompressedState const& state, StateToIdCallback stateToIdCallback); -// -// // The model used for the generation of next states. -// storm::jani::Model model; -// }; -// -// } -//} \ No newline at end of file +#pragma once + +#include "src/generator/NextStateGenerator.h" + +#include "src/storage/jani/Model.h" + +namespace storm { + namespace generator { + + template + class JaniNextStateGenerator : public NextStateGenerator { + public: + typedef typename NextStateGenerator::StateToIdCallback StateToIdCallback; + + JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options = NextStateGeneratorOptions()); + + virtual ModelType getModelType() const override; + virtual bool isDeterministicModel() const override; + virtual std::vector getInitialStates(StateToIdCallback const& stateToIdCallback) override; + + virtual StateBehavior expand(StateToIdCallback const& stateToIdCallback) override; + + virtual std::size_t getNumberOfRewardModels() const override; + virtual RewardModelInformation getRewardModelInformation(uint64_t const& index) const override; + + virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices = {}) override; + + private: + /*! + * A delegate constructor that is used to preprocess the model before the constructor of the superclass is + * being called. The last argument is only present to distinguish the signature of this constructor from the + * public one. + */ + JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool flag); + + /*! + * Applies an update to the state currently loaded into the evaluator and applies the resulting values to + * the given compressed state. + * @params state The state to which to apply the new values. + * @params update The update to apply. + * @return The resulting state. + */ + CompressedState applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& update); + + /*! + * Retrieves all choices labeled with the silent action possible from the given state. + * + * @param state The state for which to retrieve the silent choices. + * @return The silent action choices of the state. + */ + std::vector> getSilentActionChoices(CompressedState const& state, StateToIdCallback stateToIdCallback); + + /*! + * Retrieves all choices labeled with some non-silent action possible from the given state. + * + * @param state The state for which to retrieve the non-silent choices. + * @return The non-silent action choices of the state. + */ + std::vector> getNonsilentActionChoices(CompressedState const& state, StateToIdCallback stateToIdCallback); + + // The model used for the generation of next states. + storm::jani::Model model; + }; + + } +} \ No newline at end of file diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp index c1e70e1ab..7a530432b 100644 --- a/src/generator/PrismNextStateGenerator.cpp +++ b/src/generator/PrismNextStateGenerator.cpp @@ -6,6 +6,8 @@ #include "src/storage/expressions/SimpleValuation.h" +#include "src/solver/SmtSolver.h" + #include "src/utility/constants.h" #include "src/utility/macros.h" #include "src/exceptions/InvalidArgumentException.h" @@ -20,7 +22,7 @@ namespace storm { } template - PrismNextStateGenerator::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator(program.getManager(), VariableInformation(program), options), program(program.substituteConstants()), rewardModels() { + PrismNextStateGenerator::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator(program.getManager(), VariableInformation(program), options), program(program), rewardModels() { STORM_LOG_THROW(!this->program.specifiesSystemComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions."); if (this->options.isBuildAllRewardModelsSet()) { @@ -82,20 +84,48 @@ namespace storm { template std::vector PrismNextStateGenerator::getInitialStates(StateToIdCallback const& stateToIdCallback) { - // FIXME: This only works for models with exactly one initial state. We should make this more general. - CompressedState initialState(this->variableInformation.getTotalBitOffset()); + // Prepare an SMT solver to enumerate all initial states. + storm::utility::solver::SmtSolverFactory factory; + std::unique_ptr solver = factory.create(program.getManager()); - // We need to initialize the values of the variables to their initial value. - for (auto const& booleanVariable : this->variableInformation.booleanVariables) { - initialState.set(booleanVariable.bitOffset, booleanVariable.initialValue); + std::vector rangeExpressions = program.getAllRangeExpressions(); + for (auto const& expression : rangeExpressions) { + solver->add(expression); } - for (auto const& integerVariable : this->variableInformation.integerVariables) { - initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast(integerVariable.initialValue - integerVariable.lowerBound)); + solver->add(program.getInitialConstruct().getInitialStatesExpression()); + + // Proceed ss long as the solver can still enumerate initial states. + std::vector initialStateIndices; + while (solver->check() == storm::solver::SmtSolver::CheckResult::Sat) { + // Create fresh state. + CompressedState initialState(this->variableInformation.getTotalBitOffset()); + + // Read variable assignment from the solution of the solver. Also, create an expression we can use to + // prevent the variable assignment from being enumerated again. + storm::expressions::Expression blockingExpression; + std::shared_ptr model = solver->getModel(); + for (auto const& booleanVariable : this->variableInformation.booleanVariables) { + bool variableValue = model->getBooleanValue(booleanVariable.variable); + storm::expressions::Expression localBlockingExpression = variableValue ? !booleanVariable.variable : booleanVariable.variable; + blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; + initialState.set(booleanVariable.bitOffset, variableValue); + } + for (auto const& integerVariable : this->variableInformation.integerVariables) { + int_fast64_t variableValue = model->getIntegerValue(integerVariable.variable); + storm::expressions::Expression localBlockingExpression = integerVariable.variable != model->getManager().integer(variableValue); + blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; + initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast(variableValue - integerVariable.lowerBound)); + } + + // Register initial state and return it. + StateType id = stateToIdCallback(initialState); + initialStateIndices.push_back(id); + + // Block the current initial state to search for the next one. + solver->add(blockingExpression); } - - // Register initial state and return it. - StateType id = stateToIdCallback(initialState); - return {id}; + + return initialStateIndices; } template @@ -202,6 +232,11 @@ namespace storm { CompressedState PrismNextStateGenerator::applyUpdate(CompressedState const& state, storm::prism::Update const& update) { CompressedState newState(state); + // NOTE: the following process assumes that the assignments of the update are ordered in such a way that the + // assignments to boolean variables precede the assignments to all integer variables and that within the + // types, the assignments to variables are ordered (in ascending order) by the expression variables. + // This is guaranteed for PRISM models, by sorting the assignments as soon as an update is created. + auto assignmentIt = update.getAssignments().begin(); auto assignmentIte = update.getAssignments().end(); diff --git a/src/generator/VariableInformation.cpp b/src/generator/VariableInformation.cpp index a5be93a6e..1c7fc7a60 100644 --- a/src/generator/VariableInformation.cpp +++ b/src/generator/VariableInformation.cpp @@ -1,48 +1,78 @@ #include "src/generator/VariableInformation.h" +#include "src/storage/prism/Program.h" +#include "src/storage/jani/Model.h" + #include "src/utility/macros.h" #include "src/exceptions/InvalidArgumentException.h" namespace storm { namespace generator { - BooleanVariableInformation::BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset) : variable(variable), initialValue(initialValue), bitOffset(bitOffset) { + BooleanVariableInformation::BooleanVariableInformation(storm::expressions::Variable const& variable, uint_fast64_t bitOffset) : variable(variable), bitOffset(bitOffset) { // Intentionally left empty. } - IntegerVariableInformation::IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t initialValue, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth) : variable(variable), initialValue(initialValue), lowerBound(lowerBound), upperBound(upperBound), bitOffset(bitOffset), bitWidth(bitWidth) { + IntegerVariableInformation::IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth) : variable(variable), lowerBound(lowerBound), upperBound(upperBound), bitOffset(bitOffset), bitWidth(bitWidth) { // Intentionally left empty. } VariableInformation::VariableInformation(storm::prism::Program const& program) : totalBitOffset(0) { for (auto const& booleanVariable : program.getGlobalBooleanVariables()) { - booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), booleanVariable.getInitialValueExpression().evaluateAsBool(), totalBitOffset); + booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), totalBitOffset); ++totalBitOffset; - booleanVariableToIndexMap[booleanVariable.getExpressionVariable()] = booleanVariables.size() - 1; } for (auto const& integerVariable : program.getGlobalIntegerVariables()) { int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt(); int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt(); uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); - integerVariables.emplace_back(integerVariable.getExpressionVariable(), integerVariable.getInitialValueExpression().evaluateAsInt(), lowerBound, upperBound, totalBitOffset, bitwidth); + integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth); totalBitOffset += bitwidth; - integerVariableToIndexMap[integerVariable.getExpressionVariable()] = integerVariables.size() - 1; } for (auto const& module : program.getModules()) { for (auto const& booleanVariable : module.getBooleanVariables()) { - booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), booleanVariable.getInitialValueExpression().evaluateAsBool(), totalBitOffset); + booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), totalBitOffset); ++totalBitOffset; - booleanVariableToIndexMap[booleanVariable.getExpressionVariable()] = booleanVariables.size() - 1; } for (auto const& integerVariable : module.getIntegerVariables()) { int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt(); int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt(); uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); - integerVariables.emplace_back(integerVariable.getExpressionVariable(), integerVariable.getInitialValueExpression().evaluateAsInt(), lowerBound, upperBound, totalBitOffset, bitwidth); + integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth); totalBitOffset += bitwidth; - integerVariableToIndexMap[integerVariable.getExpressionVariable()] = integerVariables.size() - 1; } } + + sortVariables(); + } + + VariableInformation::VariableInformation(storm::jani::Model const& model) { + for (auto const& variable : model.getGlobalVariables().getBooleanVariables()) { + booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset); + ++totalBitOffset; + } + for (auto const& variable : model.getGlobalVariables().getBoundedIntegerVariables()) { + int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); + int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); + uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); + integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth); + totalBitOffset += bitwidth; + } + for (auto const& automaton : model.getAutomata()) { + for (auto const& variable : automaton.getVariables().getBooleanVariables()) { + booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset); + ++totalBitOffset; + } + for (auto const& variable : automaton.getVariables().getBoundedIntegerVariables()) { + int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); + int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); + uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); + integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth); + totalBitOffset += bitwidth; + } + } + + sortVariables(); } uint_fast64_t VariableInformation::getTotalBitOffset(bool roundTo64Bit) const { @@ -53,25 +83,10 @@ namespace storm { return result; } - uint_fast64_t VariableInformation::getBitOffset(storm::expressions::Variable const& variable) const { - auto const& booleanIndex = booleanVariableToIndexMap.find(variable); - if (booleanIndex != booleanVariableToIndexMap.end()) { - return booleanVariables[booleanIndex->second].bitOffset; - } - auto const& integerIndex = integerVariableToIndexMap.find(variable); - if (integerIndex != integerVariableToIndexMap.end()) { - return integerVariables[integerIndex->second].bitOffset; - } - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit index of unknown variable."); - } - - uint_fast64_t VariableInformation::getBitWidth(storm::expressions::Variable const& variable) const { - auto const& integerIndex = integerVariableToIndexMap.find(variable); - if (integerIndex != integerVariableToIndexMap.end()) { - return integerVariables[integerIndex->second].bitWidth; - } - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit width of unknown variable."); + void VariableInformation::sortVariables() { + // Sort the variables so we can make some assumptions when iterating over them (in the next-state generators). + std::sort(booleanVariables.begin(), booleanVariables.end(), [] (BooleanVariableInformation const& a, BooleanVariableInformation const& b) { return a.variable < b.variable; } ); + std::sort(integerVariables.begin(), integerVariables.end(), [] (IntegerVariableInformation const& a, IntegerVariableInformation const& b) { return a.variable < b.variable; }); } - } } \ No newline at end of file diff --git a/src/generator/VariableInformation.h b/src/generator/VariableInformation.h index 8c2841dfd..8ee9ac8f6 100644 --- a/src/generator/VariableInformation.h +++ b/src/generator/VariableInformation.h @@ -5,35 +5,36 @@ #include #include "src/storage/expressions/Variable.h" -#include "src/storage/prism/Program.h" namespace storm { + namespace prism { + class Program; + } + + namespace jani { + class Model; + } + namespace generator { // A structure storing information about the boolean variables of the program. struct BooleanVariableInformation { - BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset); + BooleanVariableInformation(storm::expressions::Variable const& variable, uint_fast64_t bitOffset); // The boolean variable. storm::expressions::Variable variable; - // Its initial value. - bool initialValue; - // Its bit offset in the compressed state. uint_fast64_t bitOffset; }; // A structure storing information about the integer variables of the program. struct IntegerVariableInformation { - IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t initialValue, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth); + IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth); // The integer variable. storm::expressions::Variable variable; - // Its initial value. - int_fast64_t initialValue; - // The lower bound of its range. int_fast64_t lowerBound; @@ -49,24 +50,26 @@ namespace storm { // A structure storing information about the used variables of the program. struct VariableInformation { - VariableInformation() = default; VariableInformation(storm::prism::Program const& program); - uint_fast64_t getTotalBitOffset(bool roundTo64Bit = false) const; + VariableInformation(storm::jani::Model const& model); - // Provide methods to access the bit offset and width of variables in the compressed state. - uint_fast64_t getBitOffset(storm::expressions::Variable const& variable) const; - uint_fast64_t getBitWidth(storm::expressions::Variable const& variable) const; + VariableInformation() = default; + uint_fast64_t getTotalBitOffset(bool roundTo64Bit = false) const; // The total bit offset over all variables. uint_fast64_t totalBitOffset; // The known boolean variables. - boost::container::flat_map booleanVariableToIndexMap; std::vector booleanVariables; // The known integer variables. - boost::container::flat_map integerVariableToIndexMap; std::vector integerVariables; + + private: + /*! + * Sorts the variables to establish a known ordering. + */ + void sortVariables(); }; } diff --git a/src/storage/jani/Automaton.cpp b/src/storage/jani/Automaton.cpp index adf74855e..1db2c5bfb 100644 --- a/src/storage/jani/Automaton.cpp +++ b/src/storage/jani/Automaton.cpp @@ -199,5 +199,12 @@ namespace storm { return actionIndices.find(actionIndex) != actionIndices.end(); } + std::vector Automaton::getAllRangeExpressions() const { + std::vector result; + for (auto const& variable : this->getVariables().getBoundedIntegerVariables()) { + result.push_back(variable.getRangeExpression()); + } + return result; + } } } \ No newline at end of file diff --git a/src/storage/jani/Automaton.h b/src/storage/jani/Automaton.h index 61e94a00f..86e3f4a7c 100644 --- a/src/storage/jani/Automaton.h +++ b/src/storage/jani/Automaton.h @@ -230,6 +230,11 @@ namespace storm { */ bool hasEdgeLabeledWithActionIndex(uint64_t actionIndex) const; + /*! + * Retrieves a list of expressions that characterize the legal values of the variables in this automaton. + */ + std::vector getAllRangeExpressions() const; + private: /// The name of the automaton. std::string name; diff --git a/src/storage/jani/BoundedIntegerVariable.cpp b/src/storage/jani/BoundedIntegerVariable.cpp index 165e1d0e8..7ef1774fc 100644 --- a/src/storage/jani/BoundedIntegerVariable.cpp +++ b/src/storage/jani/BoundedIntegerVariable.cpp @@ -23,6 +23,10 @@ namespace storm { this->upperBound = expression; } + storm::expressions::Expression BoundedIntegerVariable::getRangeExpression() const { + return this->getLowerBound() <= this->getExpressionVariable() && this->getExpressionVariable() <= this->getUpperBound(); + } + bool BoundedIntegerVariable::isBoundedIntegerVariable() const { return true; } diff --git a/src/storage/jani/BoundedIntegerVariable.h b/src/storage/jani/BoundedIntegerVariable.h index 43212992c..bc2298d05 100644 --- a/src/storage/jani/BoundedIntegerVariable.h +++ b/src/storage/jani/BoundedIntegerVariable.h @@ -33,6 +33,11 @@ namespace storm { */ void setUpperBound(storm::expressions::Expression const& expression); + /*! + * Retrieves an expression characterizing the legal range of the bounded integer variable. + */ + storm::expressions::Expression getRangeExpression() const; + virtual bool isBoundedIntegerVariable() const override; private: diff --git a/src/storage/jani/CompositionInformationVisitor.cpp b/src/storage/jani/CompositionInformationVisitor.cpp new file mode 100644 index 000000000..496332fd1 --- /dev/null +++ b/src/storage/jani/CompositionInformationVisitor.cpp @@ -0,0 +1,92 @@ +#include "src/storage/jani/CompositionInformationVisitor.h" + +#include "src/storage/jani/Model.h" +#include "src/storage/jani/Compositions.h" + +namespace storm { + namespace jani { + + CompositionInformation::CompositionInformation(std::map const& automatonNameToMultiplicity, std::set const& nonsilentActions, bool containsRenameComposition, bool containsRestrictedParallelComposition) : automatonNameToMultiplicity(automatonNameToMultiplicity), nonsilentActions(nonsilentActions), renameComposition(containsRenameComposition), restrictedParallelComposition(containsRestrictedParallelComposition) { + // Intentionally left empty. + } + + void CompositionInformation::increaseAutomatonMultiplicity(std::string const& automatonName, uint64_t count) { + automatonNameToMultiplicity[automatonName] += count; + } + + void CompositionInformation::addNonsilentAction(std::string const& actionName) { + // FIXME + } + + std::set const& CompositionInformation::getNonsilentActions() const { + // FIXME + } + + void CompositionInformation::renameNonsilentActions(std::map const& renaming) { + // FIXME + } + + void CompositionInformation::setContainsRenameComposition() { + renameComposition = true; + } + + bool CompositionInformation::containsRenameComposition() const { + return renameComposition; + } + + void CompositionInformation::setContainsRestrictedParallelComposition() { + restrictedParallelComposition = true; + } + + bool CompositionInformation::containsRestrictedParallelComposition() const { + return restrictedParallelComposition; + } + + std::map CompositionInformation::joinMultiplicityMaps(std::map const& first, std::map const& second) { + std::map result = first; + for (auto const& element : second) { + result[element.first] += element.second; + } + return result; + } + + std::map const& CompositionInformation::getAutomatonToMultiplicityMap() const { + return automatonNameToMultiplicity; + } + + CompositionInformation CompositionInformationVisitor::getInformation(Composition const& composition, Model const& model) { + return boost::any_cast(composition.accept(*this, model)); + } + + boost::any CompositionInformationVisitor::visit(AutomatonComposition const& composition, boost::any const& data) { + CompositionInformation result; + result.increaseAutomatonMultiplicity(composition.getAutomatonName()); + return result; + } + + boost::any CompositionInformationVisitor::visit(RenameComposition const& composition, boost::any const& data) { + CompositionInformation subresult = boost::any_cast(composition.getSubcomposition().accept(*this, data)); + subresult.setContainsRenameComposition(); + return subresult; + } + + boost::any CompositionInformationVisitor::visit(ParallelComposition const& composition, boost::any const& data) { + Model const& model = boost::any_cast(data); + CompositionInformation left = boost::any_cast(composition.getLeftSubcomposition().accept(*this, data)); + CompositionInformation right = boost::any_cast(composition.getRightSubcomposition().accept(*this, data)); + + // Join the information from both sides. + bool containsRenameComposition = left.containsRenameComposition() || right.containsRenameComposition(); + bool containsRestrictedParallelComposition = left.containsRestrictedParallelComposition() || right.containsRestrictedParallelComposition(); + std::map joinedAutomatonToMultiplicity = CompositionInformation::joinMultiplicityMaps(left.getAutomatonToMultiplicityMap(), right.getAutomatonToMultiplicityMap()); + + // If there was no restricted parallel composition yet, maybe the current composition is one, so check it. + if (!containsRestrictedParallelComposition) { + // FIXME. + } + + return CompositionInformation(joinedAutomatonToMultiplicity, containsRenameComposition, containsRestrictedParallelComposition); + } + + } +} \ No newline at end of file diff --git a/src/storage/jani/CompositionInformationVisitor.h b/src/storage/jani/CompositionInformationVisitor.h new file mode 100644 index 000000000..8454fbc9e --- /dev/null +++ b/src/storage/jani/CompositionInformationVisitor.h @@ -0,0 +1,60 @@ +#pragma once + +#include +#include +#include + +#include "src/storage/jani/CompositionVisitor.h" + +namespace storm { + namespace jani { + + class Model; + + class CompositionInformation { + public: + CompositionInformation() = default; + CompositionInformation(std::map const& automatonNameToMultiplicity, std::set const& nonsilentActions, bool containsRenaming, bool containsRestrictedParallelComposition); + + void increaseAutomatonMultiplicity(std::string const& automatonName, uint64_t count = 1); + + void addNonsilentAction(std::string const& actionName); + std::set const& getNonsilentActions() const; + void renameNonsilentActions(std::map const& renaming); + + void setContainsRenameComposition(); + bool containsRenameComposition() const; + + void setContainsRestrictedParallelComposition(); + bool containsRestrictedParallelComposition() const; + + static std::map joinMultiplicityMaps(std::map const& first, std::map const& second); + std::map const& getAutomatonToMultiplicityMap() const; + + private: + /// A mapping from the automata's names to the amount of times they occur in the composition. + std::map automatonNameToMultiplicity; + + /// The set of non-silent actions contained in the composition. + std::set nonsilentActions; + + /// A flag indicating whether the composition contains a renaming composition. + bool renameComposition; + + /// A flag indicating whether the composition contains + bool restrictedParallelComposition; + }; + + class CompositionInformationVisitor : public CompositionVisitor { + public: + CompositionInformationVisitor() = default; + + CompositionInformation getInformation(Composition const& composition, Model const& model); + + virtual boost::any visit(AutomatonComposition const& composition, boost::any const& data) override; + virtual boost::any visit(RenameComposition const& composition, boost::any const& data) override; + virtual boost::any visit(ParallelComposition const& composition, boost::any const& data) override; + }; + + } +} \ No newline at end of file diff --git a/src/storage/jani/CompositionVisitor.h b/src/storage/jani/CompositionVisitor.h index fdf155d96..d8c62a788 100644 --- a/src/storage/jani/CompositionVisitor.h +++ b/src/storage/jani/CompositionVisitor.h @@ -5,6 +5,7 @@ namespace storm { namespace jani { + class Composition; class AutomatonComposition; class RenameComposition; class ParallelComposition; diff --git a/src/storage/jani/Compositions.h b/src/storage/jani/Compositions.h new file mode 100644 index 000000000..ea74f3ac4 --- /dev/null +++ b/src/storage/jani/Compositions.h @@ -0,0 +1,3 @@ +#include "src/storage/jani/AutomatonComposition.h" +#include "src/storage/jani/RenameComposition.h" +#include "src/storage/jani/ParallelComposition.h" diff --git a/src/storage/jani/EdgeDestination.cpp b/src/storage/jani/EdgeDestination.cpp index bee1e0a3a..cdd295349 100644 --- a/src/storage/jani/EdgeDestination.cpp +++ b/src/storage/jani/EdgeDestination.cpp @@ -7,7 +7,7 @@ namespace storm { namespace jani { EdgeDestination::EdgeDestination(uint64_t locationId, storm::expressions::Expression const& probability, std::vector const& assignments, std::vector const& rewardIncrements) : locationId(locationId), probability(probability), assignments(assignments), rewardIncrements(rewardIncrements) { - // Intentionally left empty. + sortAssignments(); } void EdgeDestination::addAssignment(Assignment const& assignment) { @@ -16,6 +16,7 @@ namespace storm { STORM_LOG_THROW(oldAssignment.getExpressionVariable() != assignment.getExpressionVariable(), storm::exceptions::WrongFormatException, "Cannot add assignment '" << assignment << "', because another assignment '" << assignment << "' writes to the same target variable."); } assignments.push_back(assignment); + sortAssignments(); } void EdgeDestination::addRewardIncrement(RewardIncrement const& rewardIncrement) { @@ -46,5 +47,16 @@ namespace storm { return rewardIncrements; } + void EdgeDestination::sortAssignments() { + std::sort(this->assignments.begin(), this->assignments.end(), [] (storm::jani::Assignment const& assignment1, storm::jani::Assignment const& assignment2) { + bool smaller = assignment1.getExpressionVariable().getType().isBooleanType() && !assignment2.getExpressionVariable().getType().isBooleanType(); + if (!smaller) { + smaller = assignment1.getExpressionVariable() < assignment2.getExpressionVariable(); + } + return smaller; + }); + + } + } } \ No newline at end of file diff --git a/src/storage/jani/EdgeDestination.h b/src/storage/jani/EdgeDestination.h index c967518eb..5ccd79da2 100644 --- a/src/storage/jani/EdgeDestination.h +++ b/src/storage/jani/EdgeDestination.h @@ -58,6 +58,12 @@ namespace storm { std::vector const& getRewardIncrements() const; private: + /*! + * Sorts the assignments to make all assignments to boolean variables precede all others and order the + * assignments within one variable group by the expression variables. + */ + void sortAssignments(); + // The id of the destination location. uint64_t locationId; diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp index a8f442571..079f9d7ec 100644 --- a/src/storage/jani/Model.cpp +++ b/src/storage/jani/Model.cpp @@ -357,6 +357,19 @@ namespace storm { return this->getModelType() == ModelType::DTMC || this->getModelType() == ModelType::CTMC; } + std::vector Model::getAllRangeExpressions() const { + std::vector result; + for (auto const& variable : this->getGlobalVariables().getBoundedIntegerVariables()) { + result.push_back(variable.getRangeExpression()); + } + + for (auto const& automaton : automata) { + std::vector automatonRangeExpressions = automaton.getAllRangeExpressions(); + result.insert(result.end(), automatonRangeExpressions.begin(), automatonRangeExpressions.end()); + } + return result; + } + bool Model::checkValidity(bool logdbg) const { // TODO switch to exception based return value. diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h index b826763eb..caa5c730b 100644 --- a/src/storage/jani/Model.h +++ b/src/storage/jani/Model.h @@ -248,6 +248,11 @@ namespace storm { */ bool isDeterministicModel() const; + /*! + * Retrieves a list of expressions that characterize the legal values of the variables in this model. + */ + std::vector getAllRangeExpressions() const; + /*! * Checks if the model is valid JANI, which should be verified before any further operations are applied to a model. */ diff --git a/src/storage/prism/IntegerVariable.cpp b/src/storage/prism/IntegerVariable.cpp index 8ab2f9678..b2306ece0 100644 --- a/src/storage/prism/IntegerVariable.cpp +++ b/src/storage/prism/IntegerVariable.cpp @@ -14,6 +14,10 @@ namespace storm { return this->upperBoundExpression; } + storm::expressions::Expression IntegerVariable::getRangeExpression() const { + return this->getLowerBoundExpression() <= this->getExpressionVariable() && this->getExpressionVariable() <= this->getUpperBoundExpression(); + } + IntegerVariable IntegerVariable::substitute(std::map const& substitution) const { return IntegerVariable(this->getExpressionVariable(), this->getLowerBoundExpression().substitute(substitution), this->getUpperBoundExpression().substitute(substitution), this->getInitialValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); } diff --git a/src/storage/prism/IntegerVariable.h b/src/storage/prism/IntegerVariable.h index 024e1d214..fc1c6ecf5 100644 --- a/src/storage/prism/IntegerVariable.h +++ b/src/storage/prism/IntegerVariable.h @@ -45,6 +45,13 @@ namespace storm { */ storm::expressions::Expression const& getUpperBoundExpression() const; + /*! + * Retrieves an expression characterizing the legal range of the variable. + * + * @return An expression characterizing the legal range of the variable. + */ + storm::expressions::Expression getRangeExpression() const; + /*! * Substitutes all identifiers in the boolean variable according to the given map. * diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp index 47d44269a..d4168196d 100644 --- a/src/storage/prism/Module.cpp +++ b/src/storage/prism/Module.cpp @@ -43,6 +43,25 @@ namespace storm { return this->integerVariables; } + std::set Module::getAllExpressionVariables() const { + std::set result; + for (auto const& var : this->getBooleanVariables()) { + result.insert(var.getExpressionVariable()); + } + for (auto const& var : this->getIntegerVariables()) { + result.insert(var.getExpressionVariable()); + } + return result; + } + + std::vector Module::getAllRangeExpressions() const { + std::vector result; + for (auto const& integerVariable : this->integerVariables) { + result.push_back(integerVariable.getRangeExpression()); + } + return result; + } + std::size_t Module::getNumberOfCommands() const { return this->commands.size(); } diff --git a/src/storage/prism/Module.h b/src/storage/prism/Module.h index bb8c3b8d4..620432580 100644 --- a/src/storage/prism/Module.h +++ b/src/storage/prism/Module.h @@ -97,6 +97,22 @@ namespace storm { */ std::vector const& getIntegerVariables() const; + /*! + * Retrieves all expression variables used by this module. + * + * @return The set of expression variables used by this module. + */ + std::set getAllExpressionVariables() const; + + + /*! + * Retrieves a list of expressions that characterize the legal ranges of all variables declared by this + * module. + * + * @return The list of expressions that characterize the legal ranges. + */ + std::vector getAllRangeExpressions() const; + /*! * Retrieves the number of commands of this module. * diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 66758a72e..0f3fd93a5 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -349,6 +349,40 @@ namespace storm { return this->globalIntegerVariables; } + std::set Program::getAllExpressionVariables() const { + std::set result; + + for (auto const& constant : constants) { + result.insert(constant.getExpressionVariable()); + } + for (auto const& variable : globalBooleanVariables) { + result.insert(variable.getExpressionVariable()); + } + for (auto const& variable : globalIntegerVariables) { + result.insert(variable.getExpressionVariable()); + } + for (auto const& module : modules) { + auto const& moduleVariables = module.getAllExpressionVariables(); + result.insert(moduleVariables.begin(), moduleVariables.end()); + } + + return result; + } + + std::vector Program::getAllRangeExpressions() const { + std::vector result; + for (auto const& globalIntegerVariable : this->globalIntegerVariables) { + result.push_back(globalIntegerVariable.getRangeExpression()); + } + + for (auto const& module : modules) { + std::vector moduleRangeExpressions = module.getAllRangeExpressions(); + result.insert(result.end(), moduleRangeExpressions.begin(), moduleRangeExpressions.end()); + } + + return result; + } + bool Program::globalBooleanVariableExists(std::string const& variableName) const { return this->globalBooleanVariableToIndexMap.count(variableName) > 0; } diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h index cf0445503..71719c583 100644 --- a/src/storage/prism/Program.h +++ b/src/storage/prism/Program.h @@ -199,6 +199,20 @@ namespace storm { */ IntegerVariable const& getGlobalIntegerVariable(std::string const& variableName) const; + /*! + * Retrieves all expression variables used by this program. + * + * @return The set of expression variables used by this program. + */ + std::set getAllExpressionVariables() const; + + /*! + * Retrieves a list of expressions that characterize the legal ranges of all variables. + * + * @return A list of expressions that characterize the legal ranges of all variables. + */ + std::vector getAllRangeExpressions() const; + /*! * Retrieves the number of global boolean variables of the program. * diff --git a/src/storage/prism/Update.cpp b/src/storage/prism/Update.cpp index 4c3432fde..9424ee176 100644 --- a/src/storage/prism/Update.cpp +++ b/src/storage/prism/Update.cpp @@ -9,7 +9,13 @@ namespace storm { namespace prism { Update::Update(uint_fast64_t globalIndex, storm::expressions::Expression const& likelihoodExpression, std::vector const& assignments, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), likelihoodExpression(likelihoodExpression), assignments(assignments), variableToAssignmentIndexMap(), globalIndex(globalIndex) { - std::sort(this->assignments.begin(), this->assignments.end(), [] (storm::prism::Assignment const& assignment1, storm::prism::Assignment const& assignment2) { return assignment1.getVariable() < assignment2.getVariable(); } ); + std::sort(this->assignments.begin(), this->assignments.end(), [] (storm::prism::Assignment const& assignment1, storm::prism::Assignment const& assignment2) { + bool smaller = assignment1.getVariable().getType().isBooleanType() && !assignment2.getVariable().getType().isBooleanType(); + if (!smaller) { + smaller = assignment1.getVariable() < assignment2.getVariable(); + } + return smaller; + }); this->createAssignmentMapping(); }