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

started replacing ValueType template argument by model class in all instantiations 

Former-commit-id: 197e3876a4
main
dehnert 10 years ago
parent
5beb33e3d8
commit
72cb30d6b0
9 changed files with 62 additions and 64 deletions
Unified View
  1. 8
      src/counterexamples/MILPMinimalLabelSetGenerator.h
  2. 16
      src/utility/cli.h
  3. 8
      test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
  4. 22
      test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
  5. 8
      test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
  6. 8
      test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
  7. 22
      test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
  8. 28
      test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
  9. 6
      test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp

8
src/counterexamples/MILPMinimalLabelSetGenerator.h
View File

@ -6,7 +6,7 @@
#include "src/models/sparse/Mdp.h" #include "src/models/sparse/Mdp.h"
#include "src/logic/Formulas.h" #include "src/logic/Formulas.h"
#include "src/storage/prism/Program.h" #include "src/storage/prism/Program.h"
#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h"
#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/exceptions/NotImplementedException.h" #include "src/exceptions/NotImplementedException.h"
@ -932,8 +932,8 @@ namespace storm {
// (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set. // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set.
double maximalReachabilityProbability = 0; double maximalReachabilityProbability = 0;
if (checkThresholdFeasible) { if (checkThresholdFeasible) {
storm::modelchecker::SparseMdpPrctlModelChecker<T> modelchecker(labeledMdp); storm::modelchecker::helper::SparseMdpPrctlHelper<T> modelcheckerHelper;
std::vector<T> result = modelchecker.computeUntilProbabilitiesHelper(false, phiStates, psiStates, false); std::vector<T> result = modelcheckerHelper.computeUntilProbabilities(false, labeledMdp.getTransitionMatrix(), labeledMdp.getBackwardTransitions(), phiStates, psiStates, false, storm::utility::solver::MinMaxLinearEquationSolverFactory<T>());
for (auto state : labeledMdp.getInitialStates()) { for (auto state : labeledMdp.getInitialStates()) {
maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]);
} }
@ -991,7 +991,7 @@ namespace storm {
storm::storage::BitVector phiStates; storm::storage::BitVector phiStates;
storm::storage::BitVector psiStates; storm::storage::BitVector psiStates;
storm::modelchecker::SparseMdpPrctlModelChecker<T> modelchecker(labeledMdp); storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Mdp<T>> modelchecker(labeledMdp);
if (probabilityOperator.getSubformula().isUntilFormula()) { if (probabilityOperator.getSubformula().isUntilFormula()) {
storm::logic::UntilFormula const& untilFormula = probabilityOperator.getSubformula().asUntilFormula(); storm::logic::UntilFormula const& untilFormula = probabilityOperator.getSubformula().asUntilFormula();

16
src/utility/cli.h
View File

@ -72,9 +72,7 @@ namespace storm {
namespace utility { namespace utility {
namespace cli { namespace cli {
std::string getCurrentWorkingDirectory();
std::string getCurrentWorkingDirectory();
void printHeader(const int argc, const char* argv[]); void printHeader(const int argc, const char* argv[]);
@ -213,11 +211,11 @@ namespace storm {
std::unique_ptr<storm::modelchecker::CheckResult> result; std::unique_ptr<storm::modelchecker::CheckResult> result;
if (model->getType() == storm::models::ModelType::Dtmc) { if (model->getType() == storm::models::ModelType::Dtmc) {
std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>(); std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>();
storm::modelchecker::SparseDtmcPrctlModelChecker<ValueType> modelchecker(*dtmc); storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker(*dtmc);
if (modelchecker.canHandle(*formula.get())) { if (modelchecker.canHandle(*formula.get())) {
result = modelchecker.check(*formula.get()); result = modelchecker.check(*formula.get());
} else { } else {
storm::modelchecker::SparseDtmcEliminationModelChecker<ValueType> modelchecker2(*dtmc); storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker2(*dtmc);
if (modelchecker2.canHandle(*formula.get())) { if (modelchecker2.canHandle(*formula.get())) {
result = modelchecker2.check(*formula.get()); result = modelchecker2.check(*formula.get());
} }
@ -229,17 +227,17 @@ namespace storm {
storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker<ValueType> modelchecker(*mdp); storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker<ValueType> modelchecker(*mdp);
result = modelchecker.check(*formula.get()); result = modelchecker.check(*formula.get());
} else { } else {
storm::modelchecker::SparseMdpPrctlModelChecker<ValueType> modelchecker(*mdp); storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> modelchecker(*mdp);
result = modelchecker.check(*formula.get()); result = modelchecker.check(*formula.get());
} }
#else #else
storm::modelchecker::SparseMdpPrctlModelChecker<ValueType> modelchecker(*mdp); storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> modelchecker(*mdp);
result = modelchecker.check(*formula.get()); result = modelchecker.check(*formula.get());
#endif #endif
} else if (model->getType() == storm::models::ModelType::Ctmc) { } else if (model->getType() == storm::models::ModelType::Ctmc) {
std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> ctmc = model->template as<storm::models::sparse::Ctmc<ValueType>>(); std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> ctmc = model->template as<storm::models::sparse::Ctmc<ValueType>>();
storm::modelchecker::SparseCtmcCslModelChecker<ValueType> modelchecker(*ctmc); storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<ValueType>> modelchecker(*ctmc);
result = modelchecker.check(*formula.get()); result = modelchecker.check(*formula.get());
} }
@ -281,7 +279,7 @@ namespace storm {
std::cout << std::endl << "Model checking property: " << *formula << " ..."; std::cout << std::endl << "Model checking property: " << *formula << " ...";
std::unique_ptr<storm::modelchecker::CheckResult> result; std::unique_ptr<storm::modelchecker::CheckResult> result;
storm::modelchecker::SparseDtmcEliminationModelChecker<storm::RationalFunction> modelchecker(*dtmc); storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>> modelchecker(*dtmc);
if (modelchecker.canHandle(*formula.get())) { if (modelchecker.canHandle(*formula.get())) {
result = modelchecker.check(*formula.get()); result = modelchecker.check(*formula.get());
} else { } else {

8
test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
View File

@ -37,7 +37,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) {
uint_fast64_t initialState = *ctmc->getInitialStates().begin(); uint_fast64_t initialState = *ctmc->getInitialStates().begin();
// Create model checker. // Create model checker.
storm::modelchecker::SparseCtmcCslModelChecker<double> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>())); storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<double>> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
// Start checking properties. // Start checking properties.
formula = formulaParser.parseFromString("P=? [ F<=100 !\"minimum\"]"); formula = formulaParser.parseFromString("P=? [ F<=100 !\"minimum\"]");
@ -121,7 +121,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Embedded) {
uint_fast64_t initialState = *ctmc->getInitialStates().begin(); uint_fast64_t initialState = *ctmc->getInitialStates().begin();
// Create model checker. // Create model checker.
storm::modelchecker::SparseCtmcCslModelChecker<double> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>())); storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<double>> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
// Start checking properties. // Start checking properties.
formula = formulaParser.parseFromString("P=? [ F<=10000 \"down\"]"); formula = formulaParser.parseFromString("P=? [ F<=10000 \"down\"]");
@ -183,7 +183,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Polling) {
uint_fast64_t initialState = *ctmc->getInitialStates().begin(); uint_fast64_t initialState = *ctmc->getInitialStates().begin();
// Create model checker. // Create model checker.
storm::modelchecker::SparseCtmcCslModelChecker<double> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>())); storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<double>> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
// Start checking properties. // Start checking properties.
formula = formulaParser.parseFromString("P=?[ F<=10 \"target\"]"); formula = formulaParser.parseFromString("P=?[ F<=10 \"target\"]");
@ -231,7 +231,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Tandem) {
uint_fast64_t initialState = *ctmc->getInitialStates().begin(); uint_fast64_t initialState = *ctmc->getInitialStates().begin();
// Create model checker. // Create model checker.
storm::modelchecker::SparseCtmcCslModelChecker<double> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>())); storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<double>> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
// Start checking properties. // Start checking properties.
formula = formulaParser.parseFromString("P=? [ F<=10 \"network_full\" ]"); formula = formulaParser.parseFromString("P=? [ F<=10 \"network_full\" ]");

22
test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
View File

@ -21,7 +21,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) {
ASSERT_EQ(dtmc->getNumberOfStates(), 13ull); ASSERT_EQ(dtmc->getNumberOfStates(), 13ull);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull); ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull);
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>("one"); auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("one");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula); auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
@ -66,7 +66,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
ASSERT_EQ(8607ull, dtmc->getNumberOfStates()); ASSERT_EQ(8607ull, dtmc->getNumberOfStates());
ASSERT_EQ(15113ull, dtmc->getNumberOfTransitions()); ASSERT_EQ(15113ull, 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);
@ -102,7 +102,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
ASSERT_EQ(12400ull, dtmc->getNumberOfStates()); ASSERT_EQ(12400ull, dtmc->getNumberOfStates());
ASSERT_EQ(16495ull, dtmc->getNumberOfTransitions()); ASSERT_EQ(16495ull, 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);
@ -144,9 +144,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) {
ap.addLabel("a"); ap.addLabel("a");
ap.addLabelToState("a", 1); ap.addLabelToState("a", 1);
dtmc.reset(new storm::models::sparse::Dtmc<double>(transitionMatrix, ap, boost::none, boost::none, boost::none)); dtmc.reset(new storm::models::sparse::Dtmc<double>(transitionMatrix, ap));
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>("a"); auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("a");
auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(labelFormula); auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(labelFormula);
@ -169,9 +169,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) {
ap.addLabel("a"); ap.addLabel("a");
ap.addLabelToState("a", 1); ap.addLabelToState("a", 1);
dtmc.reset(new storm::models::sparse::Dtmc<double>(transitionMatrix, ap, boost::none, boost::none, boost::none)); dtmc.reset(new storm::models::sparse::Dtmc<double>(transitionMatrix, ap));
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>("a"); auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("a");
auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(labelFormula); auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(labelFormula);
@ -194,9 +194,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) {
ap.addLabel("a"); ap.addLabel("a");
ap.addLabelToState("a", 2); ap.addLabelToState("a", 2);
dtmc.reset(new storm::models::sparse::Dtmc<double>(transitionMatrix, ap, boost::none, boost::none, boost::none)); dtmc.reset(new storm::models::sparse::Dtmc<double>(transitionMatrix, ap));
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>("a"); auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("a");
auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(labelFormula); auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(labelFormula);
@ -255,9 +255,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRA) {
ap.addLabelToState("a", 13); ap.addLabelToState("a", 13);
ap.addLabelToState("a", 14); ap.addLabelToState("a", 14);
mdp.reset(new storm::models::sparse::Dtmc<double>(transitionMatrix, ap, boost::none, boost::none, boost::none)); mdp.reset(new storm::models::sparse::Dtmc<double>(transitionMatrix, ap));
storm::modelchecker::SparseDtmcPrctlModelChecker<double> checker(*mdp, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>())); storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("a"); auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("a");
auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(labelFormula); auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(labelFormula);

8
test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
View File

@ -21,7 +21,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
ASSERT_EQ(mdp->getNumberOfStates(), 169ull); ASSERT_EQ(mdp->getNumberOfStates(), 169ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull);
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>("two"); auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("two");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula); auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
@ -93,7 +93,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::sparse::Mdp<double>> stateRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>(); std::shared_ptr<storm::models::sparse::Mdp<double>> stateRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
storm::modelchecker::SparseMdpPrctlModelChecker<double> stateRewardModelChecker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>())); storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done"); labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula); reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
@ -117,7 +117,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::sparse::Mdp<double>> stateAndTransitionRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>(); std::shared_ptr<storm::models::sparse::Mdp<double>> stateAndTransitionRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
storm::modelchecker::SparseMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>())); storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done"); labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula); reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
@ -146,7 +146,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
ASSERT_EQ(3172ull, mdp->getNumberOfStates()); ASSERT_EQ(3172ull, mdp->getNumberOfStates());
ASSERT_EQ(7144ull, mdp->getNumberOfTransitions()); ASSERT_EQ(7144ull, 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 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);

