DRAFT: AO star (DO NOT MERGE YET)

libs/core/include/cynthia/core.hpp

@@ -48,72 +48,39 @@ bool is_realizable(const logic::ltlf_ptr& formula,
   return synthesis.is_realizable();
 }
 
-class ForwardSynthesis : public ISynthesis {
+class Context {
 public:
-  class Context {
-  public:
-    logic::ltlf_ptr formula;
-    logic::Context* ast_manager;
-    InputOutputPartition partition;
-    logic::ltlf_ptr nnf_formula;
-    logic::ltlf_ptr xnf_formula;
-    Closure closure_;
-    Statistics statistics_;
-    std::map<std::string, size_t> prop_to_id;
-    std::map<SddSize, bool> discovered;
-    Vtree* vtree_ = nullptr;
-    SddManager* manager = nullptr;
-    utils::Logger logger;
-    size_t indentation = 0;
-    Context(const logic::ltlf_ptr& formula,
-            const InputOutputPartition& partition);
-    ~Context() {
-      if (vtree_) {
-        sdd_vtree_free(vtree_);
-      }
-      if (manager) {
-        sdd_manager_free(manager);
-      }
-    }
-
-    logic::ltlf_ptr get_formula(size_t index) const {
-      if (index < closure_.nb_formulas()) {
-        return closure_.get_formula(index);
-      }
-      index -= closure_.nb_formulas();
-      if (index < partition.input_variables.size()) {
-        return ast_manager->make_atom(partition.input_variables[index]);
-      }
-      index -= partition.input_variables.size();
-      return ast_manager->make_atom(partition.output_variables[index]);
-    }
-  };
-  ForwardSynthesis(const logic::ltlf_ptr& formula,
-                   const InputOutputPartition& partition)
-      : context_{formula, partition}, ISynthesis(formula, partition){};
+  logic::ltlf_ptr formula;
+  logic::Context* ast_manager;
+  InputOutputPartition partition;
+  logic::ltlf_ptr nnf_formula;
+  logic::ltlf_ptr xnf_formula;
+  Closure closure_;
+  Statistics statistics_;
+  std::map<std::string, size_t> prop_to_id;
+  std::map<SddSize, bool> discovered;
+  Vtree* vtree_ = nullptr;
+  SddManager* manager = nullptr;
+  utils::Logger logger;
+  size_t indentation = 0;
+  Context(const logic::ltlf_ptr& formula,
+          const InputOutputPartition& partition);
+  ~Context();
 
+  logic::ltlf_ptr get_formula(size_t index) const;
   static std::map<std::string, size_t>
   compute_prop_to_id_map(const Closure& closure,
                          const InputOutputPartition& partition);
-  bool is_realizable() override;
 
-  bool forward_synthesis_();
-
-private:
-  Context context_;
   template <typename Arg1, typename... Args>
   inline void print_search_debug(const char* fmt, const Arg1& arg1,
                                  const Args&... args) {
-    context_.logger.debug(
-        (std::string(context_.indentation, '\t') + fmt).c_str(), arg1, args...);
+    logger.debug((std::string(indentation, '\t') + fmt).c_str(), arg1, args...);
   };
+
   inline void print_search_debug(const char* fmt) {
-    context_.logger.debug(
-        (std::string(context_.indentation, '\t') + fmt).c_str());
+    logger.debug((std::string(indentation, '\t') + fmt).c_str());
   };
-  strategy_t system_move_(const logic::ltlf_ptr& formula,
-                          std::set<SddSize>& path);
-  strategy_t env_move_(SddNodeWrapper& wrapper, std::set<SddSize>& path);
 };
 
 } // namespace core

libs/core/include/cynthia/sdd_to_formula.hpp

@@ -21,8 +21,7 @@
 namespace cynthia {
 namespace core {
 
-logic::ltlf_ptr sdd_to_formula(SddNode* sdd_node,
-                               ForwardSynthesis::Context& context_);
+logic::ltlf_ptr sdd_to_formula(SddNode* sdd_node, Context& context_);
 
 } // namespace core
 } // namespace cynthia

libs/core/include/cynthia/sddcpp.hpp

