created algorithm for turning a splitting_tree into a separating_family.

created test method for checking validity of separating_family.
removed a bunch of old, unneeded code.

CMakeLists.txt

@@ -3,6 +3,6 @@ project(complete_ads)
 
 set(CMAKE_CXX_STANDARD 17)
 
-set(SOURCE_FILES main.cpp src/main_test.cpp reachability.cpp)
+set(SOURCE_FILES main.cpp src/main_test.cpp)
 add_subdirectory("lib")
 add_subdirectory("src")
\ No newline at end of file

lib/logging.hpp

-#pragma once
-
-#include <chrono>
-#include <iostream>
-
-struct timer{
-	using clock = std::chrono::high_resolution_clock;
-	using time = std::chrono::time_point<clock>;
-	using seconds = std::chrono::duration<double>;
-
-	std::string name;
-	time begin;
-	bool active = true;
-
-	timer(std::string n)
-	: name(n)
-	, begin(clock::now())
-	{
-		std::cerr << name << std::endl;
-	}
-
-	void stop(){
-		if(!active) return;
-		time end = clock::now();
-		std::cerr << "* " << from_duration(end - begin) << '\t' << name << std::endl;
-		active = false;
-	}
-
-	~timer(){
-		stop();
-	}
-
-	static double from_duration(seconds s){
-		return s.count();
-	}
-};
-
-// has same signature, but does not log :)
-struct silent_timer {
-	silent_timer(std::string){}
-	void stop();
-};

lib/partition.hpp

@@ -7,6 +7,8 @@
 #include <type_traits>
 #include <vector>
 
