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

using exact data types for smt-based multi objective model checking tests. Also disabled a few tests that test (yet) unsupported queries or that take too long.

tempestpy_adaptions
TimQu 8 years ago
parent
1d329176ba
commit
f558cb866c
2 changed files with 7 additions and 46 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 26
      src/test/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp
  2. 27
      src/test/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp

26
src/test/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp
View File

@ -20,7 +20,7 @@ TEST(SparseMaCbMultiObjectiveModelCheckerTest, server) {
storm::prism::Program program = storm::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, "");
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program));
std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> ma = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::MarkovAutomaton<double>>();
std::shared_ptr<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>> ma = storm::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>();
uint_fast64_t const initState = *ma->getInitialStates().begin();
std::unique_ptr<storm::modelchecker::CheckResult> result;
@ -32,26 +32,4 @@ TEST(SparseMaCbMultiObjectiveModelCheckerTest, server) {
result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased);
ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]);
}
TEST(SparseMaCbMultiObjectiveModelCheckerTest, jobscheduler_achievability_3Obj) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma";
std::string formulasAsString = "multi(T<=1.31 [ F \"all_jobs_finished\" ], P>=0.17 [ F<=0.2 \"half_of_jobs_finished\" ], P<=0.31 [ F \"slowest_before_fastest\" ]) "; //true
formulasAsString += "; multi(T<=1.29 [ F \"all_jobs_finished\" ], P>=0.18 [ F<=0.2 \"half_of_jobs_finished\" ], P<=0.29 [ F \"slowest_before_fastest\" ])"; //false
storm::prism::Program program = storm::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, "");
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program));
std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> ma = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::MarkovAutomaton<double>>();
uint_fast64_t const initState = *ma->getInitialStates().begin();
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased);
ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
std::unique_ptr<storm::modelchecker::CheckResult> result2 = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased);
ASSERT_TRUE(result2->isExplicitQualitativeCheckResult());
EXPECT_FALSE(result2->asExplicitQualitativeCheckResult()[initState]);
}
}

27
src/test/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp
View File

@ -20,13 +20,10 @@ TEST(SparseMdpCbMultiObjectiveModelCheckerTest, consensus) {
storm::prism::Program program = storm::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, "");
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program));
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp = storm::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
uint_fast64_t const initState = *mdp->getInitialStates().begin();;
std::unique_ptr<storm::modelchecker::CheckResult> result;
// noQuantitativeYet result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased);
// noQuantitativeYet ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
// noQuantitativeYet EXPECT_NEAR(0.10833260970000025, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased);
ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
@ -48,7 +45,7 @@ TEST(SparseMdpCbMultiObjectiveModelCheckerTest, zeroconf) {
storm::prism::Program program = storm::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, "");
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program));
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp = storm::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
uint_fast64_t const initState = *mdp->getInitialStates().begin();
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased);
@ -56,6 +53,7 @@ TEST(SparseMdpCbMultiObjectiveModelCheckerTest, zeroconf) {
EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
}
/* This test takes a little bit too long ...
TEST(SparseMdpCbMultiObjectiveModelCheckerTest, team3with3objectives) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_team3.nm";
@ -65,27 +63,12 @@ TEST(SparseMdpCbMultiObjectiveModelCheckerTest, team3with3objectives) {
storm::prism::Program program = storm::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, "");
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program));
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp = storm::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
uint_fast64_t const initState = *mdp->getInitialStates().begin();
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased);
ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]);
}
TEST(SparseMdpCbMultiObjectiveModelCheckerTest, scheduler) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_scheduler05.nm";
std::string formulasAsString = "multi(R{\"time\"}<= 11.778[ F \"tasks_complete\" ], R{\"energy\"}<=1.45 [ F \"tasks_complete\" ]) ";
// programm, model, formula
storm::prism::Program program = storm::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, "");
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program));
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
uint_fast64_t const initState = *mdp->getInitialStates().begin();
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased);
EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
}
*/
Write Preview
Loading…
Cancel
Save