From 7861df4f202a45e213ce1d690c5aa31d71e51b7b Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 15 Jun 2016 22:43:37 +0200 Subject: [PATCH] JANI next-state generator appears to be working (without rewards) Former-commit-id: 3ca5c3ccf26f2596d351a4611f61ea580058e3f4 --- src/generator/JaniNextStateGenerator.cpp | 24 ++++--- src/generator/VariableInformation.cpp | 2 +- src/storage/jani/Automaton.cpp | 14 ++-- src/storage/jani/Automaton.h | 2 +- .../jani/CompositionInformationVisitor.cpp | 9 ++- .../jani/CompositionInformationVisitor.h | 2 +- .../prism/CompositionToJaniVisitor.cpp | 66 +++++++++++++++++++ src/storage/prism/CompositionToJaniVisitor.h | 29 ++++++++ src/storage/prism/Program.cpp | 10 ++- .../SmtPermissiveSchedulerTest.cpp | 10 +-- 10 files changed, 138 insertions(+), 30 deletions(-) create mode 100644 src/storage/prism/CompositionToJaniVisitor.cpp create mode 100644 src/storage/prism/CompositionToJaniVisitor.h diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index d8fe7e914..7c6fe0967 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -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(!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."); @@ -125,12 +125,21 @@ namespace storm { // Gather iterators to the initial locations of all the automata. std::vector::const_iterator> initialLocationsIterators; + uint64_t currentLocationVariable = 0; for (auto const& automaton : this->model.getAutomata()) { initialLocationsIterators.push_back(automaton.getInitialLocationIndices().cbegin()); + + // Initialize the locations to the first possible combination. + setLocation(initialState, this->variableInformation.locationVariables[currentLocationVariable], *initialLocationsIterators.back()); + ++currentLocationVariable; } // Now iterate through all combinations of initial locations. while (true) { + // Register initial state. + StateType id = stateToIdCallback(initialState); + initialStateIndices.push_back(id); + uint64_t index = 0; for (; index < initialLocationsIterators.size(); ++index) { ++initialLocationsIterators[index]; @@ -145,11 +154,9 @@ namespace storm { 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); + for (uint64_t j = 0; j <= index; ++j) { + setLocation(initialState, this->variableInformation.locationVariables[j], *initialLocationsIterators[j]); + } } } @@ -178,7 +185,7 @@ namespace storm { while (assignmentIt->getExpressionVariable() != boolIt->variable) { ++boolIt; } - newState.set(boolIt->bitOffset, this->evaluator.asBool(assignmentIt->getExpressionVariable())); + newState.set(boolIt->bitOffset, this->evaluator.asBool(assignmentIt->getAssignedExpression())); } // Iterate over all integer assignments and carry them out. @@ -427,7 +434,6 @@ namespace storm { } std::vector edgePointers; - edgePointers.reserve(edges.size()); for (auto const& edge : edges) { if (this->evaluator.asBool(edge.getGuard())) { edgePointers.push_back(&edge); @@ -436,7 +442,7 @@ namespace storm { // 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) { + if (edgePointers.empty()) { return std::vector>(); } diff --git a/src/generator/VariableInformation.cpp b/src/generator/VariableInformation.cpp index f941cc653..ca539432d 100644 --- a/src/generator/VariableInformation.cpp +++ b/src/generator/VariableInformation.cpp @@ -50,7 +50,7 @@ namespace storm { sortVariables(); } - VariableInformation::VariableInformation(storm::jani::Model const& model) { + VariableInformation::VariableInformation(storm::jani::Model const& model) : totalBitOffset(0) { for (auto const& variable : model.getGlobalVariables().getBooleanVariables()) { booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset); ++totalBitOffset; diff --git a/src/storage/jani/Automaton.cpp b/src/storage/jani/Automaton.cpp index d3504d353..25bb776f3 100644 --- a/src/storage/jani/Automaton.cpp +++ b/src/storage/jani/Automaton.cpp @@ -114,7 +114,7 @@ namespace storm { initialLocationIndices.insert(index); } - std::set Automaton::getInitialLocationIndices() const { + std::set const& Automaton::getInitialLocationIndices() const { return initialLocationIndices; } @@ -170,14 +170,15 @@ namespace storm { count = step; } } - + it1 = first; + // 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); + count = std::distance(it1,last); ForwardIt it2; while (count > 0) { @@ -189,6 +190,7 @@ namespace storm { count -= step + 1; } else count = step; } + it2 = first; return Edges(it1, it2); } @@ -217,6 +219,7 @@ namespace storm { count = step; } } + it1 = first; // If there is no such edge, we can return now. if (it1 != last && it1->getActionIndex() > actionIndex) { @@ -224,11 +227,11 @@ namespace storm { } // Otherwise, perform a binary search for the end of the edges with the given action index. - count = std::distance(first,last); + count = std::distance(it1,last); ForwardIt it2; while (count > 0) { - it2 = it1; + it2 = first; step = count / 2; std::advance(it2, step); if (!(actionIndex < it2->getActionIndex())) { @@ -236,6 +239,7 @@ namespace storm { count -= step + 1; } else count = step; } + it2 = first; return ConstEdges(it1, it2); } diff --git a/src/storage/jani/Automaton.h b/src/storage/jani/Automaton.h index 596c279c4..c524e7d03 100644 --- a/src/storage/jani/Automaton.h +++ b/src/storage/jani/Automaton.h @@ -164,7 +164,7 @@ namespace storm { /*! * Retrieves the indices of the initial locations. */ - std::set getInitialLocationIndices() const; + std::set const& getInitialLocationIndices() const; /*! * Retrieves the edges of the location with the given name. diff --git a/src/storage/jani/CompositionInformationVisitor.cpp b/src/storage/jani/CompositionInformationVisitor.cpp index 541b55698..d6b661b53 100644 --- a/src/storage/jani/CompositionInformationVisitor.cpp +++ b/src/storage/jani/CompositionInformationVisitor.cpp @@ -6,6 +6,10 @@ namespace storm { namespace jani { + CompositionInformation::CompositionInformation() : automatonNameToMultiplicity(), nonsilentActions(), renameComposition(false), restrictedParallelComposition(false) { + // Intentionally left empty. + } + 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. } @@ -105,9 +109,8 @@ namespace storm { if (!containsRestrictedParallelComposition) { std::set commonNonsilentActions; std::set_intersection(left.getNonsilentActions().begin(), left.getNonsilentActions().end(), right.getNonsilentActions().begin(), right.getNonsilentActions().end(), std::inserter(commonNonsilentActions, commonNonsilentActions.begin())); - if (commonNonsilentActions != composition.getSynchronizationAlphabet()) { - containsRestrictedParallelComposition = true; - } + bool allCommonActionsIncluded = std::includes(commonNonsilentActions.begin(), commonNonsilentActions.end(), composition.getSynchronizationAlphabet().begin(), composition.getSynchronizationAlphabet().end()); + containsRestrictedParallelComposition = !allCommonActionsIncluded; } return CompositionInformation(joinedAutomatonToMultiplicity, nonsilentActions, containsRenameComposition, containsRestrictedParallelComposition); diff --git a/src/storage/jani/CompositionInformationVisitor.h b/src/storage/jani/CompositionInformationVisitor.h index 9baa2c363..59a422a41 100644 --- a/src/storage/jani/CompositionInformationVisitor.h +++ b/src/storage/jani/CompositionInformationVisitor.h @@ -15,7 +15,7 @@ namespace storm { class CompositionInformation { public: - CompositionInformation() = default; + CompositionInformation(); CompositionInformation(std::map const& automatonNameToMultiplicity, std::set const& nonsilentActions, bool containsRenaming, bool containsRestrictedParallelComposition); void increaseAutomatonMultiplicity(std::string const& automatonName, uint64_t count = 1); diff --git a/src/storage/prism/CompositionToJaniVisitor.cpp b/src/storage/prism/CompositionToJaniVisitor.cpp new file mode 100644 index 000000000..173a70bdc --- /dev/null +++ b/src/storage/prism/CompositionToJaniVisitor.cpp @@ -0,0 +1,66 @@ +#include "src/storage/prism/CompositionToJaniVisitor.h" +#include "src/storage/prism/Compositions.h" + +#include "src/storage/jani/Compositions.h" +#include "src/storage/jani/Model.h" + +namespace storm { + namespace prism { + + std::shared_ptr CompositionToJaniVisitor::toJani(Composition const& composition, storm::jani::Model const& model) { + return boost::any_cast>(composition.accept(*this, model)); + } + + boost::any CompositionToJaniVisitor::visit(ModuleComposition const& composition, boost::any const& data) { + std::shared_ptr result = std::make_shared(composition.getModuleName()); + return result; + } + + boost::any CompositionToJaniVisitor::visit(RenamingComposition const& composition, boost::any const& data) { + std::map> newRenaming; + for (auto const& renamingPair : composition.getActionRenaming()) { + newRenaming.emplace(renamingPair.first, renamingPair.second); + } + auto subcomposition = boost::any_cast>(composition.getSubcomposition().accept(*this, data)); + std::shared_ptr result = std::make_shared(subcomposition, newRenaming); + return result; + } + + boost::any CompositionToJaniVisitor::visit(HidingComposition const& composition, boost::any const& data) { + std::map> newRenaming; + for (auto const& action : composition.getActionsToHide()) { + newRenaming.emplace(action, boost::none); + } + auto subcomposition = boost::any_cast>(composition.getSubcomposition().accept(*this, data)); + std::shared_ptr result = std::make_shared(subcomposition, newRenaming); + return result; + } + + boost::any CompositionToJaniVisitor::visit(SynchronizingParallelComposition const& composition, boost::any const& data) { + auto leftSubcomposition = boost::any_cast>(composition.getLeftSubcomposition().accept(*this, data)); + auto rightSubcomposition = boost::any_cast>(composition.getRightSubcomposition().accept(*this, data)); + + storm::jani::Model const& model = boost::any_cast(data); + std::set allActions; + for (auto const& action : model.getActions()) { + allActions.insert(action.getName()); + } + std::shared_ptr result = std::make_shared(leftSubcomposition, rightSubcomposition, allActions); + return result; + } + + boost::any CompositionToJaniVisitor::visit(InterleavingParallelComposition const& composition, boost::any const& data) { + auto leftSubcomposition = boost::any_cast>(composition.getLeftSubcomposition().accept(*this, data)); + auto rightSubcomposition = boost::any_cast>(composition.getRightSubcomposition().accept(*this, data)); + std::shared_ptr result = std::make_shared(leftSubcomposition, rightSubcomposition, std::set()); + return result; + } + + boost::any CompositionToJaniVisitor::visit(RestrictedParallelComposition const& composition, boost::any const& data) { + auto leftSubcomposition = boost::any_cast>(composition.getLeftSubcomposition().accept(*this, data)); + auto rightSubcomposition = boost::any_cast>(composition.getRightSubcomposition().accept(*this, data)); + std::shared_ptr result = std::make_shared(leftSubcomposition, rightSubcomposition, composition.getSynchronizingActions()); + return result; + } + } +} \ No newline at end of file diff --git a/src/storage/prism/CompositionToJaniVisitor.h b/src/storage/prism/CompositionToJaniVisitor.h new file mode 100644 index 000000000..c1fabff99 --- /dev/null +++ b/src/storage/prism/CompositionToJaniVisitor.h @@ -0,0 +1,29 @@ +#pragma once + +#include + +#include "src/storage/prism/CompositionVisitor.h" + +namespace storm { + namespace jani { + class Composition; + class Model; + } + + namespace prism { + class Composition; + + class CompositionToJaniVisitor : public CompositionVisitor { + public: + std::shared_ptr toJani(Composition const& composition, storm::jani::Model const& model); + + virtual boost::any visit(ModuleComposition const& composition, boost::any const& data) override; + virtual boost::any visit(RenamingComposition const& composition, boost::any const& data) override; + virtual boost::any visit(HidingComposition const& composition, boost::any const& data) override; + virtual boost::any visit(SynchronizingParallelComposition const& composition, boost::any const& data) override; + virtual boost::any visit(InterleavingParallelComposition const& composition, boost::any const& data) override; + virtual boost::any visit(RestrictedParallelComposition const& composition, boost::any const& data) override; + }; + + } +} \ No newline at end of file diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 44372882e..24eca0256 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -20,6 +20,7 @@ #include "src/storage/prism/CompositionVisitor.h" #include "src/storage/prism/Compositions.h" +#include "src/storage/prism/CompositionToJaniVisitor.h" namespace storm { namespace prism { @@ -1510,8 +1511,6 @@ namespace storm { } storm::jani::Model Program::toJani(bool allVariablesGlobal) const { - STORM_LOG_THROW(!this->specifiesSystemComposition(), storm::exceptions::InvalidOperationException, "Cannot translate PRISM program with custom system composition to JANI."); - // Start by creating an empty JANI model. storm::jani::ModelType modelType; switch (this->getModelType()) { @@ -1659,7 +1658,12 @@ namespace storm { janiModel.setInitialStatesExpression(globalInitialStatesExpression); // Set the standard system composition. This is possible, because we reject non-standard compositions anyway. - janiModel.setSystemComposition(janiModel.getStandardSystemComposition()); + if (this->specifiesSystemComposition()) { + CompositionToJaniVisitor visitor; + janiModel.setSystemComposition(visitor.toJani(this->getSystemCompositionConstruct().getSystemComposition(), janiModel)); + } else { + janiModel.setSystemComposition(janiModel.getStandardSystemComposition()); + } return janiModel; } diff --git a/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp b/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp index e72b2fff4..157f96ee8 100644 --- a/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp +++ b/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp @@ -11,7 +11,7 @@ #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" -#ifdef STORM_HAVE_MSAT +#if defined(STORM_HAVE_MSAT) || defined(STORM_HAVE_Z3) TEST(SmtPermissiveSchedulerTest, DieSelection) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die_c1.nm"); @@ -25,11 +25,7 @@ TEST(SmtPermissiveSchedulerTest, DieSelection) { auto formula001b = formulaParser.parseSingleFormulaFromString("P<=0.05 [ F \"one\"]")->asProbabilityOperatorFormula(); // Customize and perform model-building. - typename storm::builder::ExplicitModelBuilder::Options options; - - options = typename storm::builder::ExplicitModelBuilder::Options(formula02b); - options.addConstantDefinitionsFromString(program, ""); - options.buildCommandLabels = true; + storm::generator::NextStateGeneratorOptions options(formula02b); std::shared_ptr> mdp = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); @@ -62,4 +58,4 @@ TEST(SmtPermissiveSchedulerTest, DieSelection) { } -#endif // STORM_HAVE_MSAT +#endif // STORM_HAVE_MSAT || STORM_HAVE_Z3