+//partitions the elements bounded by iterators b and e based on their output when given to function.
+//output_size is used as a bound for the size of internal buffers and should be bigger than the biggest possible result given by function.
 template <typename Iterator, typename Fun>
 std::list<std::list<typename Iterator::value_type>>
 partition_(Iterator b, Iterator e, Fun&& function, size_t output_size) {

lib/read_mealy.cpp

@@ -174,12 +174,6 @@ std::vector<std::vector<std::string>> create_reverse_map(const std::unordered_ma
 	return ret;
 }
 
-#if 0 // Note: input and output are equal types, so this would be a redecl
-std::vector<string> create_reverse_map(const std::map<string, output> & indices) {
-	return create_reverse_map_impl(indices);
-}
-#endif
-
 translation create_translation_for_mealy(const mealy & m) {
 	translation t;
 	t.max_input = m.input_size;

lib/read_mealy.hpp

@@ -52,18 +52,5 @@ std::vector<std::string> create_reverse_map(const std::unordered_map<std::string
 
 std::vector<std::vector<std::string>> create_reverse_map(const std::unordered_map<std::string, size_t> & indices,size_t size);
 
-//todo: check of dit nog gebruikt wordt
-/*
-reverse_translation translate_translation(translation t)
-{
-	reverse_translation return_value;
-	return_value.inputs = create_reverse_map(t.input_indices);
-	return_value.outputs = create_reverse_map(t.output_indices);
-	return_value.states = create_reverse_map(t.state_indices);
-	return return_value;
-}
-*/
-
-
 /// \brief defines trivial translation (the string represent integers directly)
 translation create_translation_for_mealy(mealy const & m);

lib/readable_splitting_tree.cpp

@@ -6,26 +6,7 @@
 #include "read_mealy.hpp"
 #include <algorithm>
 
-//todo: check if this is ever used.
-/*
-const std::vector<readable_splitting_tree> & readable_splitting_tree::get_children(state s) const {
-    if (children.size() < 1)
-        throw std::runtime_error("get_children called when there were no children");
-    else if (valid_map.size() < 1 || valid_map.count(s) < 1)
-        return children[0];
-    else
-        return children[valid_map.at(s)];
-}
 
-const std::vector<std::string> &readable_splitting_tree::get_seperator(state s) const {
-    if (children.size() < 1)
-        throw std::runtime_error("get_separator called when there were no seperators");
-    else if (valid_map.size() < 1 || valid_map.count(s) < 1)
-        return separators[0];
-    else
-        return separators[valid_map.at(s)];
-}
-*/
 
 
 readable_splitting_tree translate_splitting_tree(splitting_tree & tree, std::vector<std::string> & inputs, std::vector<std::string> & states) {
@@ -52,7 +33,7 @@ readable_splitting_tree translate_splitting_tree(splitting_tree & tree, std::vec
     return translated_tree;
 }
 
-void rst_to_stream(readable_splitting_tree & tree, std::ostream & output, int ident){
+std::ostream& rst_to_stream(readable_splitting_tree & tree, std::ostream & output, int ident){
     std::string indentations(ident,'\t');
     std::vector<std::vector<std::string>> reverse_valid_map;
     if(tree.children.size()>1)
@@ -72,9 +53,10 @@ void rst_to_stream(readable_splitting_tree & tree, std::ostream & output, int id
             rst_to_stream(child,output,ident+1);
         }
     }
+    return output;
 
 
 }
 
-void rst_to_stream(readable_splitting_tree & tree, std::ostream & output){rst_to_stream(tree,output,0);}
+std::ostream& rst_to_stream(readable_splitting_tree & tree, std::ostream & output){return rst_to_stream(tree,output,0);}
 

lib/readable_splitting_tree.hpp

@@ -7,6 +7,8 @@
 
 #include "splitting_tree.hpp"
 
+
+//a regular splitting tree, but with all the state and input indexes replaced by their actual string values.
 struct readable_splitting_tree {
     /// \brief constructor that presets the internal vectors to the correct sizes for filling with iterators.
     readable_splitting_tree(size_t state_amount, size_t depth_value)
@@ -20,17 +22,13 @@ struct readable_splitting_tree {
     std::vector<std::vector<std::string>> separators;
     std::unordered_map<std::string, size_t> valid_map;
     size_t depth = 0;
-    /* todo: check if this is ever used.
-    const std::vector<readable_splitting_tree> &get_children(state s) const;
 
-    const std::vector<std::string> &get_seperator(state s) const;
-     */
 };
 
+//uses the translations described in inputs and outputs to translate a splitting tree into a readable splitting tree.
 readable_splitting_tree translate_splitting_tree(splitting_tree & tree, std::vector<std::string> & inputs, std::vector<std::string> & states);
 
-void rst_to_stream(readable_splitting_tree & tree, std::ostream & output, int ident);
-
-void rst_to_stream(readable_splitting_tree & tree, std::ostream & output);
+//outputs a readable splitting tree into an ostream. used for turning it into a string or saving it to a file.
+std::ostream& rst_to_stream(readable_splitting_tree & tree, std::ostream & output);
 
 #endif //COMPLETE_ADS_READABLE_SPLITTING_TREE_HPP

lib/separating_family.cpp

+//
+// Created by gijs on 27-10-2018.
+//
+
+#include "separating_family.hpp"
+#include "vector_printing.hpp"
+#include <unordered_map>
+#include <list>
+#include <algorithm>
+#include <cassert>
+
+
+std::ostream &separating_set_to_stream(std::ostream &s, const separating_set &set, const size_t indent_amount,
+                                       const std::vector<std::string> &inputs)
+{
+    const std::string indents(indent_amount, '\t');
+    for (word w : set)
+    {
+        std::vector<std::string> translated_word(w.size());
+        transform(w.begin(), w.end(), translated_word.begin(), [&inputs](size_t symbol_index)
+        { return inputs[symbol_index]; });
+        s << indents << join(translated_word.begin(), translated_word.end(), ",", "\n");
+    }
+    return s;
+
+}
+
+std::ostream &
+separating_family_to_stream(std::ostream &s, const separating_family &family, const std::vector<std::string> &inputs,
+                            const std::vector<std::string> &states)
+{
+    for (state i = 0; i < family.size(); i++)
+    {
+        s << "separators for state: " << states[i] << "\n";
+        separating_set_to_stream(s, family[i], 1, inputs) << "\n";
+    }
+    return s;
+
+}
+
+
+void update_CI_mapping(std::unordered_map<state, std::vector<state>> &CI_mapping, const output target_output,
+                       const mealy &specification, const word &separator)
+{
+    auto it = CI_mapping.begin();
+    const word::const_iterator start = separator.begin();
+    const word::const_iterator end = separator.end();
+
+    //updating the CI list involves changing the keys of values, and merging certain values together under a single key.
+    //this is hard to do in-place, so we use this buffer map to hold the output and then switch it with the CI_mapping at the end.
+    std::unordered_map<state, std::vector<state>> ret;
+    //reserve for the maximum posible size to prevent rehashes.
+    ret.reserve(CI_mapping.size() - 1);
+
+    while (it != CI_mapping.end())
+    {
+        mealy::edge result = apply(specification, it->first, start, end);
+        if (result.out != target_output)
+        {
+            it = CI_mapping.erase(it);
+        } else
+        {
+            std::vector<state> &possible_existing_value = ret[result.to];
+            if (possible_existing_value.size() == 0)
+                ret[result.to] = it->second;
+            else if (possible_existing_value.size() > it->second.size())
+                possible_existing_value.insert(possible_existing_value.end(), it->second.begin(), it->second.end());
+            else
+            {
+                it->second.insert(it->second.end(), possible_existing_value.begin(), possible_existing_value.end());
+                ret[result.to] = move(it->second);
+            }
+            it++;
+
+        }
+    }
+    CI_mapping = move(ret);
+
+}
+
+separating_family create_separating_family(const splitting_tree &tree, const mealy &specification)
+{
+    separating_family ret;
+    for (state global_target = 0; global_target < specification.graph_size; global_target++)
+    {
+        state target = global_target;
+        separating_set sep_set(1);
+        std::unordered_map<state, std::vector<state>> CI_mapping;
+        CI_mapping.reserve(specification.graph_size);
+        for (state s = 0; s < specification.graph_size; s++)
+        {
+            CI_mapping[s] = {s};
+        }
+        while (CI_mapping.size() > 1)
+        {
+            std::vector<bool> states(tree.states.size(), false);
+            for (std::pair<state, std::vector<state>> &&C_I_pair : CI_mapping)
+            {
+                states[C_I_pair.first] = true;
+            }
+
+            const splitting_tree &oboom = lca(tree, [&states](state state) -> bool
+            {
+                return states[state];
+            }, target);
+
+            const word separator = oboom.get_separator(target);
+            sep_set.back().insert(sep_set.back().end(), separator.begin(), separator.end());
+            mealy::edge target_result = apply(specification, target, separator.begin(), separator.end());
+            target = target_result.to;
+            update_CI_mapping(CI_mapping, target_result.out, specification, separator);
+
+            if (CI_mapping.size() == 1 && CI_mapping.begin()->second.size() > 1)
+            {
+                //if we get here then the size of the current set is 1 but the size of the initial set is still bigger than 1.
+                //to solve this we perform a reset operation, and bring the current set back to be the initial set.
+                const std::vector<state> initial_set = move(CI_mapping.begin()->second);
+                CI_mapping.clear();
+                CI_mapping.reserve(initial_set.size());
+                for (state s : initial_set)
+                {
+                    CI_mapping[s] = {s};
+                }
+                sep_set.push_back(word(0));
+                target = global_target;
+
+            }
+        }
+        assert(CI_mapping.size() == 1);
+        assert(CI_mapping.begin()->second.size() == 1);
+        assert(CI_mapping.begin()->second[0] == global_target);
+        ret.push_back(move(sep_set));
+
+    }
+    return ret;
+}
+
+
+bool test_separating_family(const separating_family &family, const mealy &specification)
+{
+    assert(family.size() == specification.graph_size);
+    for (state s = 0; s < family.size(); s++)
+    {
+        state target = s;
+        std::list<std::pair<state,state>> CI_list(specification.graph_size);
+        auto CI_it = CI_list.begin();
+        for (state i = 0; i < family.size(); i++)
+        {
+            (*CI_it) = {i,i};
+            CI_it++;
+        }
+        for (const word &word : family[s])
+        {
+            for (const input symbol : word)
+            {
+                mealy::edge expected = apply(specification, target, symbol);
+                target = expected.to;
+                auto it = CI_list.begin();
+                while (it != CI_list.end())
+                {
+                    mealy::edge observed = apply(specification, (*it).first, symbol);
+                    if (observed.out != expected.out)
+                    {
+                        it = CI_list.erase(it);
+                    }
+                    else
+                    {
+                        (*it).first = observed.to;
+                        it++;
+                    }
+                }
+            }
+            if(CI_list.size()>1)
+            {
+                for(auto &CI_pair : CI_list)
+                {
+                    CI_pair.first = CI_pair.second;
+                }
+                target = s;
+            }
+        }
+        if(CI_list.size()>1)
+            return false;
+    }
+    return true;
+
+}
+
+

lib/separating_family.hpp

+//
+// Created by gijs on 27-10-2018.
+//
+
+
+#ifndef COMPLETE_ADS_SEPARATING_FAMILY_H
+#define COMPLETE_ADS_SEPARATING_FAMILY_H
+
+#include "types.hpp"
+#include "splitting_tree.hpp"
+#include <vector>
+
+//a set of separators that you can use to differentiate one specific state from all the other states.
+using separating_set = std::vector<word>;
+//a set of separating sets that you can use to differentiate every state from every other state.
+using separating_family = std::vector<separating_set>;
+
+//creates a separating family by creating a single separating set for every state in the specification.
+//the main focus of this separating family is checking if you are in a specific state while you already have some idea of where you are.
+//you can then use one specific separating set to confirm or disprove that idea, without needing the whole separating family.
+separating_family create_separating_family(const splitting_tree &tree, const mealy &specification);
+
+//outputs a separating family to an ostream.
+std::ostream &  separating_family_to_stream(std::ostream & s, const separating_family & family,const std::vector<std::string> & inputs, const std::vector<std::string> &states);
+
+//outputs a separating set to an ostream.
+std::ostream &  separating_set_to_stream(std::ostream & s, const separating_set & set,const size_t indent_amount, const std::vector<std::string> & inputs);
+
+//returns true if family truly behaves as a separating family.
+//so for every separating set in the family,
+//if you apply that set to its target and then apply it to a random state that is not its target, the outputs have to be different.
+bool test_separating_family(const separating_family& family, const mealy & specification);
+
+#endif //COMPLETE_ADS_SEPARATING_FAMILY_H

lib/splitting_tree.cpp

@@ -24,7 +24,7 @@ splitting_tree::splitting_tree(size_t N, size_t d) : states(N), depth(d)
 struct work_set
 {
 
-    work_set(splitting_tree &tree, unordered_set<state> &&valid, bool do_output_split) : work(tree), valid_states(valid)
+    work_set(splitting_tree &tree, unordered_set<state> &&valid, bool do_output_split) : work(tree), valid_states(forward<unordered_set<state>>(valid))
     {
         split_on_output = do_output_split;
     }
@@ -46,6 +46,7 @@ struct work_set
 //fills a unordered set to the point where it contains at least all the possible states up to amount.
 void fill_set(unordered_set<state> &set, size_t amount)
 {
+    set.reserve(amount-1);
     for (size_t i = 0; i < amount; ++i)
     {
         set.emplace(i);
@@ -421,7 +422,6 @@ splitting_tree create_splitting_tree(const mealy &g)
 
                 assert(new_blocks.size() > 1);
 
-                //todo: update new_valid_set to contain only those states that were also in valid set or in targets.
                 // a succesful split, save the required information for later.
                 splits.push_back({move(word),move(new_blocks),move(new_valid_set)});
                 if(updated_separator)

lib/splitting_tree.hpp

@@ -103,43 +103,5 @@ template <typename Fun> const splitting_tree & lca(const splitting_tree & root,
 	return *store;
 }
 
-/*todo:check of dit gebruikt wordt.
-/// \brief Find "all" lca's of elements on which \p f returns true.
-/// This can be used to collect all the separating sequences for the subset of states.
-template <typename Fun>
-std::vector<std::reference_wrapper<const splitting_tree>> multi_lca(const splitting_tree & root,
-                                                                    Fun && f) {
-	std::vector<std::reference_wrapper<const splitting_tree>> ret;
-	lca_impl(root, f, [&ret](splitting_tree const & node) { ret.emplace_back(node); });
-	return ret;
-}
-*/
-
-/// \brief Structure contains options to alter the splitting tree creation.
-/// \p check_validity checks whether the transition/output map is injective on the current set of
-/// nodes which is being split. Setting this false degenerates to generating pairwise separating
-/// sequences. \p assert_minimal_order is used to produce minimal (pairwise) separating sequences.
-/// \p cach_succesors is needed by the second step in the LY algorithm and \p randomized randomizes
-/// the loops over the alphabet.
-
-//todo: check hoeveel hiervan verwijdert kan worden
-struct options {
-	bool check_validity;
-	bool assert_minimal_order;
-	bool cache_succesors;
-	bool randomized;
-	bool fail_on_invalid;
-};
-
-const options lee_yannakakis_style = {true, false, true, false,true};
-const options complete_ads = {true,false,true,false,false};
-const options hopcroft_style = {false, false, false, false,false};
-const options min_hopcroft_style = {false, true, false, false,false};
-const options randomized_lee_yannakakis_style = {true, false, true, true,true};
-const options randomized_hopcroft_style = {false, false, false, true,false};
-const options randomized_min_hopcroft_style = {false, true, false, true,false};
-
-
 /// \brief Creates a splitting tree by partition refinement.
-/// \returns a splitting tree and other calculated structures.
 splitting_tree create_splitting_tree(mealy const & m);

src/main.cpp

-#include <logging.hpp>
-#include <mealy.hpp>
-#include <reachability.hpp>
-#include <read_mealy.hpp>
-#include <splitting_tree.hpp>
+#include "mealy.hpp"
+#include "reachability.hpp"
+#include "read_mealy.hpp"
+#include "splitting_tree.hpp"
 #include "readable_splitting_tree.hpp"
 #include "vector_printing.hpp"
+#include "separating_family.hpp"
 
 
 #include <algorithm>
@@ -17,6 +17,7 @@
 #include <string>
 #include <utility>
 #include <functional>
+#include <cassert>
 
 /*
  * The reason I use getopt, instead of some library (I've used
@@ -50,6 +51,7 @@ static const char USAGE[] =
 )";
 
 static const string output_directory = "../outputs/";
+static const string input_directory = "../examples/";
 
 
 struct main_options {
@@ -59,10 +61,10 @@ struct main_options {
 	unsigned long k_max = 1;      // 3 means 2 extra states. currently not supported
 	unsigned long seed = 0;       // 0 for unset/noise. currently not supported
 
-	//"../examples/coffe_machine.dot";
-	//"../examples/lee_yannakakis_difficult.dot";
-	//"../examples/lee_yannakakis_distinguishable.dot";
-	string input_filename = "../examples/coffe_machine.dot";
+	//"coffe_machine.dot";
+	//"lee_yannakakis_difficult.dot";
+	//"lee_yannakakis_distinguishable.dot";
+	string input_filename = input_directory+"lee_yannakakis_difficult.dot";
 	string output_filename = "";
 };
 
@@ -87,7 +89,7 @@ main_options parse_options(int argc, char ** argv) {
 				opts.seed = stoul(optarg);
 				break;
 			case 'f': // input filename
-				opts.input_filename = optarg;
+				opts.input_filename = input_directory + optarg;
 				break;
 			case 'o': // output filename
 				opts.output_filename = output_directory + optarg;
@@ -105,6 +107,7 @@ main_options parse_options(int argc, char ** argv) {
 		exit(2);
 	}
 
+	//generate outputfile name based on inputfile name.
 	if(opts.output_filename == "")
 	{
 		size_t start = opts.input_filename.find_last_of('/');
@@ -120,7 +123,6 @@ main_options parse_options(int argc, char ** argv) {
 	return opts;
 }
 
-using time_logger = silent_timer;
 
 int main(int argc, char * argv[]){
 	/*
@@ -147,7 +149,6 @@ int main(int argc, char * argv[]){
 	 */
 	const auto machine_and_translation = [&] {
 		const auto & filename = args.input_filename;
-		time_logger t_("reading file " + filename);
 		if (filename == "" || filename == "-") {
 			return read_mealy_from_dot(cin);
 		}
@@ -171,19 +172,28 @@ int main(int argc, char * argv[]){
     vector<string> input_translation = create_reverse_map(translation.input_indices);
     vector<string> state_translation = create_reverse_map(translation.state_indices);
 
+    /* only usefull for debugging
     ofstream translation_file(output_directory+"translations.txt");
     translation_file << "input translation\n";
     translation_file << input_translation;
     translation_file <<"\nstate translation\n";
     translation_file << state_translation;
     translation_file.close();
+    */
 
     readable_splitting_tree translated_tree = translate_splitting_tree(complete_splitting_tree,input_translation,state_translation);
+    separating_family family = create_separating_family(complete_splitting_tree,machine);
 
 
     ofstream out_file(args.output_filename);
-    rst_to_stream(translated_tree,out_file);
+    out_file<<"the splitting tree:\n\n";
+    rst_to_stream(translated_tree,out_file)<<"\n\n\n";
+    out_file<<"the separating family:\n\n";
+    separating_family_to_stream(out_file,family,input_translation,state_translation);
+
     out_file.close();
+    //making sure the results are actually correct.
+    assert(test_separating_family(family,machine));
 
 
     cout << "finished!\n";