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

the abstraction now properly builds an instance of the game class 

Former-commit-id: 26d4effa00
tempestpy_adaptions
dehnert 9 years ago
parent
1199ab95e3
commit
7cd1e6324f
6 changed files with 130 additions and 95 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. 3
      src/models/symbolic/Model.cpp
  2. 4
      src/storage/expressions/Expression.cpp
  3. 8
      src/storage/expressions/Expression.h
  4. 69
      src/storage/prism/menu_games/AbstractProgram.cpp
  5. 39
      src/storage/prism/menu_games/AbstractProgram.h
  6. 102
      test/functional/abstraction/PrismMenuGameTest.cpp

3
src/models/symbolic/Model.cpp
View File

@ -66,11 +66,12 @@ namespace storm {
template<storm::dd::DdType Type>
storm::dd::Bdd<Type> Model<Type>::getStates(std::string const& label) const {
STORM_LOG_THROW(labelToExpressionMap.find(label) != labelToExpressionMap.end(), storm::exceptions::IllegalArgumentException, "The label " << label << " is invalid for the labeling of the model.");
return rowExpressionAdapter->translateExpression(labelToExpressionMap.at(label)).toBdd() && this->reachableStates;
return this->getStates(labelToExpressionMap.at(label));
}
template<storm::dd::DdType Type>
storm::dd::Bdd<Type> Model<Type>::getStates(storm::expressions::Expression const& expression) const {
STORM_LOG_THROW(rowExpressionAdapter != nullptr, storm::exceptions::InvalidOperationException, "Cannot create BDD for expression without expression adapter.");
return rowExpressionAdapter->translateExpression(expression).toBdd() && this->reachableStates;
}

4
src/storage/expressions/Expression.cpp
View File

@ -94,6 +94,10 @@ namespace storm {
bool Expression::isFalse() const {
return this->getBaseExpression().isFalse();
}
bool Expression::isSame(storm::expressions::Expression const& other) const {
return this->expressionPtr == other.expressionPtr;
}
std::set<storm::expressions::Variable> Expression::getVariables() const {
std::set<storm::expressions::Variable> result;

8
src/storage/expressions/Expression.h
View File

@ -190,6 +190,14 @@ namespace storm {
*/
bool isFalse() const;
/*!
* Checks whether the two expressions are the same. Note that this does not check for syntactical or even
* semantical equivalence, but only returns true if both are the very same expressions.
*
* @return True iff the two expressions are the same.
*/
bool isSame(storm::expressions::Expression const& other) const;
/*!
* Retrieves whether this expression is a relation expression, i.e., an expression that has a relation
* (equal, not equal, less, less or equal, etc.) as its top-level operator.

69
src/storage/prism/menu_games/AbstractProgram.cpp
View File

@ -5,6 +5,8 @@
#include "src/storage/dd/CuddDdManager.h"
#include "src/storage/dd/CuddAdd.h"
#include "src/models/symbolic/StandardRewardModel.h"
#include "src/utility/macros.h"
#include "src/utility/solver.h"
#include "src/exceptions/WrongFormatException.h"
@ -15,7 +17,7 @@ namespace storm {
namespace menu_games {
template <storm::dd::DdType DdType, typename ValueType>
AbstractProgram<DdType, ValueType>::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory, bool addAllGuards) : smtSolverFactory(std::move(smtSolverFactory)), ddInformation(std::make_shared<storm::dd::DdManager<DdType>>()), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program), initialStateAbstractor(expressionInformation, ddInformation, *this->smtSolverFactory), lastAbstractBdd(ddInformation.manager->getBddZero()), lastAbstractAdd(ddInformation.manager->getAddZero()), lastReachableStates(ddInformation.manager->getBddZero()) {
AbstractProgram<DdType, ValueType>::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory, bool addAllGuards) : smtSolverFactory(std::move(smtSolverFactory)), ddInformation(std::make_shared<storm::dd::DdManager<DdType>>()), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program), initialStateAbstractor(expressionInformation, ddInformation, *this->smtSolverFactory), currentGame(nullptr) {
// For now, we assume that there is a single module. If the program has more than one module, it needs
// to be flattened before the procedure.
@ -65,10 +67,15 @@ namespace storm {
// Finally, retrieve the command-update probability ADD, so we can multiply it with the abstraction BDD later.
commandUpdateProbabilitiesAdd = modules.front().getCommandUpdateProbabilitiesAdd();
// Finally, we build the game the first time.
currentGame = buildGame();
}
template <storm::dd::DdType DdType, typename ValueType>
void AbstractProgram<DdType, ValueType>::refine(std::vector<storm::expressions::Expression> const& predicates) {
STORM_LOG_THROW(!predicates.empty(), storm::exceptions::InvalidArgumentException, "Cannot refine without predicates.");
// Add the predicates to the global list of predicates.
uint_fast64_t firstNewPredicateIndex = expressionInformation.predicates.size();
expressionInformation.predicates.insert(expressionInformation.predicates.end(), predicates.begin(), predicates.end());
@ -92,20 +99,34 @@ namespace storm {
// Refine initial state abstractor.
initialStateAbstractor.refine(newPredicateIndices);
// Finally, we rebuild the game.
currentGame = buildGame();
}
template <storm::dd::DdType DdType, typename ValueType>
storm::models::symbolic::StochasticTwoPlayerGame<DdType> AbstractProgram<DdType, ValueType>::getAbstractGame() {
STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created.");
return *currentGame;
}
template <storm::dd::DdType DdType, typename ValueType>
storm::dd::Bdd<DdType> AbstractProgram<DdType, ValueType>::getStates(storm::expressions::Expression const& predicate) {
STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created.");
uint_fast64_t index = 0;
for (auto const& knownPredicate : expressionInformation.predicates) {
if (knownPredicate.isSame(predicate)) {
return currentGame->getReachableStates() && ddInformation.predicateBdds[index].first;
}
++index;
}
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given predicate is illegal, since it was neither used as an initial predicate nor used to refine the abstraction.");
}
template <storm::dd::DdType DdType, typename ValueType>
storm::dd::Add<DdType> AbstractProgram<DdType, ValueType>::getAbstractAdd() {
std::unique_ptr<storm::models::symbolic::StochasticTwoPlayerGame<DdType>> AbstractProgram<DdType, ValueType>::buildGame() {
// As long as there is only one module, we only build its game representation.
std::pair<storm::dd::Bdd<DdType>, uint_fast64_t> gameBdd = modules.front().getAbstractBdd();
// If the abstraction did not change, we can return the most recenty obtained ADD.
if (gameBdd.first == lastAbstractBdd) {
return lastAbstractAdd;
}
// Otherwise, we remember that the abstract BDD changed and perform a reachability analysis.
lastAbstractBdd = gameBdd.first;
// Construct a set of all unnecessary variables, so we can abstract from it.
std::set<storm::expressions::Variable> variablesToAbstract = {ddInformation.commandDdVariable, ddInformation.updateDdVariable};
@ -114,12 +135,13 @@ namespace storm {
}
// Do a reachability analysis on the raw transition relation.
storm::dd::Bdd<DdType> transitionRelation = lastAbstractBdd.existsAbstract(variablesToAbstract);
lastReachableStates = this->getReachableStates(initialStateAbstractor.getAbstractStates(), transitionRelation);
storm::dd::Bdd<DdType> transitionRelation = gameBdd.first.existsAbstract(variablesToAbstract);
storm::dd::Bdd<DdType> initialStates = initialStateAbstractor.getAbstractStates();
storm::dd::Bdd<DdType> reachableStates = this->getReachableStates(initialStates, transitionRelation);
// Find the deadlock states in the model.
storm::dd::Bdd<DdType> deadlockStates = transitionRelation.existsAbstract(ddInformation.successorVariables);
deadlockStates = lastReachableStates && !deadlockStates;
deadlockStates = reachableStates && !deadlockStates;
// If there are deadlock states, we fix them now.
storm::dd::Add<DdType> deadlockTransitions = ddInformation.manager->getAddZero();
@ -127,15 +149,18 @@ namespace storm {
deadlockTransitions = (deadlockStates && ddInformation.allPredicateIdentities && ddInformation.manager->getEncoding(ddInformation.commandDdVariable, 0) && ddInformation.manager->getEncoding(ddInformation.updateDdVariable, 0) && ddInformation.getMissingOptionVariableCube(0, gameBdd.second)).toAdd();
}
// Construct the final game by cutting away the transitions of unreachable states.
lastAbstractAdd = (lastAbstractBdd && lastReachableStates).toAdd() * commandUpdateProbabilitiesAdd + deadlockTransitions;
return lastAbstractAdd;
}
// Construct the transition matrix by cutting away the transitions of unreachable states.
storm::dd::Add<DdType> transitionMatrix = (gameBdd.first && reachableStates).toAdd() * commandUpdateProbabilitiesAdd + deadlockTransitions;
template <storm::dd::DdType DdType, typename ValueType>
storm::dd::Bdd<DdType> AbstractProgram<DdType, ValueType>::getReachableStates() {
return lastReachableStates;
std::set<storm::expressions::Variable> usedPlayer2Variables;
for (uint_fast64_t index = 0; index < ddInformation.optionDdVariables.size(); ++index) {
usedPlayer2Variables.insert(usedPlayer2Variables.end(), ddInformation.optionDdVariables[index].first);
}
std::set<storm::expressions::Variable> allNondeterminismVariables = usedPlayer2Variables;
allNondeterminismVariables.insert(ddInformation.commandDdVariable);
return std::unique_ptr<storm::models::symbolic::StochasticTwoPlayerGame<DdType>>(new storm::models::symbolic::StochasticTwoPlayerGame<DdType>(ddInformation.manager, reachableStates, initialStates, transitionMatrix, ddInformation.sourceVariables, nullptr, ddInformation.successorVariables, nullptr, ddInformation.predicateDdVariables, {ddInformation.commandDdVariable}, usedPlayer2Variables, allNondeterminismVariables));
}
template <storm::dd::DdType DdType, typename ValueType>

39
src/storage/prism/menu_games/AbstractProgram.h
View File

@ -10,6 +10,8 @@
#include "src/storage/expressions/Expression.h"
#include "src/models/symbolic/StochasticTwoPlayerGame.h"
namespace storm {
namespace utility {
namespace solver {
@ -17,6 +19,13 @@ namespace storm {
}
}
namespace models {
namespace symbolic {
template<storm::dd::DdType Type>
class StochasticTwoPlayerGame;
}
}
namespace prism {
// Forward-declare concrete Program class.
class Program;
@ -40,17 +49,18 @@ namespace storm {
/*!
* Uses the current set of predicates to derive the abstract menu game in the form of an ADD.
*
* @return The ADD representing the game.
* @return The abstract stochastic two player game.
*/
storm::dd::Add<DdType> getAbstractAdd();
storm::models::symbolic::StochasticTwoPlayerGame<DdType> getAbstractGame();
/*!
* Retrieves the reachable state space of the abstract game (that was previously retrieved via the
* appropriate method.
* Retrieves the set of states (represented by a BDD) satisfying the given predicate, assuming that it
* was either given as an initial predicate or used as a refining predicate later.
*
* @return The reachable state space in the form of a BDD.
* @param predicate The predicate for which to retrieve the states.
* @return The BDD representing the set of states.
*/
storm::dd::Bdd<DdType> getReachableStates();
storm::dd::Bdd<DdType> getStates(storm::expressions::Expression const& predicate);
/*!
* Refines the abstract module with the given predicates.
@ -70,6 +80,13 @@ namespace storm {
*/
storm::dd::Bdd<DdType> getReachableStates(storm::dd::Bdd<DdType> const& initialStates, storm::dd::Bdd<DdType> const& transitionRelation);
/*!
* Builds the stochastic game representing the abstraction of the program.
*
* @return The stochastic game.
*/
std::unique_ptr<storm::models::symbolic::StochasticTwoPlayerGame<DdType>> buildGame();
// A factory that can be used to create new SMT solvers.
std::unique_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
@ -91,14 +108,8 @@ namespace storm {
// An ADD characterizing the probabilities of commands and their updates.
storm::dd::Add<DdType> commandUpdateProbabilitiesAdd;
// A BDD that is the result of the last abstraction of the system.
storm::dd::Bdd<DdType> lastAbstractBdd;
// An ADD that is the result of the last abstraction of the system.
storm::dd::Add<DdType> lastAbstractAdd;
// A BDD that is the result of the reachability analysis on the abstraction of the system.
storm::dd::Bdd<DdType> lastReachableStates;
// The current game-based abstraction.
std::unique_ptr<storm::models::symbolic::StochasticTwoPlayerGame<DdType>> currentGame;
};
}
}

102
test/functional/abstraction/PrismMenuGameTest.cpp
View File

@ -13,6 +13,8 @@
#include "src/storage/dd/CuddAdd.h"
#include "src/storage/dd/CuddBdd.h"
#include "src/models/symbolic/StandardRewardModel.h"
#include "src/utility/solver.h"
TEST(PrismMenuGame, DieAbstractionTest) {
@ -25,11 +27,10 @@ TEST(PrismMenuGame, DieAbstractionTest) {
storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
EXPECT_EQ(15, abstraction.getNonZeroCount());
EXPECT_EQ(2, abstractProgram.getReachableStates().getNonZeroCount());
EXPECT_EQ(15, game.getNumberOfTransitions());
EXPECT_EQ(2, game.getNumberOfStates());
}
TEST(PrismMenuGame, DieAbstractionAndRefinementTest) {
@ -42,14 +43,12 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest) {
storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("s") == manager.integer(7)}));
ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
EXPECT_EQ(15, abstraction.getNonZeroCount());
EXPECT_EQ(3, abstractProgram.getReachableStates().getNonZeroCount());
EXPECT_EQ(15, game.getNumberOfTransitions());
EXPECT_EQ(3, game.getNumberOfStates());
}
TEST(PrismMenuGame, DieFullAbstractionTest) {
@ -77,11 +76,10 @@ TEST(PrismMenuGame, DieFullAbstractionTest) {
storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
EXPECT_EQ(20, abstraction.getNonZeroCount());
EXPECT_EQ(13, abstractProgram.getReachableStates().getNonZeroCount());
EXPECT_EQ(20, game.getNumberOfTransitions());
EXPECT_EQ(13, game.getNumberOfStates());
}
TEST(PrismMenuGame, CrowdsAbstractionTest) {
@ -95,11 +93,10 @@ TEST(PrismMenuGame, CrowdsAbstractionTest) {
storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
EXPECT_EQ(16, abstraction.getNonZeroCount());
EXPECT_EQ(2, abstractProgram.getReachableStates().getNonZeroCount());
EXPECT_EQ(16, game.getNumberOfTransitions());
EXPECT_EQ(2, game.getNumberOfStates());
}
TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest) {
@ -113,14 +110,12 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest) {
storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("observe0") + manager.getVariableExpression("observe1") + manager.getVariableExpression("observe2") + manager.getVariableExpression("observe3") + manager.getVariableExpression("observe4") <= manager.getVariableExpression("runCount")}));
ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
EXPECT_EQ(38, abstraction.getNonZeroCount());
EXPECT_EQ(4, abstractProgram.getReachableStates().getNonZeroCount());
storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
EXPECT_EQ(38, game.getNumberOfTransitions());
EXPECT_EQ(4, game.getNumberOfStates());
}
TEST(PrismMenuGame, CrowdsFullAbstractionTest) {
@ -188,11 +183,10 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest) {
storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
EXPECT_EQ(15113, abstraction.getNonZeroCount());
EXPECT_EQ(8607, abstractProgram.getReachableStates().getNonZeroCount());
EXPECT_EQ(15113, game.getNumberOfTransitions());
EXPECT_EQ(8607, game.getNumberOfStates());
}
TEST(PrismMenuGame, TwoDiceAbstractionTest) {
@ -208,11 +202,10 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest) {
storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
EXPECT_EQ(58, abstraction.getNonZeroCount());
EXPECT_EQ(4, abstractProgram.getReachableStates().getNonZeroCount());
EXPECT_EQ(58, game.getNumberOfTransitions());
EXPECT_EQ(4, game.getNumberOfStates());
}
TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest) {
@ -228,14 +221,12 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest) {
storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("d1") + manager.getVariableExpression("d2") == manager.integer(7)}));
ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
EXPECT_EQ(212, abstraction.getNonZeroCount());
EXPECT_EQ(8, abstractProgram.getReachableStates().getNonZeroCount());
storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
EXPECT_EQ(212, game.getNumberOfTransitions());
EXPECT_EQ(8, game.getNumberOfStates());
}
TEST(PrismMenuGame, TwoDiceFullAbstractionTest) {
@ -282,11 +273,10 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest) {
storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
EXPECT_EQ(436, abstraction.getNonZeroCount());
EXPECT_EQ(169, abstractProgram.getReachableStates().getNonZeroCount());
EXPECT_EQ(436, game.getNumberOfTransitions());
EXPECT_EQ(169, game.getNumberOfStates());
}
TEST(PrismMenuGame, WlanAbstractionTest) {
@ -303,11 +293,10 @@ TEST(PrismMenuGame, WlanAbstractionTest) {
storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
EXPECT_EQ(307, abstraction.getNonZeroCount());
EXPECT_EQ(4, abstractProgram.getReachableStates().getNonZeroCount());
EXPECT_EQ(307, game.getNumberOfTransitions());
EXPECT_EQ(4, game.getNumberOfStates());
}
TEST(PrismMenuGame, WlanAbstractionAndRefinementTest) {
@ -324,14 +313,12 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest) {
storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("backoff1") < manager.integer(7)}));
ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
EXPECT_EQ(612, abstraction.getNonZeroCount());
EXPECT_EQ(8, abstractProgram.getReachableStates().getNonZeroCount());
storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
EXPECT_EQ(612, game.getNumberOfTransitions());
EXPECT_EQ(8, game.getNumberOfStates());
}
TEST(PrismMenuGame, WlanFullAbstractionTest) {
@ -446,11 +433,10 @@ TEST(PrismMenuGame, WlanFullAbstractionTest) {
storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
EXPECT_EQ(59, abstraction.getNonZeroCount());
EXPECT_EQ(37, abstractProgram.getReachableStates().getNonZeroCount());
EXPECT_EQ(59, game.getNumberOfTransitions());
EXPECT_EQ(37, game.getNumberOfStates());
}
#endif
Write Preview
Loading…
Cancel
Save