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

Merge branch 'future' into gspn 

Former-commit-id: 9170d9eba7
tempestpy_adaptions
sjunges 9 years ago
parent
6896a4ca51 6f59fd7aca
commit
9bd2fc70bd
6 changed files with 49 additions and 31 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. 22
      src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
  2. 32
      test/functional/builder/ExplicitPrismModelBuilderTest.cpp
  3. 8
      test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
  4. 8
      test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
  5. 2
      test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
  6. 8
      test/functional/utility/GraphTest.cpp

22
src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
View File

@ -211,13 +211,16 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
std::vector<ValueType> SparseMdpPrctlHelper<ValueType>::computeReachabilityRewardsHelper(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) { std::vector<ValueType> SparseMdpPrctlHelper<ValueType>::computeReachabilityRewardsHelper(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
std::vector<uint_fast64_t> nondeterminsticChoiceIndices = transitionMatrix.getRowGroupIndices();
// Determine which states have a reward of infinity by definition. // Determine which states have a reward of infinity by definition.
storm::storage::BitVector infinityStates; storm::storage::BitVector infinityStates;
storm::storage::BitVector trueStates(transitionMatrix.getRowCount(), true); storm::storage::BitVector trueStates(transitionMatrix.getRowCount(), true);
if (dir == OptimizationDirection::Minimize) { if (dir == OptimizationDirection::Minimize) {
infinityStates = storm::utility::graph::performProb1E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, trueStates, targetStates);
infinityStates = storm::utility::graph::performProb1E(transitionMatrix, nondeterminsticChoiceIndices, backwardTransitions, trueStates, targetStates);
} else { } else {
infinityStates = storm::utility::graph::performProb1A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, trueStates, targetStates);
infinityStates = storm::utility::graph::performProb1A(transitionMatrix, nondeterminsticChoiceIndices, backwardTransitions, trueStates, targetStates);
} }
infinityStates.complement(); infinityStates.complement();
storm::storage::BitVector maybeStates = ~targetStates & ~infinityStates; storm::storage::BitVector maybeStates = ~targetStates & ~infinityStates;
@ -245,6 +248,21 @@ namespace storm {
// Prepare the right-hand side of the equation system. // Prepare the right-hand side of the equation system.
std::vector<ValueType> b = totalStateRewardVectorGetter(submatrix.getRowCount(), transitionMatrix, maybeStates); std::vector<ValueType> b = totalStateRewardVectorGetter(submatrix.getRowCount(), transitionMatrix, maybeStates);
// This also means that -- when minimizing -- we have to set the entries to infinity that have
// any successor that is an "infinity state". This prevents the action from "being taken" and
// forces the choice that leads to a reward less than infinity.
uint_fast64_t currentRow = 0;
for (auto state : maybeStates) {
for (uint_fast64_t row = nondeterminsticChoiceIndices[state]; row < nondeterminsticChoiceIndices[state + 1]; ++row, ++currentRow) {
for (auto const& element : transitionMatrix.getRow(row)) {
if (infinityStates.get(element.getColumn())) {
b[currentRow] = storm::utility::infinity<ValueType>();
break;
}
}
}
}
// Create vector for results for maybe states. // Create vector for results for maybe states.
std::vector<ValueType> x(maybeStates.getNumberOfSetBits()); std::vector<ValueType> x(maybeStates.getNumberOfSetBits());

32
test/functional/builder/ExplicitPrismModelBuilderTest.cpp
View File

@ -10,27 +10,27 @@
TEST(ExplicitPrismModelBuilderTest, Dtmc) { TEST(ExplicitPrismModelBuilderTest, Dtmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions()); EXPECT_EQ(20ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
EXPECT_EQ(677ul, model->getNumberOfStates()); EXPECT_EQ(677ul, model->getNumberOfStates());
EXPECT_EQ(867ul, model->getNumberOfTransitions()); EXPECT_EQ(867ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(8607ul, model->getNumberOfStates());
EXPECT_EQ(15113ul, model->getNumberOfTransitions()); EXPECT_EQ(15113ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(273ul, model->getNumberOfStates());
EXPECT_EQ(397ul, model->getNumberOfTransitions()); EXPECT_EQ(397ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
EXPECT_EQ(1728ul, model->getNumberOfStates()); EXPECT_EQ(1728ul, model->getNumberOfStates());
EXPECT_EQ(2505ul, model->getNumberOfTransitions()); EXPECT_EQ(2505ul, model->getNumberOfTransitions());
} }
@ -41,27 +41,27 @@ TEST(ExplicitPrismModelBuilderTest, Ctmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(276ul, model->getNumberOfStates());
EXPECT_EQ(1120ul, model->getNumberOfTransitions()); EXPECT_EQ(1120ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(3478ul, model->getNumberOfStates());
EXPECT_EQ(14639ul, model->getNumberOfTransitions()); EXPECT_EQ(14639ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(12ul, model->getNumberOfStates());
EXPECT_EQ(22ul, model->getNumberOfTransitions()); EXPECT_EQ(22ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm");
model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(810ul, model->getNumberOfStates());
EXPECT_EQ(3699ul, model->getNumberOfTransitions()); EXPECT_EQ(3699ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
EXPECT_EQ(66ul, model->getNumberOfStates()); EXPECT_EQ(66ul, model->getNumberOfStates());
EXPECT_EQ(189ul, model->getNumberOfTransitions()); EXPECT_EQ(189ul, model->getNumberOfTransitions());
} }
@ -69,32 +69,32 @@ TEST(ExplicitPrismModelBuilderTest, Ctmc) {
TEST(ExplicitPrismModelBuilderTest, Mdp) { TEST(ExplicitPrismModelBuilderTest, Mdp) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
EXPECT_EQ(169ul, model->getNumberOfStates()); EXPECT_EQ(169ul, model->getNumberOfStates());
EXPECT_EQ(436ul, model->getNumberOfTransitions()); EXPECT_EQ(436ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
EXPECT_EQ(364ul, model->getNumberOfStates()); EXPECT_EQ(364ul, model->getNumberOfStates());
EXPECT_EQ(654ul, model->getNumberOfTransitions()); EXPECT_EQ(654ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
EXPECT_EQ(272ul, model->getNumberOfStates()); EXPECT_EQ(272ul, model->getNumberOfStates());
EXPECT_EQ(492ul, model->getNumberOfTransitions()); EXPECT_EQ(492ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
EXPECT_EQ(1038ul, model->getNumberOfStates()); EXPECT_EQ(1038ul, model->getNumberOfStates());
EXPECT_EQ(1282ul, model->getNumberOfTransitions()); EXPECT_EQ(1282ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm"); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
EXPECT_EQ(4093ul, model->getNumberOfStates()); EXPECT_EQ(4093ul, model->getNumberOfStates());
EXPECT_EQ(5585ul, model->getNumberOfTransitions()); EXPECT_EQ(5585ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
EXPECT_EQ(37ul, model->getNumberOfStates()); EXPECT_EQ(37ul, model->getNumberOfStates());
EXPECT_EQ(59ul, model->getNumberOfTransitions()); EXPECT_EQ(59ul, model->getNumberOfTransitions());
} }

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

@ -34,7 +34,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) {
#endif #endif
options.buildAllRewardModels = false; options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_repairs"); options.rewardModelsToBuild.insert("num_repairs");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>(); std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin(); uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@ -117,7 +117,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Embedded) {
#endif #endif
options.buildAllRewardModels = false; options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("up"); options.rewardModelsToBuild.insert("up");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>(); std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin(); uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@ -179,7 +179,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Polling) {
std::shared_ptr<storm::logic::Formula> formula(nullptr); std::shared_ptr<storm::logic::Formula> formula(nullptr);
// Build the model. // Build the model.
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>(); std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin(); uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@ -226,7 +226,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Tandem) {
typename storm::builder::ExplicitPrismModelBuilder<double>::Options options; typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
#endif #endif
options.rewardModelsToBuild.insert("customers"); options.rewardModelsToBuild.insert("customers");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>(); std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin(); uint_fast64_t initialState = *ctmc->getInitialStates().begin();

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

@ -32,7 +32,7 @@ TEST(NativeCtmcCslModelCheckerTest, Cluster) {
#endif #endif
options.buildAllRewardModels = false; options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_repairs"); options.rewardModelsToBuild.insert("num_repairs");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>(); std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin(); uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@ -108,7 +108,7 @@ TEST(NativeCtmcCslModelCheckerTest, Embedded) {
#endif #endif
options.buildAllRewardModels = false; options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("up"); options.rewardModelsToBuild.insert("up");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>(); std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin(); uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@ -163,7 +163,7 @@ TEST(NativeCtmcCslModelCheckerTest, Polling) {
std::shared_ptr<storm::logic::Formula> formula(nullptr); std::shared_ptr<storm::logic::Formula> formula(nullptr);
// Build the model. // Build the model.
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>(); std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin(); uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@ -204,7 +204,7 @@ TEST(NativeCtmcCslModelCheckerTest, Tandem) {
#endif #endif
options.buildAllRewardModels = false; options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("customers"); options.rewardModelsToBuild.insert("customers");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>(); std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin(); uint_fast64_t initialState = *ctmc->getInitialStates().begin();

2
test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
View File

@ -28,7 +28,7 @@ TEST(MilpPermissiveSchedulerTest, DieSelection) {
options.addConstantDefinitionsFromString(program, ""); options.addConstantDefinitionsFromString(program, "");
options.buildCommandLabels = true; options.buildCommandLabels = true;
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options)->as<storm::models::sparse::Mdp<double>>();
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program, options)->as<storm::models::sparse::Mdp<double>>();
boost::optional<storm::ps::SubMDPPermissiveScheduler<>> perms = storm::ps::computePermissiveSchedulerViaMILP<>(*mdp, formula02); boost::optional<storm::ps::SubMDPPermissiveScheduler<>> perms = storm::ps::computePermissiveSchedulerViaMILP<>(*mdp, formula02);
EXPECT_NE(perms, boost::none); EXPECT_NE(perms, boost::none);

8
test/functional/utility/GraphTest.cpp
View File

@ -90,7 +90,7 @@ TEST(GraphTest, SymbolicProb01MinMax) {
TEST(GraphTest, ExplicitProb01) { TEST(GraphTest, ExplicitProb01) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
@ -111,7 +111,7 @@ TEST(GraphTest, ExplicitProb01) {
TEST(GraphTest, ExplicitProb01MinMax) { TEST(GraphTest, ExplicitProb01MinMax) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@ -126,7 +126,7 @@ TEST(GraphTest, ExplicitProb01MinMax) {
EXPECT_EQ(364ul, statesWithProbability01.second.getNumberOfSetBits()); EXPECT_EQ(364ul, statesWithProbability01.second.getNumberOfSetBits());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@ -147,7 +147,7 @@ TEST(GraphTest, ExplicitProb01MinMax) {
EXPECT_EQ(35ul, statesWithProbability01.second.getNumberOfSetBits()); EXPECT_EQ(35ul, statesWithProbability01.second.getNumberOfSetBits());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);

Write Preview
Loading…
Cancel
Save