8
test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
View File

@ -37,7 +37,7 @@ TEST(SparseCtmcCslModelCheckerTest, Cluster) {
uint_fast64_t initialState = *ctmc->getInitialStates().begin(); uint_fast64_t initialState = *ctmc->getInitialStates().begin();
// Create model checker. // Create model checker.
storm::modelchecker::SparseCtmcCslModelChecker<double> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>())); storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<double>> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
// Start checking properties. // Start checking properties.
formula = formulaParser.parseFromString("P=? [ F<=100 !\"minimum\"]"); formula = formulaParser.parseFromString("P=? [ F<=100 !\"minimum\"]");
@ -113,7 +113,7 @@ TEST(SparseCtmcCslModelCheckerTest, Embedded) {
uint_fast64_t initialState = *ctmc->getInitialStates().begin(); uint_fast64_t initialState = *ctmc->getInitialStates().begin();
// Create model checker. // Create model checker.
storm::modelchecker::SparseCtmcCslModelChecker<double> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>())); storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<double>> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
// Start checking properties. // Start checking properties.
formula = formulaParser.parseFromString("P=? [ F<=10000 \"down\"]"); formula = formulaParser.parseFromString("P=? [ F<=10000 \"down\"]");
@ -168,7 +168,7 @@ TEST(SparseCtmcCslModelCheckerTest, Polling) {
uint_fast64_t initialState = *ctmc->getInitialStates().begin(); uint_fast64_t initialState = *ctmc->getInitialStates().begin();
// Create model checker. // Create model checker.
storm::modelchecker::SparseCtmcCslModelChecker<double> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>())); storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<double>> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
// Start checking properties. // Start checking properties.
formula = formulaParser.parseFromString("P=?[ F<=10 \"target\"]"); formula = formulaParser.parseFromString("P=?[ F<=10 \"target\"]");
@ -209,7 +209,7 @@ TEST(SparseCtmcCslModelCheckerTest, Tandem) {
uint_fast64_t initialState = *ctmc->getInitialStates().begin(); uint_fast64_t initialState = *ctmc->getInitialStates().begin();
// Create model checker. // Create model checker.
storm::modelchecker::SparseCtmcCslModelChecker<double> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>())); storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<double>> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
// Start checking properties. // Start checking properties.
formula = formulaParser.parseFromString("P=? [ F<=10 \"network_full\" ]"); formula = formulaParser.parseFromString("P=? [ F<=10 \"network_full\" ]");

