Browse Source

fixed displaying of non const states and transitions

Former-commit-id: 6f621d6980
tempestpy_adaptions
TimQu 9 years ago
parent
commit
2b320523b5
  1. 4
      src/cli/entrypoints.h
  2. 2
      src/storage/SparseMatrix.cpp

4
src/cli/entrypoints.h

@ -28,8 +28,8 @@ namespace storm {
template<> template<>
inline void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) { inline void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
if (storm::settings::generalSettings().isParametricRegionSet()){ if (storm::settings::generalSettings().isParametricRegionSet()){
std::cout << "Num of states with nonconstant transitions; Num of nonconstant transitions" << std::endl;
std::cout << "NUM_PARS" << model->getTransitionMatrix().getNonconstantRowGroupCount() << ";" << model->getTransitionMatrix().getNonconstantEntryCount() << std::endl;
// std::cout << "Num of states with nonconstant transitions; Num of nonconstant transitions" << std::endl;
// std::cout << "NUM_PARS;" << model->getTransitionMatrix().getNonconstantRowGroupCount() << ";" << model->getTransitionMatrix().getNonconstantEntryCount() << std::endl;
auto regions=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::getRegionsFromSettings(); auto regions=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::getRegionsFromSettings();
std::shared_ptr<storm::modelchecker::region::AbstractSparseRegionModelChecker<storm::models::sparse::Model<storm::RationalFunction>, double>> modelchecker; std::shared_ptr<storm::modelchecker::region::AbstractSparseRegionModelChecker<storm::models::sparse::Model<storm::RationalFunction>, double>> modelchecker;
if(model->isOfType(storm::models::ModelType::Dtmc)){ if(model->isOfType(storm::models::ModelType::Dtmc)){

2
src/storage/SparseMatrix.cpp

@ -1157,7 +1157,7 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
typename SparseMatrix<ValueType>::index_type SparseMatrix<ValueType>::getNonconstantRowGroupCount() const { typename SparseMatrix<ValueType>::index_type SparseMatrix<ValueType>::getNonconstantRowGroupCount() const {
index_type nonConstRowGroups = 0; index_type nonConstRowGroups = 0;
for (index_type rowGroup=0; rowGroup < this->getRowGroupIndices().size(); ++rowGroup) {
for (index_type rowGroup=0; rowGroup < this->getRowGroupCount(); ++rowGroup) {
for( auto const& entry : this->getRowGroup(rowGroup)){ for( auto const& entry : this->getRowGroup(rowGroup)){
if(!storm::utility::isConstant(entry.getValue())){ if(!storm::utility::isConstant(entry.getValue())){
++nonConstRowGroups; ++nonConstRowGroups;

Loading…
Cancel
Save