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

Merge branch 'future' into python_api 

Former-commit-id: b056d49e73
main
sjunges 10 years ago
parent
8e07f5855d 3bdd87e7a7
commit
ed66cb2daf
7 changed files with 39 additions and 19 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. 6
      src/adapters/MathsatExpressionAdapter.h
  2. 2
      src/builder/ExplicitPrismModelBuilder.cpp
  3. 2
      src/models/sparse/Model.cpp
  4. 13
      src/storage/SparseMatrix.cpp
  5. 14
      src/storage/SparseMatrix.h
  6. 16
      src/utility/graph.cpp
  7. 5
      test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp

6
src/adapters/MathsatExpressionAdapter.h
View File

@ -22,9 +22,9 @@
namespace std {
// Define hashing operator for MathSAT's declarations.
template <>
struct std::hash<msat_decl> {
std::size_t operator()(msat_decl const& declaration) const {
return std::hash<void*>()(declaration.repr);
struct hash<msat_decl> {
size_t operator()(msat_decl const& declaration) const {
return hash<void*>()(declaration.repr);
}
};
}

2
src/builder/ExplicitPrismModelBuilder.cpp
View File

@ -244,7 +244,7 @@ namespace storm {
// not only appear in the probabilities, we re
if (!std::is_same<ValueType, storm::RationalFunction>::value && preparedProgram->hasUndefinedConstants()) {
#else
if (preparedProgram.hasUndefinedConstants()) {
if (preparedProgram->hasUndefinedConstants()) {
#endif
std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = preparedProgram->getUndefinedConstants();
std::stringstream stream;

2
src/models/sparse/Model.cpp
View File

@ -320,7 +320,7 @@ namespace storm {
return this->rewardModels;
}
std::set<storm::Variable> getProbabilityParameters(Model<storm::RationalNumber> const& model) {
std::set<storm::Variable> getProbabilityParameters(Model<storm::RationalFunction> const& model) {
return storm::storage::getVariables(model.getTransitionMatrix());
}

13
src/storage/SparseMatrix.cpp
View File

@ -1208,6 +1208,19 @@ namespace storm {
return result;
}
#ifdef STORM_HAVE_CARL
std::set<storm::Variable> getVariables(SparseMatrix<storm::RationalFunction> const& matrix)
{
std::set<storm::Variable> result;
for(auto const& entry : matrix) {
entry.getValue().gatherVariables(result);
}
return result;
}
#endif
// Explicitly instantiate the entry, builder and the matrix.
// double
template class MatrixEntry<typename SparseMatrix<double>::index_type, double>;

14
src/storage/SparseMatrix.h
View File

@ -8,7 +8,7 @@
#include <iterator>
#include "src/utility/OsDetection.h"
#include "src/adapters/CarlAdapter.h"
#include <boost/functional/hash.hpp>
// Forward declaration for adapter classes.
@ -970,14 +970,10 @@ namespace storm {
};
std::set<storm::Variable> getVariables(SparseMatrix<storm::RationalFunction> const& matrix) {
std::set<storm::Variable> result;
for(auto const& entry : matrix) {
entry.probability.gatherVariables(result);
}
return result;
}
#ifdef STORM_HAVE_CARL
std::set<storm::Variable> getVariables(SparseMatrix<storm::RationalFunction> const& matrix);
#endif
} // namespace storage
} // namespace storm

16
src/utility/graph.cpp
View File

@ -986,9 +986,10 @@ namespace storm {
template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<double>> const& model, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>> const& model, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<double>> const& model, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
#ifdef STORM_HAVE_CARL
template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>> const& model, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
#endif
template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
@ -1004,19 +1005,24 @@ namespace storm {
template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<double>> const& model, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
#ifdef STORM_HAVE_CARL
template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>> const& model, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
#endif
template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
template storm::storage::BitVector performProb1A(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<double>> const& model, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
#ifdef STORM_HAVE_CARL
template storm::storage::BitVector performProb1A(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>> const& model, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
#endif
template storm::storage::BitVector performProb1A( storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<double>> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
#ifdef STORM_HAVE_CARL
template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
#endif
template std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<double> const& matrix) ;

5
test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
View File

@ -10,6 +10,9 @@
#include "src/models/sparse/StandardRewardModel.h"
#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#ifdef STORM_HAVE_MSAT
TEST(SmtPermissiveSchedulerTest, DieSelection) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die_c1.nm");
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
@ -58,3 +61,5 @@ TEST(SmtPermissiveSchedulerTest, DieSelection) {
//
}
#endif // STORM_HAVE_MSAT
Write Preview
Loading…
Cancel
Save