Gr1

.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

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))))));
+  }
+
+}

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)))

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

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)))

example/GR1benchmarks/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);
+  }
+
+}

example/GR1benchmarks/tcp_handshake_agn_safety.ltlf

@@ -0,0 +1 @@
+(G !(syn_ack) -> G !(ack))

example/GR1benchmarks/tcp_handshake_env_gr1.txt

@@ -0,0 +1,7 @@
+--Env-Justice--
+syn
+--Justice-End--
+--Agn-Justice--
+syn_ack
+--Justice-End--
+End

example/GR1benchmarks/tcp_handshake_env_safety.ltlf

@@ -0,0 +1 @@
+(G !(syn) -> G !(syn_ack))

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 <fstream>
+#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<CUDD::BDD> env_justices;
+        std::vector<CUDD::BDD> agn_justices;
+        /**
+         * \brief Stores a player justice
+         */
+        static CUDD::BDD read_gr1_justice(std::shared_ptr<VarMgr>& 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<std::string> tokens;
+                    trim(line); // remove leading and trailing whitespace
+                    tokens = split(line, " ");
+                    std::vector<std::string> 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<VarMgr>& 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

src/synthesis/header/GR1ReachabilitySynthesizer.h

@@ -0,0 +1,121 @@
+//
+// 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<VarMgr> 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();
+
+        std::string slugs_dir_;
+
+        /**
+         * \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;
+
+        /**
+         * Get the path to the SLUGS binary.
+         *
+         * @return the path to the SLUGS binary.
+         */
+        std::string get_slugs_path();
+
+    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
+         * \param slugs_dir  The root directory of the SLUGS project
+         *
+         */
+        GR1ReachabilitySynthesizer(std::shared_ptr<VarMgr> var_mgr, GR1 gr1, SymbolicStateDfa env_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);
+
+        /**
+         * \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

src/synthesis/header/SymbolicStateDfa.h

@@ -148,6 +148,8 @@ class SymbolicStateDfa {
 
   static std::vector<int> state_to_binary(std::size_t state,
                                             std::size_t bit_count);
+
+    void new_sink_states(const CUDD::BDD& sink_states);
 };
 
 }

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;
 
 };