sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

commented in some more tests, however the main entry points need to be fixed because of the new templating of the bisimulation class 

Former-commit-id: 7133025049
tempestpy_adaptions
dehnert 9 years ago
parent
11c21eb338
commit
1428f1647b
3 changed files with 55 additions and 57 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 3
      src/cli/entrypoints.h
  2. 3
      src/utility/storm.h
  3. 106
      test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp

3
src/cli/entrypoints.h
View File

@ -7,7 +7,6 @@
namespace storm {
namespace cli {
template<typename ValueType>
void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
for (auto const& formula : formulas) {
@ -86,7 +85,6 @@ namespace storm {
}
}
template<typename ValueType>
void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
std::shared_ptr<storm::models::ModelBase> model = buildSymbolicModel<ValueType>(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<storm::models::ModelBase> model = buildExplicitModel<ValueType>(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional<std::string>(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional<std::string>(), settings.isChoiceLabelingSet() ? settings.getChoiceLabelingFilename() : boost::optional<std::string>());
// Preprocess the model if needed.
model = preprocessModel<ValueType>(model, formulas);

3
src/utility/storm.h
View File

@ -131,7 +131,7 @@ namespace storm {
options = typename storm::storage::DeterministicModelBisimulationDecomposition<ValueType>::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<storm::RationalFunction>::ConstraintCollector const& constraintCollector, std::string const& path) {

106
test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp
View File

@ -69,30 +69,30 @@ TEST(DeterministicModelBisimulationDecomposition, Crowds) {
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
// storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim(*dtmc);
storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim(*dtmc);
std::shared_ptr<storm::models::sparse::Model<double>> 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<storm::models::sparse::Dtmc<double>>::Options options;
//#else
// typename storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options options;
//#endif
// options.respectedAtomicPropositions = std::set<std::string>({"observe0Greater1"});
//
// storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> 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<storm::models::sparse::Dtmc<double>>::Options options;
#else
typename storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options options;
#endif
options.respectedAtomicPropositions = std::set<std::string>({"observe0Greater1"});
storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> 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<storm::logic::ProbabilityOperatorFormula>(eventuallyFormula);
//
//#ifdef WINDOWS
// storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options options3(*dtmc, *probabilityOperatorFormula);
//#else
// typename storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options options3(*dtmc, *probabilityOperatorFormula);
//#endif
// storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> 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<storm::logic::BoundedUntilFormula>(std::make_shared<storm::logic::BooleanLiteralFormula>(true), labelFormula, 50);
//
//#ifdef WINDOWS
// storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options options4(*dtmc, *boundedUntilFormula);
//#else
// typename storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options options4(*dtmc, *boundedUntilFormula);
//#endif
// storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> 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<storm::logic::ProbabilityOperatorFormula>(eventuallyFormula);
#ifdef WINDOWS
storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options options3(*dtmc, *probabilityOperatorFormula);
#else
typename storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options options3(*dtmc, *probabilityOperatorFormula);
#endif
storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> 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<storm::logic::BoundedUntilFormula>(std::make_shared<storm::logic::BooleanLiteralFormula>(true), labelFormula, 50);
#ifdef WINDOWS
storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options options4(*dtmc, *boundedUntilFormula);
#else
typename storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options options4(*dtmc, *boundedUntilFormula);
#endif
storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> 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());
}
Write Preview
Loading…
Cancel
Save