From 712faae653be929a282c7cd0ef363aee91f92ca7 Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Thu, 20 Sep 2018 11:06:20 +0200 Subject: [PATCH] Create test for LatticeExtender --- .../analysis/LatticeExtenderTest.cpp | 98 +++++++++++++++++++ 1 file changed, 98 insertions(+) create mode 100644 src/test/storm-pars/analysis/LatticeExtenderTest.cpp diff --git a/src/test/storm-pars/analysis/LatticeExtenderTest.cpp b/src/test/storm-pars/analysis/LatticeExtenderTest.cpp new file mode 100644 index 000000000..59f739b84 --- /dev/null +++ b/src/test/storm-pars/analysis/LatticeExtenderTest.cpp @@ -0,0 +1,98 @@ +// +// Created by Jip Spel on 20.09.18. +// + +// TODO: cleanup includes +#include "gtest/gtest.h" +#include "storm-config.h" +#include "test/storm_gtest.h" + +#include "storm-parsers/parser/FormulaParser.h" +#include "storm/logic/Formulas.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm-parsers/parser/AutoParser.h" +#include "storm-parsers/parser/PrismParser.h" +#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/api/builder.h" + +#include "storm-pars/analysis/Lattice.h" +#include "storm-pars/analysis/LatticeExtender.h" +#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" + +#include "storm-pars/api/storm-pars.h" +#include "storm/api/storm.h" + +#include "storm-parsers/api/storm-parsers.h" + +TEST(LatticeExtenderTest, Brp_with_bisimulation) { + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; + std::string formulaAsString = "P=? [F s=4 & i=N ]"; + std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + // Program and formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> dtmc = model->as>(); + auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); + model = simplifier.getSimplifiedModel(); + + // Apply bisimulation + storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong; + if (storm::settings::getModule().isWeakBisimulationSet()) { + bisimType = storm::storage::BisimulationType::Weak; + } + + dtmc = storm::api::performBisimulationMinimization(model, formulas, bisimType)->as>(); + + ASSERT_EQ(dtmc->getNumberOfStates(), 99ull); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 195ull); + + auto *extender = new storm::analysis::LatticeExtender(dtmc); + auto criticalTuple = extender->toLattice(formulas); + EXPECT_EQ(dtmc->getNumberOfStates(), std::get<1>(criticalTuple)); + EXPECT_EQ(dtmc->getNumberOfStates(), std::get<2>(criticalTuple)); + + auto lattice = std::get<0>(criticalTuple); + for (auto i = 0; i < dtmc->getNumberOfStates(); ++i) { + EXPECT_TRUE(lattice->getAddedStates()[i]); + } + + // Check on some nodes + EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice->compare(1,0)); + EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice->compare(1,5)); + EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice->compare(5,0)); + EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice->compare(94,5)); + EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, lattice->compare(7,13)); +} + +TEST(LatticeExtenderTest, Brp_without_bisimulation) { + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; + std::string formulaAsString = "P=? [F s=4 & i=N ]"; + std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + // Program and formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> dtmc = model->as>(); + auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); + model = simplifier.getSimplifiedModel(); + dtmc = model->as>(); + + ASSERT_EQ(dtmc->getNumberOfStates(), 193ull); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 383ull); + + auto *extender = new storm::analysis::LatticeExtender(dtmc); + auto criticalTuple = extender->toLattice(formulas); + EXPECT_EQ(183, std::get<1>(criticalTuple)); + EXPECT_EQ(186, std::get<2>(criticalTuple)); +} + +