From 6147b35fc8525cd560274e28a7c1347b4a214ba5 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 6 Feb 2020 14:28:22 +0100 Subject: [PATCH] collect number of variables --- src/storm/storage/jani/Model.cpp | 8 ++++++++ src/storm/storage/jani/Model.h | 8 +++++++- src/storm/storage/jani/VariableSet.cpp | 11 ++++++++++- src/storm/storage/jani/VariableSet.h | 20 +++++++++++++++----- 4 files changed, 40 insertions(+), 7 deletions(-) diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index c05417ae2..224857989 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -676,6 +676,14 @@ namespace storm { return res; } + std::size_t Model::getTotalNumberOfNonTransientVariables() const { + std::size_t res = globalVariables.getNumberOfNontransientVariables(); + for (auto const& aut : getAutomata()) { + res += aut.getVariables().getNumberOfNontransientVariables(); + } + return res; + } + Variable const& Model::addVariable(Variable const& variable) { if (variable.isBooleanVariable()) { return addVariable(variable.asBooleanVariable()); diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index 3adbdd51c..c213fb937 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -384,7 +384,13 @@ namespace storm { * Retrieves the total number of edges in this model. */ std::size_t getNumberOfEdges() const; - + + /*! + * Number of global and local variables. + */ + std::size_t getTotalNumberOfNonTransientVariables() const; + + /*! * Sets the system composition expression of the JANI model. */ diff --git a/src/storm/storage/jani/VariableSet.cpp b/src/storm/storage/jani/VariableSet.cpp index c3ba52a5a..2633c3856 100644 --- a/src/storm/storage/jani/VariableSet.cpp +++ b/src/storm/storage/jani/VariableSet.cpp @@ -321,7 +321,16 @@ namespace storm { bool VariableSet::empty() const { return !(containsBooleanVariable() || containsBoundedIntegerVariable() || containsUnboundedIntegerVariables() || containsRealVariables() || containsArrayVariables() || containsClockVariables()); } - + + uint64_t VariableSet::getNumberOfVariables() const { + return variables.size(); + } + + + uint64_t VariableSet::getNumberOfNontransientVariables() const { + return getNumberOfVariables() - getNumberOfTransientVariables(); + } + uint_fast64_t VariableSet::getNumberOfTransientVariables() const { uint_fast64_t result = 0; for (auto const& variable : variables) { diff --git a/src/storm/storage/jani/VariableSet.h b/src/storm/storage/jani/VariableSet.h index 612d2e992..53f45a359 100644 --- a/src/storm/storage/jani/VariableSet.h +++ b/src/storm/storage/jani/VariableSet.h @@ -228,26 +228,36 @@ namespace storm { * Retrieves whether this variable set is empty. */ bool empty() const; - + + /*! + * Total number of variables, including transient variables. + */ + uint64_t getNumberOfVariables() const; + + /* + * Total number of nontransient variables + */ + uint64_t getNumberOfNontransientVariables() const; + /*! * Retrieves the number of transient variables in this variable set. */ - uint_fast64_t getNumberOfTransientVariables() const; + uint64_t getNumberOfTransientVariables() const; /*! * Retrieves the number of real transient variables in this variable set. */ - uint_fast64_t getNumberOfRealTransientVariables() const; + uint64_t getNumberOfRealTransientVariables() const; /*! * Retrieves the number of unbounded integer transient variables in this variable set. */ - uint_fast64_t getNumberOfUnboundedIntegerTransientVariables() const; + uint64_t getNumberOfUnboundedIntegerTransientVariables() const; /*! * Retrieves the number of numerical (i.e. real, or integer) transient variables in this variable set. */ - uint_fast64_t getNumberOfNumericalTransientVariables() const; + uint64_t getNumberOfNumericalTransientVariables() const; /*! * Retrieves the transient variables in this variable set.