22
test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
View File

@ -22,7 +22,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, Die) {
ASSERT_EQ(dtmc->getNumberOfStates(), 13ull); ASSERT_EQ(dtmc->getNumberOfStates(), 13ull);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull); ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull);
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>("one"); auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("one");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula); auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
@ -67,7 +67,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, Crowds) {
ASSERT_EQ(8607ull, dtmc->getNumberOfStates()); ASSERT_EQ(8607ull, dtmc->getNumberOfStates());
ASSERT_EQ(15113ull, dtmc->getNumberOfTransitions()); ASSERT_EQ(15113ull, 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);
@ -103,7 +103,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, SynchronousLeader) {
ASSERT_EQ(12400ull, dtmc->getNumberOfStates()); ASSERT_EQ(12400ull, dtmc->getNumberOfStates());
ASSERT_EQ(16495ull, dtmc->getNumberOfTransitions()); ASSERT_EQ(16495ull, 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);
@ -145,9 +145,9 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) {
ap.addLabel("a"); ap.addLabel("a");
ap.addLabelToState("a", 1); ap.addLabelToState("a", 1);
dtmc.reset(new storm::models::sparse::Dtmc<double>(transitionMatrix, ap, boost::none, boost::none, boost::none)); dtmc.reset(new storm::models::sparse::Dtmc<double>(transitionMatrix, ap));
storm::modelchecker::SparseDtmcPrctlModelChecker<double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>(storm::solver::NativeLinearEquationSolver<double>::SolutionMethod::SOR, 0.9))); storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>(storm::solver::NativeLinearEquationSolver<double>::SolutionMethod::SOR, 0.9)));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("a"); auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("a");
auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(labelFormula); auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(labelFormula);
@ -170,9 +170,9 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) {
ap.addLabel("a"); ap.addLabel("a");
ap.addLabelToState("a", 1); ap.addLabelToState("a", 1);
dtmc.reset(new storm::models::sparse::Dtmc<double>(transitionMatrix, ap, boost::none, boost::none, boost::none)); dtmc.reset(new storm::models::sparse::Dtmc<double>(transitionMatrix, ap));
storm::modelchecker::SparseDtmcPrctlModelChecker<double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>(storm::solver::NativeLinearEquationSolver<double>::SolutionMethod::SOR, 0.9))); storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>(storm::solver::NativeLinearEquationSolver<double>::SolutionMethod::SOR, 0.9)));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("a"); auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("a");
auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(labelFormula); auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(labelFormula);
@ -195,9 +195,9 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) {
ap.addLabel("a"); ap.addLabel("a");
ap.addLabelToState("a", 2); ap.addLabelToState("a", 2);
dtmc.reset(new storm::models::sparse::Dtmc<double>(transitionMatrix, ap, boost::none, boost::none, boost::none)); dtmc.reset(new storm::models::sparse::Dtmc<double>(transitionMatrix, ap));
storm::modelchecker::SparseDtmcPrctlModelChecker<double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>(storm::solver::NativeLinearEquationSolver<double>::SolutionMethod::SOR, 0.9))); storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>(storm::solver::NativeLinearEquationSolver<double>::SolutionMethod::SOR, 0.9)));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("a"); auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("a");
auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(labelFormula); auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(labelFormula);
@ -256,9 +256,9 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRA) {
ap.addLabelToState("a", 13); ap.addLabelToState("a", 13);
ap.addLabelToState("a", 14); ap.addLabelToState("a", 14);
mdp.reset(new storm::models::sparse::Dtmc<double>(transitionMatrix, ap, boost::none, boost::none, boost::none)); mdp.reset(new storm::models::sparse::Dtmc<double>(transitionMatrix, ap));
storm::modelchecker::SparseDtmcPrctlModelChecker<double> checker(*mdp, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>(storm::solver::NativeLinearEquationSolver<double>::SolutionMethod::SOR, 0.9))); storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>(storm::solver::NativeLinearEquationSolver<double>::SolutionMethod::SOR, 0.9)));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("a"); auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("a");
auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(labelFormula); auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(labelFormula);

