Reduce: Simulation algorithm #434

samo538 · 2024-08-26T14:24:41Z

Implementation of a reduction algorithm that uses simulation. The pseudo code for this algorithm can be viewed here: https://github.com/ondrik/iny-fix/blob/master/main.pdf

ondrik

I added some comments about how to improve the code

ondrik · 2024-08-26T18:42:43Z

src/nfa/operations.cc

@@ -56,6 +56,126 @@ namespace {
        return lts_for_simulation.compute_simulation();
    }

+    bool vec_contains(std::vector<std::pair<State, State>> vec, std::pair<State, State> par){


instead of passing the first argument by value, it should be better to pass by constant reference

anyway, using a vector here does not look like a good choice

This function no longer exists .. (Tested the algorithm a bit after removing it ... it made the code like 3x faster)

ondrik · 2024-08-26T18:43:52Z

src/nfa/operations.cc

+        Nfa result_nfa;
+        Nfa reverted_nfa;
+
+        std::vector<std::pair<State, State>> result_sim {}; // R


instead of std::vector, some other data structure with faster lookup would be better (sparse bitmap/std::set/std::unordered_set, ...)

ondrik · 2024-08-26T18:47:10Z

src/nfa/operations.cc

+        size_t ***matrix;
+
+        // Matrix allocation
+        matrix = static_cast<size_t ***>(malloc(sizeof(size_t **) * alph_syms.size()));


no malloc/free in C++, better use new/delete

anyway, the best is to completely avoid dynamic allocation and just use a std::vector

also, no need to do nested arrays, just use one-dimensional and write index functions to access the right cell

size_t probably an overkill, a 32b counter should be enough

Using one dimensional array now.

ondrik · 2024-08-26T18:49:51Z

src/nfa/operations.cc

+        // ! Propagate until fixpoint
+        size_t worklist_size;
+        std::pair<State, State> working_pair;
+        while ((worklist_size = worklist.size()) != 0) {


maybe just use worklist.size()? compiler should be able to optimize the two calls...

Testing for (non-)emptiness should be done using worklist.empty(), optionally with ! in front of the expression for non-emptiness. And we can then use size() inside the loop body.

Adda0

Great work. I added some initial thoughts about the code quality and possible optimizations. A more thorough review will follow later on when the PR is more mature.

When the algorithm is finished, tests for the added function(s) should be added, too.

Adda0 · 2024-08-27T11:16:07Z

src/nfa/operations.cc

+    }
+
+    Nfa reduce_testing(const Nfa& aut){
+        // ! Preprocessing


Is the format // ! supposed to mean something specific? Like a critical section or something? I use this notation to highlight something important. Like a note of warning etc. This does not look like this case, however.

The pseudo code for this algorithm is "split" into sections with these descriptions. I tried make clear which parts of the real code represent which parts of the pseudo code.

Sounds good. Great idea. And it makes reading the code much easier. I would however use a more readable notation. Something like // Pseudocode: Preprocessing. or similar. Otherwise, everyone will be unsure of what the // ! should represent.

Adda0 · 2024-08-27T11:27:11Z

src/nfa/operations.cc

+        std::vector<std::pair<State, State>> worklist {}; // Worklist
+
+        // Alphabet extraction
+        mata::OnTheFlyAlphabet alph;


Since you are extracting the alphabet from the automaton, you could also add the alphabet as an optional parameter (probably const Alphabet* alphabet = nullptr) to the reduction function and fill the alphabet manually here only when the optional parameter is left empty.

Adda0 · 2024-08-27T11:28:51Z

src/nfa/operations.cc

+        aut.fill_alphabet(alph);
+        std::vector<Symbol> alph_syms = alph.get_alphabet_symbols().to_vector();
+
+        size_t no_states = aut.num_of_states();


When you define variables which will not change in the future, use const to help the optimizer optimize the code further.

PS: We usually use num_<something>, <something>_num etc. for variable containing a number of something in Mata.

Adda0 · 2024-08-27T11:30:37Z

src/nfa/operations.cc

+        std::vector<Symbol> alph_syms = alph.get_alphabet_symbols().to_vector();
+
+        size_t no_states = aut.num_of_states();
+        size_t ***matrix;


At least a comment would be needed here describing what the variables holds, but as @ondrik said, we should avoid dynamic allocation entirely, or if it is completely necessary, use C++ smart pointers such as std::shared_ptr or std::unique_ptr.

Resolved this

Adda0 · 2024-08-27T11:31:35Z

src/nfa/operations.cc

+        return false;
+    }
+
+    Nfa reduce_testing(const Nfa& aut){


The name should be descriptive. Something like reduce_by_<name_of_the_algorithm> or similar.

Done. The new name is a modified copy of an already existing function that computes the simulation relation (just in a different way)

Adda0 · 2024-08-28T05:04:32Z

src/nfa/operations.cc

@@ -56,6 +56,126 @@ namespace {
        return lts_for_simulation.compute_simulation();
    }

+    bool vec_contains(std::vector<std::pair<State, State>> vec, std::pair<State, State> par){


Furthermore, one should not create a custom function to search a container, unless they want to use some special non-standard search algorithm, but instead use std::find, or <container_instance>.find() != <container_instance.end()> or <container_instance>.contains() etc.

This function no longer exists

Adda0 · 2024-08-28T05:16:29Z

src/nfa/operations.cc

+                        }
+                        for (State p: (*symbol_p_).targets.to_vector()) {
+                            if (!vec_contains(result_sim, std::pair(p,q))) {
+                                result_sim.push_back(std::pair(p,q)); // R append 


Instead of push_back(std::pair(...)), one can use emplace_back(...) to construct the pair in-place at the location in the vector.

Adda0 · 2024-08-28T05:17:00Z

src/nfa/operations.cc

+        //Printig of the final relation:
+        std::cout << "The final relation is:" << std::endl;
+        for (std::pair final: result_sim){
+            std::cout << final.first << " , " << final.second << std::endl;


Do not forget to remove the debug prints later on.

ondrik · 2024-09-04T18:38:21Z

what's the issue with the automata in 4ff753a ?

samo538 · 2024-09-05T09:48:22Z

what's the issue with the automata in 4ff753a ?

Functions load_automata() and load_automaton() used in benchmarking codes could not parse these automata because they used keywords 'true' and 'false'. I consulted this with @Adda0 and changed all occurences of 'true' to '/true' which the functions can parse (and did the same with 'false'). However, i dont know why github shows huges changes in some files (which at the first glance dont change anything, like in tests-integration/automata/b-armc-incl-easiest/aut2.mata).

Adda0 · 2024-10-31T06:18:37Z

@samo538 Could you move the fix for the true and false values in .mata format to a separate PR? We could iterate quickly on this and merge the changes. And resolve why seemingly unrelated lines in the files were changed. Maybe trimming trailing newlines?

ondrik reviewed Aug 26, 2024

View reviewed changes

ondrik self-assigned this Aug 26, 2024

Adda0 reviewed Aug 28, 2024

View reviewed changes

samo538 force-pushed the simulation branch 5 times, most recently from 5e66ce5 to 4ff753a Compare September 4, 2024 17:52

samo538 force-pushed the simulation branch 7 times, most recently from 544c62d to eb4cf7f Compare September 11, 2024 15:24

samo538 added 3 commits September 11, 2024 17:57

Reduce: Simulation algorithm

c3d9118

Reduce: Benchmarking

aa3ccd6

Fix: benchmarking automata

07df042

samo538 force-pushed the simulation branch from eb4cf7f to 07df042 Compare September 11, 2024 18:36

1. Update: Matrix removal

7599acf

samo538 force-pushed the simulation branch 2 times, most recently from a3e561f to 7d41d03 Compare October 25, 2024 13:31

reduced number of binary searches

550c81d

samo538 force-pushed the simulation branch from 7d41d03 to 550c81d Compare October 25, 2024 14:47

samo538 force-pushed the simulation branch 2 times, most recently from 8dc0d17 to 6302fe7 Compare November 26, 2024 18:56

Deleted hash map

178a790

samo538 force-pushed the simulation branch from 6302fe7 to 178a790 Compare November 26, 2024 19:24

reduced binary searches

d232b58

samo538 force-pushed the simulation branch from b97255d to 30c0db7 Compare December 20, 2024 16:37

faster vector, better loops

1bbd7ea

samo538 force-pushed the simulation branch from 30c0db7 to 1bbd7ea Compare December 20, 2024 21:43

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Reduce: Simulation algorithm #434

Reduce: Simulation algorithm #434

samo538 commented Aug 26, 2024 •

edited

Loading

ondrik left a comment

ondrik Aug 26, 2024

samo538 Oct 7, 2024

ondrik Aug 26, 2024

ondrik Aug 26, 2024

samo538 Oct 7, 2024

ondrik Aug 26, 2024

Adda0 Aug 28, 2024

Adda0 left a comment •

edited

Loading

Adda0 Aug 27, 2024

samo538 Aug 28, 2024 •

edited

Loading

Adda0 Aug 29, 2024 •

edited

Loading

Adda0 Aug 27, 2024

Adda0 Aug 27, 2024

Adda0 Aug 27, 2024

samo538 Oct 7, 2024

Adda0 Aug 27, 2024

samo538 Sep 10, 2024

Adda0 Aug 28, 2024

samo538 Oct 7, 2024

Adda0 Aug 28, 2024

Adda0 Aug 28, 2024

ondrik commented Sep 4, 2024

samo538 commented Sep 5, 2024

Adda0 commented Oct 31, 2024

Reduce: Simulation algorithm #434

Are you sure you want to change the base?

Reduce: Simulation algorithm #434

Conversation

samo538 commented Aug 26, 2024 • edited Loading

ondrik left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Adda0 left a comment • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

samo538 Aug 28, 2024 • edited Loading

Choose a reason for hiding this comment

Adda0 Aug 29, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ondrik commented Sep 4, 2024

samo538 commented Sep 5, 2024

Adda0 commented Oct 31, 2024

samo538 commented Aug 26, 2024 •

edited

Loading

Adda0 left a comment •

edited

Loading

samo538 Aug 28, 2024 •

edited

Loading

Adda0 Aug 29, 2024 •

edited

Loading