diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index cb7e064ec..f5606a095 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -27,6 +27,7 @@ ExternalProject_Get_Property(l3pp_ext source_dir) set(l3pp_INCLUDE "${source_dir}/") add_imported_library_interface(l3pp "${l3pp_INCLUDE}") list(APPEND STORM_DEP_TARGETS l3pp) +add_dependencies(l3pp l3pp_ext) ############################################################# ## diff --git a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index c43e3e66a..1d6864fa3 100644 --- a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -530,11 +530,13 @@ namespace storm { // Then compute the reward vector to use in the computation. storm::dd::Add subvector = rewardModel.getTotalRewardVector(maybeStatesAdd, choiceFilterAdd, submatrix, model.getColumnVariables()); + std::vector rowGroupSizes = (submatrix.notZero().existsAbstract(model.getColumnVariables()) || subvector.notZero()).template toAdd().sumAbstract(model.getNondeterminismVariables()).toVector(odd); + // Finally cut away all columns targeting non-maybe states (or non-(maybe or target) states, respectively). submatrix *= extendMaybeStates ? maybeStatesWithTargetStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd() : maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); // Translate the symbolic matrix/vector to their explicit representations. - std::pair, std::vector> explicitRepresentation = submatrix.toMatrixVector(subvector, model.getNondeterminismVariables(), odd, odd); + std::pair, std::vector> explicitRepresentation = submatrix.toMatrixVector(std::move(rowGroupSizes), subvector, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), odd, odd); // Fulfill the solver's requirements. SolverRequirementsData solverRequirementsData; diff --git a/src/storm/storage/dd/Add.cpp b/src/storm/storage/dd/Add.cpp index ed8e2a966..a62600562 100644 --- a/src/storm/storage/dd/Add.cpp +++ b/src/storm/storage/dd/Add.cpp @@ -799,6 +799,14 @@ namespace storm { template std::pair, std::vector> Add::toMatrixVector(storm::dd::Add const& vector, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { + + // Count how many choices each row group has. + std::vector rowGroupIndices = (this->notZero().existsAbstract(columnMetaVariables) || vector.notZero()).template toAdd().sumAbstract(groupMetaVariables).toVector(rowOdd); + return toMatrixVector(std::move(rowGroupIndices), vector, rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd); + } + + template + std::pair, std::vector> Add::toMatrixVector(std::vector&& rowGroupIndices, storm::dd::Add const& vector, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { std::vector ddRowVariableIndices; std::vector ddColumnVariableIndices; std::vector ddGroupVariableIndices; @@ -829,9 +837,6 @@ namespace storm { std::sort(ddGroupVariableIndices.begin(), ddGroupVariableIndices.end()); Bdd columnVariableCube = Bdd::getCube(this->getDdManager(), columnMetaVariables); - - // Count how many choices each row group has. - std::vector rowGroupIndices = (this->notZero().existsAbstract(columnMetaVariables) || vector.notZero()).template toAdd().sumAbstract(groupMetaVariables).toVector(rowOdd); // Transform the row group sizes to the actual row group indices. rowGroupIndices.resize(rowGroupIndices.size() + 1); @@ -853,7 +858,7 @@ namespace storm { for (auto const& internalAdd : internalAddGroups) { groups.push_back(std::make_pair(Add(this->getDdManager(), internalAdd.first, rowAndColumnMetaVariables), Add(this->getDdManager(), internalAdd.second, rowMetaVariables))); } - + // Create the actual storage for the non-zero entries. std::vector> columnsAndValues(this->getNonZeroCount()); @@ -866,12 +871,12 @@ namespace storm { std::pair, Add> const& ddPair = groups[i]; Bdd matrixDdNotZero = ddPair.first.notZero(); Bdd vectorDdNotZero = ddPair.second.notZero(); - + std::vector tmpRowIndications = matrixDdNotZero.template toAdd().sumAbstract(columnMetaVariables).toVector(rowOdd); for (uint64_t offset = 0; offset < tmpRowIndications.size(); ++offset) { rowIndications[rowGroupIndices[offset]] += tmpRowIndications[offset]; } - + ddPair.second.internalAdd.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, explicitVector, std::plus()); statesWithGroupEnabled[i] = (matrixDdNotZero.existsAbstract(columnMetaVariables) || vectorDdNotZero).template toAdd(); @@ -881,7 +886,7 @@ namespace storm { // Since we modified the rowGroupIndices, we need to restore the correct values. stateToRowGroupCount.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::minus()); - + // Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector. tmp = 0; tmp2 = 0; @@ -908,10 +913,11 @@ namespace storm { rowIndications[i] = rowIndications[i - 1]; } rowIndications[0] = 0; - + return std::make_pair(storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)), std::move(explicitVector)); - } + } + template void Add::exportToDot(std::string const& filename, bool showVariablesIfPossible) const { internalAdd.exportToDot(filename, this->getDdManager().getDdVariableNames(), showVariablesIfPossible); diff --git a/src/storm/storage/dd/Add.h b/src/storm/storage/dd/Add.h index 8f3100b18..c25b5a8c4 100644 --- a/src/storm/storage/dd/Add.h +++ b/src/storm/storage/dd/Add.h @@ -639,7 +639,8 @@ namespace storm { * @return The matrix that is represented by this ADD. */ std::pair, std::vector> toMatrixVector(storm::dd::Add const& vector, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; - + std::pair, std::vector> toMatrixVector(std::vector&& rowGroupSizes, storm::dd::Add const& vector, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; + /*! * Exports the DD to the given file in the dot format. * diff --git a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp index 0a1715a5d..d6ee3b41e 100644 --- a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp @@ -8,7 +8,7 @@ namespace storm { namespace bisimulation { template - MdpPartitionRefiner::MdpPartitionRefiner(storm::models::symbolic::Mdp const& mdp, Partition const& initialStatePartition) : PartitionRefiner(mdp, initialStatePartition), choicePartition(Partition::createTrivialChoicePartition(mdp, initialStatePartition.getBlockVariables())), stateSignatureComputer(mdp.getQualitativeTransitionMatrix(), mdp.getColumnAndNondeterminismVariables(), SignatureMode::Qualitative, true), stateSignatureRefiner(mdp.getManager(), this->statePartition.getBlockVariable(), mdp.getRowVariables(), true) { + MdpPartitionRefiner::MdpPartitionRefiner(storm::models::symbolic::Mdp const& mdp, Partition const& initialStatePartition) : PartitionRefiner(mdp, initialStatePartition), mdp(mdp), choicePartition(Partition::createTrivialChoicePartition(mdp, initialStatePartition.getBlockVariables())), stateSignatureRefiner(mdp.getManager(), this->statePartition.getBlockVariable(), mdp.getRowVariables(), true) { // Intentionally left empty. } @@ -29,10 +29,19 @@ namespace storm { } else { this->choicePartition = newChoicePartition; - // If the choice partition changed, refine the state partition. Use qualitative mode we must properly abstract from choice counts. + // Compute state signatures. + storm::dd::Bdd choicePartitionAsBdd; + if (this->choicePartition.storedAsBdd()) { + choicePartitionAsBdd = this->choicePartition.asBdd(); + } else { + choicePartitionAsBdd = this->choicePartition.asAdd().notZero(); + } + Signature stateSignature(choicePartitionAsBdd.existsAbstract(mdp.getNondeterminismVariables()).template toAdd()); + + // If the choice partition changed, refine the state partition. STORM_LOG_TRACE("Refining state partition."); - Partition newStatePartition = this->internalRefine(this->stateSignatureComputer, this->stateSignatureRefiner, this->statePartition, this->choicePartition, SignatureMode::Qualitative); - + Partition newStatePartition = this->internalRefine(stateSignature, this->stateSignatureRefiner, this->statePartition); + if (newStatePartition == this->statePartition) { this->status = Status::FixedPoint; return false; diff --git a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.h b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.h index bafd9d97f..77766dd95 100644 --- a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.h +++ b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.h @@ -34,12 +34,12 @@ namespace storm { private: virtual bool refineWrtStateActionRewards(storm::dd::Add const& stateActionRewards) override; + // The model to refine. + storm::models::symbolic::Mdp const& mdp; + // The choice partition in the refinement process. Partition choicePartition; - // The object used to compute the state signatures. - SignatureComputer stateSignatureComputer; - // The object used to refine the state partition based on the signatures. SignatureRefiner stateSignatureRefiner; }; diff --git a/src/storm/storage/dd/bisimulation/Partition.cpp b/src/storm/storage/dd/bisimulation/Partition.cpp index 33e3fd48e..a923c199c 100644 --- a/src/storm/storage/dd/bisimulation/Partition.cpp +++ b/src/storm/storage/dd/bisimulation/Partition.cpp @@ -100,7 +100,7 @@ namespace storm { template Partition Partition::createTrivialChoicePartition(storm::models::symbolic::NondeterministicModel const& model, std::pair const& blockVariables) { - storm::dd::Bdd choicePartitionBdd = (!model.getIllegalMask() && model.getReachableStates()).renameVariables(model.getRowVariables(), model.getColumnVariables()) && model.getManager().getEncoding(blockVariables.first, 0, false); + storm::dd::Bdd choicePartitionBdd = (!model.getIllegalMask() && model.getReachableStates()) && model.getManager().getEncoding(blockVariables.first, 0, false); // Store the partition as an ADD only in the case of CUDD. if (DdType == storm::dd::DdType::CUDD) { diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp index 167efd529..6f587ad36 100644 --- a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp @@ -64,14 +64,27 @@ namespace storm { } auto totalTimeInRefinement = std::chrono::duration_cast(std::chrono::high_resolution_clock::now() - start).count(); - ++refinements; STORM_LOG_TRACE("Refinement " << refinements << " produced " << newPartition.getNumberOfBlocks() << " blocks and was completed in " << totalTimeInRefinement << "ms (signature: " << signatureTime << "ms, refinement: " << refinementTime << "ms)."); + ++refinements; return newPartition; } else { return oldPartition; } } + template + Partition PartitionRefiner::internalRefine(Signature const& signature, SignatureRefiner& signatureRefiner, Partition const& oldPartition) { + + STORM_LOG_TRACE("Signature " << refinements << " DD has " << signature.getSignatureAdd().getNodeCount() << " nodes."); + auto start = std::chrono::high_resolution_clock::now(); + auto newPartition = signatureRefiner.refine(oldPartition, signature); + auto totalTimeInRefinement = std::chrono::duration_cast(std::chrono::high_resolution_clock::now() - start).count(); + STORM_LOG_TRACE("Refinement " << refinements << " produced " << newPartition.getNumberOfBlocks() << " blocks and was completed in " << totalTimeInRefinement << "ms."); + + ++refinements; + return newPartition; + } + template bool PartitionRefiner::refineWrtRewardModel(storm::models::symbolic::StandardRewardModel const& rewardModel) { STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Symbolic bisimulation currently does not support transition rewards."); diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.h b/src/storm/storage/dd/bisimulation/PartitionRefiner.h index 5ae860201..c3398e826 100644 --- a/src/storm/storage/dd/bisimulation/PartitionRefiner.h +++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.h @@ -50,7 +50,8 @@ namespace storm { protected: Partition internalRefine(SignatureComputer& stateSignatureComputer, SignatureRefiner& signatureRefiner, Partition const& oldPartition, Partition const& targetPartition, SignatureMode const& mode = SignatureMode::Eager); - + Partition internalRefine(Signature const& signature, SignatureRefiner& signatureRefiner, Partition const& oldPartition); + virtual bool refineWrtStateRewards(storm::dd::Add const& stateRewards); virtual bool refineWrtStateActionRewards(storm::dd::Add const& stateActionRewards); diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp index 273ecb8fc..3e8682b6d 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -427,7 +427,7 @@ namespace storm { void createBlockToOffsetMappingRec(DdNodePtr partitionNode, DdNodePtr representativesNode, DdNodePtr variables, storm::dd::Odd const& odd, uint64_t offset) { STORM_LOG_ASSERT(partitionNode != Cudd_ReadLogicZero(ddman) || representativesNode == Cudd_ReadLogicZero(ddman), "Expected representative to be zero if the partition is zero."); - if (representativesNode == Cudd_ReadLogicZero(ddman)) { + if (representativesNode == Cudd_ReadLogicZero(ddman) || partitionNode == Cudd_ReadLogicZero(ddman)) { return; } @@ -471,7 +471,7 @@ namespace storm { } void extractVectorRec(DdNodePtr vector, DdNodePtr representativesNode, DdNodePtr variables, storm::dd::Odd const& odd, uint64_t offset, std::vector& result) { - if (representativesNode == Cudd_ReadLogicZero(ddman)) { + if (representativesNode == Cudd_ReadLogicZero(ddman) || vector == Cudd_ReadZero(ddman)) { return; } @@ -643,7 +643,7 @@ namespace storm { } void extractVectorRec(MTBDD vector, BDD representativesNode, BDD variables, storm::dd::Odd const& odd, uint64_t offset, std::vector& result) { - if (representativesNode == sylvan_false) { + if (representativesNode == sylvan_false || mtbdd_iszero(vector)) { return; } @@ -680,7 +680,7 @@ namespace storm { void createBlockToOffsetMappingRec(BDD partitionNode, BDD representativesNode, BDD variables, storm::dd::Odd const& odd, uint64_t offset) { STORM_LOG_ASSERT(partitionNode != sylvan_false || representativesNode == sylvan_false, "Expected representative to be zero if the partition is zero."); - if (representativesNode == sylvan_false) { + if (representativesNode == sylvan_false || partitionNode == sylvan_false) { return; } @@ -892,6 +892,7 @@ namespace storm { boost::optional> quotientStateActionRewards; if (rewardModel.hasStateActionRewards()) { + rewardModel.getStateActionRewardVector().exportToDot("vector.dot"); quotientStateActionRewards = sparseExtractor.extractStateActionVector(rewardModel.getStateActionRewardVector()); } diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp index 3eca707ca..ce1576956 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -57,9 +57,7 @@ namespace storm { bool negated = mtbdd_hascomp(node); STORM_LOG_ASSERT(mtbdd_gettype(node) == sylvan_storm_rational_number_get_type(), "Expected a storm::RationalNumber value."); - uint64_t value = mtbdd_getvalue(node); - storm_rational_number_ptr ptr = (storm_rational_number_ptr)value; - + storm_rational_number_ptr ptr = (storm_rational_number_ptr)mtbdd_getstorm_rational_number_ptr(node); storm::RationalNumber* rationalNumber = (storm::RationalNumber*)(ptr); return negated ? -(*rationalNumber) : (*rationalNumber); diff --git a/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp b/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp index e4508b72c..76a1a92a6 100644 --- a/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp +++ b/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp @@ -34,7 +34,7 @@ namespace storm { for (uint_fast64_t vertexIndex : vertexIndices){ insidePoint += points[vertexIndex]; } - insidePoint /= storm::utility::convertNumber((uint_fast64_t) vertexIndices.size()); + insidePoint /= storm::utility::convertNumber(static_cast(vertexIndices.size())); // Create the initial facets from the found vertices. std::vector facets = computeInitialFacets(points, vertexIndices, insidePoint); diff --git a/src/storm/utility/KwekMehlhorn.cpp b/src/storm/utility/KwekMehlhorn.cpp index 367c9a595..985f12789 100644 --- a/src/storm/utility/KwekMehlhorn.cpp +++ b/src/storm/utility/KwekMehlhorn.cpp @@ -31,7 +31,7 @@ namespace storm { std::pair::IntegerType, typename NumberTraits::IntegerType> truncateToRational(ImpreciseType const& value, uint64_t precision) { typedef typename NumberTraits::IntegerType IntegerType; - IntegerType powerOfTen = storm::utility::pow(storm::utility::convertNumber(10ull), precision); + IntegerType powerOfTen = storm::utility::pow(storm::utility::convertNumber(static_cast(10)), precision); IntegerType truncated = storm::utility::trunc(value * powerOfTen); return std::make_pair(truncated, powerOfTen); } diff --git a/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp b/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp index f7f15fd42..2f9b217e2 100644 --- a/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp +++ b/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp @@ -87,11 +87,11 @@ TEST(SymbolicModelBisimulationDecomposition, TwoDice_Cudd) { decomposition.compute(); std::shared_ptr> quotient = decomposition.getQuotient(); - EXPECT_EQ(135ul, quotient->getNumberOfStates()); - EXPECT_EQ(366ul, quotient->getNumberOfTransitions()); + EXPECT_EQ(77ul, quotient->getNumberOfStates()); + EXPECT_EQ(210ul, quotient->getNumberOfTransitions()); EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType()); EXPECT_TRUE(quotient->isSymbolicModel()); - EXPECT_EQ(194ul, (quotient->as>()->getNumberOfChoices())); + EXPECT_EQ(116ul, (quotient->as>()->getNumberOfChoices())); storm::parser::FormulaParser formulaParser; std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); @@ -103,11 +103,11 @@ TEST(SymbolicModelBisimulationDecomposition, TwoDice_Cudd) { decomposition2.compute(); quotient = decomposition2.getQuotient(); - EXPECT_EQ(40ul, quotient->getNumberOfStates()); - EXPECT_EQ(110ul, quotient->getNumberOfTransitions()); + EXPECT_EQ(11ul, quotient->getNumberOfStates()); + EXPECT_EQ(34ul, quotient->getNumberOfTransitions()); EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType()); EXPECT_TRUE(quotient->isSymbolicModel()); - EXPECT_EQ(66ul, (quotient->as>()->getNumberOfChoices())); + EXPECT_EQ(19ul, (quotient->as>()->getNumberOfChoices())); } TEST(SymbolicModelBisimulationDecomposition, AsynchronousLeader_Cudd) { @@ -125,11 +125,11 @@ TEST(SymbolicModelBisimulationDecomposition, AsynchronousLeader_Cudd) { decomposition.compute(); std::shared_ptr> quotient = decomposition.getQuotient(); - EXPECT_EQ(1166ul, quotient->getNumberOfStates()); - EXPECT_EQ(2769ul, quotient->getNumberOfTransitions()); + EXPECT_EQ(252ul, quotient->getNumberOfStates()); + EXPECT_EQ(624ul, quotient->getNumberOfTransitions()); EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType()); EXPECT_TRUE(quotient->isSymbolicModel()); - EXPECT_EQ(2237ul, (quotient->as>()->getNumberOfChoices())); + EXPECT_EQ(500ul, (quotient->as>()->getNumberOfChoices())); std::vector> formulas; formulas.push_back(formula); @@ -138,9 +138,9 @@ TEST(SymbolicModelBisimulationDecomposition, AsynchronousLeader_Cudd) { decomposition2.compute(); quotient = decomposition2.getQuotient(); - EXPECT_EQ(1166ul, quotient->getNumberOfStates()); - EXPECT_EQ(2769ul, quotient->getNumberOfTransitions()); + EXPECT_EQ(1107ul, quotient->getNumberOfStates()); + EXPECT_EQ(2684ul, quotient->getNumberOfTransitions()); EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType()); EXPECT_TRUE(quotient->isSymbolicModel()); - EXPECT_EQ(2237ul, (quotient->as>()->getNumberOfChoices())); + EXPECT_EQ(2152ul, (quotient->as>()->getNumberOfChoices())); }