diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index c17b2fda9..f541ef4d2 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -7,7 +7,6 @@ namespace storm { namespace cli { - template void verifySparseModel(std::shared_ptr> model, std::vector> const& formulas) { for (auto const& formula : formulas) { @@ -86,7 +85,6 @@ namespace storm { } } - template void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { std::shared_ptr model = buildSymbolicModel(program, formulas); @@ -127,6 +125,7 @@ namespace storm { STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files."); std::shared_ptr model = buildExplicitModel(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional(), settings.isChoiceLabelingSet() ? settings.getChoiceLabelingFilename() : boost::optional()); + // Preprocess the model if needed. model = preprocessModel(model, formulas); diff --git a/src/utility/storm.h b/src/utility/storm.h index 3281d342b..c7fe8581d 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -131,7 +131,7 @@ namespace storm { options = typename storm::storage::DeterministicModelBisimulationDecomposition::Options(*sparseModel, formulas); } if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) { - options.weak = true; + options.type = storm::storage::BisimulationType::Weak; options.bounded = false; } @@ -231,7 +231,6 @@ namespace storm { return result; } - #ifdef STORM_HAVE_CARL inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::models::sparse::Dtmc::ConstraintCollector const& constraintCollector, std::string const& path) { diff --git a/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp b/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp index f9ff877eb..881e2514a 100644 --- a/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp +++ b/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp @@ -69,30 +69,30 @@ TEST(DeterministicModelBisimulationDecomposition, Crowds) { ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); std::shared_ptr> dtmc = abstractModel->as>(); -// storm::storage::DeterministicModelBisimulationDecomposition> bisim(*dtmc); + storm::storage::DeterministicModelBisimulationDecomposition> bisim(*dtmc); std::shared_ptr> result; -// ASSERT_NO_THROW(bisim.computeBisimulationDecomposition()); -// ASSERT_NO_THROW(result = bisim.getQuotient()); -// -// EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType()); -// EXPECT_EQ(334ul, result->getNumberOfStates()); -// EXPECT_EQ(546ul, result->getNumberOfTransitions()); - -//#ifdef WINDOWS -// storm::storage::DeterministicModelBisimulationDecomposition>::Options options; -//#else -// typename storm::storage::DeterministicModelBisimulationDecomposition>::Options options; -//#endif -// options.respectedAtomicPropositions = std::set({"observe0Greater1"}); -// -// storm::storage::DeterministicModelBisimulationDecomposition> bisim2(*dtmc, options); -// ASSERT_NO_THROW(bisim2.computeBisimulationDecomposition()); -// ASSERT_NO_THROW(result = bisim2.getQuotient()); -// -// EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType()); -// EXPECT_EQ(65ul, result->getNumberOfStates()); -// EXPECT_EQ(105ul, result->getNumberOfTransitions()); -// + ASSERT_NO_THROW(bisim.computeBisimulationDecomposition()); + ASSERT_NO_THROW(result = bisim.getQuotient()); + + EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType()); + EXPECT_EQ(334ul, result->getNumberOfStates()); + EXPECT_EQ(546ul, result->getNumberOfTransitions()); + +#ifdef WINDOWS + storm::storage::DeterministicModelBisimulationDecomposition>::Options options; +#else + typename storm::storage::DeterministicModelBisimulationDecomposition>::Options options; +#endif + options.respectedAtomicPropositions = std::set({"observe0Greater1"}); + + storm::storage::DeterministicModelBisimulationDecomposition> bisim2(*dtmc, options); + ASSERT_NO_THROW(bisim2.computeBisimulationDecomposition()); + ASSERT_NO_THROW(result = bisim2.getQuotient()); + + EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType()); + EXPECT_EQ(65ul, result->getNumberOfStates()); + EXPECT_EQ(105ul, result->getNumberOfTransitions()); + // options.bounded = false; // options.type = storm::storage::BisimulationType::Weak; // @@ -119,34 +119,34 @@ TEST(DeterministicModelBisimulationDecomposition, Crowds) { EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType()); EXPECT_EQ(64ul, result->getNumberOfStates()); EXPECT_EQ(104ul, result->getNumberOfTransitions()); -// -// auto probabilityOperatorFormula = std::make_shared(eventuallyFormula); -// -//#ifdef WINDOWS -// storm::storage::DeterministicModelBisimulationDecomposition>::Options options3(*dtmc, *probabilityOperatorFormula); -//#else -// typename storm::storage::DeterministicModelBisimulationDecomposition>::Options options3(*dtmc, *probabilityOperatorFormula); -//#endif -// storm::storage::DeterministicModelBisimulationDecomposition> bisim5(*dtmc, options3); -// ASSERT_NO_THROW(bisim5.computeBisimulationDecomposition()); -// ASSERT_NO_THROW(result = bisim5.getQuotient()); -// -// EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType()); -// EXPECT_EQ(64ul, result->getNumberOfStates()); -// EXPECT_EQ(104ul, result->getNumberOfTransitions()); -// -// auto boundedUntilFormula = std::make_shared(std::make_shared(true), labelFormula, 50); -// -//#ifdef WINDOWS -// storm::storage::DeterministicModelBisimulationDecomposition>::Options options4(*dtmc, *boundedUntilFormula); -//#else -// typename storm::storage::DeterministicModelBisimulationDecomposition>::Options options4(*dtmc, *boundedUntilFormula); -//#endif -// storm::storage::DeterministicModelBisimulationDecomposition> bisim6(*dtmc, options4); -// ASSERT_NO_THROW(bisim6.computeBisimulationDecomposition()); -// ASSERT_NO_THROW(result = bisim6.getQuotient()); -// -// EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType()); -// EXPECT_EQ(65ul, result->getNumberOfStates()); -// EXPECT_EQ(105ul, result->getNumberOfTransitions()); + + auto probabilityOperatorFormula = std::make_shared(eventuallyFormula); + +#ifdef WINDOWS + storm::storage::DeterministicModelBisimulationDecomposition>::Options options3(*dtmc, *probabilityOperatorFormula); +#else + typename storm::storage::DeterministicModelBisimulationDecomposition>::Options options3(*dtmc, *probabilityOperatorFormula); +#endif + storm::storage::DeterministicModelBisimulationDecomposition> bisim5(*dtmc, options3); + ASSERT_NO_THROW(bisim5.computeBisimulationDecomposition()); + ASSERT_NO_THROW(result = bisim5.getQuotient()); + + EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType()); + EXPECT_EQ(64ul, result->getNumberOfStates()); + EXPECT_EQ(104ul, result->getNumberOfTransitions()); + + auto boundedUntilFormula = std::make_shared(std::make_shared(true), labelFormula, 50); + +#ifdef WINDOWS + storm::storage::DeterministicModelBisimulationDecomposition>::Options options4(*dtmc, *boundedUntilFormula); +#else + typename storm::storage::DeterministicModelBisimulationDecomposition>::Options options4(*dtmc, *boundedUntilFormula); +#endif + storm::storage::DeterministicModelBisimulationDecomposition> bisim6(*dtmc, options4); + ASSERT_NO_THROW(bisim6.computeBisimulationDecomposition()); + ASSERT_NO_THROW(result = bisim6.getQuotient()); + + EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType()); + EXPECT_EQ(65ul, result->getNumberOfStates()); + EXPECT_EQ(105ul, result->getNumberOfTransitions()); }