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

fixing settings/tests

main
dehnert 7 years ago
parent
4134630fa6
commit
5706831ad6
3 changed files with 109 additions and 50 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. 4
      src/storm/settings/modules/AbstractionSettings.cpp
  2. 7
      src/storm/settings/modules/AbstractionSettings.h
  3. 148
      src/test/storm/abstraction/PrismMenuGameTest.cpp

4
src/storm/settings/modules/AbstractionSettings.cpp
View File

@ -180,6 +180,10 @@ namespace storm {
this->getOption(addAllGuardsOptionName).getArgumentByName("value").setFromStringValue(value ? "on" : "off");
}
void AbstractionSettings::setAddAllInitialExpressions(bool value) {
this->getOption(addInitialExpressionsOptionName).getArgumentByName("value").setFromStringValue(value ? "on" : "off");
}
bool AbstractionSettings::isUseInterpolationSet() const {
return this->getOption(useInterpolationOptionName).getArgumentByName("value").getValueAsString() == "on";
}

7
src/storm/settings/modules/AbstractionSettings.h
View File

@ -76,6 +76,13 @@ namespace storm {
*/
void setAddAllGuards(bool value);
/*!
* Sets the option to add all initial expressions to the specified value.
*
* @param value The new value.
*/
void setAddAllInitialExpressions(bool value);
/*!
* Retrieves whether the option to use interpolation was set.
*

148
src/test/storm/abstraction/PrismMenuGameTest.cpp
View File

@ -23,7 +23,9 @@
#include "storm/settings/modules/AbstractionSettings.h"
TEST(PrismMenuGame, DieAbstractionTest_Cudd) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
auto& settings = storm::settings::mutableAbstractionSettings();
settings.setAddAllGuards(false);
settings.setAddAllInitialExpressions(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
@ -47,8 +49,10 @@ TEST(PrismMenuGame, DieAbstractionTest_Cudd) {
}
TEST(PrismMenuGame, DieAbstractionTest_Sylvan) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
auto& settings = storm::settings::mutableAbstractionSettings();
settings.setAddAllGuards(false);
settings.setAddAllInitialExpressions(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
std::vector<storm::expressions::Expression> initialPredicates;
@ -97,8 +101,10 @@ TEST(PrismMenuGame, DieAbstractionTest_Sylvan) {
#endif
TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Cudd) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
auto& settings = storm::settings::mutableAbstractionSettings();
settings.setAddAllGuards(false);
settings.setAddAllInitialExpressions(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
std::vector<storm::expressions::Expression> initialPredicates;
@ -124,8 +130,10 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Cudd) {
}
TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Sylvan) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
auto& settings = storm::settings::mutableAbstractionSettings();
settings.setAddAllGuards(false);
settings.setAddAllInitialExpressions(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
std::vector<storm::expressions::Expression> initialPredicates;
@ -151,8 +159,10 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Sylvan) {
}
TEST(PrismMenuGame, DieFullAbstractionTest_Cudd) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
auto& settings = storm::settings::mutableAbstractionSettings();
settings.setAddAllGuards(false);
settings.setAddAllInitialExpressions(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
std::vector<storm::expressions::Expression> initialPredicates;
@ -191,8 +201,10 @@ TEST(PrismMenuGame, DieFullAbstractionTest_Cudd) {
}
TEST(PrismMenuGame, DieFullAbstractionTest_Sylvan) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
auto& settings = storm::settings::mutableAbstractionSettings();
settings.setAddAllGuards(false);
settings.setAddAllInitialExpressions(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
std::vector<storm::expressions::Expression> initialPredicates;
@ -231,8 +243,10 @@ TEST(PrismMenuGame, DieFullAbstractionTest_Sylvan) {
}
TEST(PrismMenuGame, CrowdsAbstractionTest_Cudd) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
auto& settings = storm::settings::mutableAbstractionSettings();
settings.setAddAllGuards(false);
settings.setAddAllInitialExpressions(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
program = program.substituteConstants();
@ -257,8 +271,10 @@ TEST(PrismMenuGame, CrowdsAbstractionTest_Cudd) {
}
TEST(PrismMenuGame, CrowdsAbstractionTest_Sylvan) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
auto& settings = storm::settings::mutableAbstractionSettings();
settings.setAddAllGuards(false);
settings.setAddAllInitialExpressions(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
program = program.substituteConstants();
@ -283,8 +299,10 @@ TEST(PrismMenuGame, CrowdsAbstractionTest_Sylvan) {
}
TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Cudd) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
auto& settings = storm::settings::mutableAbstractionSettings();
settings.setAddAllGuards(false);
settings.setAddAllInitialExpressions(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
program = program.substituteConstants();
@ -311,8 +329,10 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Cudd) {
}
TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Sylvan) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
auto& settings = storm::settings::mutableAbstractionSettings();
settings.setAddAllGuards(false);
settings.setAddAllInitialExpressions(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
program = program.substituteConstants();
@ -339,8 +359,10 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Sylvan) {
}
TEST(PrismMenuGame, CrowdsFullAbstractionTest_Cudd) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
auto& settings = storm::settings::mutableAbstractionSettings();
settings.setAddAllGuards(false);
settings.setAddAllInitialExpressions(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
program = program.substituteConstants();
@ -419,8 +441,10 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest_Cudd) {
}
TEST(PrismMenuGame, CrowdsFullAbstractionTest_Sylvan) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
auto& settings = storm::settings::mutableAbstractionSettings();
settings.setAddAllGuards(false);
settings.setAddAllInitialExpressions(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
program = program.substituteConstants();
@ -499,8 +523,10 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest_Sylvan) {
}
TEST(PrismMenuGame, TwoDiceAbstractionTest_Cudd) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
auto& settings = storm::settings::mutableAbstractionSettings();
settings.setAddAllGuards(false);
settings.setAddAllInitialExpressions(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
program = program.substituteConstants();
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
@ -527,8 +553,10 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest_Cudd) {
}
TEST(PrismMenuGame, TwoDiceAbstractionTest_Sylvan) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
auto& settings = storm::settings::mutableAbstractionSettings();
settings.setAddAllGuards(false);
settings.setAddAllInitialExpressions(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
program = program.substituteConstants();
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
@ -555,8 +583,10 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest_Sylvan) {
}
TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Cudd) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
auto& settings = storm::settings::mutableAbstractionSettings();
settings.setAddAllGuards(false);
settings.setAddAllInitialExpressions(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
program = program.substituteConstants();
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
@ -585,8 +615,10 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Cudd) {
}
TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Sylvan) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
auto& settings = storm::settings::mutableAbstractionSettings();
settings.setAddAllGuards(false);
settings.setAddAllInitialExpressions(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
program = program.substituteConstants();
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
@ -615,8 +647,10 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Sylvan) {
}
TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Cudd) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
auto& settings = storm::settings::mutableAbstractionSettings();
settings.setAddAllGuards(false);
settings.setAddAllInitialExpressions(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
program = program.substituteConstants();
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
@ -674,8 +708,10 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Cudd) {
}
TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Sylvan) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
auto& settings = storm::settings::mutableAbstractionSettings();
settings.setAddAllGuards(false);
settings.setAddAllInitialExpressions(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
program = program.substituteConstants();
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
@ -733,8 +769,10 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Sylvan) {
}
TEST(PrismMenuGame, WlanAbstractionTest_Cudd) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
auto& settings = storm::settings::mutableAbstractionSettings();
settings.setAddAllGuards(false);
settings.setAddAllInitialExpressions(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm");
program = program.substituteConstants();
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
@ -754,7 +792,7 @@ TEST(PrismMenuGame, WlanAbstractionTest_Cudd) {
storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractor.abstract();
EXPECT_EQ(915ull, game.getNumberOfTransitions());
EXPECT_EQ(903ull, game.getNumberOfTransitions());
EXPECT_EQ(8ull, game.getNumberOfStates());
EXPECT_EQ(4ull, game.getBottomStates().getNonZeroCount());
@ -762,8 +800,10 @@ TEST(PrismMenuGame, WlanAbstractionTest_Cudd) {
}
TEST(PrismMenuGame, WlanAbstractionTest_Sylvan) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
auto& settings = storm::settings::mutableAbstractionSettings();
settings.setAddAllGuards(false);
settings.setAddAllInitialExpressions(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm");
program = program.substituteConstants();
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
@ -783,7 +823,7 @@ TEST(PrismMenuGame, WlanAbstractionTest_Sylvan) {
storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractor.abstract();
EXPECT_EQ(915ull, game.getNumberOfTransitions());
EXPECT_EQ(903ull, game.getNumberOfTransitions());
EXPECT_EQ(8ull, game.getNumberOfStates());
EXPECT_EQ(4ull, game.getBottomStates().getNonZeroCount());
@ -791,7 +831,9 @@ TEST(PrismMenuGame, WlanAbstractionTest_Sylvan) {
}
TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Cudd) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
auto& settings = storm::settings::mutableAbstractionSettings();
settings.setAddAllGuards(false);
settings.setAddAllInitialExpressions(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm");
program = program.substituteConstants();
@ -814,7 +856,7 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Cudd) {
storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractor.abstract();
EXPECT_EQ(1824ull, game.getNumberOfTransitions());
EXPECT_EQ(1800ull, game.getNumberOfTransitions());
EXPECT_EQ(16ull, game.getNumberOfStates());
EXPECT_EQ(8ull, game.getBottomStates().getNonZeroCount());
@ -822,8 +864,10 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Cudd) {
}
TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Sylvan) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
auto& settings = storm::settings::mutableAbstractionSettings();
settings.setAddAllGuards(false);
settings.setAddAllInitialExpressions(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm");
program = program.substituteConstants();
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
@ -845,7 +889,7 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Sylvan) {
storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractor.abstract();
EXPECT_EQ(1824ull, game.getNumberOfTransitions());
EXPECT_EQ(1800ull, game.getNumberOfTransitions());
EXPECT_EQ(16ull, game.getNumberOfStates());
EXPECT_EQ(8ull, game.getBottomStates().getNonZeroCount());
@ -853,8 +897,10 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Sylvan) {
}
TEST(PrismMenuGame, WlanFullAbstractionTest_Cudd) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
auto& settings = storm::settings::mutableAbstractionSettings();
settings.setAddAllGuards(false);
settings.setAddAllInitialExpressions(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm");
program = program.substituteConstants();
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
@ -980,8 +1026,10 @@ TEST(PrismMenuGame, WlanFullAbstractionTest_Cudd) {
}
TEST(PrismMenuGame, WlanFullAbstractionTest_Sylvan) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
auto& settings = storm::settings::mutableAbstractionSettings();
settings.setAddAllGuards(false);
settings.setAddAllInitialExpressions(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm");
program = program.substituteConstants();
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());

Write Preview
Loading…
Cancel
Save