Fix simulation reduction

3rdparty/simlib/include/mata/simlib/explicit_lts.hh

@@ -21,6 +21,7 @@ namespace Simlib { class ExplicitLTS; }
 
 class Simlib::ExplicitLTS {
 
+	std::unordered_map<size_t, size_t> symbol_map{};
 	size_t states_{};
 	size_t transitions_;
 	std::vector<

3rdparty/simlib/src/explicit_lts_sim.cc

@@ -903,11 +903,9 @@ BinaryRelation Simlib::ExplicitLTS::compute_simulation()
 }
 
 
-void Simlib::ExplicitLTS::add_transition(
-	size_t   q,
-	size_t   a,
-	size_t   r)
-{
+void Simlib::ExplicitLTS::add_transition(size_t q, size_t a, size_t r) {
+	if (!symbol_map.contains(a)) { symbol_map[a] = symbol_map.size(); };
+	a = symbol_map[a];
 	if (a >= this->data_.size())
 	{
 		this->data_.resize(a + 1);

src/nfa/operations.cc

@@ -38,15 +38,12 @@ using StateBoolArray = std::vector<bool>; ///< Bool array for states in the auto
 
 namespace {
     Simlib::Util::BinaryRelation compute_fw_direct_simulation(const Nfa& aut) {
-        Symbol maxSymbol = 0;
+        Symbol maxSymbol{ aut.get_max_symbol() };
         const size_t state_num = aut.size();
         Simlib::ExplicitLTS LTSforSimulation(state_num);
 
         for (const Transition& transition : aut.delta.transitions()) {
             LTSforSimulation.add_transition(transition.source, transition.symbol, transition.target);
-            if (transition.symbol > maxSymbol) {
-                maxSymbol = transition.symbol;
-            }
         }
 
         // final states cannot be simulated by nonfinal -> we add new selfloops over final states with new symbol in LTS

tests-integration/src/reduce_epsilon.cc

@@ -0,0 +1,39 @@
+#include "utils/utils.hh"
+
+#include "mata/nfa/nfa.hh"
+
+#include <cstdlib>
+#include <iostream>
+#include <iomanip>
+#include <fstream>
+#include <chrono>
+#include <string>
+#include <cstring>
+
+using namespace mata::nfa;
+
+int main() {
+    Nfa b{10};
+    b.initial.insert(0);
+    b.final.insert({2, 4, 8, 7});
+    b.delta.add(0, 'b', 1);
+    b.delta.add(0, 'a', 2);
+    b.delta.add(2, 'a', 4);
+    b.delta.add(2, EPSILON, 3);
+    b.delta.add(3, 'b', 4);
+    b.delta.add(0, 'c', 5);
+    b.delta.add(5, 'a', 8);
+    b.delta.add(5, EPSILON, 6);
+    b.delta.add(6, 'a', 9);
+    b.delta.add(6, 'b', 7);
+
+    Nfa c;
+    TIME_BLOCK(reduce,
+        for (size_t i{ 0 }; i < 1'000; ++i) {
+            c = reduce(b);
+        }
+    );
+    if (!are_equivalent(b, c)) { // Check correctness.
+        return EXIT_FAILURE;
+    }
+}