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

performance tests now compile again. also fixed some warnings 

Former-commit-id: 2fa8c2abd9
main
dehnert 10 years ago
parent
6c5f6b5d5e
commit
29716ea5f8
16 changed files with 164 additions and 269 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/logic/BinaryPathFormula.h
  2. 2
      src/logic/BinaryStateFormula.h
  3. 2
      src/logic/UnaryPathFormula.h
  4. 2
      src/logic/UnaryStateFormula.h
  5. 2
      src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
  6. 2
      src/models/sparse/DeterministicModel.h
  7. 8
      src/models/sparse/Model.h
  8. 4
      src/models/sparse/NondeterministicModel.h
  9. 4
      src/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp
  10. 4
      src/storage/dd/CuddAdd.h
  11. 1
      test/performance/graph/GraphTest.cpp
  12. 6
      test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
  13. 96
      test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
  14. 5
      test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
  15. 108
      test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
  16. 185
      test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp

2
src/logic/BinaryPathFormula.h
View File

@ -32,7 +32,7 @@ namespace storm {
virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override; virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override; virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const;
virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
private: private:
std::shared_ptr<Formula const> leftSubformula; std::shared_ptr<Formula const> leftSubformula;

2
src/logic/BinaryStateFormula.h
View File

@ -30,7 +30,7 @@ namespace storm {
virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override; virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override; virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const;
virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
private: private:
std::shared_ptr<Formula const> leftSubformula; std::shared_ptr<Formula const> leftSubformula;

2
src/logic/UnaryPathFormula.h
View File

@ -30,7 +30,7 @@ namespace storm {
virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override; virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override; virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const;
virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
private: private:
std::shared_ptr<Formula const> subformula; std::shared_ptr<Formula const> subformula;

2
src/logic/UnaryStateFormula.h
View File

@ -29,7 +29,7 @@ namespace storm {
virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override; virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override; virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const;
virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
private: private:
std::shared_ptr<Formula const> subformula; std::shared_ptr<Formula const> subformula;

2
src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
View File

@ -25,7 +25,7 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override; virtual std::unique_ptr<CheckResult> computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional<std::string> const& rewardModelName = boost::optional<std::string>(), bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override; virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional<std::string> const& rewardModelName = boost::optional<std::string>(), bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
virtual std::unique_ptr<CheckResult> computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override; virtual std::unique_ptr<CheckResult> computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
virtual std::unique_ptr<CheckResult> computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>());
virtual std::unique_ptr<CheckResult> computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
private: private:
// An object that is used for retrieving solvers for systems of linear equations that are the result of nondeterministic choices. // An object that is used for retrieving solvers for systems of linear equations that are the result of nondeterministic choices.

2
src/models/sparse/DeterministicModel.h
View File

@ -54,7 +54,7 @@ namespace storm {
virtual void reduceToStateBasedRewards() override; virtual void reduceToStateBasedRewards() override;
virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector<ValueType> const* firstValue = nullptr, std::vector<ValueType> const* secondValue = nullptr, std::vector<uint_fast64_t> const* stateColoring = nullptr, std::vector<std::string> const* colors = nullptr, std::vector<uint_fast64_t>* scheduler = nullptr, bool finalizeOutput = true) const;
virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector<ValueType> const* firstValue = nullptr, std::vector<ValueType> const* secondValue = nullptr, std::vector<uint_fast64_t> const* stateColoring = nullptr, std::vector<std::string> const* colors = nullptr, std::vector<uint_fast64_t>* scheduler = nullptr, bool finalizeOutput = true) const override;
}; };
} // namespace sparse } // namespace sparse

8
src/models/sparse/Model.h
View File

