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

started on tests and added a ton of debug output

tempestpy_adaptions
dehnert 7 years ago
parent
11d2ee2fda
commit
a7dcdcd84d
5 changed files with 178 additions and 10 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
      resources/examples/testfiles/mdp/leader3.nm
  2. 2
      src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp
  3. 1
      src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
  4. 36
      src/storm/storage/dd/bisimulation/SignatureRefiner.cpp
  5. 146
      src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp

3
resources/examples/testfiles/mdp/leader3.nm
View File

@ -84,6 +84,9 @@ module process2=process1[s1=s2,p1=p2,c1=c2,sent1=sent2,receive1=receive2,p12=p23
module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p31,p31=p23,c12=c31,c31=c23,p3=p2,c3=c2] endmodule
//----------------------------------------------------------------------------------------------------------------------------
rewards "rounds"
[c12] true : 1;
endrewards
//----------------------------------------------------------------------------------------------------------------------------
formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0);

2
src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp
View File

@ -32,7 +32,7 @@ namespace storm {
// If the choice partition changed, refine the state partition. Use qualitative mode we must properly abstract from choice counts.
STORM_LOG_TRACE("Refining state partition.");
Partition<DdType, ValueType> newStatePartition = this->internalRefine(this->stateSignatureComputer, this->stateSignatureRefiner, this->statePartition, this->choicePartition, SignatureMode::Qualitative);
if (newStatePartition == this->statePartition) {
this->status = Status::FixedPoint;
return false;

1
src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
View File

@ -846,6 +846,7 @@ namespace storm {
auto states = partition.getStates().swapVariables(model.getRowColumnMetaVariablePairs());
storm::dd::Bdd<DdType> partitionAsBdd = partition.storedAsAdd() ? partition.asAdd().toBdd() : partition.asBdd();
partitionAsBdd.exportToDot("part.dot");
partitionAsBdd = partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables());
auto start = std::chrono::high_resolution_clock::now();

36
src/storm/storage/dd/bisimulation/SignatureRefiner.cpp
View File

@ -26,6 +26,9 @@
#include "sylvan_table.h"
#include "sylvan_int.h"
// FIXME: remove
#include "storm/storage/dd/DdManager.h"
namespace storm {
namespace dd {
namespace bisimulation {
@ -58,7 +61,7 @@ namespace storm {
template<typename ValueType>
class InternalSignatureRefiner<storm::dd::DdType::CUDD, ValueType> {
public:
InternalSignatureRefiner(storm::dd::DdManager<storm::dd::DdType::CUDD> const& manager, storm::expressions::Variable const& blockVariable, storm::dd::Bdd<storm::dd::DdType::CUDD> const& nondeterminismVariables, storm::dd::Bdd<storm::dd::DdType::CUDD> const& nonBlockVariables) : manager(manager), internalDdManager(manager.getInternalDdManager()), blockVariable(blockVariable), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), nextFreeBlockIndex(0), numberOfRefinements(0), lastNumberOfVisitedNodes(10000), signatureCache(lastNumberOfVisitedNodes), reuseBlocksCache(lastNumberOfVisitedNodes) {
InternalSignatureRefiner(storm::dd::DdManager<storm::dd::DdType::CUDD> const& manager, storm::expressions::Variable const& blockVariable, storm::dd::Bdd<storm::dd::DdType::CUDD> const& nondeterminismVariables, storm::dd::Bdd<storm::dd::DdType::CUDD> const& nonBlockVariables) : manager(manager), internalDdManager(manager.getInternalDdManager()), ddman(internalDdManager.getCuddManager().getManager()), blockVariable(blockVariable), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), nextFreeBlockIndex(0), numberOfRefinements(0), lastNumberOfVisitedNodes(10000), signatureCache(lastNumberOfVisitedNodes), reuseBlocksCache(lastNumberOfVisitedNodes) {
// Initialize precomputed data.
auto const& ddMetaVariable = manager.getMetaVariable(blockVariable);
@ -81,6 +84,7 @@ namespace storm {
// Clear the caches.
signatureCache.clear();
reuseBlocksCache.clear();
std::cout << "clearing reuse, " << reuseBlocksCache.size() << std::endl;
nextFreeBlockIndex = oldPartition.getNextFreeBlockIndex();
// Perform the actual recursive refinement step.
@ -98,22 +102,20 @@ namespace storm {
blockEncoding[blockDdVariableIndex] = blockIndex & 1 ? 1 : 0;
blockIndex >>= 1;
}
::DdManager* ddMan = internalDdManager.getCuddManager().getManager();
DdNodePtr bddEncoding = Cudd_CubeArrayToBdd(ddMan, blockEncoding.data());
DdNodePtr bddEncoding = Cudd_CubeArrayToBdd(ddman, blockEncoding.data());
Cudd_Ref(bddEncoding);
DdNodePtr result = Cudd_BddToAdd(ddMan, bddEncoding);
DdNodePtr result = Cudd_BddToAdd(ddman, bddEncoding);
Cudd_Ref(result);
Cudd_RecursiveDeref(ddMan, bddEncoding);
Cudd_RecursiveDeref(ddman, bddEncoding);
Cudd_Deref(result);
return result;
}
DdNodePtr refine(DdNode* partitionNode, DdNode* signatureNode, DdNode* nondeterminismVariablesNode, DdNode* nonBlockVariablesNode) {
::DdManager* ddman = internalDdManager.getCuddManager().getManager();
// If we arrived at the constant zero node, then this was an illegal state encoding (we require
// all states to be non-deadlock).
if (partitionNode == Cudd_ReadZero(ddman)) {
std::cout << "returning zero " << partitionNode << std::endl;
return partitionNode;
}
@ -121,6 +123,7 @@ namespace storm {
auto nodePair = std::make_pair(signatureNode, partitionNode);
auto it = signatureCache.find(nodePair);
if (it != signatureCache.end()) {
std::cout << "cache hit " << it->second << std::endl;
// If so, we return the corresponding result.
return it->second;
}
@ -129,13 +132,18 @@ namespace storm {
if (Cudd_IsConstant(nonBlockVariablesNode)) {
// If this is the first time (in this traversal) that we encounter this signature, we check
// whether we can assign the old block number to it.
std::cout << "reuse size: " << reuseBlocksCache.size() << std::endl;
auto& reuseEntry = reuseBlocksCache[partitionNode];
std::cout << "reused? " << reuseEntry.isReused() << std::endl;
if (!reuseEntry.isReused()) {
reuseEntry.setReused();
std::cout << "setting " << partitionNode << " to being reused" << std::endl;
signatureCache[nodePair] = partitionNode;
std::cout << "reuse cache hit " << partitionNode << std::endl;
return partitionNode;
} else {
DdNode* result = encodeBlock(nextFreeBlockIndex++);
std::cout << "block encoding " << result << std::endl;
signatureCache[nodePair] = result;
return result;
}
@ -190,7 +198,10 @@ namespace storm {
Cudd_Ref(thenResult);
DdNode* elseResult = refine(partitionElse, signatureElse, offset == 0 ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode));
Cudd_Ref(elseResult);
std::cout << "got then " << thenResult << std::endl;
std::cout << "got else " << elseResult << std::endl;
DdNode* result;
if (thenResult == elseResult) {
Cudd_Deref(thenResult);
@ -200,6 +211,7 @@ namespace storm {
// Get the node to connect the subresults.
bool complemented = Cudd_IsComplement(thenResult);
result = cuddUniqueInter(ddman, Cudd_NodeReadIndex(nonBlockVariablesNode) + offset, Cudd_Regular(thenResult), complemented ? Cudd_Not(elseResult) : elseResult);
std::cout << "got " << result << " as a result node, idx " << (Cudd_NodeReadIndex(nonBlockVariablesNode) + offset) << " and children " << Cudd_NodeReadIndex(thenResult) << " [" << Cudd_IsConstant(thenResult) << "] (" << thenResult << ") and " << Cudd_NodeReadIndex(elseResult) << " [" << Cudd_IsConstant(elseResult) << "] (" << elseResult << ")" << std::endl;
if (complemented) {
result = Cudd_Not(result);
}
@ -210,12 +222,14 @@ namespace storm {
// Store the result in the cache.
signatureCache[nodePair] = result;
std::cout << "returning " << result << " with index " << Cudd_NodeReadIndex(result) << ", const? " << Cudd_IsConstant(result) << std::endl;
return result;
}
}
storm::dd::DdManager<storm::dd::DdType::CUDD> const& manager;
storm::dd::InternalDdManager<storm::dd::DdType::CUDD> const& internalDdManager;
::DdManager* ddman;
storm::expressions::Variable const& blockVariable;
// The cubes representing all non-block and all nondeterminism variables, respectively.
@ -480,7 +494,11 @@ namespace storm {
template<storm::dd::DdType DdType, typename ValueType>
Partition<DdType, ValueType> SignatureRefiner<DdType, ValueType>::refine(Partition<DdType, ValueType> const& oldPartition, Signature<DdType, ValueType> const& signature) {
return internalRefiner->refine(oldPartition, signature);
oldPartition.asAdd().getDdManager().debugCheck();
oldPartition.asAdd().exportToDot("lastpart.dot");
Partition<DdType, ValueType> result = internalRefiner->refine(oldPartition, signature);
oldPartition.asAdd().getDdManager().debugCheck();
return result;
}
template class SignatureRefiner<storm::dd::DdType::CUDD, double>;

146
src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp
View File

@ -0,0 +1,146 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "storm/parser/PrismParser.h"
#include "storm/parser/FormulaParser.h"
#include "storm/builder/DdPrismModelBuilder.h"
#include "storm/storage/dd/BisimulationDecomposition.h"
#include "storm/storage/SymbolicModelDescription.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/models/symbolic/Mdp.h"
#include "storm/models/symbolic/StandardRewardModel.h"
TEST(SymbolicModelBisimulationDecomposition, Die_Cudd) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD, double>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD, double>().build(program);
storm::dd::BisimulationDecomposition<storm::dd::DdType::CUDD, double> decomposition(*model, storm::storage::BisimulationType::Strong);
decomposition.compute();
std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient();
EXPECT_EQ(11ul, quotient->getNumberOfStates());
EXPECT_EQ(17ul, quotient->getNumberOfTransitions());
EXPECT_EQ(storm::models::ModelType::Dtmc, quotient->getType());
EXPECT_TRUE(quotient->isSymbolicModel());
storm::parser::FormulaParser formulaParser;
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
formulas.push_back(formula);
storm::dd::BisimulationDecomposition<storm::dd::DdType::CUDD, double> decomposition2(*model, formulas, storm::storage::BisimulationType::Strong);
decomposition2.compute();
quotient = decomposition2.getQuotient();
EXPECT_EQ(5ul, quotient->getNumberOfStates());
EXPECT_EQ(8ul, quotient->getNumberOfTransitions());
EXPECT_EQ(storm::models::ModelType::Dtmc, quotient->getType());
EXPECT_TRUE(quotient->isSymbolicModel());
}
TEST(SymbolicModelBisimulationDecomposition, Crowds_Cudd) {
storm::storage::SymbolicModelDescription smd = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds5_5.pm");
// Preprocess model to substitute all constants.
smd = smd.preprocess();
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD, double>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD, double>().build(smd.asPrismProgram());
storm::dd::BisimulationDecomposition<storm::dd::DdType::CUDD, double> decomposition(*model, storm::storage::BisimulationType::Strong);
decomposition.compute();
std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient();
EXPECT_EQ(2007ul, quotient->getNumberOfStates());
EXPECT_EQ(3738ul, quotient->getNumberOfTransitions());
EXPECT_EQ(storm::models::ModelType::Dtmc, quotient->getType());
EXPECT_TRUE(quotient->isSymbolicModel());
storm::parser::FormulaParser formulaParser;
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
formulas.push_back(formula);
storm::dd::BisimulationDecomposition<storm::dd::DdType::CUDD, double> decomposition2(*model, formulas, storm::storage::BisimulationType::Strong);
decomposition2.compute();
quotient = decomposition2.getQuotient();
EXPECT_EQ(65ul, quotient->getNumberOfStates());
EXPECT_EQ(105ul, quotient->getNumberOfTransitions());
EXPECT_EQ(storm::models::ModelType::Dtmc, quotient->getType());
EXPECT_TRUE(quotient->isSymbolicModel());
}
TEST(SymbolicModelBisimulationDecomposition, TwoDice_Cudd) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD, double>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD, double>().build(program);
storm::dd::BisimulationDecomposition<storm::dd::DdType::CUDD, double> decomposition(*model, storm::storage::BisimulationType::Strong);
decomposition.compute();
std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient();
EXPECT_EQ(77ul, quotient->getNumberOfStates());
EXPECT_EQ(210ul, quotient->getNumberOfTransitions());
EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType());
EXPECT_TRUE(quotient->isSymbolicModel());
EXPECT_EQ(116ul, (quotient->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>()->getNumberOfChoices()));
storm::parser::FormulaParser formulaParser;
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
formulas.push_back(formula);
storm::dd::BisimulationDecomposition<storm::dd::DdType::CUDD, double> decomposition2(*model, formulas, storm::storage::BisimulationType::Strong);
decomposition2.compute();
quotient = decomposition2.getQuotient();
EXPECT_EQ(19ul, quotient->getNumberOfStates());
EXPECT_EQ(58ul, quotient->getNumberOfTransitions());
EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType());
EXPECT_TRUE(quotient->isSymbolicModel());
EXPECT_EQ(34ul, (quotient->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>()->getNumberOfChoices()));
}
TEST(SymbolicModelBisimulationDecomposition, AsynchronousLeader_Cudd) {
storm::storage::SymbolicModelDescription smd = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm");
// Preprocess model to substitute all constants.
smd = smd.preprocess();
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD, double>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD, double>().build(smd.asPrismProgram());
storm::dd::BisimulationDecomposition<storm::dd::DdType::CUDD, double> decomposition(*model, storm::storage::BisimulationType::Strong);
decomposition.compute();
std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient();
EXPECT_EQ(252ul, quotient->getNumberOfStates());
EXPECT_EQ(624ul, quotient->getNumberOfTransitions());
EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType());
EXPECT_TRUE(quotient->isSymbolicModel());
EXPECT_EQ(500ul, (quotient->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>()->getNumberOfChoices()));
storm::parser::FormulaParser formulaParser;
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
formulas.push_back(formula);
storm::dd::BisimulationDecomposition<storm::dd::DdType::CUDD, double> decomposition2(*model, formulas, storm::storage::BisimulationType::Strong);
decomposition2.compute();
quotient = decomposition2.getQuotient();
EXPECT_EQ(19ul, quotient->getNumberOfStates());
EXPECT_EQ(58ul, quotient->getNumberOfTransitions());
EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType());
EXPECT_TRUE(quotient->isSymbolicModel());
EXPECT_EQ(34ul, (quotient->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>()->getNumberOfChoices()));
}
Write Preview
Loading…
Cancel
Save