fix gmp, replace size_t

randriu · Jun 11, 2024 · 0d69279 · 0d69279
1 parent b690fa7
commit 0d69279
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git a/payntbind/src/synthesis/counterexamples/CounterexampleMdp.cpp b/payntbind/src/synthesis/counterexamples/CounterexampleMdp.cpp
@@ -133,7 +133,7 @@ void CounterexampleGeneratorMdp<ValueType,StateType>::prepareMdp(
     this->hole_wave.clear();
     this->wave_states.clear();
     this->state_horizon_blocking.clear();
-    this->unregistered_holes_count = std::vector<size_t>(mdp_states);
+    this->unregistered_holes_count = std::vector<uint64_t>(mdp_states);
     this->mdp_holes = std::vector<std::set<uint64_t>>(mdp_states);
     this->current_wave = 0;
     this->reachable_flag = storm::storage::BitVector(mdp_states, false);
@@ -172,7 +172,7 @@ template <typename ValueType, typename StateType>
 bool CounterexampleGeneratorMdp<ValueType,StateType>::exploreWave () {
 
     storm::storage::SparseMatrix<ValueType> const& transition_matrix = this->mdp->getTransitionMatrix();
-    std::vector<size_t> row_group_indices = transition_matrix.getRowGroupIndices();
+    std::vector<uint64_t> row_group_indices = transition_matrix.getRowGroupIndices();
     uint64_t mdp_states = this->mdp->getNumberOfStates();
 
     // Expand the non-blocking horizon
@@ -391,7 +391,7 @@ std::pair<bool,bool> CounterexampleGeneratorMdp<ValueType,StateType>::expandAndC
     // Get MDP info
     uint64_t mdp_states = this->mdp->getNumberOfStates();
     storm::storage::SparseMatrix<ValueType> const& transition_matrix = this->mdp->getTransitionMatrix();
-    std::vector<size_t> row_group_indices = transition_matrix.getRowGroupIndices();
+    std::vector<uint64_t> row_group_indices = transition_matrix.getRowGroupIndices();
     StateType initial_state = *(this->mdp->getInitialStates().begin());
     std::vector<StateType> to_expand = this->wave_states[current_wave-1];
     // Expand states from the new wave:

diff --git a/payntbind/src/synthesis/quotient/JaniChoices.h b/payntbind/src/synthesis/quotient/JaniChoices.h
@@ -1,5 +1,6 @@
 #pragma once
 
+#include <storm/adapters/RationalNumberAdapter.h>
 #include <storm/models/sparse/Model.h>
 
 namespace synthesis {