@ -91,14 +91,14 @@ namespace storm {
* *
* @return The number of states of the model. * @return The number of states of the model.
*/ */
virtual uint_fast64_t getNumberOfStates() const;
virtual uint_fast64_t getNumberOfStates() const override;
/*! /*!
* Returns the number of (non-zero) transitions of the model. * Returns the number of (non-zero) transitions of the model.
* *
* @return The number of (non-zero) transitions of the model. * @return The number of (non-zero) transitions of the model.
*/ */
virtual uint_fast64_t getNumberOfTransitions() const;
virtual uint_fast64_t getNumberOfTransitions() const override;
/*! /*!
* Retrieves the initial states of the model. * Retrieves the initial states of the model.
@ -228,14 +228,14 @@ namespace storm {
* *
* @return The size of the internal representation of the model measured in bytes. * @return The size of the internal representation of the model measured in bytes.
*/ */
virtual std::size_t getSizeInBytes() const;
virtual std::size_t getSizeInBytes() const override;
/*! /*!
* Prints information about the model to the specified stream. * Prints information about the model to the specified stream.
* *
* @param out The stream the information is to be printed to. * @param out The stream the information is to be printed to.
*/ */
virtual void printModelInformationToStream(std::ostream& out) const;
virtual void printModelInformationToStream(std::ostream& out) const override;
/*! /*!
* Exports the model to the dot-format and prints the result to the given stream. * Exports the model to the dot-format and prints the result to the given stream.

4
src/models/sparse/NondeterministicModel.h
View File

@ -75,9 +75,9 @@ namespace storm {
virtual void reduceToStateBasedRewards() override; virtual void reduceToStateBasedRewards() override;
virtual void printModelInformationToStream(std::ostream& out) const;
virtual void printModelInformationToStream(std::ostream& out) const override;
virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector<ValueType> const* firstValue = nullptr, std::vector<ValueType> const* secondValue = nullptr, std::vector<uint_fast64_t> const* stateColoring = nullptr, std::vector<std::string> const* colors = nullptr, std::vector<uint_fast64_t>* scheduler = nullptr, bool finalizeOutput = true) const;
virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector<ValueType> const* firstValue = nullptr, std::vector<ValueType> const* secondValue = nullptr, std::vector<uint_fast64_t> const* stateColoring = nullptr, std::vector<std::string> const* colors = nullptr, std::vector<uint_fast64_t>* scheduler = nullptr, bool finalizeOutput = true) const override;
}; };
} // namespace sparse } // namespace sparse

4
src/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp
View File

@ -53,10 +53,6 @@ namespace storm {
} }
bool TopologicalValueIterationEquationSolverSettings::check() const { bool TopologicalValueIterationEquationSolverSettings::check() const {
bool optionsSet = isMaximalIterationCountSet() || isPrecisionSet() || isConvergenceCriterionSet();
//STORM_LOG_WARN_COND(storm::settings::generalSettings().getEquationSolver() == storm::settings::modules::GeneralSettings::EquationSolver::Gmmxx || !optionsSet, "gmm++ is not selected as the equation solver, so setting options for gmm++ has no effect.");
return true; return true;
} }

4
src/storage/dd/CuddAdd.h
View File

@ -406,7 +406,7 @@ namespace storm {
* *
* @return The support represented as a BDD. * @return The support represented as a BDD.
*/ */
Bdd<DdType::CUDD> getSupport() const;
Bdd<DdType::CUDD> getSupport() const override;
/*! /*!
* Retrieves the number of encodings that are mapped to a non-zero value. * Retrieves the number of encodings that are mapped to a non-zero value.
@ -610,7 +610,7 @@ namespace storm {
* *
* @param filename The name of the file to which the DD is to be exported. * @param filename The name of the file to which the DD is to be exported.
*/ */
void exportToDot(std::string const& filename = "") const;
void exportToDot(std::string const& filename = "") const override;
/*! /*!
* Retrieves an iterator that points to the first meta variable assignment with a non-zero function value. * Retrieves an iterator that points to the first meta variable assignment with a non-zero function value.

1
test/performance/graph/GraphTest.cpp
View File

@ -6,6 +6,7 @@
#include "src/storage/StronglyConnectedComponentDecomposition.h" #include "src/storage/StronglyConnectedComponentDecomposition.h"
#include "src/models/sparse/Mdp.h" #include "src/models/sparse/Mdp.h"
#include "src/models/sparse/Dtmc.h" #include "src/models/sparse/Dtmc.h"
#include "src/models/sparse/StandardRewardModel.h"
TEST(GraphTest, ExplicitProb01) { TEST(GraphTest, ExplicitProb01) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", ""); std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", "");

6
test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
View File

@ -8,7 +8,7 @@
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/utility/solver.h" #include "src/utility/solver.h"
#include "src/parser/AutoParser.h" #include "src/parser/AutoParser.h"
#include "src/models/sparse/StandardRewardModel.h"
TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", ""); std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", "");
@ -20,7 +20,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
ASSERT_EQ(2036647ull, dtmc->getNumberOfStates()); ASSERT_EQ(2036647ull, dtmc->getNumberOfStates());
ASSERT_EQ(7362293ull, dtmc->getNumberOfTransitions()); ASSERT_EQ(7362293ull, dtmc->getNumberOfTransitions());
storm::modelchecker::SparseDtmcPrctlModelChecker<double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observe0Greater1"); auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observe0Greater1");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula); auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
@ -58,7 +58,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
ASSERT_EQ(1312334ull, dtmc->getNumberOfStates()); ASSERT_EQ(1312334ull, dtmc->getNumberOfStates());
ASSERT_EQ(1574477ull, dtmc->getNumberOfTransitions()); ASSERT_EQ(1574477ull, dtmc->getNumberOfTransitions());
storm::modelchecker::SparseDtmcPrctlModelChecker<double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected"); auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula); auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);

96
test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
View File

@ -7,64 +7,63 @@
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/utility/solver.h" #include "src/utility/solver.h"
#include "src/parser/AutoParser.h" #include "src/parser/AutoParser.h"
#include "src/models/sparse/StandardRewardModel.h"
#include "src/parser/FormulaParser.h"
TEST(GmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { TEST(GmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew"); std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew");
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp);
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>(); std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
ASSERT_EQ(2095783ull, mdp->getNumberOfStates()); ASSERT_EQ(2095783ull, mdp->getNumberOfStates());
ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions()); ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions());
storm::modelchecker::SparseMdpPrctlModelChecker<double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
auto minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minProbabilityOperatorFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
auto maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
formula = parser.parseFromString("Pmax=? [F \"elected\"]");
result = checker.check(*maxProbabilityOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula>(trueFormula, labelFormula, 25);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, boundedUntilFormula);
formula = parser.parseFromString("Pmin=? [F<=25 \"elected\"]");
result = checker.check(*minProbabilityOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision());
maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, boundedUntilFormula);
formula = parser.parseFromString("Pmax=? [F<=25 \"elected\"]");
result = checker.check(*maxProbabilityOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
auto minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmin=? [F \"elected\"]");
result = checker.check(*minRewardOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(6.172433512, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(6.172433512, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision());
auto maxRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmax=? [F \"elected\"]");
result = checker.check(*maxRewardOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(6.1724344, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(6.1724344, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -75,85 +74,68 @@ TEST(GmxxMdpPrctlModelCheckerTest, Consensus) {
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp);
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>(); std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
ASSERT_EQ(63616ull, mdp->getNumberOfStates()); ASSERT_EQ(63616ull, mdp->getNumberOfStates());
ASSERT_EQ(213472ull, mdp->getNumberOfTransitions()); ASSERT_EQ(213472ull, mdp->getNumberOfTransitions());
storm::modelchecker::SparseMdpPrctlModelChecker<double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
auto minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"finished\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minProbabilityOperatorFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult1[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0, quantitativeResult1[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto labelFormula2 = std::make_shared<storm::logic::AtomicLabelFormula>("all_coins_equal_0");
auto andFormula = std::make_shared<storm::logic::BinaryBooleanStateFormula>(storm::logic::BinaryBooleanStateFormula::OperatorType::And, labelFormula, labelFormula2);
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(andFormula);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
formula = parser.parseFromString("Pmin=? [F \"finished\" & \"all_coins_equal_0\"]");
result = checker.check(*minProbabilityOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.4374282832, quantitativeResult2[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.4374282832, quantitativeResult2[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
labelFormula2 = std::make_shared<storm::logic::AtomicLabelFormula>("all_coins_equal_1");
andFormula = std::make_shared<storm::logic::BinaryBooleanStateFormula>(storm::logic::BinaryBooleanStateFormula::OperatorType::And, labelFormula, labelFormula2);
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(andFormula);
auto maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
formula = parser.parseFromString("Pmax=? [F \"finished\" & \"all_coins_equal_1\"]");
result = checker.check(*maxProbabilityOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.5293286369, quantitativeResult3[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.5293286369, quantitativeResult3[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
labelFormula2 = std::make_shared<storm::logic::AtomicLabelFormula>("agree");
auto notFormula = std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, labelFormula2);
andFormula = std::make_shared<storm::logic::BinaryBooleanStateFormula>(storm::logic::BinaryBooleanStateFormula::OperatorType::And, labelFormula, notFormula);
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(andFormula);
maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
formula = parser.parseFromString("Pmax=? [F \"finished\" & !\"agree\"]");
result = checker.check(*maxProbabilityOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.10414097, quantitativeResult4[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.10414097, quantitativeResult4[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula>(trueFormula, labelFormula, 50);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, boundedUntilFormula);
formula = parser.parseFromString("Pmin=? [F<=50 \"finished\"]");
result = checker.check(*minProbabilityOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult5[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0, quantitativeResult5[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, boundedUntilFormula);
formula = parser.parseFromString("Pmax=? [F<=50 \"finished\"]");
result = checker.check(*maxProbabilityOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult6[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0, quantitativeResult6[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
auto minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmin=? [F \"finished\"]");
result = checker.check(*minRewardOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1725.593313, quantitativeResult7[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1725.593313, quantitativeResult7[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
auto maxRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmax=? [F \"finished\"]");
result = checker.check(*maxRewardOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult8 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult8 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(2183.142422, quantitativeResult8[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(2183.142422, quantitativeResult8[31168], storm::settings::nativeEquationSolverSettings().getPrecision());

5
test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
View File

@ -9,6 +9,7 @@
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/utility/solver.h" #include "src/utility/solver.h"
#include "src/parser/AutoParser.h" #include "src/parser/AutoParser.h"
#include "src/models/sparse/StandardRewardModel.h"
TEST(NativeDtmcPrctlModelCheckerTest, Crowds) { TEST(NativeDtmcPrctlModelCheckerTest, Crowds) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", ""); std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", "");
@ -20,7 +21,7 @@ TEST(NativeDtmcPrctlModelCheckerTest, Crowds) {
ASSERT_EQ(2036647ull, dtmc->getNumberOfStates()); ASSERT_EQ(2036647ull, dtmc->getNumberOfStates());
ASSERT_EQ(7362293ull, dtmc->getNumberOfTransitions()); ASSERT_EQ(7362293ull, dtmc->getNumberOfTransitions());
storm::modelchecker::SparseDtmcPrctlModelChecker<double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observe0Greater1"); auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observe0Greater1");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula); auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
@ -58,7 +59,7 @@ TEST(NativeDtmcPrctlModelCheckerTest, SynchronousLeader) {
ASSERT_EQ(1312334ull, dtmc->getNumberOfStates()); ASSERT_EQ(1312334ull, dtmc->getNumberOfStates());
ASSERT_EQ(1574477ull, dtmc->getNumberOfTransitions()); ASSERT_EQ(1574477ull, dtmc->getNumberOfTransitions());
storm::modelchecker::SparseDtmcPrctlModelChecker<double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected"); auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula); auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);

108
test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
View File

@ -8,64 +8,63 @@
#include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/settings/modules/NativeEquationSolverSettings.h"
#include "src/utility/solver.h" #include "src/utility/solver.h"
#include "src/parser/AutoParser.h" #include "src/parser/AutoParser.h"
#include "src/models/sparse/StandardRewardModel.h"
#include "src/parser/FormulaParser.h"
TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew"); std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew");
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp);
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>(); std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
ASSERT_EQ(2095783ull, mdp->getNumberOfStates()); ASSERT_EQ(2095783ull, mdp->getNumberOfStates());
ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions()); ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions());
storm::modelchecker::SparseMdpPrctlModelChecker<double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
auto minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minProbabilityOperatorFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
auto maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
formula = parser.parseFromString("Pmax=? [F \"elected\"]");
result = checker.check(*maxProbabilityOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula>(trueFormula, labelFormula, 25);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, boundedUntilFormula);
result = checker.check(*minProbabilityOperatorFormula);
formula = parser.parseFromString("Pmin=? [F<=25 \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision());
maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, boundedUntilFormula);
formula = parser.parseFromString("Pmax=? [F<=25 \"elected\"]");
result = checker.check(*maxProbabilityOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
auto minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
result = checker.check(*minRewardOperatorFormula);
formula = parser.parseFromString("Rmin=? [F \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(6.172433512, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(6.172433512, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision());
auto maxRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmax=? [F \"elected\"]");
result = checker.check(*maxRewardOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(6.1724344, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(6.1724344, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -76,85 +75,68 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp);
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>(); std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
ASSERT_EQ(63616ull, mdp->getNumberOfStates()); ASSERT_EQ(63616ull, mdp->getNumberOfStates());
ASSERT_EQ(213472ull, mdp->getNumberOfTransitions()); ASSERT_EQ(213472ull, mdp->getNumberOfTransitions());
storm::modelchecker::SparseMdpPrctlModelChecker<double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
auto minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minProbabilityOperatorFormula);
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"finished\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult1[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0, quantitativeResult1[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto labelFormula2 = std::make_shared<storm::logic::AtomicLabelFormula>("all_coins_equal_0");
auto andFormula = std::make_shared<storm::logic::BinaryBooleanStateFormula>(storm::logic::BinaryBooleanStateFormula::OperatorType::And, labelFormula, labelFormula2);
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(andFormula);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
formula = parser.parseFromString("Pmin=? [F \"finished\" & \"all_coins_equal_0\"]");
result = checker.check(*minProbabilityOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.4374282832, quantitativeResult2[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.4374282832, quantitativeResult2[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
labelFormula2 = std::make_shared<storm::logic::AtomicLabelFormula>("all_coins_equal_1");
andFormula = std::make_shared<storm::logic::BinaryBooleanStateFormula>(storm::logic::BinaryBooleanStateFormula::OperatorType::And, labelFormula, labelFormula2);
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(andFormula);
auto maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
formula = parser.parseFromString("Pmax=? [F \"finished\" & \"all_coins_equal_1\"]");
result = checker.check(*maxProbabilityOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.5293286369, quantitativeResult3[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.5293286369, quantitativeResult3[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
labelFormula2 = std::make_shared<storm::logic::AtomicLabelFormula>("agree");
auto notFormula = std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, labelFormula2);
andFormula = std::make_shared<storm::logic::BinaryBooleanStateFormula>(storm::logic::BinaryBooleanStateFormula::OperatorType::And, labelFormula, notFormula);
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(andFormula);
maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
result = checker.check(*maxProbabilityOperatorFormula);
formula = parser.parseFromString("Pmax=? [F \"finished\" & !\"agree\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.10414097, quantitativeResult4[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.10414097, quantitativeResult4[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula>(trueFormula, labelFormula, 50);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, boundedUntilFormula);
result = checker.check(*minProbabilityOperatorFormula);
formula = parser.parseFromString("Pmin=? [F<=50 \"finished\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult5[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0, quantitativeResult5[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, boundedUntilFormula);
formula = parser.parseFromString("Pmax=? [F<=50 \"finished\"]");
result = checker.check(*maxProbabilityOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult6[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0, quantitativeResult6[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
auto minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
result = checker.check(*minRewardOperatorFormula);
formula = parser.parseFromString("Rmin=? [F \"finished\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1725.593313, quantitativeResult7[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1725.593313, quantitativeResult7[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
auto maxRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmax=? [F \"finished\"]");
result = checker.check(*maxRewardOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult8 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult8 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(2183.142422, quantitativeResult8[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(2183.142422, quantitativeResult8[31168], storm::settings::nativeEquationSolverSettings().getPrecision());

185
test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
View File

@ -8,74 +8,51 @@
#include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h" #include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h"
#include "src/settings/SettingMemento.h" #include "src/settings/SettingMemento.h"
#include "src/parser/AutoParser.h" #include "src/parser/AutoParser.h"
#include "src/models/sparse/StandardRewardModel.h"
#include "src/parser/FormulaParser.h"
TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) { TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) {
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew")->as<storm::models::sparse::Mdp<double>>(); std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew")->as<storm::models::sparse::Mdp<double>>();
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull); ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull);
storm::modelchecker::SparseMdpPrctlModelChecker<double> mc(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>()));
auto apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(apFormula);
auto probFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = mc.check(*probFormula);
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 1.0),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probFormula.reset();
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(apFormula);
probFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
result = mc.check(*probFormula);
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 1.0),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probFormula.reset();
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>()));
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto boundedEventuallyFormula = std::make_shared<storm::logic::BoundedUntilFormula>(std::make_shared<storm::logic::BooleanLiteralFormula>(true), apFormula, 25);
probFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, boundedEventuallyFormula);
result = mc.check(*probFormula);
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 0.0),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probFormula.reset();
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
boundedEventuallyFormula = std::make_shared<storm::logic::BoundedUntilFormula>(std::make_shared<storm::logic::BooleanLiteralFormula>(true), apFormula, 25);
probFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, boundedEventuallyFormula);
result = mc.check(*probFormula);
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 0.0),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probFormula.reset();
ASSERT_NEAR(1.0, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(apFormula);
auto rewardFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
formula = parser.parseFromString("Pmax=? [F \"elected\"]");
result = checker.check(*formula);
ASSERT_NEAR(1.0, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
result = mc.check(*rewardFormula);
formula = parser.parseFromString("Pmin=? [F<=25 \"elected\"]");
result = checker.check(*formula);
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 6.172433512),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
rewardFormula.reset();
ASSERT_NEAR(0.0, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(apFormula);
rewardFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
formula = parser.parseFromString("Pmax=? [F<=25 \"elected\"]");
result = checker.check(*formula);
ASSERT_NEAR(0.0, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
result = mc.check(*rewardFormula);
formula = parser.parseFromString("Rmin=? [F \"elected\"]");
result = checker.check(*formula);
ASSERT_NEAR(6.172433512, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 6.1724344),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
rewardFormula.reset();
formula = parser.parseFromString("Rmax=? [F \"elected\"]");
result = checker.check(*formula);
ASSERT_NEAR(6.1724344, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
} }
TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, Consensus) { TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, Consensus) {
@ -84,96 +61,52 @@ TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, Consensus) {
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", "")->as<storm::models::sparse::Mdp<double>>(); std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", "")->as<storm::models::sparse::Mdp<double>>();
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
ASSERT_EQ(mdp->getNumberOfStates(), 63616ull); ASSERT_EQ(mdp->getNumberOfStates(), 63616ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull);
storm::modelchecker::SparseMdpPrctlModelChecker<double> mc(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>()));
auto apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(apFormula);
auto probFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"finished\"]");
auto result = mc.check(*probFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[31168] - 1.0),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probFormula.reset();
ASSERT_NEAR(1.0, result->asExplicitQuantitativeCheckResult<double>()[31168], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto apFormula2 = std::make_shared<storm::logic::AtomicLabelFormula>("all_coins_equal_0");
auto andFormula = std::make_shared<storm::logic::BinaryBooleanStateFormula>(storm::logic::BinaryBooleanStateFormula::OperatorType::And, apFormula, apFormula2);
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(andFormula);
probFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
formula = parser.parseFromString("Pmin=? [F \"finished\" & \"all_coins_equal_0\"]");
result = mc.check(*probFormula);
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[31168] - 0.4374282832),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probFormula.reset();
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
apFormula2 = std::make_shared<storm::logic::AtomicLabelFormula>("all_coins_equal_1");
andFormula = std::make_shared<storm::logic::BinaryBooleanStateFormula>(storm::logic::BinaryBooleanStateFormula::OperatorType::And, apFormula, apFormula2);
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(andFormula);
probFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
result = checker.check(*formula);
ASSERT_NEAR(0.4374282832, result->asExplicitQuantitativeCheckResult<double>()[31168], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
result = mc.check(*probFormula);
formula = parser.parseFromString("Pmax=? [F \"finished\" & \"all_coins_equal_1\"]");
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[31168] - 0.5293286369),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probFormula.reset();
result = checker.check(*formula);
ASSERT_NEAR(0.5293286369, result->asExplicitQuantitativeCheckResult<double>()[31168], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
apFormula2 = std::make_shared<storm::logic::AtomicLabelFormula>("agree");
auto notFormula = std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, apFormula2);
andFormula = std::make_shared<storm::logic::BinaryBooleanStateFormula>(storm::logic::BinaryBooleanStateFormula::OperatorType::And, apFormula, notFormula);
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(andFormula);
probFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
result = mc.check(*probFormula);
formula = parser.parseFromString("Pmax=? [F \"finished\" & !\"agree\"]");
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[31168] - 0.10414097),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probFormula.reset();
result = checker.check(*formula);
ASSERT_NEAR(0.10414097, result->asExplicitQuantitativeCheckResult<double>()[31168], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto boundedEventuallyFormula = std::make_shared<storm::logic::BoundedUntilFormula>(std::make_shared<storm::logic::BooleanLiteralFormula>(true), apFormula, 50ull);
probFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
result = mc.check(*probFormula);
formula = parser.parseFromString("Pmin=? [F<=50 \"finished\"]");
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[31168] - 0.0),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probFormula.reset();
result = checker.check(*formula);
ASSERT_NEAR(0.0, result->asExplicitQuantitativeCheckResult<double>()[31168], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
boundedEventuallyFormula = std::make_shared<storm::logic::BoundedUntilFormula>(std::make_shared<storm::logic::BooleanLiteralFormula>(true), apFormula, 50ull);
probFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
formula = parser.parseFromString("Pmax=? [F<=50 \"finished\"]");
result = mc.check(*probFormula);
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[31168] - 0.0),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probFormula.reset();
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(apFormula);
auto rewardFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
result = checker.check(*formula);
ASSERT_NEAR(0.0, result->asExplicitQuantitativeCheckResult<double>()[31168], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
result = mc.check(*rewardFormula);
formula = parser.parseFromString("Rmin=? [F \"finished\"]");
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[31168] - 1725.593313),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probFormula.reset();
result = checker.check(*formula);
ASSERT_NEAR(1725.593313, result->asExplicitQuantitativeCheckResult<double>()[31168], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(apFormula);
rewardFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
result = mc.check(*rewardFormula);
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[31168] - 2183.142422),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probFormula.reset();
formula = parser.parseFromString("Rmax=? [F \"finished\"\"]");
result = checker.check(*formula);
ASSERT_NEAR(2183.142422, result->asExplicitQuantitativeCheckResult<double>()[31168], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
} }
Write Preview
Loading…
Cancel
Save