28
test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
View File

@ -20,7 +20,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
ASSERT_EQ(mdp->getNumberOfStates(), 169ull); ASSERT_EQ(mdp->getNumberOfStates(), 169ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull);
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>("two"); auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("two");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula); auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
@ -92,7 +92,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::sparse::Mdp<double>> stateRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>(); std::shared_ptr<storm::models::sparse::Mdp<double>> stateRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
storm::modelchecker::SparseMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>())); storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done"); labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula); reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
@ -116,7 +116,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::sparse::Mdp<double>> stateAndTransitionRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>(); std::shared_ptr<storm::models::sparse::Mdp<double>> stateAndTransitionRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
storm::modelchecker::SparseMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>())); storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done"); labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula); reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
@ -145,7 +145,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
ASSERT_EQ(3172ull, mdp->getNumberOfStates()); ASSERT_EQ(3172ull, mdp->getNumberOfStates());
ASSERT_EQ(7144ull, mdp->getNumberOfTransitions()); ASSERT_EQ(7144ull, 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 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);
@ -211,9 +211,9 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
ap.addLabel("a"); ap.addLabel("a");
ap.addLabelToState("a", 1); ap.addLabelToState("a", 1);
mdp.reset(new storm::models::sparse::Mdp<double>(transitionMatrix, ap, boost::none, boost::none, boost::none)); mdp.reset(new storm::models::sparse::Mdp<double>(transitionMatrix, ap));
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>("a"); auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("a");
auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(storm::logic::OptimalityType::Maximize, labelFormula); auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(storm::logic::OptimalityType::Maximize, labelFormula);
@ -244,9 +244,9 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
ap.addLabel("a"); ap.addLabel("a");
ap.addLabelToState("a", 1); ap.addLabelToState("a", 1);
mdp.reset(new storm::models::sparse::Mdp<double>(transitionMatrix, ap, boost::none, boost::none, boost::none)); mdp.reset(new storm::models::sparse::Mdp<double>(transitionMatrix, ap));
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>("a"); auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("a");
auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(storm::logic::OptimalityType::Maximize, labelFormula); auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(storm::logic::OptimalityType::Maximize, labelFormula);
@ -286,9 +286,9 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
ap.addLabelToState("c", 0); ap.addLabelToState("c", 0);
ap.addLabelToState("c", 2); ap.addLabelToState("c", 2);
mdp.reset(new storm::models::sparse::Mdp<double>(transitionMatrix, ap, boost::none, boost::none, boost::none)); mdp.reset(new storm::models::sparse::Mdp<double>(transitionMatrix, ap));
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>("a"); auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("a");
auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(storm::logic::OptimalityType::Maximize, labelFormula); auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(storm::logic::OptimalityType::Maximize, labelFormula);
@ -372,9 +372,9 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
ap.addLabel("c"); ap.addLabel("c");
ap.addLabelToState("c", 2); ap.addLabelToState("c", 2);
mdp.reset(new storm::models::sparse::Mdp<double>(transitionMatrix, ap, boost::none, boost::none, boost::none)); mdp.reset(new storm::models::sparse::Mdp<double>(transitionMatrix, ap));
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>("a"); auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("a");
auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(storm::logic::OptimalityType::Maximize, labelFormula); auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(storm::logic::OptimalityType::Maximize, labelFormula);
@ -497,9 +497,9 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
ap.addLabelToState("a", 13); ap.addLabelToState("a", 13);
ap.addLabelToState("a", 14); ap.addLabelToState("a", 14);
mdp.reset(new storm::models::sparse::Mdp<double>(transitionMatrix, ap, boost::none, boost::none, boost::none)); mdp.reset(new storm::models::sparse::Mdp<double>(transitionMatrix, ap));
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>("a"); auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("a");
auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(storm::logic::OptimalityType::Maximize, labelFormula); auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(storm::logic::OptimalityType::Maximize, labelFormula);

