From dd9874219a87d545f4e9c6b36b5271d46b3cc6c4 Mon Sep 17 00:00:00 2001 From: Shufang-Zhu Date: Mon, 22 Jan 2024 20:45:55 +0100 Subject: [PATCH 1/6] added LTLf GR1 --- example/tcp_handshake_agn_goal.tlsf | 23 ++ example/tcp_handshake_agn_safety.ltlf | 1 + example/tcp_handshake_env_gr1.txt | 7 + example/tcp_handshake_env_safety.ltlf | 1 + src/synthesis/header/GR1.h | 134 ++++++++ .../header/GR1ReachabilitySynthesizer.h | 113 +++++++ src/synthesis/header/SymbolicStateDfa.h | 2 + src/synthesis/header/VarMgr.h | 8 + .../source/GR1ReachabilitySynthesizer.cpp | 288 ++++++++++++++++++ src/synthesis/source/SymbolicStateDfa.cpp | 12 + src/synthesis/source/VarMgr.cpp | 61 +++- src/utils/string_utilities.cpp | 15 + src/utils/string_utilities.h | 3 +- test/test_gr1reachability_synthesis.cpp | 111 +++++++ test/utils.hpp | 5 + 15 files changed, 775 insertions(+), 9 deletions(-) create mode 100644 example/tcp_handshake_agn_goal.tlsf create mode 100644 example/tcp_handshake_agn_safety.ltlf create mode 100644 example/tcp_handshake_env_gr1.txt create mode 100644 example/tcp_handshake_env_safety.ltlf create mode 100644 src/synthesis/header/GR1.h create mode 100644 src/synthesis/header/GR1ReachabilitySynthesizer.h create mode 100644 src/synthesis/source/GR1ReachabilitySynthesizer.cpp create mode 100644 test/test_gr1reachability_synthesis.cpp diff --git a/example/tcp_handshake_agn_goal.tlsf b/example/tcp_handshake_agn_goal.tlsf new file mode 100644 index 0000000..3971156 --- /dev/null +++ b/example/tcp_handshake_agn_goal.tlsf @@ -0,0 +1,23 @@ +INFO { + TITLE: "LTLf-test" + DESCRIPTION: "LTLf-test example" + SEMANTICS: Finite,Moore + TARGET: Moore +} + +MAIN { + + INPUTS { + syn_ack; + } + + OUTPUTS { + syn; + ack; + } + + GUARANTEES { + F (ack); + } + +} diff --git a/example/tcp_handshake_agn_safety.ltlf b/example/tcp_handshake_agn_safety.ltlf new file mode 100644 index 0000000..d01a6ce --- /dev/null +++ b/example/tcp_handshake_agn_safety.ltlf @@ -0,0 +1 @@ +(G !(syn_ack) -> G !(ack)) diff --git a/example/tcp_handshake_env_gr1.txt b/example/tcp_handshake_env_gr1.txt new file mode 100644 index 0000000..52f4551 --- /dev/null +++ b/example/tcp_handshake_env_gr1.txt @@ -0,0 +1,7 @@ +--Env-Justice-- +syn +--Justice-End-- +--Agn-Justice-- +syn_ack +--Justice-End-- +End diff --git a/example/tcp_handshake_env_safety.ltlf b/example/tcp_handshake_env_safety.ltlf new file mode 100644 index 0000000..3dd8449 --- /dev/null +++ b/example/tcp_handshake_env_safety.ltlf @@ -0,0 +1 @@ +(G !(syn) -> G !(syn_ack)) diff --git a/src/synthesis/header/GR1.h b/src/synthesis/header/GR1.h new file mode 100644 index 0000000..27a43d7 --- /dev/null +++ b/src/synthesis/header/GR1.h @@ -0,0 +1,134 @@ +// +// Created by shuzhu on 21/01/24. +// + +#ifndef LYDIASYFT_GR1_H +#define LYDIASYFT_GR1_H + +#include +#include "string_utilities.h" + +namespace Syft { + /** + * GR(1) file format is similar to the regular CNF format, such that every justice + * is represented as a conjunction over disjunctive clauses. + * Each justice is labeled with `env` or `agn` to refer to environment or + * agent justice respectively, and ended with `end`. + * Consider GR(1) formula + * GF(p_1) & GF(p_1 & q_1) & ... & GF(!p_1 & (q_1 | q_2)) -> + * GF(q_1) & GF(p_1 & q_1) & ... & GF(!q_1 & (p_1 | p_2)), + * this formula is written as follows (variables in uppercase): + * --Env-Justice-- + * P_1 + * --Justice-End-- + * + * --Env-Justice-- + * P_1 + * Q_1 + * --Justice-End-- + * + * --Env-Justice-- + * !P_1 + * Q_1 Q_2 + * --Justice-End-- + * + * --Agn-Justice-- + * Q_1 + * --Justice-End-- + * + * --Agn-Justice-- + * P_1 + * Q_1 + * --Justice-End-- + * + * --Agn-Justice-- + * !Q_1 + * P_1 Q_1 + * --Justice-End-- + * End + */ + + struct GR1 { + std::vector env_justices; + std::vector agn_justices; + /** + * \brief Stores a player justice + */ + static CUDD::BDD read_gr1_justice(std::shared_ptr& var_mgr, + std::istream& in, + std::size_t& line_number){ + std::string line; + CUDD::BDD justice = var_mgr->cudd_mgr()->bddOne(); + + while (std::getline(in, line) && (line.find("Justice-End") == std::string::npos)) { + + CUDD::BDD clause = var_mgr->cudd_mgr()->bddZero(); + if (line == "true") { + clause = var_mgr->cudd_mgr()->bddOne(); + } + else if (line == "false") { + clause = var_mgr->cudd_mgr()->bddZero(); + } + else{ + std::vector tokens; + trim(line); // remove leading and trailing whitespace + tokens = split(line, " "); + std::vector variable_names; + + for (std::string token : tokens) { + std::string variable_name; + variable_name = (line.find("!") == std::string::npos)? token : token.substr(2, token.size()-3); +// variable_name = to_upper_copy(variable_name); // turn variable names into uppercase to match the variable names in InputOutputPartition + variable_names.push_back(variable_name); + var_mgr->create_named_variables(variable_names); + CUDD::BDD variable_bdd = var_mgr->name_to_variable(variable_name); + clause = (line.find("!") == std::string::npos)? (clause | variable_bdd) : (clause | !variable_bdd); + } + } + justice = justice & clause; + ++line_number; + } + return justice; + } + + static std::runtime_error bad_file_format_exception( + std::size_t line_number) { + return std::runtime_error("Incorrect format in line " + + std::to_string(line_number) + + " of the GR(1) file."); + } + /** + * \brief Stores a GR(1) condition. + * + * \param gr1_filename The name of the file to read the GR(1) condition from. + * \return The GR(1) condition stored in the file + */ + static GR1 read_from_gr1_file(std::shared_ptr& var_mgr, + const std::string& gr1_filename) { + GR1 gr1; + std::ifstream in(gr1_filename); + std::size_t line_number = 0; + std::string line; + while (std::getline(in, line) && line != "End") { + if (line.find("Justice") != std::string::npos){ + if (line.find("Env") == std::string::npos && line.find("Agn") == std::string::npos) { + throw bad_file_format_exception(line_number); + } + ++line_number; + CUDD::BDD justice = read_gr1_justice(var_mgr, in, line_number); + if (line.find("Env") != std::string::npos) { + gr1.env_justices.push_back(justice); + } else { + gr1.agn_justices.push_back(justice); + } + } + ++line_number; + } + return gr1; + } + }; + + +} + +#endif //LYDIASYFT_GR1_H diff --git a/src/synthesis/header/GR1ReachabilitySynthesizer.h b/src/synthesis/header/GR1ReachabilitySynthesizer.h new file mode 100644 index 0000000..01f5887 --- /dev/null +++ b/src/synthesis/header/GR1ReachabilitySynthesizer.h @@ -0,0 +1,113 @@ +// +// Created by shuzhu on 21/01/24. +// + +#ifndef LYDIASYFT_GR1REACHABILITYSYNTHESIZER_H +#define LYDIASYFT_GR1REACHABILITYSYNTHESIZER_H +#include "ExplicitStateDfa.h" +#include "InputOutputPartition.h" +#include "Player.h" +#include "GR1.h" +#include "Stopwatch.h" +#include "SymbolicStateDfa.h" +#include "Synthesizer.h" + + + +namespace Syft { + + class GR1ReachabilitySynthesizer{ + private: + std::shared_ptr var_mgr_; + GR1 gr1_; + SymbolicStateDfa env_safety_; + SymbolicStateDfa agn_safety_; + SymbolicStateDfa agn_reach_; + Player starting_player_; + + CUDD::BDD safe_states_ = var_mgr_->cudd_mgr()->bddOne(); + + /** + * \brief Prints out INPUT and OUTPUT variables in Slugs format + * [INPUT] + * a + * b:0...10 + * + * [OUTPUT] + * c:2...8 + * d + * + * \param GR1 game arena + * \param The file that should be written to + */ + void print_variables(const SymbolicStateDfa arena, const std::string& filename) const; + + /** + * \brief Prints out INITIAL conditions in Slugs format + * Boolean formulas are in infix notations + * [ENV_INIT] + * !a + * b = 1 + * [SYS_INIT] + * c | d + * \param GR1 game arena + * \param The file that should be written to + */ + void print_initial_conditions(const CUDD::BDD& arena_initial_state_bdd, const std::string& filename) const; + + /** + * \brief Prints out TRANSITIONS in Slugs format + * [ENV_TRANS] + * !a + * b | b' + * [SYS_TRANS] + * c | d + * + * \param GR1 game arena + * \param The file that should be written to + */ + void print_transitions(const SymbolicStateDfa arena, const std::string& filename) const; + + /** + * \brief Prints out LIVENESS constraints in Slugs format + * [ENV_LIVENESS] + * ! a | (b = 3) + * [SYS_LIVENESS] + * d + * c = 2 + * \param GR1 game arena + * \param The file that should be written to + */ + void print_liveness_constraints(const SymbolicStateDfa arena, const std::string& filename) const; + + + + public: + + /** + * \brief Construct a synthesizer for the given LTLf/GR(1) game. + * + * \param gr1 A GR(1) formula stating the winning condition. + * \param env_safety A symbolic-state DFA representing the environment safety game arena + * \param agn_reach A symbolic-state DFA representing the system reachability game arena + * \param agn_safety A symbolic-state DFA representing the system safety game arena + * + */ + GR1ReachabilitySynthesizer(std::shared_ptr var_mgr, GR1 gr1, SymbolicStateDfa env_safety, + SymbolicStateDfa agn_reach, SymbolicStateDfa agn_safety); + + const std::string exec_slugs(const std::string& slugs, const std::string& slugs_input_file, + const std::string& slugs_res_file, const std::string& slugs_strategy_file); + + /** + * \brief Solves the LTLf/GR(1) game. + * + * \return The result consists of + * realizability + * a set of agent winning states + * a transducer representing a winning strategy or nullptr if the game is unrealizable. + */ + SynthesisResult run(std::string& benchmark_name); + }; +} +#endif //LYDIASYFT_GR1REACHABILITYSYNTHESIZER_H diff --git a/src/synthesis/header/SymbolicStateDfa.h b/src/synthesis/header/SymbolicStateDfa.h index 879e0ee..9f9370b 100644 --- a/src/synthesis/header/SymbolicStateDfa.h +++ b/src/synthesis/header/SymbolicStateDfa.h @@ -148,6 +148,8 @@ class SymbolicStateDfa { static std::vector state_to_binary(std::size_t state, std::size_t bit_count); + + void new_sink_states(const CUDD::BDD& sink_states); }; } diff --git a/src/synthesis/header/VarMgr.h b/src/synthesis/header/VarMgr.h index bfecad9..bec4c70 100644 --- a/src/synthesis/header/VarMgr.h +++ b/src/synthesis/header/VarMgr.h @@ -265,6 +265,14 @@ class VarMgr { * */ std::size_t automaton_num () const; + + /** + * \brief Prints a BDD as a Boolean formula, where each variable has a specific label. + * + * \param A given BDD. + * \return A string that represents a Boolean formula. + */ + std::string bdd_to_string(const CUDD::BDD& bdd) const; }; diff --git a/src/synthesis/source/GR1ReachabilitySynthesizer.cpp b/src/synthesis/source/GR1ReachabilitySynthesizer.cpp new file mode 100644 index 0000000..99a546b --- /dev/null +++ b/src/synthesis/source/GR1ReachabilitySynthesizer.cpp @@ -0,0 +1,288 @@ +// +// Created by shuzhu on 21/01/24. +// +#include "GR1ReachabilitySynthesizer.h" +#include "string_utilities.h" +#include + + +namespace Syft { + + GR1ReachabilitySynthesizer::GR1ReachabilitySynthesizer(std::shared_ptr var_mgr, GR1 gr1, SymbolicStateDfa env_safety, + SymbolicStateDfa agn_reach, SymbolicStateDfa agn_safety) + : var_mgr_(var_mgr), gr1_(gr1), env_safety_(env_safety), agn_reach_(agn_reach), + agn_safety_(agn_safety) + {} + + void GR1ReachabilitySynthesizer::print_variables(const SymbolicStateDfa arena, const std::string& filename) const{ + std::ofstream to_slugs; + to_slugs.open(filename); + if(to_slugs.is_open()) { + + std::vector input_variable_labels = var_mgr_->input_variable_labels(); + std::vector output_variable_labels = var_mgr_->output_variable_labels(); + + to_slugs << "[INPUT]\n"; + for (std::string output_variable_label : output_variable_labels) { + to_slugs << to_lower_copy(output_variable_label) << "\n"; + } + to_slugs << "\n"; + + to_slugs << "[OUTPUT]\n"; + for (std::string input_variable_label : input_variable_labels) { + to_slugs << to_lower_copy(input_variable_label) << "\n"; + } + size_t state_variable_count = var_mgr_->total_state_variable_count(); + for (size_t i = 0; i < state_variable_count; i++) { + to_slugs << "z" + std::to_string(i) << "\n"; + } + + to_slugs << "\n"; + to_slugs.close(); + } + else{ + std::cout << "Unable to open file "+filename; + } + + } + + void GR1ReachabilitySynthesizer::print_initial_conditions(const CUDD::BDD& arena_initial_state_bdd, const std::string& filename) const{ + std::ofstream to_slugs; + to_slugs.open(filename, std::ios::app); + if(to_slugs.is_open()) { + + to_slugs<<"[ENV_INIT]\n"; + to_slugs<<"TRUE\n"; + + + to_slugs<<"[SYS_INIT]\n"; + + to_slugs<bdd_to_string(arena_initial_state_bdd)); + to_slugs<<"\n\n"; + + to_slugs<<"\n"; + to_slugs.close(); + } + else{ + std::cout << "Unable to open file "+filename; + } + } + + + void GR1ReachabilitySynthesizer::print_transitions(const SymbolicStateDfa arena, const std::string& filename) const { + std::ofstream to_slugs; + to_slugs.open(filename, std::ios::app); + if(to_slugs.is_open()) { + + to_slugs<<"[ENV_TRANS]\n"; + to_slugs<<"TRUE\n\n"; + + std::vector variable_labels = var_mgr_->variable_labels(); + std::unordered_map rename_map; + + std::vector output_variable_labels = var_mgr_->output_variable_labels(); + for (std::string output_variable_label : output_variable_labels){ + std::string output_variable_new_label = output_variable_label+'\''; + rename_map["("+output_variable_label+")"] = "("+output_variable_new_label+")"; + } + + std::vector input_variable_labels = var_mgr_->input_variable_labels(); + for (std::string input_variable_label : input_variable_labels){ + std::string input_variable_new_label = input_variable_label+'\''; + rename_map["("+input_variable_label+")"] = "("+input_variable_new_label+")"; + } + + std::vector transition_function = arena.transition_function(); + + std::unordered_map rename_state_vars_map; + for (size_t i = 0; i < transition_function.size(); i++){ + std::string state_variable_new_label = "Z" + std::to_string(i) + "\'"; + rename_state_vars_map["(Z" + std::to_string(i)+")"] = "("+state_variable_new_label+")"; + } + + + + + to_slugs<<"[SYS_TRANS]\n"; + for (size_t i = 0; i < transition_function.size(); i++){ + std::string tran = var_mgr_->bdd_to_string(transition_function[i]); + for (auto& item : rename_map) { + size_t index = 0; + while (true) { + /* Locate the substring to replace. */ + index = tran.find(item.first, index); + if (index == std::string::npos) break; + + /* Make the replacement. */ + tran.replace(index, item.first.size(), item.second); + + /* Advance index forward so the next iteration doesn't pick it up as well. */ + index += item.first.size(); + } + } + tran = tran + " <-> " + "Z" + std::to_string(i) + "\'"; + + to_slugs<bdd_to_string(safe_states_); + to_slugs<cudd_mgr()->bddOne() || justice == var_mgr_->cudd_mgr()->bddZero()) { + to_slugs<bdd_to_string(justice))<<"\n"; + } + else{ + to_slugs<bdd_to_string(justice))<<"\n"; + } + } + to_slugs<<"\n\n"; + + to_slugs<<"[SYS_LIVENESS]\n"; + for (CUDD::BDD justice : gr1_.agn_justices){ + if (justice == var_mgr_->cudd_mgr()->bddOne() || justice == var_mgr_->cudd_mgr()->bddZero()) { + to_slugs<bdd_to_string(justice))<<"\n"; + } + else { + to_slugs <bdd_to_string(justice)) << "\n"; + } + } + to_slugs.close(); + } + else{ + std::cout << "Unable to open file "+filename; + } + } + + const std::string GR1ReachabilitySynthesizer::exec_slugs(const std::string& slugs, const std::string& slugs_input_file, const std::string& slugs_res_file, const std::string& slugs_strategy_file) { + std::string result; + + std::string run_slugs = slugs+" --counterStrategy " + slugs_input_file + " > " + slugs_strategy_file + " 2> "+slugs_res_file; + + const char* cmd = run_slugs.c_str(); + system(cmd); + std::ifstream in(slugs_res_file); + std::string line; + std::vector substr; + std::getline(in, line); + substr = split(line, ":"); + assert (substr[0] == "SLUGS"); + + std::getline(in, line); + substr = split(line, ":"); + assert (substr[0] == "RESULT"); + trim(substr[1]); // remove leading and trailing whitespace + substr = split(substr[1], " "); + if (substr[3] == "unrealizable."){ + result = "unrealizable"; + std::ifstream in(slugs_strategy_file); + std::string line; + std::vector substr; + std::getline(in, line); + if (line == ""){ + result = "realizable"; + } + } + else{ + result = "realizable"; + } + return result; + } + + SynthesisResult GR1ReachabilitySynthesizer::run(std::string& benchmark_name) { + Syft::Stopwatch reduction_to_gr1_stopwatch; // stopwatch for reducing to GR1 + reduction_to_gr1_stopwatch.start(); + std::cout << "* Start reducing to GR1 game...\n"; + + SymbolicStateDfa reach_safe = SymbolicStateDfa::product({agn_reach_, agn_safety_}); + + CUDD::BDD reach_goal_t1 = agn_reach_.final_states(); + CUDD::BDD safe_region_t2 = agn_safety_.final_states() | agn_safety_.initial_state_bdd(); + + reach_safe.new_sink_states(!safe_region_t2); + + SymbolicStateDfa arena = SymbolicStateDfa::product({env_safety_, reach_safe}); + CUDD::BDD arena_initial_state_bdd = agn_reach_.initial_state_bdd() & agn_safety_.initial_state_bdd() & env_safety_.initial_state_bdd(); + + safe_states_ = (env_safety_.final_states() & !(reach_safe.final_states())) | arena_initial_state_bdd; + + std::string to_slugs_parser = benchmark_name + ".parser"; + print_variables(arena, to_slugs_parser); + print_initial_conditions(arena_initial_state_bdd, to_slugs_parser); + print_transitions(arena, to_slugs_parser); + print_liveness_constraints(arena, to_slugs_parser); + + auto reduction_to_gr1_time = reduction_to_gr1_stopwatch.stop(); + std::cout << "* Finish reducing to GR1 game, took time: " + << reduction_to_gr1_time.count() << " ms" << std::endl; + + Syft::Stopwatch gr1_game_stopwatch; // stopwatch for GR1 game solver Slugs + gr1_game_stopwatch.start(); + std::cout << "* Start calling GR1 game solver Slugs...\n"; + + std::string slugs_input_file = benchmark_name+".slugsin"; + std::string slugs_parser = "StructuredSlugsParser/compiler.py"; + std::string run_slugs_parser = "python3 "+slugs_parser+" "+to_slugs_parser+" > " + slugs_input_file; + +// std::cout<& return product_automaton; } + void SymbolicStateDfa::new_sink_states(const CUDD::BDD& states) { + int i = 0; + while (i < transition_function_.size()) { + CUDD::BDD bit_function = transition_function_[i]; + CUDD::BDD bit = var_mgr()->state_variable(automaton_id_, i); +// var_mgr()->dump_dot(bit.Add(), "bit"+std::to_string(i)); + CUDD::BDD new_bit_function = (bit_function & !states) | (states * bit); + transition_function_[i] = new_bit_function; + i++; + } + } + } diff --git a/src/synthesis/source/VarMgr.cpp b/src/synthesis/source/VarMgr.cpp index 7724ec8..a9200af 100644 --- a/src/synthesis/source/VarMgr.cpp +++ b/src/synthesis/source/VarMgr.cpp @@ -2,7 +2,8 @@ #include #include -#include +#include +#include namespace Syft { @@ -31,12 +32,16 @@ std::size_t VarMgr::create_state_variables(std::size_t variable_count) { state_variables_.emplace_back(); state_variables_[automaton_id].reserve(variable_count); - for (std::size_t i = 0; i < variable_count; ++i) { - // Creates a new variable at the top of the variable ordering - CUDD::BDD new_state_variable = mgr_->bddNewVarAtLevel(0); - - state_variables_[automaton_id].push_back(new_state_variable); - } + for (std::size_t i = 0; i < variable_count; ++i) { + // Creates a new variable at the top of the variable ordering + CUDD::BDD new_state_variable = mgr_->bddNewVarAtLevel(0); + + state_variables_[automaton_id].push_back(new_state_variable); + int new_index = new_state_variable.NodeReadIndex(); + std::string name = "Z"+std::to_string(state_variable_count_+i); + name_to_variable_[name] = new_state_variable; + index_to_name_[new_index] = name; + } state_variable_count_ += variable_count; @@ -315,5 +320,45 @@ void VarMgr::dump_dot(const std::vector& adds, std::size_t VarMgr::automaton_num() const { return state_variables_.size(); } - + +std::string VarMgr::bdd_to_string(const CUDD::BDD& bdd) const { + std::stringstream ss; + ss << bdd; + std::string s = ss.str(); + + // Replace x with $ in the variable representation to avoid problems if a + // var label happens to have the form x#. This assumes that the var labels + // cannot have the form $#. + while (true) { + std::size_t pos = s.find("x"); + + if (pos == std::string::npos) { + break; + } + + s.replace(pos, 1, "$"); + } + + // Sort ids from highest to lowest so that ids with more digits get replaced + // before ids with fewer digits. + std::vector ids = bdd.SupportIndices(); + std::sort(ids.begin(), ids.end(), std::greater()); + + + for (unsigned int id : ids) { + std::string var_string = "$" + std::to_string(id); + + while (true) { + std::size_t pos = s.find(var_string); + + if (pos == std::string::npos) { + break; + } + + s.replace(pos, var_string.size(), "("+index_to_name(id)+")"); + } + } + + return s; +} } diff --git a/src/utils/string_utilities.cpp b/src/utils/string_utilities.cpp index 08abc3c..999aab9 100644 --- a/src/utils/string_utilities.cpp +++ b/src/utils/string_utilities.cpp @@ -3,6 +3,7 @@ #include #include #include +#include namespace Syft { @@ -27,4 +28,18 @@ namespace Syft { }).base(), trimmed_str.end()); return trimmed_str; } + + std::string to_lower_copy(const std::string& str) { + std::string data = str; + std::transform(data.begin(), data.end(), data.begin(), + [](unsigned char c){ return std::tolower(c); }); + return data; + } + + std::string to_upper_copy(const std::string& str) { + std::string data = str; + std::transform(data.begin(), data.end(), data.begin(), + [](unsigned char c){ return std::toupper(c); }); + return data; + } } \ No newline at end of file diff --git a/src/utils/string_utilities.h b/src/utils/string_utilities.h index 379d630..23aac1f 100644 --- a/src/utils/string_utilities.h +++ b/src/utils/string_utilities.h @@ -9,7 +9,8 @@ namespace Syft { std::vector split(const std::string& str, const std::string& delimiter = " "); std::string trim(const std::string& str); - + std::string to_lower_copy(const std::string& str); + std::string to_upper_copy(const std::string& str); } #endif //LYDIASYFT_STRING_UTILITIES_H diff --git a/test/test_gr1reachability_synthesis.cpp b/test/test_gr1reachability_synthesis.cpp new file mode 100644 index 0000000..a624fb7 --- /dev/null +++ b/test/test_gr1reachability_synthesis.cpp @@ -0,0 +1,111 @@ +// +// Created by shuzhu on 21/01/24. +// +// +// Created by shuzhu on 21/01/24. +// +#include "catch2/catch_test_macros.hpp" +#include "catch2/generators/catch_generators_all.hpp" + +#include "ExplicitStateDfaMona.h" +#include "InputOutputPartition.h" +#include "GR1ReachabilitySynthesizer.h" +#include "GR1.h" +#include "Preprocessing.h" +#include "Parser.h" +#include "utils.hpp" +#include + +TEST_CASE("GR1 Synthesis test", "[gr1 synthesis]") { + Syft::Parser parser; + parser = Syft::Parser::read_from_file(Syft::Test::SYFCO_LOCATION, Syft::Test::GR1SYNTHESIS_TEST_AGN_GOAL); + + bool sys_first = parser.get_sys_first(); + + Syft::Player starting_player = sys_first? Syft::Player::Agent : Syft::Player::Environment; + Syft::Player protagonist_player = Syft::Player::Agent; + + Syft::InputOutputPartition partition = + Syft::InputOutputPartition::construct_from_input(parser.get_input_variables(), parser.get_output_variables()); + std::shared_ptr var_mgr = std::make_shared(); + var_mgr->create_named_variables(partition.input_variables); + var_mgr->create_named_variables(partition.output_variables); + + var_mgr->partition_variables(partition.input_variables, + partition.output_variables); + + // Parsing the formula agn_goal + std::shared_ptr driver_agn_goal; + driver_agn_goal = std::make_shared(); + std::stringstream formula_stream(parser.get_formula()); + driver_agn_goal->parse(formula_stream); + whitemech::lydia::ltlf_ptr parsed_formula_agn_goal = driver_agn_goal->get_result(); + // Apply no-empty semantics + auto context = driver_agn_goal->context; + auto not_end = context->makeLtlfNotEnd(); + parsed_formula_agn_goal = context->makeLtlfAnd({parsed_formula_agn_goal, not_end}); + + Syft::ExplicitStateDfaMona explicit_dfa_mona_agn_goal = Syft::ExplicitStateDfaMona::dfa_of_formula(*parsed_formula_agn_goal); + + Syft::ExplicitStateDfa explicit_dfa_agn_goal = Syft::ExplicitStateDfa::from_dfa_mona(var_mgr, explicit_dfa_mona_agn_goal); + + + Syft::SymbolicStateDfa symbolic_dfa_agn_goal = Syft::SymbolicStateDfa::from_explicit( + std::move(explicit_dfa_agn_goal)); + + // Parsing the formula env_safety + std::shared_ptr driver_env_safety; + driver_env_safety = std::make_shared(); + std::ifstream in_env_safety(Syft::Test::GR1SYNTHESIS_TEST_ENV_SAFETY); + std::string env_safety; + std::getline(in_env_safety, env_safety); + std::stringstream formula_stream_env_safety(env_safety); + driver_env_safety->parse(formula_stream_env_safety); + whitemech::lydia::ltlf_ptr parsed_formula_env_safety = driver_env_safety->get_result(); + // Apply no-empty semantics + parsed_formula_env_safety = context->makeLtlfAnd({parsed_formula_env_safety, not_end}); + + Syft::ExplicitStateDfaMona explicit_dfa_mona_env_safety = Syft::ExplicitStateDfaMona::dfa_of_formula(*parsed_formula_env_safety); + + Syft::ExplicitStateDfa explicit_dfa_env_safety = Syft::ExplicitStateDfa::from_dfa_mona(var_mgr, explicit_dfa_mona_env_safety); + + + Syft::SymbolicStateDfa symbolic_dfa_env_safety = Syft::SymbolicStateDfa::from_explicit( + std::move(explicit_dfa_env_safety)); + + // Parsing the formula agn_safety + std::shared_ptr driver_agn_safetyy; + driver_env_safety = std::make_shared(); + std::ifstream in_agn_safety(Syft::Test::GR1SYNTHESIS_TEST_AGN_SAFETY); + std::string agn_safety; + std::getline(in_agn_safety, agn_safety); + std::stringstream formula_stream_agn_safety(agn_safety); + driver_env_safety->parse(formula_stream_agn_safety); + whitemech::lydia::ltlf_ptr parsed_formula_agn_safety = driver_env_safety->get_result(); + // Apply no-empty semantics + parsed_formula_agn_safety = context->makeLtlfAnd({parsed_formula_agn_safety, not_end}); + + Syft::ExplicitStateDfaMona explicit_dfa_mona_agn_safety = Syft::ExplicitStateDfaMona::dfa_of_formula(*parsed_formula_agn_safety); + + Syft::ExplicitStateDfa explicit_dfa_agn_safety = Syft::ExplicitStateDfa::from_dfa_mona(var_mgr, explicit_dfa_mona_agn_safety); + + Syft::SymbolicStateDfa symbolic_dfa_agn_safety = Syft::SymbolicStateDfa::from_explicit( + std::move(explicit_dfa_agn_safety)); + + // gr1 + Syft::GR1 gr1 = Syft::GR1::read_from_gr1_file(var_mgr, Syft::Test::GR1SYNTHESIS_TEST_ENV_GR1); + + + + Syft::GR1ReachabilitySynthesizer synthesizer(var_mgr, gr1, symbolic_dfa_env_safety, + symbolic_dfa_agn_goal, symbolic_dfa_agn_safety); + + std::string benchmark_name = "hand_shake"; + Syft::SynthesisResult result = synthesizer.run(benchmark_name); + + bool expected = true; + REQUIRE(result.realizability == expected); +} + + + diff --git a/test/utils.hpp b/test/utils.hpp index 09ce14a..e62bb2d 100644 --- a/test/utils.hpp +++ b/test/utils.hpp @@ -25,6 +25,11 @@ namespace Syft::Test { static std::string FAIRSTABLESYNTHESIS_UNREA_TEST_TLSF = ROOT_DIRECTORY + "/example/fair_stable_unrea_test.tlsf"; static std::string FAIRSTABLESYNTHESIS_TEST_ASSUMPTION = ROOT_DIRECTORY + "/example/fair_stable_test_assumption.txt"; + static std::string GR1SYNTHESIS_TEST_ENV_GR1 = ROOT_DIRECTORY + "/example/tcp_handshake_env_gr1.txt"; + static std::string GR1SYNTHESIS_TEST_ENV_SAFETY = ROOT_DIRECTORY + "/example/tcp_handshake_env_safety.ltlf"; + static std::string GR1SYNTHESIS_TEST_AGN_SAFETY = ROOT_DIRECTORY + "/example/tcp_handshake_agn_safety.ltlf"; + static std::string GR1SYNTHESIS_TEST_AGN_GOAL = ROOT_DIRECTORY + "/example/tcp_handshake_agn_goal.tlsf"; + inline std::string get_time_str() { // Get current time as a time_point object auto now = std::chrono::system_clock::now(); From 813ff66c465e0f8f9debd80d8085f7faea1aa842 Mon Sep 17 00:00:00 2001 From: Marco Favorito Date: Mon, 22 Jan 2024 21:43:14 +0100 Subject: [PATCH 2/6] fix: var number check in VarMgr::partition_variables --- src/synthesis/source/VarMgr.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/synthesis/source/VarMgr.cpp b/src/synthesis/source/VarMgr.cpp index a9200af..435df8e 100644 --- a/src/synthesis/source/VarMgr.cpp +++ b/src/synthesis/source/VarMgr.cpp @@ -97,7 +97,7 @@ void VarMgr::partition_variables(const std::vector& input_names, // } - if (input_names.size() + output_names.size() != index_to_name_.size()) { + if (input_names.size() + output_names.size() != (index_to_name_.size() - state_variable_count_)) { throw std::runtime_error( "Error: Input-output partition is the wrong size."); } From c818e437712c5203cd0f57b7b72223b6f24580ae Mon Sep 17 00:00:00 2001 From: Shufang-Zhu Date: Mon, 22 Jan 2024 19:13:30 +0000 Subject: [PATCH 3/6] GR1 passed test --- .../GR1benchmarks/finding_nemo_agn_goal.tlsf | 29 ++++++ .../finding_nemo_agn_safety.ltlf | 1 + .../GR1benchmarks/finding_nemo_env_gr1.txt | 10 ++ .../finding_nemo_env_safety.ltlf | 1 + .../tcp_handshake_agn_goal.tlsf | 0 .../tcp_handshake_agn_safety.ltlf | 0 .../tcp_handshake_env_gr1.txt | 0 .../tcp_handshake_env_safety.ltlf | 0 test/test_gr1reachability_synthesis.cpp | 93 +++++++++++++++++++ test/utils.hpp | 13 ++- 10 files changed, 143 insertions(+), 4 deletions(-) create mode 100644 example/GR1benchmarks/finding_nemo_agn_goal.tlsf create mode 100644 example/GR1benchmarks/finding_nemo_agn_safety.ltlf create mode 100644 example/GR1benchmarks/finding_nemo_env_gr1.txt create mode 100644 example/GR1benchmarks/finding_nemo_env_safety.ltlf rename example/{ => GR1benchmarks}/tcp_handshake_agn_goal.tlsf (100%) rename example/{ => GR1benchmarks}/tcp_handshake_agn_safety.ltlf (100%) rename example/{ => GR1benchmarks}/tcp_handshake_env_gr1.txt (100%) rename example/{ => GR1benchmarks}/tcp_handshake_env_safety.ltlf (100%) diff --git a/example/GR1benchmarks/finding_nemo_agn_goal.tlsf b/example/GR1benchmarks/finding_nemo_agn_goal.tlsf new file mode 100644 index 0000000..0ecfe68 --- /dev/null +++ b/example/GR1benchmarks/finding_nemo_agn_goal.tlsf @@ -0,0 +1,29 @@ +INFO { + TITLE: "LTLf-test" + DESCRIPTION: "LTLf-test example" + SEMANTICS: Finite,Moore + TARGET: Moore +} + +MAIN { + + INPUTS { + sense_nemo; + nemo_leaving; + } + + OUTPUTS { + camera_on; + hallway_0; + hallway_1; + room_0; + room_1; + room_2; + room_3; + } + + GUARANTEES { + (F ((sense_nemo && camera_on) && X[!](F ((sense_nemo && camera_on) && X[!](F (sense_nemo && camera_on)))))); + } + +} diff --git a/example/GR1benchmarks/finding_nemo_agn_safety.ltlf b/example/GR1benchmarks/finding_nemo_agn_safety.ltlf new file mode 100644 index 0000000..025a09a --- /dev/null +++ b/example/GR1benchmarks/finding_nemo_agn_safety.ltlf @@ -0,0 +1 @@ +(G ((hallway_0 -> (!(hallway_1) & !(room_0) & !(room_1) & !(room_2) & !(room_3))) & (hallway_1 -> (!(hallway_0) & !(room_0) & !(room_1) & !(room_2) & !(room_3))) & (room_0 -> (!(hallway_0) & !(hallway_1) & !(room_1) & !(room_2) & !(room_3))) & (room_1 -> (!(hallway_0) & !(hallway_1) & !(room_0) & !(room_2) & !(room_3))) & (room_2 -> (!(hallway_0) & !(hallway_1) & !(room_0) & !(room_1) & !(room_3))) & (room_3 -> (!(hallway_0) & !(hallway_1) & !(room_0) & !(room_1) & !(room_2)))) & G ((hallway_0 -> (X room_0 || X room_1 || X hallway_1 || X hallway_0 || X hallway_1)) & (hallway_1 -> (X room_2 || X room_3 || X hallway_0 || X hallway_1 || X hallway_0)) & (room_0 -> (X room_0 || X hallway_0)) & (room_1 -> (X room_1 || X hallway_0)) & (room_2 -> (X room_2 || X hallway_1)) & (room_3 -> (X room_3 || X hallway_1))) & G (!(sense_nemo) -> !(camera_on))) diff --git a/example/GR1benchmarks/finding_nemo_env_gr1.txt b/example/GR1benchmarks/finding_nemo_env_gr1.txt new file mode 100644 index 0000000..fc1eb93 --- /dev/null +++ b/example/GR1benchmarks/finding_nemo_env_gr1.txt @@ -0,0 +1,10 @@ +--Env-Justice-- +room_1 +--Justice-End-- +--Env-Justice-- +room_3 +--Justice-End-- +--Agn-Justice-- +sense_nemo +--Justice-End-- +End diff --git a/example/GR1benchmarks/finding_nemo_env_safety.ltlf b/example/GR1benchmarks/finding_nemo_env_safety.ltlf new file mode 100644 index 0000000..24ee48f --- /dev/null +++ b/example/GR1benchmarks/finding_nemo_env_safety.ltlf @@ -0,0 +1 @@ +(G ((hallway_0 -> (!(hallway_1) & !(room_0) & !(room_1) & !(room_2) & !(room_3))) & (hallway_1 -> (!(hallway_0) & !(room_0) & !(room_1) & !(room_2) & !(room_3))) & (room_0 -> (!(hallway_0) & !(hallway_1) & !(room_1) & !(room_2) & !(room_3))) & (room_1 -> (!(hallway_0) & !(hallway_1) & !(room_0) & !(room_2) & !(room_3))) & (room_2 -> (!(hallway_0) & !(hallway_1) & !(room_0) & !(room_1) & !(room_3))) & (room_3 -> (!(hallway_0) & !(hallway_1) & !(room_0) & !(room_1) & !(room_2)))) -> (G ((!(room_1) & !(room_3)) -> !(sense_nemo)) & G ((sense_nemo & ((hallway_0 & X hallway_0) || (hallway_1 & X hallway_1) || (room_0 & X room_0) || (room_1 & X room_1) || (room_2 & X room_2) || (room_3 & X room_3))) -> (X sense_nemo <-> !(nemo_leaving))) & G ((!(sense_nemo) & X sense_nemo & ((X hallway_0 & X X hallway_0) || (X hallway_1 & X X hallway_1) || (X room_0 & X X room_0) || (X room_1 & X X room_1) || (X room_2 & X X room_2) || (X room_3 & X X room_3))) -> X X sense_nemo))) diff --git a/example/tcp_handshake_agn_goal.tlsf b/example/GR1benchmarks/tcp_handshake_agn_goal.tlsf similarity index 100% rename from example/tcp_handshake_agn_goal.tlsf rename to example/GR1benchmarks/tcp_handshake_agn_goal.tlsf diff --git a/example/tcp_handshake_agn_safety.ltlf b/example/GR1benchmarks/tcp_handshake_agn_safety.ltlf similarity index 100% rename from example/tcp_handshake_agn_safety.ltlf rename to example/GR1benchmarks/tcp_handshake_agn_safety.ltlf diff --git a/example/tcp_handshake_env_gr1.txt b/example/GR1benchmarks/tcp_handshake_env_gr1.txt similarity index 100% rename from example/tcp_handshake_env_gr1.txt rename to example/GR1benchmarks/tcp_handshake_env_gr1.txt diff --git a/example/tcp_handshake_env_safety.ltlf b/example/GR1benchmarks/tcp_handshake_env_safety.ltlf similarity index 100% rename from example/tcp_handshake_env_safety.ltlf rename to example/GR1benchmarks/tcp_handshake_env_safety.ltlf diff --git a/test/test_gr1reachability_synthesis.cpp b/test/test_gr1reachability_synthesis.cpp index a624fb7..845bde3 100644 --- a/test/test_gr1reachability_synthesis.cpp +++ b/test/test_gr1reachability_synthesis.cpp @@ -108,4 +108,97 @@ TEST_CASE("GR1 Synthesis test", "[gr1 synthesis]") { } +TEST_CASE("GR1 Synthesis finding_nemo", "[gr1 synthesis]") { + Syft::Parser parser; + parser = Syft::Parser::read_from_file(Syft::Test::SYFCO_LOCATION, Syft::Test::GR1SYNTHESIS_FINDING_NEMO_AGN_GOAL); + + bool sys_first = parser.get_sys_first(); + + Syft::Player starting_player = sys_first? Syft::Player::Agent : Syft::Player::Environment; + Syft::Player protagonist_player = Syft::Player::Agent; + + Syft::InputOutputPartition partition = + Syft::InputOutputPartition::construct_from_input(parser.get_input_variables(), parser.get_output_variables()); + std::shared_ptr var_mgr = std::make_shared(); + var_mgr->create_named_variables(partition.input_variables); + var_mgr->create_named_variables(partition.output_variables); + + var_mgr->partition_variables(partition.input_variables, + partition.output_variables); + + // Parsing the formula agn_goal + std::shared_ptr driver_agn_goal; + driver_agn_goal = std::make_shared(); + std::stringstream formula_stream(parser.get_formula()); + driver_agn_goal->parse(formula_stream); + whitemech::lydia::ltlf_ptr parsed_formula_agn_goal = driver_agn_goal->get_result(); + // Apply no-empty semantics + auto context = driver_agn_goal->context; + auto not_end = context->makeLtlfNotEnd(); + parsed_formula_agn_goal = context->makeLtlfAnd({parsed_formula_agn_goal, not_end}); + + Syft::ExplicitStateDfaMona explicit_dfa_mona_agn_goal = Syft::ExplicitStateDfaMona::dfa_of_formula(*parsed_formula_agn_goal); + + Syft::ExplicitStateDfa explicit_dfa_agn_goal = Syft::ExplicitStateDfa::from_dfa_mona(var_mgr, explicit_dfa_mona_agn_goal); + + + Syft::SymbolicStateDfa symbolic_dfa_agn_goal = Syft::SymbolicStateDfa::from_explicit( + std::move(explicit_dfa_agn_goal)); + + // Parsing the formula env_safety + std::shared_ptr driver_env_safety; + driver_env_safety = std::make_shared(); + std::ifstream in_env_safety(Syft::Test::GR1SYNTHESIS_FINDING_NEMO_ENV_SAFETY); + std::string env_safety; + std::getline(in_env_safety, env_safety); + std::stringstream formula_stream_env_safety(env_safety); + driver_env_safety->parse(formula_stream_env_safety); + whitemech::lydia::ltlf_ptr parsed_formula_env_safety = driver_env_safety->get_result(); + // Apply no-empty semantics + parsed_formula_env_safety = context->makeLtlfAnd({parsed_formula_env_safety, not_end}); + + Syft::ExplicitStateDfaMona explicit_dfa_mona_env_safety = Syft::ExplicitStateDfaMona::dfa_of_formula(*parsed_formula_env_safety); + + Syft::ExplicitStateDfa explicit_dfa_env_safety = Syft::ExplicitStateDfa::from_dfa_mona(var_mgr, explicit_dfa_mona_env_safety); + + + Syft::SymbolicStateDfa symbolic_dfa_env_safety = Syft::SymbolicStateDfa::from_explicit( + std::move(explicit_dfa_env_safety)); + + // Parsing the formula agn_safety + std::shared_ptr driver_agn_safetyy; + driver_env_safety = std::make_shared(); + std::ifstream in_agn_safety(Syft::Test::GR1SYNTHESIS_FINDING_NEMO_AGN_SAFETY); + std::string agn_safety; + std::getline(in_agn_safety, agn_safety); + std::stringstream formula_stream_agn_safety(agn_safety); + driver_env_safety->parse(formula_stream_agn_safety); + whitemech::lydia::ltlf_ptr parsed_formula_agn_safety = driver_env_safety->get_result(); + // Apply no-empty semantics + parsed_formula_agn_safety = context->makeLtlfAnd({parsed_formula_agn_safety, not_end}); + + Syft::ExplicitStateDfaMona explicit_dfa_mona_agn_safety = Syft::ExplicitStateDfaMona::dfa_of_formula(*parsed_formula_agn_safety); + + Syft::ExplicitStateDfa explicit_dfa_agn_safety = Syft::ExplicitStateDfa::from_dfa_mona(var_mgr, explicit_dfa_mona_agn_safety); + + Syft::SymbolicStateDfa symbolic_dfa_agn_safety = Syft::SymbolicStateDfa::from_explicit( + std::move(explicit_dfa_agn_safety)); + + // gr1 + Syft::GR1 gr1 = Syft::GR1::read_from_gr1_file(var_mgr, Syft::Test::GR1SYNTHESIS_FINDING_NEMO_ENV_GR1); + + + + Syft::GR1ReachabilitySynthesizer synthesizer(var_mgr, gr1, symbolic_dfa_env_safety, + symbolic_dfa_agn_goal, symbolic_dfa_agn_safety); + + std::string benchmark_name = "finding_nemo"; + + Syft::SynthesisResult result = synthesizer.run(benchmark_name); + + bool expected = true; + REQUIRE(result.realizability == expected); +} + + diff --git a/test/utils.hpp b/test/utils.hpp index e62bb2d..f704110 100644 --- a/test/utils.hpp +++ b/test/utils.hpp @@ -25,10 +25,15 @@ namespace Syft::Test { static std::string FAIRSTABLESYNTHESIS_UNREA_TEST_TLSF = ROOT_DIRECTORY + "/example/fair_stable_unrea_test.tlsf"; static std::string FAIRSTABLESYNTHESIS_TEST_ASSUMPTION = ROOT_DIRECTORY + "/example/fair_stable_test_assumption.txt"; - static std::string GR1SYNTHESIS_TEST_ENV_GR1 = ROOT_DIRECTORY + "/example/tcp_handshake_env_gr1.txt"; - static std::string GR1SYNTHESIS_TEST_ENV_SAFETY = ROOT_DIRECTORY + "/example/tcp_handshake_env_safety.ltlf"; - static std::string GR1SYNTHESIS_TEST_AGN_SAFETY = ROOT_DIRECTORY + "/example/tcp_handshake_agn_safety.ltlf"; - static std::string GR1SYNTHESIS_TEST_AGN_GOAL = ROOT_DIRECTORY + "/example/tcp_handshake_agn_goal.tlsf"; + static std::string GR1SYNTHESIS_TEST_ENV_GR1 = ROOT_DIRECTORY + "/example/GR1benchmarks/tcp_handshake_env_gr1.txt"; + static std::string GR1SYNTHESIS_TEST_ENV_SAFETY = ROOT_DIRECTORY + "/example/GR1benchmarks/tcp_handshake_env_safety.ltlf"; + static std::string GR1SYNTHESIS_TEST_AGN_SAFETY = ROOT_DIRECTORY + "/example/GR1benchmarks/tcp_handshake_agn_safety.ltlf"; + static std::string GR1SYNTHESIS_TEST_AGN_GOAL = ROOT_DIRECTORY + "/example/GR1benchmarks/tcp_handshake_agn_goal.tlsf"; + + static std::string GR1SYNTHESIS_FINDING_NEMO_ENV_GR1 = ROOT_DIRECTORY + "/example/GR1benchmarks/finding_nemo_env_gr1.txt"; + static std::string GR1SYNTHESIS_FINDING_NEMO_ENV_SAFETY = ROOT_DIRECTORY + "/example/GR1benchmarks/finding_nemo_env_safety.ltlf"; + static std::string GR1SYNTHESIS_FINDING_NEMO_AGN_SAFETY = ROOT_DIRECTORY + "/example/GR1benchmarks/finding_nemo_agn_safety.ltlf"; + static std::string GR1SYNTHESIS_FINDING_NEMO_AGN_GOAL = ROOT_DIRECTORY + "/example/GR1benchmarks/finding_nemo_agn_goal.tlsf"; inline std::string get_time_str() { // Get current time as a time_point object From ac8bff4b085761bef3b3aa1b69c18222b5ba230d Mon Sep 17 00:00:00 2001 From: Marco Favorito Date: Mon, 22 Jan 2024 22:19:02 +0100 Subject: [PATCH 4/6] fix: handling of path to Slugs root directory --- src/synthesis/header/GR1ReachabilitySynthesizer.h | 12 ++++++++++-- .../source/GR1ReachabilitySynthesizer.cpp | 15 +++++++++------ test/test_gr1reachability_synthesis.cpp | 4 ++-- test/utils.hpp | 1 + 4 files changed, 22 insertions(+), 10 deletions(-) diff --git a/src/synthesis/header/GR1ReachabilitySynthesizer.h b/src/synthesis/header/GR1ReachabilitySynthesizer.h index 01f5887..95ee8f2 100644 --- a/src/synthesis/header/GR1ReachabilitySynthesizer.h +++ b/src/synthesis/header/GR1ReachabilitySynthesizer.h @@ -27,6 +27,8 @@ namespace Syft { CUDD::BDD safe_states_ = var_mgr_->cudd_mgr()->bddOne(); + std::string slugs_dir_; + /** * \brief Prints out INPUT and OUTPUT variables in Slugs format * [INPUT] @@ -80,7 +82,12 @@ namespace Syft { */ void print_liveness_constraints(const SymbolicStateDfa arena, const std::string& filename) const; - + /** + * Get the path to the SLUGS binary. + * + * @return the path to the SLUGS binary. + */ + std::string get_slugs_path(); public: @@ -91,10 +98,11 @@ namespace Syft { * \param env_safety A symbolic-state DFA representing the environment safety game arena * \param agn_reach A symbolic-state DFA representing the system reachability game arena * \param agn_safety A symbolic-state DFA representing the system safety game arena + * \param slugs_dir The root directory of the SLUGS project * */ GR1ReachabilitySynthesizer(std::shared_ptr var_mgr, GR1 gr1, SymbolicStateDfa env_safety, - SymbolicStateDfa agn_reach, SymbolicStateDfa agn_safety); + SymbolicStateDfa agn_reach, SymbolicStateDfa agn_safety, std::string slugs_dir); const std::string exec_slugs(const std::string& slugs, const std::string& slugs_input_file, const std::string& slugs_res_file, const std::string& slugs_strategy_file); diff --git a/src/synthesis/source/GR1ReachabilitySynthesizer.cpp b/src/synthesis/source/GR1ReachabilitySynthesizer.cpp index 99a546b..3636b27 100644 --- a/src/synthesis/source/GR1ReachabilitySynthesizer.cpp +++ b/src/synthesis/source/GR1ReachabilitySynthesizer.cpp @@ -9,9 +9,9 @@ namespace Syft { GR1ReachabilitySynthesizer::GR1ReachabilitySynthesizer(std::shared_ptr var_mgr, GR1 gr1, SymbolicStateDfa env_safety, - SymbolicStateDfa agn_reach, SymbolicStateDfa agn_safety) + SymbolicStateDfa agn_reach, SymbolicStateDfa agn_safety, std::string slugs_dir) : var_mgr_(var_mgr), gr1_(gr1), env_safety_(env_safety), agn_reach_(agn_reach), - agn_safety_(agn_safety) + agn_safety_(agn_safety), slugs_dir_{slugs_dir} {} void GR1ReachabilitySynthesizer::print_variables(const SymbolicStateDfa arena, const std::string& filename) const{ @@ -188,7 +188,7 @@ namespace Syft { const std::string GR1ReachabilitySynthesizer::exec_slugs(const std::string& slugs, const std::string& slugs_input_file, const std::string& slugs_res_file, const std::string& slugs_strategy_file) { std::string result; - std::string run_slugs = slugs+" --counterStrategy " + slugs_input_file + " > " + slugs_strategy_file + " 2> "+slugs_res_file; + std::string run_slugs = slugs + " --counterStrategy " + slugs_input_file + " > " + slugs_strategy_file + " 2> "+slugs_res_file; const char* cmd = run_slugs.c_str(); system(cmd); @@ -252,8 +252,8 @@ namespace Syft { std::cout << "* Start calling GR1 game solver Slugs...\n"; std::string slugs_input_file = benchmark_name+".slugsin"; - std::string slugs_parser = "StructuredSlugsParser/compiler.py"; - std::string run_slugs_parser = "python3 "+slugs_parser+" "+to_slugs_parser+" > " + slugs_input_file; + std::string slugs_parser = slugs_dir_ + "/tools/StructuredSlugsParser/compiler.py"; + std::string run_slugs_parser = "python3 "+ slugs_parser + " " + to_slugs_parser + " > " + slugs_input_file; // std::cout< Date: Mon, 22 Jan 2024 22:29:53 +0100 Subject: [PATCH 5/6] ci: build slugs --- .github/workflows/cmake.yml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.github/workflows/cmake.yml b/.github/workflows/cmake.yml index 6217eff..d91f499 100644 --- a/.github/workflows/cmake.yml +++ b/.github/workflows/cmake.yml @@ -34,6 +34,10 @@ jobs: # install graphviz sudo apt-get install graphviz libgraphviz-dev + + # build slugs + sudo apt install -y libboost-all-dev + cd submodules/slugs/src && make -j - name: Install Z3 run: | wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.12/z3-4.8.12-x64-glibc-2.31.zip From 776788c5fcfa5990c0e427b9f5cf1d34943bfa73 Mon Sep 17 00:00:00 2001 From: Marco Favorito Date: Mon, 22 Jan 2024 22:30:54 +0100 Subject: [PATCH 6/6] fix: replace 'X\[\!\]' with 'strongX' in Catch test names --- test/test_one_step_realizability_check.cpp | 4 ++-- test/test_one_step_unrealizability_check.cpp | 4 ++-- test/test_preprocessing.cpp | 4 ++-- test/test_synthesis.cpp | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/test/test_one_step_realizability_check.cpp b/test/test_one_step_realizability_check.cpp index a84832a..6e66244 100644 --- a/test/test_one_step_realizability_check.cpp +++ b/test/test_one_step_realizability_check.cpp @@ -50,7 +50,7 @@ TEST_CASE("One-step realizability check of a", "[one-step-realizability-check]") } -TEST_CASE("One-step realizability check of X\\[\\!\\] a", "[one-step-realizability-check]") { +TEST_CASE("One-step realizability check of strongX a", "[one-step-realizability-check]") { auto driver = std::make_shared(); auto var_mgr = std::make_shared(); @@ -220,7 +220,7 @@ TEST_CASE("One-step realizability check of random formula 1", "[one-step-unreali } } -TEST_CASE("One-step realizability check of a U X\\[\\!\\]b", "[one-step-unrealizability-check]") { +TEST_CASE("One-step realizability check of a U strongXb", "[one-step-unrealizability-check]") { auto driver = std::make_shared(); auto var_mgr = std::make_shared(); diff --git a/test/test_one_step_unrealizability_check.cpp b/test/test_one_step_unrealizability_check.cpp index 4152b83..c0c378c 100644 --- a/test/test_one_step_unrealizability_check.cpp +++ b/test/test_one_step_unrealizability_check.cpp @@ -50,7 +50,7 @@ TEST_CASE("One-step unrealizability check of a", "[one-step-unrealizability-chec } -TEST_CASE("One-step unrealizability check of X\\[\\!\\] a", "[one-step-unrealizability-check]") { +TEST_CASE("One-step unrealizability check of strongX a", "[one-step-unrealizability-check]") { auto driver = std::make_shared(); auto var_mgr = std::make_shared(); @@ -234,7 +234,7 @@ TEST_CASE("One-step unrealizability check of random formula 1", "[one-step-unrea } } -TEST_CASE("One-step unrealizability check of a U X\\[\\!\\]b", "[one-step-unrealizability-check]") { +TEST_CASE("One-step unrealizability check of a U strongXb", "[one-step-unrealizability-check]") { auto driver = std::make_shared(); auto var_mgr = std::make_shared(); diff --git a/test/test_preprocessing.cpp b/test/test_preprocessing.cpp index ff9a21d..24e3a40 100644 --- a/test/test_preprocessing.cpp +++ b/test/test_preprocessing.cpp @@ -55,7 +55,7 @@ TEST_CASE("Preprocessing of a", "[preprocessing]") { } -TEST_CASE("Preprocessing of X\\[\\!\\] a", "[preprocessing]") { +TEST_CASE("Preprocessing of strongX a", "[preprocessing]") { auto driver = std::make_shared(); auto var_mgr = std::make_shared(); @@ -232,7 +232,7 @@ TEST_CASE("Preprocessing of random formula 1", "[one-step-unrealizability-check] } } -TEST_CASE("Preprocessing of a U X\\[\\!\\]b", "[one-step-unrealizability-check]") { +TEST_CASE("Preprocessing of a U strongXb", "[one-step-unrealizability-check]") { auto driver = std::make_shared(); auto var_mgr = std::make_shared(); diff --git a/test/test_synthesis.cpp b/test/test_synthesis.cpp index 6d93a47..7247cda 100644 --- a/test/test_synthesis.cpp +++ b/test/test_synthesis.cpp @@ -87,7 +87,7 @@ TEST_CASE("Synthesis of a or b", "[synthesis]") { } } -TEST_CASE("Synthesis of X\\[\\!\\] a", "[synthesis]") { +TEST_CASE("Synthesis of strongX a", "[synthesis]") { std::string formula = "X[!] a";