mirror of
https://github.com/Jaxan/hybrid-ads.git
synced 2025-04-27 15:07:45 +02:00
Adds possibility to read stdin
This commit is contained in:
parent
1c9f56a6ec
commit
c4625bf775
6 changed files with 228 additions and 49 deletions
|
@ -20,6 +20,8 @@ mealy read_mealy_from_dot(istream& in){
|
|||
string line;
|
||||
stringstream ss;
|
||||
while(getline(in, line)){
|
||||
if(line.find("}") != string::npos) return m;
|
||||
|
||||
const auto i = line.find("->");
|
||||
if(i == string::npos) continue;
|
||||
|
||||
|
|
115
src/conf-hyp.cpp
Normal file
115
src/conf-hyp.cpp
Normal file
|
@ -0,0 +1,115 @@
|
|||
#include <mealy.hpp>
|
||||
#include <read_mealy_from_dot.hpp>
|
||||
|
||||
#include <io.hpp>
|
||||
|
||||
#include <fstream>
|
||||
#include <iostream>
|
||||
#include <string>
|
||||
|
||||
using namespace std;
|
||||
|
||||
template <typename T>
|
||||
vector<string> create_reverse_map(map<string, T> const & indices){
|
||||
vector<string> ret(indices.size());
|
||||
for(auto&& p : indices){
|
||||
ret[p.second.base()] = p.first;
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
|
||||
template <typename T>
|
||||
vector<T> resize_new(vector<T> const & in, size_t N){
|
||||
vector<T> ret(N);
|
||||
copy_n(in.begin(), N, ret.begin());
|
||||
return ret;
|
||||
}
|
||||
|
||||
vector<string> conform(mealy const & spec, vector<string> const & spec_o_map, mealy const & impl, vector<string> const & impl_o_map, vector<vector<string>> const & suite){
|
||||
for(auto && test : suite){
|
||||
state s = 0;
|
||||
state t = 0;
|
||||
|
||||
size_t count = 0;
|
||||
for(auto && i : test){
|
||||
const auto i1 = spec.input_indices.at(i);
|
||||
const auto r1 = apply(spec, s, i1);
|
||||
const auto o1 = spec_o_map[r1.output.base()];
|
||||
s = r1.to;
|
||||
|
||||
const auto i2 = spec.input_indices.at(i);
|
||||
const auto r2 = apply(impl, t, i2);
|
||||
const auto o2 = impl_o_map[r2.output.base()];
|
||||
t = r2.to;
|
||||
|
||||
if(o1 != o2){
|
||||
return resize_new(test, count+1);
|
||||
}
|
||||
count++;
|
||||
}
|
||||
}
|
||||
|
||||
return {};
|
||||
}
|
||||
|
||||
vector<vector<string>> open_suite(string suite_filename){
|
||||
boost::iostreams::filtering_istream suite_file;
|
||||
suite_file.push(boost::iostreams::gzip_decompressor());
|
||||
suite_file.push(boost::iostreams::file_descriptor_source(suite_filename));
|
||||
boost::archive::text_iarchive archive(suite_file);
|
||||
|
||||
vector<vector<string>> suite;
|
||||
archive >> suite;
|
||||
return suite;
|
||||
}
|
||||
|
||||
int main(int argc, char *argv[]){
|
||||
const size_t N = 136;
|
||||
vector< pair<mealy, vector<string>> > machines_and_maps(N);
|
||||
vector< vector<vector<string>> > suites(N);
|
||||
for(int i = 0; i < N; ++i){
|
||||
cout << "reading " << i << "\r" << flush;
|
||||
|
||||
const string filename = "hyp." + to_string(i) + ".obf.dot";
|
||||
machines_and_maps[i].first = read_mealy_from_dot(filename);
|
||||
machines_and_maps[i].second = create_reverse_map(machines_and_maps[i].first.output_indices);
|
||||
|
||||
const string suite_filename = filename + "test_suite";
|
||||
suites[i] = open_suite(suite_filename);
|
||||
}
|
||||
cout << "done reading" << endl;
|
||||
|
||||
const string red = "\x1b[31m";
|
||||
const string yellow = "\x1b[33m";
|
||||
const string cyan = "\x1B[36m";
|
||||
const string reset = "\033[0m";
|
||||
|
||||
size_t fails = 0;
|
||||
for(int i = 0; i < N; ++i){
|
||||
for(int j = 0; j < N; ++j){
|
||||
cout << "checking " << i << " against " << j << "\r" << flush;
|
||||
const auto & spec = machines_and_maps[i];
|
||||
const auto & impl = machines_and_maps[j];
|
||||
const auto & suite = suites[i];
|
||||
const auto result = conform(spec.first, spec.second, impl.first, impl.second, suite);
|
||||
|
||||
if(i == j && !result.empty()){
|
||||
cout << cyan << "FAIL: " << i << " " << j << " is the same machine" << reset << endl;
|
||||
fails++;
|
||||
}
|
||||
|
||||
if(i < j && result.empty()){
|
||||
cout << red << "FAIL: " << i << " " << j << " no flaw detected" << reset << endl;
|
||||
fails++;
|
||||
}
|
||||
|
||||
if(i > j && result.empty()){
|
||||
cout << yellow << "FAIL: " << i << " " << j << " no flaw detected" << reset << endl;
|
||||
fails++;
|
||||
}
|
||||
}
|
||||
}
|
||||
cout << "done checking" << endl;
|
||||
cout << "total of " << fails << " fails out of " << N*N << endl;
|
||||
}
|
||||
|
72
src/conf.cpp
72
src/conf.cpp
|
@ -18,31 +18,14 @@ vector<string> create_reverse_map(map<string, T> const & indices){
|
|||
return ret;
|
||||
}
|
||||
|
||||
int main(int argc, char *argv[]){
|
||||
if(argc != 4) return 37;
|
||||
template <typename T>
|
||||
vector<T> resize_new(vector<T> const & in, size_t N){
|
||||
vector<T> ret(N);
|
||||
copy_n(in.begin(), N, ret.begin());
|
||||
return ret;
|
||||
}
|
||||
|
||||
const string spec_filename = argv[1];
|
||||
const string impl_filename = argv[2];
|
||||
const string suite_filename = argv[3];
|
||||
|
||||
ifstream spec_file(spec_filename);
|
||||
ifstream impl_file(impl_filename);
|
||||
|
||||
boost::iostreams::filtering_istream suite_file;
|
||||
suite_file.push(boost::iostreams::gzip_decompressor());
|
||||
suite_file.push(boost::iostreams::file_descriptor_source(suite_filename));
|
||||
boost::archive::text_iarchive archive(suite_file);
|
||||
|
||||
const auto spec = read_mealy_from_dot(spec_file);
|
||||
const auto impl = read_mealy_from_dot(impl_file);
|
||||
|
||||
const auto spec_o_map = create_reverse_map(spec.output_indices);
|
||||
const auto impl_o_map = create_reverse_map(impl.output_indices);
|
||||
|
||||
vector<vector<string>> suite;
|
||||
archive >> suite;
|
||||
|
||||
size_t tcount = 0;
|
||||
vector<string> conform(mealy const & spec, vector<string> const & spec_o_map, mealy const & impl, vector<string> const & impl_o_map, vector<vector<string>> const & suite){
|
||||
for(auto && test : suite){
|
||||
state s = 0;
|
||||
state t = 0;
|
||||
|
@ -56,21 +39,46 @@ int main(int argc, char *argv[]){
|
|||
|
||||
const auto i2 = spec.input_indices.at(i);
|
||||
const auto r2 = apply(impl, t, i2);
|
||||
const auto o2 = spec_o_map[r2.output.base()];
|
||||
const auto o2 = impl_o_map[r2.output.base()];
|
||||
t = r2.to;
|
||||
|
||||
if(o1 != o2){
|
||||
cout << "conformance fail" << endl;
|
||||
cout << o1 << " != " << o2 << endl;
|
||||
cout << "at test " << tcount << endl;
|
||||
cout << "at char " << count << endl;
|
||||
return 1;
|
||||
return resize_new(test, count+1);
|
||||
}
|
||||
count++;
|
||||
}
|
||||
tcount++;
|
||||
}
|
||||
|
||||
cout << "conformance succes " << tcount << endl;
|
||||
return {};
|
||||
}
|
||||
|
||||
vector<vector<string>> open_suite(string suite_filename){
|
||||
boost::iostreams::filtering_istream suite_file;
|
||||
suite_file.push(boost::iostreams::gzip_decompressor());
|
||||
suite_file.push(boost::iostreams::file_descriptor_source(suite_filename));
|
||||
boost::archive::text_iarchive archive(suite_file);
|
||||
|
||||
vector<vector<string>> suite;
|
||||
archive >> suite;
|
||||
return suite;
|
||||
}
|
||||
|
||||
int main(int argc, char *argv[]){
|
||||
if(argc != 3) return 1;
|
||||
|
||||
const auto spec = read_mealy_from_dot(argv[1]);
|
||||
const auto spec_o_map = create_reverse_map(spec.output_indices);
|
||||
|
||||
const auto impl = read_mealy_from_dot(argv[2]);
|
||||
const auto impl_o_map = create_reverse_map(impl.output_indices);
|
||||
|
||||
const auto suite = open_suite(argv[1] + string("test_suite"));
|
||||
|
||||
const auto counter_example = conform(spec, spec_o_map, impl, impl_o_map, suite);
|
||||
if(counter_example.empty()){
|
||||
cerr << "No counter example found" << endl;
|
||||
}
|
||||
for(auto && i : counter_example) cout << i << ' ';
|
||||
cout << endl;
|
||||
}
|
||||
|
||||
|
|
21
src/main.cpp
21
src/main.cpp
|
@ -47,10 +47,15 @@ std::vector<std::vector<T>> all_seqs(T min, T max, std::vector<std::vector<T>> c
|
|||
int main(int argc, char *argv[]){
|
||||
if(argc != 2) return 1;
|
||||
const string filename = argv[1];
|
||||
const bool use_stdio = filename == "--";
|
||||
|
||||
const auto machine = [&]{
|
||||
timer t("reading file " + filename);
|
||||
return read_mealy_from_dot(filename);
|
||||
if(use_stdio){
|
||||
return read_mealy_from_dot(cin);
|
||||
} else {
|
||||
return read_mealy_from_dot(filename);
|
||||
}
|
||||
}();
|
||||
|
||||
auto all_pair_seperating_sequences_fut = async([&]{
|
||||
|
@ -96,7 +101,6 @@ int main(int argc, char *argv[]){
|
|||
|
||||
const auto transfer_sequences = transfer_sequences_fut.get();
|
||||
const auto inputs = create_reverse_map(machine.input_indices);
|
||||
const auto outputs = create_reverse_map(machine.output_indices);
|
||||
|
||||
{
|
||||
timer t("making test suite");
|
||||
|
@ -119,16 +123,13 @@ int main(int argc, char *argv[]){
|
|||
return seq2;
|
||||
});
|
||||
|
||||
// for(auto && test : real_suite) {
|
||||
// for(auto && s : test) {
|
||||
// cout << s << " ";
|
||||
// }
|
||||
// cout << endl;
|
||||
// }
|
||||
|
||||
boost::iostreams::filtering_ostream compressed_stream;
|
||||
compressed_stream.push(boost::iostreams::gzip_compressor());
|
||||
compressed_stream.push(boost::iostreams::file_descriptor_sink("test_suite"));
|
||||
if(use_stdio){
|
||||
compressed_stream.push(cout);
|
||||
} else {
|
||||
compressed_stream.push(boost::iostreams::file_descriptor_sink(filename + "test_suite"));
|
||||
}
|
||||
|
||||
boost::archive::text_oarchive archive(compressed_stream);
|
||||
archive << real_suite;
|
||||
|
|
|
@ -1,17 +1,16 @@
|
|||
#include <read_mealy_from_dot.hpp>
|
||||
#include <io.hpp>
|
||||
#include <mealy.hpp>
|
||||
#include <read_mealy_from_dot.hpp>
|
||||
|
||||
#include <algorithm>
|
||||
#include <fstream>
|
||||
#include <iostream>
|
||||
#include <numeric>
|
||||
|
||||
using namespace std;
|
||||
|
||||
int main(int argc, char *argv[]){
|
||||
if(argc != 2) return 37;
|
||||
|
||||
const auto filename = argv[1];
|
||||
ifstream file(filename);
|
||||
const auto machine = read_mealy_from_dot(file);
|
||||
void print_stats_for_machine(string filename){
|
||||
const auto machine = read_mealy_from_dot(filename);
|
||||
|
||||
cout << "machine " << filename << " has\n";
|
||||
cout << '\t' << machine.graph_size << " states\n";
|
||||
|
@ -19,3 +18,33 @@ int main(int argc, char *argv[]){
|
|||
cout << '\t' << machine.output_size << " outputs\n";
|
||||
}
|
||||
|
||||
void print_stats_for_suite(string filename){
|
||||
boost::iostreams::filtering_istream suite_file;
|
||||
suite_file.push(boost::iostreams::gzip_decompressor());
|
||||
suite_file.push(boost::iostreams::file_descriptor_source(filename));
|
||||
boost::archive::text_iarchive archive(suite_file);
|
||||
|
||||
vector<vector<string>> suite;
|
||||
archive >> suite;
|
||||
|
||||
const auto & longest = *max_element(suite.begin(), suite.end(), [](const auto & x, const auto & y){ return x.size() < y.size(); });
|
||||
const auto total_length = accumulate(suite.begin(), suite.end(), 0, [](const auto & x, const auto & y){ return x + y.size(); });
|
||||
|
||||
cout << "suite " << filename << " has\n";
|
||||
cout << '\t' << suite.size() << " sequences\n";
|
||||
cout << '\t' << total_length << " input symbols in total\n";
|
||||
cout << '\t' << double(total_length) / suite.size() << " input symbols on average per test\n";
|
||||
cout << '\t' << longest.size() << " inputs symbols in the longest test\n";
|
||||
}
|
||||
|
||||
int main(int argc, char *argv[]){
|
||||
if(argc != 2) return 37;
|
||||
|
||||
const string filename = argv[1];
|
||||
if(filename.find("test_suite") == string::npos){
|
||||
print_stats_for_machine(filename);
|
||||
} else {
|
||||
print_stats_for_suite(filename);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
24
src/table.cpp
Normal file
24
src/table.cpp
Normal file
|
@ -0,0 +1,24 @@
|
|||
#include <iostream>
|
||||
#include <sstream>
|
||||
#include <vector>
|
||||
|
||||
using namespace std;
|
||||
|
||||
int main(int argc, char *argv[]){
|
||||
stringstream input("1 2 1 3 1 4 1 5 1 6 1 7 1 8 1 9 2 3 2 4 2 5 2 6 2 7 2 8 2 9 3 4 3 5 3 6 3 7 3 8 3 9 4 5 4 6 4 7 4 8 4 9 5 6 5 7 5 8 5 9 6 7 6 8 6 9 7 8 7 9 8 9 10 11 11 12 11 13 11 14 11 15 11 16 11 17 11 18 11 19 11 20 11 21 11 22 11 23 11 24 11 25 12 13 12 14 12 15 12 16 12 17 12 18 12 19 12 20 12 21 12 22 12 23 12 24 12 25 13 14 13 15 13 16 13 17 13 18 13 19 13 20 13 21 13 22 13 23 13 24 13 25 14 15 14 16 14 17 14 18 14 19 14 20 14 21 14 22 14 23 14 24 14 25 15 16 15 17 15 18 15 19 15 20 15 21 15 22 15 23 15 24 15 25 16 17 16 18 16 19 16 20 16 21 16 22 16 23 16 24 16 25 17 18 17 19 17 20 17 21 17 22 17 23 17 24 17 25 18 19 18 20 18 21 18 22 18 23 18 24 18 25 19 20 19 21 19 22 19 23 19 24 19 25 20 21 20 22 20 23 20 24 20 25 21 22 21 23 21 24 21 25 22 23 22 24 22 25 23 24 23 25 24 25 27 28 27 29 27 30 27 31 27 32 27 33 27 34 27 35 27 36 27 37 27 38 28 29 28 30 28 31 28 32 28 33 28 34 28 35 28 36 28 37 28 38 29 30 29 31 29 32 29 33 29 34 29 35 29 36 29 37 29 38 30 31 30 32 30 33 30 34 30 35 30 36 30 37 30 38 31 32 31 33 31 34 31 35 31 36 31 37 31 38 32 33 32 34 32 35 32 36 32 37 32 38 33 34 33 35 33 36 33 37 33 38 34 35 34 36 34 37 34 38 35 36 35 37 35 38 36 37 36 38 37 38 39 40 39 41 39 42 39 43 39 44 39 45 39 46 39 47 39 48 40 41 40 42 40 43 40 44 40 45 40 46 40 47 40 48 41 42 41 43 41 44 41 45 41 46 41 47 41 48 42 43 45 46 45 47 45 48 46 47 46 48 47 48 49 50 51 52 51 53 51 54 51 55 51 56 51 57 51 58 51 59 51 60 51 61 51 62 51 63 51 64 51 65 51 66 51 67 53 54 53 55 53 56 53 57 53 58 53 59 53 60 53 61 53 62 53 63 53 64 53 65 53 66 53 67 54 55 54 56 54 57 54 58 54 59 54 60 54 61 54 62 54 63 54 64 54 65 54 66 54 67 55 56 55 57 55 58 55 59 55 60 55 61 55 62 55 63 55 64 55 65 55 66 55 67 56 57 56 58 56 59 56 60 56 61 56 62 56 63 56 64 56 65 56 66 56 67 57 58 57 59 57 60 57 61 57 62 57 63 57 64 57 65 57 66 57 67 58 59 58 60 58 61 58 62 58 63 58 64 58 65 58 66 58 67 59 60 59 61 59 62 59 63 59 64 59 65 59 66 59 67 62 63 62 64 62 65 62 66 62 67 63 64 63 65 63 66 64 65 64 66 64 67 65 66 65 67 66 67 68 69 68 70 68 71 68 72 68 73 68 74 68 75 68 76 68 77 68 78 68 79 68 80 68 81 68 82 68 83 68 84 68 85 68 86 68 87 68 88 68 89 68 90 68 91 68 92 68 93 69 70 69 71 69 72 69 73 69 74 69 75 69 76 69 77 69 78 69 79 69 80 69 81 69 82 69 83 69 84 69 85 69 86 69 87 69 88 69 89 69 90 69 91 69 92 69 93 70 71 70 72 70 73 70 74 70 75 70 76 70 77 70 78 70 79 70 80 70 81 70 82 70 83 70 84 70 85 70 86 70 87 70 88 70 89 70 90 70 91 70 92 70 93 71 72 71 73 71 74 71 75 71 76 71 77 71 78 71 79 71 80 71 81 71 82 71 83 71 84 71 85 71 86 71 87 71 88 71 89 71 90 71 91 71 92 71 93 72 73 72 74 72 75 72 76 72 77 72 78 72 79 72 80 72 81 72 82 72 83 72 84 72 85 72 86 72 87 72 88 72 89 72 90 72 91 72 92 72 93 73 74 73 75 73 76 73 77 73 78 73 79 73 80 73 81 73 82 73 83 73 84 73 85 73 86 73 87 73 88 73 89 73 90 73 91 73 92 73 93 74 75 74 76 74 77 74 78 74 79 74 80 74 81 74 82 74 83 74 84 74 85 74 86 74 87 74 88 74 89 74 90 74 91 74 92 74 93 75 76 75 77 75 78 75 79 75 80 75 81 75 82 75 83 75 84 75 85 75 86 75 87 75 88 75 89 75 90 75 91 75 92 75 93 76 77 76 78 76 79 76 80 76 81 76 82 76 83 76 84 76 85 76 86 76 87 76 88 76 89 76 90 76 91 76 92 76 93 77 78 77 79 78 79 80 81 80 82 80 83 80 84 80 85 80 86 80 87 80 88 80 89 80 90 80 91 80 92 80 93 81 82 81 83 81 84 81 85 81 86 81 87 81 88 81 89 81 90 81 91 81 92 81 93 82 83 82 84 82 85 82 86 82 87 82 88 82 89 82 90 82 91 82 92 82 93 84 85 84 86 84 87 84 88 84 89 84 90 84 91 84 92 84 93 87 88 87 89 87 90 87 91 87 92 87 93 88 89 88 90 88 91 88 92 88 93 89 90 89 91 89 92 89 93 90 91 90 92 90 93 91 92 91 93 92 93 94 95 94 96 95 96 97 98 97 99 97 100 97 101 97 102 97 103 97 104 97 105 97 106 97 107 97 108 97 109 97 110 97 111 97 112 97 113 97 114 97 115 100 101 100 102 100 103 101 102 101 103 102 103 104 105 104 106 104 107 104 108 104 109 104 110 104 111 104 112 104 113 104 114 104 115 105 106 105 107 105 108 105 109 105 110 105 111 105 112 105 113 105 114 105 115 106 107 106 108 106 109 106 110 106 111 106 112 106 113 106 114 106 115 107 108 107 109 107 110 107 111 107 112 107 113 107 114 107 115 108 109 108 110 108 111 108 112 108 113 108 114 108 115 109 110 109 111 109 112 109 113 109 114 109 115 110 111 110 112 110 113 110 114 110 115 111 112 111 113 111 114 111 115 112 113 112 114 112 115 113 114 113 115 114 115 116 117 116 118 116 119 116 120 117 118 117 119 117 120 118 119 118 120 119 120 122 123 122 124 126 130 127 128 127 129 128 129 132 133 132 134 132 135");
|
||||
|
||||
vector<vector<bool>> table(136, vector<bool>(136, false));
|
||||
int x, y;
|
||||
while(input >> x >> y){
|
||||
table[x][y] = true;
|
||||
}
|
||||
|
||||
for(int r = 0; r < 136; ++r){
|
||||
for(int c = 0; c < 136; ++c){
|
||||
if(c == r) cout << '=';
|
||||
else if(table[r][c]) cout << 'X';
|
||||
else cout << ' ';
|
||||
}
|
||||
cout << endl;
|
||||
}
|
||||
}
|
Loading…
Add table
Reference in a new issue