@@ -28,13 +28,13 @@ namespace cynthia {
 namespace core {
 
 class SddNodeChildrenIterator;
-class SddTransitionIterator;
 
 class SddNodeWrapper {
 private:
   SddNode* raw_{};
   SddNodeSize nb_children_ = 0;
   SddNode** children_ = nullptr;
+  SddNodeSize id;
 
 public:
   SddNodeWrapper() = default;
@@ -46,10 +46,12 @@ class SddNodeWrapper {
   bool is_decision() const;
   long node_literal() const;
   long nb_children() const;
+  bool at_vtree_root() const;
+  bool parent_at_vtree_root() const;
+  SddNodeSize get_id() const;
   SddNodeChildrenIterator begin() const;
+
   SddNodeChildrenIterator end() const;
-  SddTransitionIterator transitions_begin() const;
-  SddTransitionIterator transitions_end() const;
 };
 
 struct SddNodeChildrenIterator {

libs/core/include/cynthia/strategies/breadth_first.hpp

@@ -0,0 +1,190 @@
+#pragma once
+/*
+ * This file is part of Cynthia.
+ *
+ * Cynthia is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * Cynthia is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with Cynthia.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include <cynthia/core.hpp>
+#include <queue>
+
+namespace cynthia {
+namespace core {
+
+constexpr inline size_t infty() { return std::numeric_limits<size_t>::max(); }
+
+enum Label { SOLVED = 1, UNKNOWN = 0, FAILED = -1 };
+enum NodeType {
+  UNDEFINED = 0,
+  TERMINAL = 1,
+  AND = 2,
+  OR = 3,
+};
+
+enum SddNodeType {
+  STATE = 0,
+  ENV_STATE = 1,
+  SYSTEM_STATE = 2,
+  SYSTEM_ENV_STATE = 3,
+};
+
+class node_t;
+typedef std::shared_ptr<node_t> node_ptr;
+
+struct node_t {
+public:
+  size_t id;
+  SddNodeWrapper sdd_node;
+  SddNodeType sdd_node_type;
+  NodeType type;
+  Label label;
+  unsigned long f;
+  unsigned long f_new;
+  unsigned long f_old;
+
+  explicit node_t(const SddNodeWrapper& sdd_node, bool is_terminal = false) {
+    this->sdd_node = sdd_node;
+    id = sdd_node.get_id();
+    sdd_node_type = get_sdd_node_type_(sdd_node);
+    type = get_node_type_(sdd_node_type);
+    label = is_terminal ? Label::SOLVED : Label::UNKNOWN;
+    f = 0;
+  }
+
+  inline bool solved() const { return label == Label::SOLVED; }
+  inline bool failed() const { return label == Label::FAILED; }
+  inline bool is_cost_infinite() const {
+    return f == std::numeric_limits<size_t>::max();
+  }
+  inline void set_node_type(NodeType new_node_type) {
+    if (type != NodeType::UNDEFINED and type != new_node_type) {
+      throw std::logic_error("type already set");
+    }
+    type = new_node_type;
+  }
+
+private:
+  static inline NodeType get_node_type_(SddNodeType sdd_node_type) {
+    if (sdd_node_type == SYSTEM_ENV_STATE or sdd_node_type == SYSTEM_STATE) {
+      return NodeType::OR;
+    }
+    if (sdd_node_type == ENV_STATE) {
+      return NodeType::AND;
+    }
+    return NodeType::UNDEFINED;
+  }
+
+  static inline SddNodeType get_sdd_node_type_(const SddNodeWrapper& wrapper) {
+    if (!wrapper.is_decision()) {
+      return STATE;
+    } else if (!wrapper.at_vtree_root()) {
+      if (!wrapper.parent_at_vtree_root()) {
+        return STATE;
+      }
+      return ENV_STATE;
+    } else {
+      if (!SddNodeWrapper((wrapper.begin()).get_sub()).parent_at_vtree_root()) {
+        return SYSTEM_STATE;
+      }
+      return SYSTEM_ENV_STATE;
+    }
+  }
+};
+
+struct node_comparator {
+  size_t operator()(node_ptr const& a, node_ptr const& b) const {
+    return a->id < b->id;
+  }
+};
+
+struct graph_t {
+  std::map<size_t, node_ptr> id_to_node;
+  std::map<size_t, std::vector<size_t>> successors;
+  std::map<size_t, std::vector<size_t>> marked_successors;
+  std::map<size_t, std::set<size_t>> marked_predecessors;
+  std::queue<node_ptr> tips;
+  std::set<size_t> tip_set;
+
+  inline void add_node(const node_ptr& node) {
+    id_to_node[node->id] = node;
+    tips.push(node);
+    tip_set.insert(node->id);
+  }
+  inline void add_successors(size_t node_id,
+                             std::vector<size_t> node_successors) {
+    std::sort(node_successors.begin(), node_successors.end());
+    successors[node_id] = node_successors;
+  }
+
+  inline bool is_already_added(size_t node_id) const {
+    return id_to_node.find(node_id) != id_to_node.end();
+  }
+  inline bool has_next() const { return tips.empty(); }
+  inline bool is_tip(size_t node_id) const {
+    return tip_set.find(node_id) != tip_set.end();
+  }
+  inline node_ptr next() {
+    auto result = tips.front();
+    tips.pop();
+    tip_set.erase(result->id);
+    return result;
+  }
+  inline std::set<size_t> get_marked_predecessors(size_t node_id) const {
+    if (marked_predecessors.find(node_id) == marked_predecessors.end()) {
+      return {};
+    }
+    return marked_predecessors.at(node_id);
+  }
+  inline void mark_arc(const node_ptr& left, const node_ptr& right) {
+    if (left->type == NodeType::OR) {
+      auto left_marked_successors = marked_successors[left->id];
+      left_marked_successors.clear();
+      left_marked_successors.push_back(right->id);
+      // TODO
+    }
+  }
+};
+
+class BfsContext : public Context {
+public:
+  graph_t graph;
+  BfsContext(const logic::ltlf_ptr& formula,
+             const InputOutputPartition& partition)
+      : Context(formula, partition){};
+};
+
+class ForwardBfsSynthesis : public ISynthesis {
+public:
+  ForwardBfsSynthesis(const logic::ltlf_ptr& formula,
+                      const InputOutputPartition& partition)
+      : context_{formula, partition}, ISynthesis(formula, partition){};
+
+  bool is_realizable() override;
+
+  bool forward_synthesis_();
+  node_ptr get_state_node(const SddNodeWrapper& wrapper);
+  node_ptr get_env_node(const SddNodeWrapper& wrapper);
+  std::vector<node_ptr> get_successors(node_t& node);
+  static SddNodeType get_node_type(const SddNodeWrapper& wrapper);
+
+private:
+  BfsContext context_;
+
+  void build_revisable(size_t node, std::set<size_t>& z_set);
+  void init_open(size_t node, std::set<size_t>& o_set,
+                 const std::set<size_t>& z_set);
+};
+
+} // namespace core
+} // namespace cynthia

libs/core/include/cynthia/strategies/depth_first.hpp

@@ -0,0 +1,44 @@
+#pragma once
+/*
+ * This file is part of Cynthia.
+ *
+ * Cynthia is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * Cynthia is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with Cynthia.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include <cynthia/core.hpp>
+
+namespace cynthia {
+namespace core {
+
+class ForwardDfsSynthesis : public ISynthesis {
+public:
+  ForwardDfsSynthesis(const logic::ltlf_ptr& formula,
+                      const InputOutputPartition& partition)
+      : context_{formula, partition}, ISynthesis(formula, partition){};
+
+  bool is_realizable() override;
+
+  bool forward_synthesis_();
+
+private:
+  Context context_;
+
+  strategy_t system_move_(const logic::ltlf_ptr& formula,
+                          std::set<SddSize>& path);
+
+  strategy_t env_move_(SddNodeWrapper& wrapper, std::set<SddSize>& path);
+};
+
+} // namespace core
+} // namespace cynthia

libs/core/include/cynthia/to_sdd.hpp

@@ -24,12 +24,11 @@ namespace core {
 
 class ToSddVisitor : public logic::Visitor {
 private:
-  ForwardSynthesis::Context& context_;
+  Context& context_;
   SddNode* result{};
 
 public:
-  explicit ToSddVisitor(ForwardSynthesis::Context& context)
-      : context_{context} {}
+  explicit ToSddVisitor(Context& context) : context_{context} {}
   void visit(const logic::LTLfTrue&) override;
   void visit(const logic::LTLfFalse&) override;
   void visit(const logic::LTLfPropTrue&) override;
@@ -57,8 +56,7 @@ class ToSddVisitor : public logic::Visitor {
   }
 };
 
-SddNode* to_sdd(const logic::LTLfFormula& formula,
-                ForwardSynthesis::Context& context);
+SddNode* to_sdd(const logic::LTLfFormula& formula, Context& context);
 
 // returns an SDD node representing ( node1 => node2 )
 SddNode* sdd_imply(SddNode* node1, SddNode* node2, SddManager* manager);