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

Adapted some code to work with carl. 

Former-commit-id: 722669f4bf
tempestpy_adaptions
dehnert 10 years ago
parent
5857fff138
commit
4804ed636d
7 changed files with 61 additions and 37 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. 1
      src/adapters/ExplicitModelAdapter.h
  2. 35
      src/adapters/extendedCarl.h
  3. 8
      src/storage/SparseMatrix.cpp
  4. 2
      src/storage/StronglyConnectedComponentDecomposition.cpp
  5. 40
      src/storage/expressions/ExpressionEvaluation.h
  6. 6
      src/storage/parameters.h
  7. 6
      src/stormParametric.cpp

1
src/adapters/ExplicitModelAdapter.h
View File

@ -646,7 +646,6 @@ namespace storm {
ModelComponents modelComponents;
expressions::ExpressionEvaluation<ValueType> eval;
VariableInformation variableInformation;
for (auto const& integerVariable : program.getGlobalIntegerVariables()) {
variableInformation.variableToBoundsMap[integerVariable.getName()] = std::make_pair(integerVariable.getLowerBoundExpression().evaluateAsInt(), integerVariable.getUpperBoundExpression().evaluateAsInt());

35
src/adapters/extendedCarl.h
View File

@ -1,4 +1,4 @@
/**
/**
* @file: extendedCarl.h
* @author: Sebastian Junges
*
@ -13,22 +13,29 @@
#include <carl/core/RationalFunction.h>
#include <carl/core/VariablePool.h>
#include <carl/core/Constraint.h>
#include <carl/core/FactorizedPolynomial.h>
namespace carl
{
template<typename C, typename O, typename P>
inline size_t hash_value(carl::MultivariatePolynomial<C,O,P> const& p)
{
std::hash<carl::MultivariatePolynomial<C,O,P>> h;
return h(p);
}
template<typename Pol>
inline size_t hash_value(carl::RationalFunction<Pol> const& f)
{
std::hash<Pol> h;
return h(f.nominator()) ^ h(f.denominator());
}
template<typename C, typename O, typename P>
inline size_t hash_value(carl::MultivariatePolynomial<C,O,P> const& p)
{
std::hash<carl::MultivariatePolynomial<C,O,P>> h;
return h(p);
}
template<typename Pol>
inline size_t hash_value(carl::RationalFunction<Pol> const& f)
{
std::hash<Pol> h;
return h(f.nominator()) ^ h(f.denominator());
}
template<typename Pol>
inline size_t hash_value(carl::FactorizedPolynomial<Pol> const& p)
{
std::hash<FactorizedPolynomial<Pol>> h;
return h(p);
}
}

8
src/storage/SparseMatrix.cpp
View File

@ -239,7 +239,7 @@ namespace storm {
template<typename ValueType>
SparseMatrix<ValueType>::SparseMatrix(index_type columnCount, std::vector<index_type> const& rowIndications, std::vector<MatrixEntry<index_type, ValueType>> const& columnsAndValues, std::vector<index_type> const& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(columnsAndValues), rowIndications(rowIndications), rowGroupIndices(rowGroupIndices) {
for (auto const& element : *this) {
if (element.getValue() != storm::utility::constantZero<ValueType>()) {
if (!storm::utility::isZero(element.getValue())) {
++this->nonzeroEntryCount;
}
}
@ -248,7 +248,7 @@ namespace storm {
template<typename ValueType>
SparseMatrix<ValueType>::SparseMatrix(index_type columnCount, std::vector<index_type>&& rowIndications, std::vector<MatrixEntry<index_type, ValueType>>&& columnsAndValues, std::vector<index_type>&& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(std::move(columnsAndValues)), rowIndications(std::move(rowIndications)), rowGroupIndices(std::move(rowGroupIndices)) {
for (auto const& element : *this) {
if (element.getValue() != storm::utility::constantZero<ValueType>()) {
if (!storm::utility::isZero(element.getValue())) {
++this->nonzeroEntryCount;
}
}
@ -604,7 +604,7 @@ namespace storm {
// First, we need to count how many entries each column has.
for (index_type group = 0; group < columnCount; ++group) {
for (auto const& transition : joinGroups ? this->getRowGroup(group) : this->getRow(group)) {
if (transition.getValue() != storm::utility::constantZero<ValueType>()) {
if (!storm::utility::isZero(transition.getValue())) {
++rowIndications[transition.getColumn() + 1];
}
}
@ -623,7 +623,7 @@ namespace storm {
// Now we are ready to actually fill in the values of the transposed matrix.
for (index_type group = 0; group < columnCount; ++group) {
for (auto const& transition : joinGroups ? this->getRowGroup(group) : this->getRow(group)) {
if (transition.getValue() != storm::utility::constantZero<ValueType>()) {
if (!storm::utility::isZero(transition.getValue())) {
columnsAndValues[nextIndices[transition.getColumn()]] = std::make_pair(group, transition.getValue());
nextIndices[transition.getColumn()]++;
}

2
src/storage/StronglyConnectedComponentDecomposition.cpp
View File

@ -171,7 +171,7 @@ namespace storm {
p.push_back(currentState);
for (auto const& successor : transitionMatrix.getRowGroup(currentState)) {
if (subsystem.get(successor.getColumn()) && successor.getValue() != storm::utility::constantZero<ValueType>()) {
if (subsystem.get(successor.getColumn()) && !storm::utility::isZero(successor.getValue())) {
if (currentState == successor.getColumn()) {
statesWithSelfLoop.set(currentState);
}

40
src/storage/expressions/ExpressionEvaluation.h
View File

@ -40,19 +40,29 @@ namespace expressions {
{
typedef std::map<std::string, carl::Variable> type;
};
struct ExpressionEvaluationSettings {
static const bool useFactorizedPolynomials = false;
};
struct FactorizedPolynomialsEvaluationSettings : ExpressionEvaluationSettings {
static const bool useFactorizedPolynomials = true;
};
#endif
template<typename T, typename S>
template<typename T, typename S, typename X = FactorizedPolynomialsEvaluationSettings>
class ExpressionEvaluationVisitor : public ExpressionVisitor
{
public:
ExpressionEvaluationVisitor(S* sharedState)
: mSharedState(sharedState)
: mSharedState(sharedState), cache(new carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>())
{
}
virtual ~ExpressionEvaluationVisitor() {}
virtual ~ExpressionEvaluationVisitor() {
}
virtual void visit(IfThenElseExpression const* expression)
{
@ -101,13 +111,13 @@ namespace expressions {
auto it = mSharedState->find(varName);
if(it != mSharedState->end())
{
mValue = T(it->second);
mValue = T(typename T::PolyType(typename T::PolyType::PolyType(it->second), cache));
}
else
{
carl::Variable nVar = carl::VariablePool::getInstance().getFreshVariable(varName);
mSharedState->emplace(varName,nVar);
mValue = T(nVar);
mValue = convertVariableToPolynomial(nVar);
}
}
virtual void visit(UnaryBooleanFunctionExpression const* expression)
@ -124,17 +134,25 @@ namespace expressions {
}
virtual void visit(IntegerLiteralExpression const* expression)
{
// mValue = T(typename T::CoeffType(std::to_string(expression->getValue()), 10));
mValue = T(expression->getValue());
mValue = T(typename T::PolyType(typename T::CoeffType(expression->getValue())));
}
virtual void visit(DoubleLiteralExpression const* expression)
{
std::stringstream str;
str << std::fixed << std::setprecision( 3 ) << expression->getValue();
mValue = T(carl::rationalize<cln::cl_RA>(str.str()));
mValue = T(carl::rationalize<cln::cl_RA>(str.str()));
}
template<typename TP = typename T::PolyType, carl::EnableIf<carl::needs_cache<TP>> = carl::dummy>
T convertVariableToPolynomial(carl::Variable const& nVar) {
return T(typename T::PolyType(typename T::PolyType::PolyType(nVar), cache));
}
template<typename TP = typename T::PolyType, carl::DisableIf<carl::needs_cache<TP>> = carl::dummy>
T convertVariableToPolynomial(carl::Variable const& nVar) {
return T(nVar);
}
const T& value() const
{
return mValue;
@ -143,6 +161,7 @@ namespace expressions {
private:
S* mSharedState;
T mValue;
carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>* cache;
};
template<typename T>
@ -182,9 +201,6 @@ namespace expressions {
return expr.evaluateAsDouble(val);
}
};
}
}

6
src/storage/parameters.h
View File

@ -10,9 +10,11 @@
namespace storm
{
typedef carl::MultivariatePolynomial<cln::cl_RA> Polynomial;
// typedef carl::MultivariatePolynomial<cln::cl_RA> Polynomial;
typedef carl::Variable Variable;
typedef carl::MultivariatePolynomial<cln::cl_RA> RawPolynomial;
typedef carl::FactorizedPolynomial<RawPolynomial> Polynomial;
// typedef RawPolynomial Polynomial;
typedef carl::CompareRelation CompareRelation;
typedef carl::RationalFunction<Polynomial> RationalFunction;

6
src/stormParametric.cpp
View File

@ -9,7 +9,7 @@
#include "src/utility/export.h"
#include "src/modelchecker/reachability/CollectConstraints.h"
#include "src/modelchecker/reachability/DirectEncoding.h"
//#include "src/modelchecker/reachability/DirectEncoding.h"
#include "src/modelchecker/reachability/SparseSccModelChecker.h"
#include "src/storage/parameters.h"
/*!
@ -75,8 +75,8 @@ int main(const int argc, const char** argv) {
}
if(storm::settings::parametricSettings().exportToSmt2File()) {
storm::modelchecker::reachability::DirectEncoding dec;
//storm::utility::exportStreamToFile(dec.encodeAsSmt2(modelChecker.getMatrix(), parameters,));
// storm::modelchecker::reachability::DirectEncoding dec;
// storm::utility::exportStreamToFile(dec.encodeAsSmt2(modelChecker.getMatrix(), parameters,));
}

Write Preview
Loading…
Cancel
Save