From 08112d98aa8e927f4c27534ee430ee27d40ee1f8 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 15 Jun 2016 13:39:19 +0200 Subject: [PATCH] more work on JANI next state generator and the corresponding tests Former-commit-id: e170c9989c0985a78a5fd777144cafb43ff9c69b --- src/builder/ExplicitModelBuilder.cpp | 6 + src/builder/ExplicitModelBuilder.h | 9 +- src/generator/JaniNextStateGenerator.cpp | 225 ++++++++++++++++-- src/generator/JaniNextStateGenerator.h | 28 ++- src/generator/PrismNextStateGenerator.cpp | 2 +- src/storage/jani/Automaton.cpp | 109 +++++++++ src/storage/jani/Automaton.h | 21 ++ src/storage/jani/Model.cpp | 7 + src/storage/jani/Model.h | 8 + .../builder/ExplicitJaniModelBuilderTest.cpp | 124 ++++++++++ .../builder/ExplicitPrismModelBuilderTest.cpp | 8 +- 11 files changed, 518 insertions(+), 29 deletions(-) create mode 100644 test/functional/builder/ExplicitJaniModelBuilderTest.cpp diff --git a/src/builder/ExplicitModelBuilder.cpp b/src/builder/ExplicitModelBuilder.cpp index e99f2f37a..ff5cb2ea6 100644 --- a/src/builder/ExplicitModelBuilder.cpp +++ b/src/builder/ExplicitModelBuilder.cpp @@ -13,6 +13,7 @@ #include "src/settings/modules/IOSettings.h" #include "src/generator/PrismNextStateGenerator.h" +#include "src/generator/JaniNextStateGenerator.h" #include "src/utility/prism.h" #include "src/utility/constants.h" @@ -105,6 +106,11 @@ namespace storm { // Intentionally left empty. } + template + ExplicitModelBuilder::ExplicitModelBuilder(storm::jani::Model const& model, storm::generator::NextStateGeneratorOptions const& generatorOptions, Options const& builderOptions) : ExplicitModelBuilder(std::make_shared>(model, generatorOptions), builderOptions) { + // Intentionally left empty. + } + template storm::storage::sparse::StateValuations const& ExplicitModelBuilder::getStateValuations() const { STORM_LOG_THROW(static_cast(stateValuations), storm::exceptions::InvalidOperationException, "The state information was not properly build."); diff --git a/src/builder/ExplicitModelBuilder.h b/src/builder/ExplicitModelBuilder.h index c78c79493..296c15b7d 100644 --- a/src/builder/ExplicitModelBuilder.h +++ b/src/builder/ExplicitModelBuilder.h @@ -88,11 +88,18 @@ namespace storm { ExplicitModelBuilder(std::shared_ptr> const& generator, Options const& options = Options()); /*! - * Creates an explicit model builder for the given PRISM program.. + * Creates an explicit model builder for the given PRISM program. * * @param program The program for which to build the model. */ ExplicitModelBuilder(storm::prism::Program const& program, storm::generator::NextStateGeneratorOptions const& generatorOptions = storm::generator::NextStateGeneratorOptions(), Options const& builderOptions = Options()); + + /*! + * Creates an explicit model builder for the given JANI model. + * + * @param model The JANI model for which to build the model. + */ + ExplicitModelBuilder(storm::jani::Model const& model, storm::generator::NextStateGeneratorOptions const& generatorOptions = storm::generator::NextStateGeneratorOptions(), Options const& builderOptions = Options()); /*! * Convert the program given at construction time to an abstract model. The type of the model is the one diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index 5cf2b2da4..d8fe7e914 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -14,7 +14,7 @@ namespace storm { namespace generator { - + template JaniNextStateGenerator::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options) : JaniNextStateGenerator(model.substituteConstants(), options, false) { // Intentionally left empty. @@ -22,7 +22,7 @@ namespace storm { 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(!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."); STORM_LOG_THROW(!this->options.isBuildChoiceLabelsSet(), storm::exceptions::InvalidSettingsException, "JANI next-state generator cannot generate choice labels."); @@ -59,7 +59,35 @@ namespace storm { bool JaniNextStateGenerator::isDiscreteTimeModel() const { return model.isDiscreteTimeModel(); } - + + template + uint64_t JaniNextStateGenerator::getLocation(CompressedState const& state, LocationVariableInformation const& locationVariable) const { + if (locationVariable.bitWidth == 0) { + return 0; + } else { + return state.getAsInt(locationVariable.bitOffset, locationVariable.bitWidth); + } + } + + template + void JaniNextStateGenerator::setLocation(CompressedState& state, LocationVariableInformation const& locationVariable, uint64_t locationIndex) const { + if (locationVariable.bitWidth != 0) { + state.setFromInt(locationVariable.bitOffset, locationVariable.bitWidth, locationIndex); + } + } + + template + std::vector JaniNextStateGenerator::getLocations(CompressedState const& state) const { + std::vector result(this->variableInformation.locationVariables.size()); + + auto resultIt = result.begin(); + for (auto it = this->variableInformation.locationVariables.begin(), ite = this->variableInformation.locationVariables.end(); it != ite; ++it, ++resultIt) { + *resultIt = getLocation(state, *it); + } + + return result; + } + template std::vector JaniNextStateGenerator::getInitialStates(StateToIdCallback const& stateToIdCallback) { // Prepare an SMT solver to enumerate all initial states. @@ -72,7 +100,7 @@ namespace storm { } solver->add(model.getInitialStatesExpression(true)); - // Proceed ss long as the solver can still enumerate initial states. + // Proceed as long as the solver can still enumerate initial states. std::vector initialStateIndices; while (solver->check() == storm::solver::SmtSolver::CheckResult::Sat) { // Create fresh state. @@ -95,11 +123,35 @@ namespace storm { initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast(variableValue - integerVariable.lowerBound)); } - // FIXME: iterate through all combinations of initial locations and set them in the initial state. + // Gather iterators to the initial locations of all the automata. + std::vector::const_iterator> initialLocationsIterators; + for (auto const& automaton : this->model.getAutomata()) { + initialLocationsIterators.push_back(automaton.getInitialLocationIndices().cbegin()); + } - // Register initial state and return it. - StateType id = stateToIdCallback(initialState); - initialStateIndices.push_back(id); + // Now iterate through all combinations of initial locations. + while (true) { + uint64_t index = 0; + for (; index < initialLocationsIterators.size(); ++index) { + ++initialLocationsIterators[index]; + if (initialLocationsIterators[index] == this->model.getAutomata()[index].getInitialLocationIndices().cend()) { + initialLocationsIterators[index] = this->model.getAutomata()[index].getInitialLocationIndices().cbegin(); + } else { + break; + } + } + + // If we are at the end, leave the loop. Otherwise, create the next initial state. + if (index == initialLocationsIterators.size()) { + break; + } else { + setLocation(initialState, this->variableInformation.locationVariables[index], *initialLocationsIterators[index]); + + // 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); @@ -107,7 +159,7 @@ namespace storm { return initialStateIndices; } - + template CompressedState JaniNextStateGenerator::applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& destination) { CompressedState newState(state); @@ -161,9 +213,12 @@ namespace storm { } } + // Retrieve the locations from the state. + std::vector locations = getLocations(*this->state); + // Get all choices for the state. - std::vector> allChoices = getSilentActionChoices(*this->state, stateToIdCallback); - std::vector> allLabeledChoices = getNonsilentActionChoices(*this->state, stateToIdCallback); + std::vector> allChoices = getSilentActionChoices(locations, *this->state, stateToIdCallback); + std::vector> allLabeledChoices = getNonsilentActionChoices(locations, *this->state, stateToIdCallback); for (auto& choice : allLabeledChoices) { allChoices.push_back(std::move(choice)); } @@ -210,18 +265,16 @@ namespace storm { } template - std::vector> JaniNextStateGenerator::getSilentActionChoices(CompressedState const& state, StateToIdCallback stateToIdCallback) { + std::vector> JaniNextStateGenerator::getSilentActionChoices(std::vector const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback) { std::vector> result; // Iterate over all automata. - auto locationVariableIt = this->variableInformation.locationVariables.begin(); + uint64_t automatonIndex = 0; for (auto const& automaton : model.getAutomata()) { - - // Determine the location of the automaton in the given state. - uint64_t locationIndex = state.getAsInt(locationVariableIt->bitOffset, locationVariableIt->bitWidth); + uint64_t location = locations[automatonIndex]; // Iterate over all edges from the source location. - for (auto const& edge : automaton.getEdgesFromLocation(locationIndex)) { + for (auto const& edge : automaton.getEdgesFromLocation(location)) { // Skip the edge if it is labeled with a non-silent action. if (edge.getActionIndex() != model.getSilentActionIndex()) { continue; @@ -252,16 +305,146 @@ namespace storm { STORM_LOG_THROW(!this->isDiscreteTimeModel() || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for edge (actually sum to " << probabilitySum << ")."); } - // After we have processed all edges of the current automaton, move to the next location variable. - ++locationVariableIt; + ++automatonIndex; } return result; } template - std::vector> JaniNextStateGenerator::getNonsilentActionChoices(CompressedState const& state, StateToIdCallback stateToIdCallback) { + std::vector> JaniNextStateGenerator::getNonsilentActionChoices(std::vector const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback) { + std::vector> result; + for (uint64_t actionIndex : model.getNonsilentActionIndices()) { + std::vector> enabledEdges = getEnabledEdges(locations, actionIndex); + + // Only process this action, if there is at least one feasible solution. + if (!enabledEdges.empty()) { + std::vector::const_iterator> iteratorList(enabledEdges.size()); + + // Initialize the list of iterators. + for (size_t i = 0; i < enabledEdges.size(); ++i) { + iteratorList[i] = enabledEdges[i].cbegin(); + } + + // As long as there is one feasible combination of commands, keep on expanding it. + bool done = false; + while (!done) { + boost::container::flat_map* currentTargetStates = new boost::container::flat_map(); + boost::container::flat_map* newTargetStates = new boost::container::flat_map(); + + currentTargetStates->emplace(state, storm::utility::one()); + + for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { + storm::jani::Edge const& edge = **iteratorList[i]; + + for (auto const& destination : edge.getDestinations()) { + for (auto const& stateProbabilityPair : *currentTargetStates) { + // Compute the new state under the current update and add it to the set of new target states. + CompressedState newTargetState = applyUpdate(stateProbabilityPair.first, destination); + + // If the new state was already found as a successor state, update the probability + // and otherwise insert it. + auto targetStateIt = newTargetStates->find(newTargetState); + if (targetStateIt != newTargetStates->end()) { + targetStateIt->second += stateProbabilityPair.second * this->evaluator.asRational(destination.getProbability()); + } else { + newTargetStates->emplace(newTargetState, stateProbabilityPair.second * this->evaluator.asRational(destination.getProbability())); + } + } + } + + // If there is one more command to come, shift the target states one time step back. + if (i < iteratorList.size() - 1) { + delete currentTargetStates; + currentTargetStates = newTargetStates; + newTargetStates = new boost::container::flat_map(); + } + } + + // At this point, we applied all commands of the current command combination and newTargetStates + // contains all target states and their respective probabilities. That means we are now ready to + // add the choice to the list of transitions. + result.push_back(Choice(actionIndex)); + + // Now create the actual distribution. + Choice& choice = result.back(); + + // Add the probabilities/rates to the newly created choice. + ValueType probabilitySum = storm::utility::zero(); + for (auto const& stateProbabilityPair : *newTargetStates) { + StateType actualIndex = stateToIdCallback(stateProbabilityPair.first); + choice.addProbability(actualIndex, stateProbabilityPair.second); + probabilitySum += stateProbabilityPair.second; + } + + // Check that the resulting distribution is in fact a distribution. + STORM_LOG_THROW(!this->isDiscreteTimeModel() || !this->comparator.isConstant(probabilitySum) || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ")."); + + // Dispose of the temporary maps. + delete currentTargetStates; + delete newTargetStates; + + // Now, check whether there is one more command combination to consider. + bool movedIterator = false; + for (uint64_t j = 0; !movedIterator && j < iteratorList.size(); ++j) { + ++iteratorList[j]; + if (iteratorList[j] != enabledEdges[j].end()) { + movedIterator = true; + } else { + // Reset the iterator to the beginning of the list. + iteratorList[j] = enabledEdges[j].begin(); + } + } + + done = !movedIterator; + } + } + } + + return result; + } + + template + std::vector> JaniNextStateGenerator::getEnabledEdges(std::vector const& locationIndices, uint64_t actionIndex) { + std::vector> result; + + // Iterate over all automata. + uint64_t automatonIndex = 0; + for (auto const& automaton : model.getAutomata()) { + + // If the automaton has no edge labeled with the given action, we can skip it. + if (!automaton.hasEdgeLabeledWithActionIndex(actionIndex)) { + continue; + } + + auto edges = automaton.getEdgesFromLocation(locationIndices[automatonIndex], actionIndex); + + // If the automaton contains the action, but there is no edge available labeled with + // this action, we don't have any feasible command combinations. + if (edges.empty()) { + return std::vector>(); + } + + std::vector edgePointers; + edgePointers.reserve(edges.size()); + for (auto const& edge : edges) { + if (this->evaluator.asBool(edge.getGuard())) { + edgePointers.push_back(&edge); + } + } + + // If there was no enabled edge although the automaton has some edge with the required action, we must + // not return anything. + if (edgePointers.size() == 0) { + return std::vector>(); + } + + result.emplace_back(std::move(edgePointers)); + ++automatonIndex; + } + + return result; } template @@ -279,7 +462,7 @@ namespace storm { 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; diff --git a/src/generator/JaniNextStateGenerator.h b/src/generator/JaniNextStateGenerator.h index 1d6241ab7..3bb4939e5 100644 --- a/src/generator/JaniNextStateGenerator.h +++ b/src/generator/JaniNextStateGenerator.h @@ -27,6 +27,21 @@ namespace storm { virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices = {}) override; private: + /*! + * Retrieves the location index from the given state. + */ + uint64_t getLocation(CompressedState const& state, LocationVariableInformation const& locationVariable) const; + + /*! + * Sets the location index from the given state. + */ + void setLocation(CompressedState& state, LocationVariableInformation const& locationVariable, uint64_t locationIndex) const; + + /*! + * Retrieves the tuple of locations of the given state. + */ + std::vector getLocations(CompressedState const& state) const; + /*! * 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 @@ -46,18 +61,27 @@ namespace storm { /*! * Retrieves all choices labeled with the silent action possible from the given state. * + * @param locations The current locations of all automata. * @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); + std::vector> getSilentActionChoices(std::vector const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback); /*! * Retrieves all choices labeled with some non-silent action possible from the given state. * + * @param locations THe current locations of all automata. * @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); + std::vector> getNonsilentActionChoices(std::vector const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback); + + /*! + * Retrieves a list of lists of edges such that the list at index i are all edges of automaton i enabled in + * the current state. If the list is empty, it means there was at least one automaton containing edges with + * the desired action, but none of them were enabled. + */ + std::vector> getEnabledEdges(std::vector const& locationIndices, uint64_t actionIndex); // The model used for the generation of next states. storm::jani::Model model; diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp index dcac0ebc6..b746913a0 100644 --- a/src/generator/PrismNextStateGenerator.cpp +++ b/src/generator/PrismNextStateGenerator.cpp @@ -479,7 +479,7 @@ namespace storm { // Now, check whether there is one more command combination to consider. bool movedIterator = false; - for (int_fast64_t j = iteratorList.size() - 1; j >= 0; --j) { + for (int_fast64_t j = iteratorList.size() - 1; !movedIterator && j >= 0; --j) { ++iteratorList[j]; if (iteratorList[j] != activeCommandList[j].end()) { movedIterator = true; diff --git a/src/storage/jani/Automaton.cpp b/src/storage/jani/Automaton.cpp index 33cca31e6..d3504d353 100644 --- a/src/storage/jani/Automaton.cpp +++ b/src/storage/jani/Automaton.cpp @@ -24,6 +24,10 @@ namespace storm { return it == ite; } + std::size_t Edges::size() const { + return std::distance(it, ite); + } + ConstEdges::ConstEdges(const_iterator it, const_iterator ite) : it(it), ite(ite) { // Intentionally left empty. } @@ -39,6 +43,10 @@ namespace storm { bool ConstEdges::empty() const { return it == ite; } + + std::size_t ConstEdges::size() const { + return std::distance(it, ite); + } } Automaton::Automaton(std::string const& name) : name(name) { @@ -138,6 +146,100 @@ namespace storm { return ConstEdges(it, ite); } + Automaton::Edges Automaton::getEdgesFromLocation(uint64_t locationIndex, uint64_t actionIndex) { + typedef std::vector::iterator ForwardIt; + + // Perform binary search for start of edges with the given action index. + auto first = edges.begin(); + std::advance(first, locationToStartingIndex[locationIndex]); + auto last = edges.begin(); + std::advance(last, locationToStartingIndex[locationIndex + 1]); + typename std::iterator_traits::difference_type count, step; + count = std::distance(first, last); + + ForwardIt it1; + while (count > 0) { + it1 = first; + step = count / 2; + std::advance(it1, step); + if (it1->getActionIndex() < actionIndex) { + first = ++it1; + count -= step + 1; + } + else { + count = step; + } + } + + // If there is no such edge, we can return now. + if (it1 != last && it1->getActionIndex() > actionIndex) { + return Edges(last, last); + } + + // Otherwise, perform a binary search for the end of the edges with the given action index. + count = std::distance(first,last); + + ForwardIt it2; + while (count > 0) { + it2 = it1; + step = count / 2; + std::advance(it2, step); + if (!(actionIndex < it2->getActionIndex())) { + first = ++it2; + count -= step + 1; + } else count = step; + } + + return Edges(it1, it2); + } + + Automaton::ConstEdges Automaton::getEdgesFromLocation(uint64_t locationIndex, uint64_t actionIndex) const { + typedef std::vector::const_iterator ForwardIt; + + // Perform binary search for start of edges with the given action index. + auto first = edges.begin(); + std::advance(first, locationToStartingIndex[locationIndex]); + auto last = edges.begin(); + std::advance(last, locationToStartingIndex[locationIndex + 1]); + typename std::iterator_traits::difference_type count, step; + count = std::distance(first, last); + + ForwardIt it1; + while (count > 0) { + it1 = first; + step = count / 2; + std::advance(it1, step); + if (it1->getActionIndex() < actionIndex) { + first = ++it1; + count -= step + 1; + } + else { + count = step; + } + } + + // If there is no such edge, we can return now. + if (it1 != last && it1->getActionIndex() > actionIndex) { + return ConstEdges(last, last); + } + + // Otherwise, perform a binary search for the end of the edges with the given action index. + count = std::distance(first,last); + + ForwardIt it2; + while (count > 0) { + it2 = it1; + step = count / 2; + std::advance(it2, step); + if (!(actionIndex < it2->getActionIndex())) { + first = ++it2; + count -= step + 1; + } else count = step; + } + + return ConstEdges(it1, it2); + } + void Automaton::addEdge(Edge const& edge) { STORM_LOG_THROW(edge.getSourceLocationIndex() < locations.size(), storm::exceptions::InvalidArgumentException, "Cannot add edge with unknown source location index '" << edge.getSourceLocationIndex() << "'."); @@ -151,6 +253,13 @@ namespace storm { ++locationToStartingIndex[locationIndex]; } + // Sort all edges form the source location of the newly introduced edge by their action indices. + auto it = edges.begin(); + std::advance(it, locationToStartingIndex[edge.getSourceLocationIndex()]); + auto ite = edges.begin(); + std::advance(ite, locationToStartingIndex[edge.getSourceLocationIndex() + 1]); + std::sort(it, ite, [] (Edge const& a, Edge const& b) { return a.getActionIndex() < b.getActionIndex(); } ); + // Update the set of action indices of this automaton. actionIndices.insert(edge.getActionIndex()); } diff --git a/src/storage/jani/Automaton.h b/src/storage/jani/Automaton.h index fea88bfc1..596c279c4 100644 --- a/src/storage/jani/Automaton.h +++ b/src/storage/jani/Automaton.h @@ -3,6 +3,7 @@ #include #include #include +#include #include "src/storage/jani/VariableSet.h" #include "src/storage/jani/Edge.h" @@ -36,6 +37,11 @@ namespace storm { */ bool empty() const; + /*! + * Retrieves the number of edges. + */ + std::size_t size() const; + private: iterator it; iterator ite; @@ -62,6 +68,11 @@ namespace storm { * Determines whether this set of edges is empty. */ bool empty() const; + + /*! + * Retrieves the number of edges. + */ + std::size_t size() const; private: const_iterator it; @@ -175,6 +186,16 @@ namespace storm { */ ConstEdges getEdgesFromLocation(uint64_t index) const; + /*! + * Retrieves the edges of the location with the given index labeled with the given action index. + */ + Edges getEdgesFromLocation(uint64_t locationIndex, uint64_t actionIndex); + + /*! + * Retrieves the edges of the location with the given index. + */ + ConstEdges getEdgesFromLocation(uint64_t locationIndex, uint64_t actionIndex) const; + /*! * Adds an edge to the automaton. */ diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp index b83fead78..bef0f8d06 100644 --- a/src/storage/jani/Model.cpp +++ b/src/storage/jani/Model.cpp @@ -47,6 +47,9 @@ namespace storm { STORM_LOG_THROW(it == actionToIndex.end(), storm::exceptions::WrongFormatException, "Action with name '" << action.getName() << "' already exists"); actionToIndex.emplace(action.getName(), actions.size()); actions.push_back(action); + if (action.getName() != SILENT_ACTION_NAME) { + nonsilentActionIndices.insert(actions.size() - 1); + } return actions.size() - 1; } @@ -68,6 +71,10 @@ namespace storm { return actions; } + boost::container::flat_set const& Model::getNonsilentActionIndices() const { + return nonsilentActionIndices; + } + uint64_t Model::addConstant(Constant const& constant) { auto it = constantToIndex.find(constant.getName()); STORM_LOG_THROW(it == constantToIndex.end(), storm::exceptions::WrongFormatException, "Cannot add constant with name '" << constant.getName() << "', because a constant with that name already exists."); diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h index 094c650ce..7ec380bb9 100644 --- a/src/storage/jani/Model.h +++ b/src/storage/jani/Model.h @@ -77,6 +77,11 @@ namespace storm { */ std::vector const& getActions() const; + /*! + * Retrieves all non-silent action indices of the model. + */ + boost::container::flat_set const& getNonsilentActionIndices() const; + /*! * Adds the given constant to the model. */ @@ -288,6 +293,9 @@ namespace storm { /// A mapping from names to action indices. std::unordered_map actionToIndex; + /// The set of non-silent action indices. + boost::container::flat_set nonsilentActionIndices; + /// The index of the silent action. uint64_t silentActionIndex; diff --git a/test/functional/builder/ExplicitJaniModelBuilderTest.cpp b/test/functional/builder/ExplicitJaniModelBuilderTest.cpp new file mode 100644 index 000000000..23e1119a7 --- /dev/null +++ b/test/functional/builder/ExplicitJaniModelBuilderTest.cpp @@ -0,0 +1,124 @@ +#include "gtest/gtest.h" +#include "storm-config.h" +#include "src/models/sparse/StandardRewardModel.h" +#include "src/settings/SettingMemento.h" +#include "src/parser/PrismParser.h" +#include "src/builder/ExplicitModelBuilder.h" +#include "src/storage/jani/Model.h" + +#include "src/settings/modules/IOSettings.h" + +TEST(ExplicitJaniModelBuilderTest, Dtmc) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::jani::Model janiModel = program.toJani(); + + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(janiModel).build(); + EXPECT_EQ(13ul, model->getNumberOfStates()); + EXPECT_EQ(20ul, model->getNumberOfTransitions()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); + janiModel = program.toJani(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); + EXPECT_EQ(677ul, model->getNumberOfStates()); + EXPECT_EQ(867ul, model->getNumberOfTransitions()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + janiModel = program.toJani(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); + EXPECT_EQ(8607ul, model->getNumberOfStates()); + EXPECT_EQ(15113ul, model->getNumberOfTransitions()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + janiModel = program.toJani(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); + EXPECT_EQ(273ul, model->getNumberOfStates()); + EXPECT_EQ(397ul, model->getNumberOfTransitions()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); + janiModel = program.toJani(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); + EXPECT_EQ(1728ul, model->getNumberOfStates()); + EXPECT_EQ(2505ul, model->getNumberOfTransitions()); +} + +TEST(ExplicitJaniModelBuilderTest, Ctmc) { + // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); + + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::jani::Model janiModel = program.toJani(); + + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); + EXPECT_EQ(276ul, model->getNumberOfStates()); + EXPECT_EQ(1120ul, model->getNumberOfTransitions()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + janiModel = program.toJani(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); + EXPECT_EQ(3478ul, model->getNumberOfStates()); + EXPECT_EQ(14639ul, model->getNumberOfTransitions()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + janiModel = program.toJani(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); + EXPECT_EQ(12ul, model->getNumberOfStates()); + EXPECT_EQ(22ul, model->getNumberOfTransitions()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); + janiModel = program.toJani(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); + EXPECT_EQ(810ul, model->getNumberOfStates()); + EXPECT_EQ(3699ul, model->getNumberOfTransitions()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + janiModel = program.toJani(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); + EXPECT_EQ(66ul, model->getNumberOfStates()); + EXPECT_EQ(189ul, model->getNumberOfTransitions()); +} + +TEST(ExplicitJaniModelBuilderTest, Mdp) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::jani::Model janiModel = program.toJani(); + + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); + EXPECT_EQ(169ul, model->getNumberOfStates()); + EXPECT_EQ(436ul, model->getNumberOfTransitions()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + janiModel = program.toJani(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); + EXPECT_EQ(364ul, model->getNumberOfStates()); + EXPECT_EQ(654ul, model->getNumberOfTransitions()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + janiModel = program.toJani(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); + EXPECT_EQ(272ul, model->getNumberOfStates()); + EXPECT_EQ(492ul, model->getNumberOfTransitions()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + janiModel = program.toJani(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); + EXPECT_EQ(1038ul, model->getNumberOfStates()); + EXPECT_EQ(1282ul, model->getNumberOfTransitions()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm"); + janiModel = program.toJani(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); + EXPECT_EQ(4093ul, model->getNumberOfStates()); + EXPECT_EQ(5585ul, model->getNumberOfTransitions()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); + janiModel = program.toJani(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); + EXPECT_EQ(37ul, model->getNumberOfStates()); + EXPECT_EQ(59ul, model->getNumberOfTransitions()); +} + +TEST(ExplicitJaniModelBuilderTest, Fail) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm"); + storm::jani::Model janiModel = program.toJani(); + + ASSERT_THROW(storm::builder::ExplicitModelBuilder(janiModel).build(), storm::exceptions::WrongFormatException); +} diff --git a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp index d91eb64c4..b7e579366 100644 --- a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp +++ b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp @@ -7,7 +7,7 @@ #include "src/settings/modules/IOSettings.h" -TEST(ExplicitModelBuilderTest, Dtmc) { +TEST(ExplicitPrismModelBuilderTest, Dtmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); @@ -35,7 +35,7 @@ TEST(ExplicitModelBuilderTest, Dtmc) { EXPECT_EQ(2505ul, model->getNumberOfTransitions()); } -TEST(ExplicitModelBuilderTest, Ctmc) { +TEST(ExplicitPrismModelBuilderTest, Ctmc) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); @@ -66,7 +66,7 @@ TEST(ExplicitModelBuilderTest, Ctmc) { EXPECT_EQ(189ul, model->getNumberOfTransitions()); } -TEST(ExplicitModelBuilderTest, Mdp) { +TEST(ExplicitPrismModelBuilderTest, Mdp) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); @@ -99,7 +99,7 @@ TEST(ExplicitModelBuilderTest, Mdp) { EXPECT_EQ(59ul, model->getNumberOfTransitions()); } -TEST(ExplicitModelBuilderTest, Fail) { +TEST(ExplicitPrismModelBuilderTest, Fail) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm"); ASSERT_THROW(storm::builder::ExplicitModelBuilder(program).build(), storm::exceptions::WrongFormatException);