Merge lp:~tapaal-ltl/verifypn/buchi-better-cleanup into lp:~tapaal-ltl/verifypn/ltl-model-checker

[Nikolaj Jensen Ulrik]

Use `spot::twa_graph_ptr::release_iter` instead of `delete` to clean-up used `spot::twa_succ_iterator`. According to the documentation, this lets spot reuse memory for iterators, thus saving heap allocation and deallocation steps. Uses custom deleter support in `std::unique_ptr` to accomplish this.

[Simon Virenfeldt (simwir)]

review: Approve

=== modified file 'include/LTL/BuchiSuccessorGenerator.h'
--- include/LTL/BuchiSuccessorGenerator.h	2021-02-01 11:17:38 +0000
+++ include/LTL/BuchiSuccessorGenerator.h	2021-02-15 13:10:57 +0000
@@ -29,44 +29,67 @@
     class BuchiSuccessorGenerator {
     public:
         explicit BuchiSuccessorGenerator(Structures::BuchiAutomaton automaton)
-                : aut(std::move(automaton)) {
+                : aut(std::move(automaton))
+        {
+            deleter = SuccIterDeleter{&aut};
         }
 
-        void prepare(size_t state) {
+        void prepare(size_t state)
+        {
             auto curstate = aut.buchi->state_from_number(state);
-            succ = std::unique_ptr<spot::twa_succ_iterator>{aut.buchi->succ_iter(curstate)};
+            succ = _succ_iter{aut.buchi->succ_iter(curstate), SuccIterDeleter{&aut}};
             succ->first();
         }
 
-        bool next(size_t &state, bdd &cond) {
+        bool next(size_t &state, bdd &cond)
+        {
             if (!succ->done()) {
-                state = aut.buchi->state_number(succ->dst());
+                auto dst = succ->dst();
+                state = aut.buchi->state_number(dst);
                 cond = succ->cond();
                 succ->next();
+                dst->destroy();
                 return true;
             }
             return false;
         }
 
-        [[nodiscard]] bool is_accepting(size_t state) const {
+        [[nodiscard]] bool is_accepting(size_t state) const
+        {
             return aut.buchi->state_is_accepting(state);
         }
 
-        [[nodiscard]] size_t initial_state_number() const {
+        [[nodiscard]] size_t initial_state_number() const
+        {
             return aut.buchi->get_init_state_number();
         }
 
-        [[nodiscard]] Condition_ptr getExpression(size_t i) const {
+        [[nodiscard]] Condition_ptr getExpression(size_t i) const
+        {
             return aut.ap_info.at(i).expression;
         }
 
-        [[nodiscard]] bool is_weak() const {
+        [[nodiscard]] bool is_weak() const
+        {
             return (bool) aut.buchi->prop_weak();
         }
 
     private:
         Structures::BuchiAutomaton aut;
-        std::unique_ptr<spot::twa_succ_iterator> succ;
+
+        struct SuccIterDeleter {
+            Structures::BuchiAutomaton *aut;
+
+            void operator()(spot::twa_succ_iterator *iter) const
+            {
+                aut->buchi->release_iter(iter);
+            }
+        };
+
+        SuccIterDeleter deleter{};
+
+        using _succ_iter = std::unique_ptr<spot::twa_succ_iterator, SuccIterDeleter>;
+        _succ_iter succ = nullptr;
     };
 }
 #endif //VERIFYPN_BUCHISUCCESSORGENERATOR_H