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

Renamed NonDeterministic to Nondeterministic in all places. Fixed (hopefully) all occurrences of these names. Implemented Prob0A algorithm.

tempestpy_adaptions
dehnert 12 years ago
parent
73ab4a78a9
commit
8c248c05c5
11 changed files with 88 additions and 45 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. 28
      src/models/AbstractNondeterministicModel.h
  2. 8
      src/models/Ctmdp.h
  3. 8
      src/models/Mdp.h
  4. 6
      src/parser/AutoParser.h
  5. 8
      src/parser/NondeterministicModelParser.cpp
  6. 7
      src/parser/NondeterministicModelParser.h
  7. 6
      src/parser/NondeterministicSparseTransitionParser.cpp
  8. 4
      src/parser/NondeterministicSparseTransitionParser.h
  9. 44
      src/utility/GraphAnalyzer.h
  10. 6
      test/parser/ParseMdpTest.cpp
  11. 8
      test/storage/SparseMatrixTest.cpp

28
src/models/AbstractNonDeterministicModel.h → src/models/AbstractNondeterministicModel.h
View File

@ -16,7 +16,7 @@ namespace models {
* This is base class defines a common interface for all non-deterministic models.
*/
template<class T>
class AbstractNonDeterministicModel: public AbstractModel<T> {
class AbstractNondeterministicModel: public AbstractModel<T> {
public:
/*! Constructs an abstract non-determinstic model from the given parameters.
@ -27,27 +27,27 @@ class AbstractNonDeterministicModel: public AbstractModel<T> {
* @param stateRewardVector The reward values associated with the states.
* @param transitionRewardMatrix The reward values associated with the transitions of the model.
*/
AbstractNonDeterministicModel(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix,
AbstractNondeterministicModel(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix,
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices,
std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices,
std::shared_ptr<std::vector<T>> stateRewardVector,
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix)
: AbstractModel<T>(transitionMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix),
choiceIndices(choiceIndices) {
nondeterministicChoiceIndices(nondeterministicChoiceIndices) {
}
/*!
* Destructor.
*/
virtual ~AbstractNonDeterministicModel() {
virtual ~AbstractNondeterministicModel() {
// Intentionally left empty.
}
/*!
* Copy Constructor.
*/
AbstractNonDeterministicModel(AbstractNonDeterministicModel const& other) : AbstractModel<T>(other),
choiceIndices(other.choiceIndices) {
AbstractNondeterministicModel(AbstractNondeterministicModel const& other) : AbstractModel<T>(other),
nondeterministicChoiceIndices(other.nondeterministicChoiceIndices) {
// Intentionally left empty.
}
@ -57,12 +57,22 @@ class AbstractNonDeterministicModel: public AbstractModel<T> {
* measured in bytes.
*/
virtual uint_fast64_t getSizeInMemory() const {
return AbstractModel<T>::getSizeInMemory() + choiceIndices->size() * sizeof(uint_fast64_t);
return AbstractModel<T>::getSizeInMemory() + nondeterministicChoiceIndices->size() * sizeof(uint_fast64_t);
}
/*!
* Retrieves the vector indicating which matrix rows represent non-deterministic choices
* of a certain state.
* @param the vector indicating which matrix rows represent non-deterministic choices
* of a certain state.
*/
std::shared_ptr<std::vector<uint_fast64_t>> getNondeterministicChoiceIndices() const {
return nondeterministicChoiceIndices;
}
private:
/*! A vector of indices mapping states to the choices (rows) in the transition matrix. */
std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices;
std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices;
};
} // namespace models

8
src/models/Ctmdp.h
View File

@ -12,7 +12,7 @@
#include <vector>
#include "AtomicPropositionsLabeling.h"
#include "AbstractNonDeterministicModel.h"
#include "AbstractNondeterministicModel.h"
#include "src/storage/SparseMatrix.h"
#include "src/utility/Settings.h"
@ -25,7 +25,7 @@ namespace models {
* labeled with atomic propositions.
*/
template <class T>
class Ctmdp : public storm::models::AbstractNonDeterministicModel<T> {
class Ctmdp : public storm::models::AbstractNondeterministicModel<T> {
public:
//! Constructor
@ -42,7 +42,7 @@ public:
std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices,
std::shared_ptr<std::vector<T>> stateRewardVector = nullptr,
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix = nullptr)
: AbstractNonDeterministicModel<T>(probabilityMatrix, stateLabeling, choiceIndices, stateRewardVector, transitionRewardMatrix) {
: AbstractNondeterministicModel<T>(probabilityMatrix, stateLabeling, choiceIndices, stateRewardVector, transitionRewardMatrix) {
if (!this->checkValidityOfProbabilityMatrix()) {
LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
@ -54,7 +54,7 @@ public:
* Copy Constructor. Performs a deep copy of the given CTMDP.
* @param ctmdp A reference to the CTMDP that is to be copied.
*/
Ctmdp(const Ctmdp<T> &ctmdp) : AbstractNonDeterministicModel<T>(ctmdp) {
Ctmdp(const Ctmdp<T> &ctmdp) : AbstractNondeterministicModel<T>(ctmdp) {
if (!this->checkValidityOfProbabilityMatrix()) {
LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";

8
src/models/Mdp.h
View File

@ -16,7 +16,7 @@
#include "AtomicPropositionsLabeling.h"
#include "src/storage/SparseMatrix.h"
#include "src/utility/Settings.h"
#include "src/models/AbstractNonDeterministicModel.h"
#include "src/models/AbstractNondeterministicModel.h"
namespace storm {
@ -27,7 +27,7 @@ namespace models {
* labeled with atomic propositions.
*/
template <class T>
class Mdp : public storm::models::AbstractNonDeterministicModel<T> {
class Mdp : public storm::models::AbstractNondeterministicModel<T> {
public:
//! Constructor
@ -44,7 +44,7 @@ public:
std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices,
std::shared_ptr<std::vector<T>> stateRewardVector = nullptr,
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix = nullptr)
: AbstractNonDeterministicModel<T>(probabilityMatrix, stateLabeling, choiceIndices, stateRewardVector, transitionRewardMatrix) {
: AbstractNondeterministicModel<T>(probabilityMatrix, stateLabeling, choiceIndices, stateRewardVector, transitionRewardMatrix) {
if (!this->checkValidityOfProbabilityMatrix()) {
LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
@ -56,7 +56,7 @@ public:
* Copy Constructor. Performs a deep copy of the given MDP.
* @param mdp A reference to the MDP that is to be copied.
*/
Mdp(const Mdp<T> &mdp) : AbstractNonDeterministicModel<T>(mdp) {
Mdp(const Mdp<T> &mdp) : AbstractNondeterministicModel<T>(mdp) {
if (!this->checkValidityOfProbabilityMatrix()) {
LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";

6
src/parser/AutoParser.h
View File

@ -7,7 +7,7 @@
#include "src/exceptions/WrongFileFormatException.h"
#include "src/models/AbstractModel.h"
#include "src/parser/DeterministicModelParser.h"
#include "src/parser/NonDeterministicModelParser.h"
#include "src/parser/NondeterministicModelParser.h"
#include <memory>
#include <iostream>
@ -57,12 +57,12 @@ class AutoParser : Parser {
break;
}
case storm::models::MDP: {
NonDeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
NondeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
this->model = parser.getMdp();
break;
}
case storm::models::CTMDP: {
NonDeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
NondeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
this->model = parser.getCtmdp();
break;
}

8
src/parser/NonDeterministicModelParser.cpp → src/parser/NondeterministicModelParser.cpp
View File

@ -10,7 +10,7 @@
#include <string>
#include <vector>
#include "src/parser/NonDeterministicSparseTransitionParser.h"
#include "src/parser/NondeterministicSparseTransitionParser.h"
#include "src/parser/AtomicPropositionLabelingParser.h"
#include "src/parser/SparseStateRewardParser.h"
@ -27,9 +27,9 @@ namespace parser {
* @param stateRewardFile String containing the location of the state reward file (...srew)
* @param transitionRewardFile String containing the location of the transition reward file (...trew)
*/
NonDeterministicModelParser::NonDeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile,
NondeterministicModelParser::NondeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & stateRewardFile, std::string const & transitionRewardFile) {
storm::parser::NonDeterministicSparseTransitionParser tp(transitionSystemFile);
storm::parser::NondeterministicSparseTransitionParser tp(transitionSystemFile);
uint_fast64_t stateCount = tp.getMatrix()->getRowCount();
storm::parser::AtomicPropositionLabelingParser lp(stateCount, labelingFile);
@ -38,7 +38,7 @@ NonDeterministicModelParser::NonDeterministicModelParser(std::string const & tra
this->stateRewards = srp.getStateRewards();
}
if (transitionRewardFile != "") {
storm::parser::NonDeterministicSparseTransitionParser trp(transitionRewardFile);
storm::parser::NondeterministicSparseTransitionParser trp(transitionRewardFile);
this->transitionRewardMatrix = trp.getMatrix();
}

7
src/parser/NonDeterministicModelParser.h → src/parser/NondeterministicModelParser.h
View File

@ -13,6 +13,7 @@
#include "src/models/Ctmdp.h"
namespace storm {
namespace parser {
/*!
@ -23,9 +24,9 @@ namespace parser {
*
* @note The labeling representation in the file may use at most as much nodes as are specified in the mdp.
*/
class NonDeterministicModelParser: public storm::parser::Parser {
class NondeterministicModelParser: public storm::parser::Parser {
public:
NonDeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile,
NondeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "");
std::shared_ptr<storm::models::Mdp<double>> getMdp() {
@ -58,5 +59,7 @@ private:
};
} /* namespace parser */
} /* namespace storm */
#endif /* STORM_PARSER_NONDETERMINISTICMODELPARSER_H_ */

6
src/parser/NonDeterministicSparseTransitionParser.cpp → src/parser/NondeterministicSparseTransitionParser.cpp
View File

@ -5,7 +5,7 @@
* Author: Gereon Kremer
*/
#include "src/parser/NonDeterministicSparseTransitionParser.h"
#include "src/parser/NondeterministicSparseTransitionParser.h"
#include <errno.h>
#include <time.h>
@ -49,7 +49,7 @@ namespace parser {
* @param maxnode Is set to highest id of all nodes.
* @return The number of non-zero elements.
*/
uint_fast64_t NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode) {
uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode) {
/*
* Check file header and extract number of transitions.
*/
@ -154,7 +154,7 @@ uint_fast64_t NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_
* @return a pointer to the created sparse matrix.
*/
NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(std::string const &filename)
NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(std::string const &filename)
: matrix(nullptr) {
/*
* Enforce locale where decimal point is '.'.

4
src/parser/NonDeterministicSparseTransitionParser.h → src/parser/NondeterministicSparseTransitionParser.h
View File

@ -17,9 +17,9 @@ namespace parser {
* @brief Load a nondeterministic transition system from file and create a
* sparse adjacency matrix whose entries represent the weights of the edges
*/
class NonDeterministicSparseTransitionParser : public Parser {
class NondeterministicSparseTransitionParser : public Parser {
public:
NonDeterministicSparseTransitionParser(std::string const &filename);
NondeterministicSparseTransitionParser(std::string const &filename);
inline std::shared_ptr<storm::storage::SparseMatrix<double>> getMatrix() const {
return this->matrix;

44
src/utility/GraphAnalyzer.h
View File

@ -9,7 +9,7 @@
#define STORM_UTILITY_GRAPHANALYZER_H_
#include "src/models/AbstractDeterministicModel.h"
#include "src/models/AbstractNonDeterministicModel.h"
#include "src/models/AbstractNondeterministicModel.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "log4cplus/logger.h"
@ -149,7 +149,7 @@ public:
}
template <class T>
static void performProb01Max(storm::models::AbstractNonDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) {
static void performProb01Max(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) {
// Check for valid parameters.
if (statesWithProbability0 == nullptr) {
LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null.");
@ -166,17 +166,47 @@ public:
}
template <class T>
static void performProb0A(storm::models::AbstractNonDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) {
static void performProb0A(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) {
// Check for valid parameter.
if (statesWithProbability0 == nullptr) {
LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null.");
throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability0' must not be null.");
}
// Get the backwards transition relation from the model to ease the search.
storm::models::GraphTransitions<T> backwardTransitions(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), false);
// Add all psi states as the already satisfy the condition.
*statesWithProbability0 |= psiStates;
// Initialize the stack used for the DFS with the states
std::vector<uint_fast64_t> stack;
stack.reserve(model.getNumberOfStates());
psiStates.getList(stack);
// Perform the actual DFS.
while(!stack.empty()) {
uint_fast64_t currentState = stack.back();
stack.pop_back();
for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) {
if (phiStates.get(*it) && !statesWithProbability0->get(*it)) {
statesWithProbability0->set(*it, true);
stack.push_back(*it);
}
}
}
statesWithProbability0->complement();
}
template <class T>
static void performProb1E(storm::models::AbstractNonDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) {
static void performProb1E(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) {
}
template <class T>
static void performProb01Min(storm::models::AbstractNonDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) {
static void performProb01Min(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) {
// Check for valid parameters.
if (statesWithProbability0 == nullptr) {
LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null.");
@ -193,12 +223,12 @@ public:
}
template <class T>
static void performProb0E(storm::models::AbstractNonDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) {
static void performProb0E(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) {
}
template <class T>
static void performProb1A(storm::models::AbstractNonDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) {
static void performProb1A(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) {
// This result is a rough guess and does not compute all states with probability 1.
// TODO: Check whether it makes sense to implement the precise but complicated algorithm here.
*statesWithProbability1 = psiStates;

6
test/parser/ParseMdpTest.cpp
View File

@ -8,12 +8,12 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/parser/NonDeterministicModelParser.h"
#include "src/parser/NondeterministicModelParser.h"
#include "src/utility/IoUtility.h"
TEST(ParseMdpTest, parseAndOutput) {
storm::parser::NonDeterministicModelParser* mdpParser = nullptr;
ASSERT_NO_THROW(mdpParser = new storm::parser::NonDeterministicModelParser(
storm::parser::NondeterministicModelParser* mdpParser = nullptr;
ASSERT_NO_THROW(mdpParser = new storm::parser::NondeterministicModelParser(
STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_general_input_01.tra",
STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));

8
test/storage/SparseMatrixTest.cpp
View File

@ -80,7 +80,7 @@ TEST(SparseMatrixTest, Test) {
int position_row[50] = {
2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
2, 2, 2, 2, /* first row empty, one full row ��������� 25 minus the diagonal entry */
2, 2, 2, 2, /* first row empty, one full row 25 minus the diagonal entry */
4, 4, /* one empty row, then first and last column */
13, 13, 13, 13, /* a few empty rows, middle columns */
24, 24, 24, 24, 24, 24, 24, 24, 24, 24,
@ -288,9 +288,9 @@ TEST(SparseMatrixTest, ConversionFromSparseEigen_RowMajor_SparseMatrixTest) {
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady);
const std::vector<uint_fast64_t> rowP = ssm->getRowIndicationsPointer();
const std::vector<uint_fast64_t> colP = ssm->getColumnIndicationsPointer();
const std::vector<int> valP = ssm->getStoragePointer();
const std::vector<uint_fast64_t> rowP = ssm->getRowIndications();
const std::vector<uint_fast64_t> colP = ssm->getColumnIndications();
const std::vector<int> valP = ssm->getStorage();
int target = -1;
for (auto &coeff: tripletList) {

Write Preview
Loading…
Cancel
Save