6
test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp
View File

@ -20,7 +20,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Die) {
ASSERT_EQ(dtmc->getNumberOfStates(), 13ull); ASSERT_EQ(dtmc->getNumberOfStates(), 13ull);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull); ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull);
storm::modelchecker::SparseDtmcEliminationModelChecker<double> checker(*dtmc); storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc);
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("one"); auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("one");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula); auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
@ -65,7 +65,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Crowds) {
ASSERT_EQ(8607ull, dtmc->getNumberOfStates()); ASSERT_EQ(8607ull, dtmc->getNumberOfStates());
ASSERT_EQ(15113ull, dtmc->getNumberOfTransitions()); ASSERT_EQ(15113ull, dtmc->getNumberOfTransitions());
storm::modelchecker::SparseDtmcEliminationModelChecker<double> checker(*dtmc); storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc);
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);
@ -125,7 +125,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, SynchronousLeader) {
ASSERT_EQ(12400ull, dtmc->getNumberOfStates()); ASSERT_EQ(12400ull, dtmc->getNumberOfStates());
ASSERT_EQ(16495ull, dtmc->getNumberOfTransitions()); ASSERT_EQ(16495ull, dtmc->getNumberOfTransitions());
storm::modelchecker::SparseDtmcEliminationModelChecker<double> checker(*dtmc); storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc);
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);

Write Preview
|||||||
100:0
Loading…
Cancel
Save