fix: handling of path to Slugs root directory

whitemech · Jan 22, 2024 · e51edd2 · e51edd2
1 parent ba502b9
commit e51edd2
Show file tree

Hide file tree

Showing 4 changed files with 22 additions and 10 deletions.
diff --git 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<VarMgr> 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
@@ -9,9 +9,9 @@
 namespace Syft {
 
     GR1ReachabilitySynthesizer::GR1ReachabilitySynthesizer(std::shared_ptr<VarMgr> 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,16 +252,16 @@ 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<<run_slugs_parser;
         system(run_slugs_parser.c_str());
 
         std::string detele_to_slugs_parser = "rm "+to_slugs_parser;
         system(detele_to_slugs_parser.c_str());
 
-        std::string slugs= "./slugs";
+        std::string slugs= get_slugs_path();
         std::string slugs_strategy_file= benchmark_name+".strategy";
         std::string slugs_res_file= benchmark_name+".res";
         std::string slugs_result = exec_slugs(slugs, slugs_input_file, slugs_res_file, slugs_strategy_file);
@@ -283,6 +283,9 @@ namespace Syft {
         return result;
     }
 
+    std::string GR1ReachabilitySynthesizer::get_slugs_path() {
+        return slugs_dir_ + "/src/slugs";
+    }
 
 
 }
diff --git a/test/test_gr1reachability_synthesis.cpp b/test/test_gr1reachability_synthesis.cpp
@@ -98,7 +98,7 @@ TEST_CASE("GR1 Synthesis test", "[gr1 synthesis]") {
 
 
     Syft::GR1ReachabilitySynthesizer synthesizer(var_mgr, gr1, symbolic_dfa_env_safety,
-                                         symbolic_dfa_agn_goal, symbolic_dfa_agn_safety);
+                                         symbolic_dfa_agn_goal, symbolic_dfa_agn_safety, Syft::Test::SLUGS_DIR_LOCATION);
 
     std::string benchmark_name = "hand_shake";
     Syft::SynthesisResult result = synthesizer.run(benchmark_name);
@@ -190,7 +190,7 @@ TEST_CASE("GR1 Synthesis finding_nemo", "[gr1 synthesis]") {
 
 
     Syft::GR1ReachabilitySynthesizer synthesizer(var_mgr, gr1, symbolic_dfa_env_safety,
-                                                 symbolic_dfa_agn_goal, symbolic_dfa_agn_safety);
+                                                 symbolic_dfa_agn_goal, symbolic_dfa_agn_safety, Syft::Test::SLUGS_DIR_LOCATION);
 
     std::string benchmark_name = "finding_nemo";
 

diff --git a/test/utils.hpp b/test/utils.hpp
@@ -16,6 +16,7 @@ namespace Syft::Test {
 
   static std::string ROOT_DIRECTORY = __ROOT_DIRECTORY;
   static std::string SYFCO_LOCATION = ROOT_DIRECTORY + "/syfco";
+  static std::string SLUGS_DIR_LOCATION = ROOT_DIRECTORY + "/submodules/slugs";
   static std::string EXAMPLE_TEST_TLSF = ROOT_DIRECTORY + "/example/test.tlsf";
   static std::string EXAMPLE_001_TLSF = ROOT_DIRECTORY + "/example/001.tlsf";
   static std::string DATASET_FOLDER = ROOT_DIRECTORY + "/example/TLSF";