dehnert
12 years ago
40 changed files with 133 additions and 426 deletions
-
4CMakeLists.txt
-
6src/adapters/ExplicitModelAdapter.h
-
2src/counterexamples/GenerateCounterexample.h
-
2src/counterexamples/MILPMinimalLabelSetGenerator.h
-
2src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
-
2src/modelchecker/prctl/CreatePrctlModelChecker.h
-
2src/models/Ctmdp.h
-
2src/models/Dtmc.h
-
2src/models/Mdp.h
-
2src/parser/DeterministicSparseTransitionParser.cpp
-
4src/parser/MarkovAutomatonSparseTransitionParser.cpp
-
2src/parser/NondeterministicSparseTransitionParser.cpp
-
4src/settings/InternalOptionMemento.h
-
4src/settings/Option.h
-
58src/settings/Settings.cpp
-
23src/settings/Settings.h
-
0src/settings/modules/Settings.h
-
12src/solver/GlpkLpSolver.cpp
-
2src/solver/GmmxxLinearEquationSolver.cpp
-
2src/solver/GmmxxNondeterministicLinearEquationSolver.cpp
-
2src/solver/NativeLinearEquationSolver.cpp
-
2src/solver/NativeNondeterministicLinearEquationSolver.cpp
-
6src/storage/dd/CuddDdManager.cpp
-
4src/storm.cpp
-
6src/utility/CLI.h
-
195src/utility/CuddUtility.cpp
-
65src/utility/CuddUtility.h
-
2src/utility/InitializeLogging.h
-
6src/utility/solver.cpp
-
6test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
-
4test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
-
24test/functional/solver/GlpkLpSolverTest.cpp
-
44test/functional/solver/GmmxxLinearEquationSolverTest.cpp
-
14test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp
-
8test/functional/solver/NativeLinearEquationSolverTest.cpp
-
14test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp
-
8test/functional/storm-functional-tests.cpp
-
4test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
-
4test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
-
4test/performance/storm-performance-tests.cpp
@ -1,195 +0,0 @@ |
|||||
/*
|
|
||||
* CuddUtility.cpp |
|
||||
* |
|
||||
* Created on: 26.01.2013 |
|
||||
* Author: Christian Dehnert |
|
||||
*/ |
|
||||
|
|
||||
#include "CuddUtility.h"
|
|
||||
#include "src/exceptions/InvalidArgumentException.h"
|
|
||||
|
|
||||
#include "log4cplus/logger.h"
|
|
||||
#include "log4cplus/loggingmacros.h"
|
|
||||
|
|
||||
extern log4cplus::Logger logger; |
|
||||
|
|
||||
#include <stdio.h>
|
|
||||
#include <iostream>
|
|
||||
|
|
||||
namespace storm { |
|
||||
|
|
||||
namespace utility { |
|
||||
|
|
||||
storm::utility::CuddUtility* storm::utility::CuddUtility::instance = nullptr; |
|
||||
|
|
||||
ADD* CuddUtility::getNewAddVariable() { |
|
||||
ADD* result = new ADD(manager.addVar()); |
|
||||
allDecisionDiagramVariables.push_back(result); |
|
||||
return result; |
|
||||
} |
|
||||
|
|
||||
ADD* CuddUtility::getAddVariable(int index) const { |
|
||||
return new ADD(manager.addVar(index)); |
|
||||
} |
|
||||
|
|
||||
ADD* CuddUtility::getOne() const { |
|
||||
return new ADD(manager.addOne()); |
|
||||
} |
|
||||
|
|
||||
ADD* CuddUtility::getZero() const { |
|
||||
return new ADD(manager.addZero()); |
|
||||
} |
|
||||
|
|
||||
ADD* CuddUtility::getConstantEncoding(uint_fast64_t constant, std::vector<ADD*> const& variables) const { |
|
||||
if ((constant >> variables.size()) != 0) { |
|
||||
LOG4CPLUS_ERROR(logger, "Cannot create encoding for constant " << constant << " with " |
|
||||
<< variables.size() << " variables."); |
|
||||
throw storm::exceptions::InvalidArgumentException() << "Cannot create encoding" |
|
||||
<< " for constant " << constant << " with " << variables.size() |
|
||||
<< " variables."; |
|
||||
} |
|
||||
|
|
||||
// Determine whether the new ADD will be rooted by the first variable or its complement.
|
|
||||
ADD initialNode; |
|
||||
if ((constant & (1ull << (variables.size() - 1))) != 0) { |
|
||||
initialNode = *variables[0]; |
|
||||
} else { |
|
||||
initialNode = ~(*variables[0]); |
|
||||
} |
|
||||
ADD* result = new ADD(initialNode); |
|
||||
|
|
||||
// Add (i.e. multiply) the other variables as well according to whether their bit is set or not.
|
|
||||
for (uint_fast64_t i = 1; i < variables.size(); ++i) { |
|
||||
if ((constant & (1ull << (variables.size() - i - 1))) != 0) { |
|
||||
*result *= *variables[i]; |
|
||||
} else { |
|
||||
*result *= ~(*variables[i]); |
|
||||
} |
|
||||
} |
|
||||
|
|
||||
return result; |
|
||||
} |
|
||||
|
|
||||
void CuddUtility::setValueAtIndex(ADD* add, uint_fast64_t index, std::vector<ADD*> const& variables, double value) const { |
|
||||
if ((index >> variables.size()) != 0) { |
|
||||
LOG4CPLUS_ERROR(logger, "Cannot create encoding for index " << index << " with " |
|
||||
<< variables.size() << " variables."); |
|
||||
throw storm::exceptions::InvalidArgumentException() << "Cannot create encoding" |
|
||||
<< " for index " << index << " with " << variables.size() |
|
||||
<< " variables."; |
|
||||
} |
|
||||
|
|
||||
// Determine whether the new ADD will be rooted by the first variable or its complement.
|
|
||||
ADD initialNode; |
|
||||
if ((index & (1ull << (variables.size() - 1))) != 0) { |
|
||||
initialNode = *variables[0]; |
|
||||
} else { |
|
||||
initialNode = ~(*variables[0]); |
|
||||
} |
|
||||
ADD* encoding = new ADD(initialNode); |
|
||||
|
|
||||
// Add (i.e. multiply) the other variables as well according to whether their bit is set or not.
|
|
||||
for (uint_fast64_t i = 1; i < variables.size(); ++i) { |
|
||||
if ((index & (1ull << (variables.size() - i - 1))) != 0) { |
|
||||
*encoding *= *variables[i]; |
|
||||
} else { |
|
||||
*encoding *= ~(*variables[i]); |
|
||||
} |
|
||||
} |
|
||||
|
|
||||
*add = encoding->Ite(manager.constant(value), *add); |
|
||||
} |
|
||||
|
|
||||
void CuddUtility::setValueAtIndices(ADD* add, uint_fast64_t rowIndex, uint_fast64_t columnIndex, std::vector<ADD*> const& rowVariables, std::vector<ADD*> const& columnVariables, double value) const { |
|
||||
if ((rowIndex >> rowVariables.size()) != 0) { |
|
||||
LOG4CPLUS_ERROR(logger, "Cannot create encoding for index " << rowIndex << " with " |
|
||||
<< rowVariables.size() << " variables."); |
|
||||
throw storm::exceptions::InvalidArgumentException() << "Cannot create encoding" |
|
||||
<< " for index " << rowIndex << " with " << rowVariables.size() |
|
||||
<< " variables."; |
|
||||
} |
|
||||
if ((columnIndex >> columnVariables.size()) != 0) { |
|
||||
LOG4CPLUS_ERROR(logger, "Cannot create encoding for index " << columnIndex << " with " |
|
||||
<< columnVariables.size() << " variables."); |
|
||||
throw storm::exceptions::InvalidArgumentException() << "Cannot create encoding" |
|
||||
<< " for index " << columnIndex << " with " << columnVariables.size() |
|
||||
<< " variables."; |
|
||||
} |
|
||||
if (rowVariables.size() != columnVariables.size()) { |
|
||||
LOG4CPLUS_ERROR(logger, "Number of variables for indices encodings does not match."); |
|
||||
throw storm::exceptions::InvalidArgumentException() |
|
||||
<< "Number of variables for indices encodings does not match."; |
|
||||
} |
|
||||
|
|
||||
ADD initialNode; |
|
||||
if ((rowIndex & (1ull << (rowVariables.size() - 1))) != 0) { |
|
||||
initialNode = *rowVariables[0]; |
|
||||
} else { |
|
||||
initialNode = ~(*rowVariables[0]); |
|
||||
} |
|
||||
ADD* encoding = new ADD(initialNode); |
|
||||
if ((columnIndex & (1ull << (rowVariables.size() - 1))) != 0) { |
|
||||
*encoding *= *columnVariables[0]; |
|
||||
} else { |
|
||||
*encoding *= ~(*columnVariables[0]); |
|
||||
} |
|
||||
|
|
||||
for (uint_fast64_t i = 1; i < rowVariables.size(); ++i) { |
|
||||
if ((rowIndex & (1ull << (rowVariables.size() - i - 1))) != 0) { |
|
||||
*encoding *= *rowVariables[i]; |
|
||||
} else { |
|
||||
*encoding *= ~(*rowVariables[i]); |
|
||||
} |
|
||||
if ((columnIndex & (1ull << (columnVariables.size() - i - 1))) != 0) { |
|
||||
*encoding *= *columnVariables[i]; |
|
||||
} else { |
|
||||
*encoding *= ~(*columnVariables[i]); |
|
||||
} |
|
||||
} |
|
||||
|
|
||||
*add = encoding->Ite(manager.constant(value), *add); |
|
||||
} |
|
||||
|
|
||||
|
|
||||
ADD* CuddUtility::getConstant(double value) const { |
|
||||
return new ADD(manager.constant(value)); |
|
||||
} |
|
||||
|
|
||||
ADD* CuddUtility::permuteVariables(ADD* add, std::vector<ADD*> fromVariables, std::vector<ADD*> toVariables, uint_fast64_t totalNumberOfVariables) const { |
|
||||
std::vector<int> permutation; |
|
||||
permutation.resize(totalNumberOfVariables); |
|
||||
for (uint_fast64_t i = 0; i < totalNumberOfVariables; ++i) { |
|
||||
permutation[i] = static_cast<int>(i); |
|
||||
} |
|
||||
for (uint_fast64_t i = 0; i < fromVariables.size(); ++i) { |
|
||||
permutation[fromVariables[i]->NodeReadIndex()] = toVariables[i]->NodeReadIndex(); |
|
||||
} |
|
||||
return new ADD(add->Permute(&permutation[0])); |
|
||||
} |
|
||||
|
|
||||
void CuddUtility::dumpDotToFile(ADD* add, std::string filename) const { |
|
||||
std::vector<ADD> nodes; |
|
||||
nodes.push_back(*add); |
|
||||
|
|
||||
FILE* filePtr; |
|
||||
filePtr = fopen(filename.c_str(), "w"); |
|
||||
manager.DumpDot(nodes, 0, 0, filePtr); |
|
||||
fclose(filePtr); |
|
||||
} |
|
||||
|
|
||||
Cudd const& CuddUtility::getManager() const { |
|
||||
return manager; |
|
||||
} |
|
||||
|
|
||||
CuddUtility* cuddUtilityInstance() { |
|
||||
if (CuddUtility::instance == nullptr) { |
|
||||
CuddUtility::instance = new CuddUtility(); |
|
||||
} |
|
||||
return CuddUtility::instance; |
|
||||
} |
|
||||
|
|
||||
} // namespace utility
|
|
||||
|
|
||||
} // namespace storm
|
|
||||
|
|
||||
|
|
||||
@ -1,65 +0,0 @@ |
|||||
/* |
|
||||
* CuddUtility.h |
|
||||
* |
|
||||
* Created on: 26.01.2013 |
|
||||
* Author: Christian Dehnert |
|
||||
*/ |
|
||||
|
|
||||
#ifndef STORM_UTILITY_CUDDUTILITY_H_ |
|
||||
#define STORM_UTILITY_CUDDUTILITY_H_ |
|
||||
|
|
||||
#include "cuddObj.hh" |
|
||||
|
|
||||
#include <cstdint> |
|
||||
|
|
||||
namespace storm { |
|
||||
|
|
||||
namespace utility { |
|
||||
|
|
||||
class CuddUtility { |
|
||||
public: |
|
||||
~CuddUtility() { |
|
||||
for (auto element : allDecisionDiagramVariables) { |
|
||||
delete element; |
|
||||
} |
|
||||
} |
|
||||
|
|
||||
ADD* getNewAddVariable(); |
|
||||
ADD* getAddVariable(int index) const; |
|
||||
|
|
||||
ADD* getOne() const; |
|
||||
ADD* getZero() const; |
|
||||
|
|
||||
ADD* getConstantEncoding(uint_fast64_t constant, std::vector<ADD*> const& variables) const; |
|
||||
|
|
||||
void setValueAtIndex(ADD* add, uint_fast64_t index, std::vector<ADD*> const& variables, double value) const; |
|
||||
void setValueAtIndices(ADD* add, uint_fast64_t rowIndex, uint_fast64_t columnIndex, std::vector<ADD*> const& rowVariables, std::vector<ADD*> const& columnVariables, double value) const; |
|
||||
|
|
||||
ADD* getConstant(double value) const; |
|
||||
|
|
||||
ADD* permuteVariables(ADD* add, std::vector<ADD*> fromVariables, std::vector<ADD*> toVariables, uint_fast64_t totalNumberOfVariables) const; |
|
||||
|
|
||||
void dumpDotToFile(ADD* add, std::string filename) const; |
|
||||
|
|
||||
Cudd const& getManager() const; |
|
||||
|
|
||||
friend CuddUtility* cuddUtilityInstance(); |
|
||||
|
|
||||
private: |
|
||||
CuddUtility() : manager(), allDecisionDiagramVariables() { |
|
||||
|
|
||||
} |
|
||||
|
|
||||
Cudd manager; |
|
||||
std::vector<ADD*> allDecisionDiagramVariables; |
|
||||
|
|
||||
static CuddUtility* instance; |
|
||||
}; |
|
||||
|
|
||||
CuddUtility* cuddUtilityInstance(); |
|
||||
|
|
||||
} // namespace utility |
|
||||
|
|
||||
} // namespace storm |
|
||||
|
|
||||
#endif /* STORM_UTILITY_CUDDUTILITY_H_ */ |
|
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue