Refuse plans that rest on a belief in a contradiction

dependency_repos.repos

@@ -7,6 +7,15 @@ repositories:
     type: git
     url: https://github.com/fmrico/popf.git
     version: rolling-devel
+  # The epistemic planner. plansys2_epistemic_planner links its planning core
+  # as a library, and its epistemic_planner binary is what
+  # plansys2_aletheia_plan_solver runs; colcon installs it into <prefix>/bin.
+  # Pinned to a commit, because the plugins validate and serialise plans with
+  # this library and a moving branch would change what they accept.
+  aletheia:
+    type: git
+    url: https://github.com/HanielUlises/del-planner.git
+    version: 314bc29f55ed8c0b62778b4b2954a55480a29428
   # The EPDDL grounder plansys2_epddl_grounder runs. It is a plain CMake
   # project rather than a ROS package, so colcon builds it as one and installs
   # the binary into <prefix>/bin, which puts `plank` on PATH once the workspace
@@ -15,15 +24,6 @@ repositories:
   #
   # Pinned like Aletheia above: grounding decides what the planner searches
   # over, so which grounder produced a task is part of what a release is.
-  # The epistemic planner. plansys2_epistemic_planner links its planning core
-  # as a library, and its epistemic_planner binary is what
-  # plansys2_aletheia_plan_solver runs; colcon installs it into <prefix>/bin.
-  # Pinned to a commit, because the plugins validate and serialise plans with
-  # this library and a moving branch would change what they accept.
-  aletheia:
-    type: git
-    url: https://github.com/HanielUlises/Aletheia.git
-    version: 32036843b1277f68f62b61aaa6fa58233894a779
   plank:
     type: git
     url: https://github.com/HanielUlises/plank.git

eplansys_docs/concepts/architecture.rst

@@ -98,7 +98,8 @@ are strings except where noted:
      - empty
      - Action-type libraries the domain declares. Empty supplies the
        ``intermediate`` library packaged with ``plansys2_epddl_grounder``.
-       This one is a string array; the rest are strings.
+       This one is a string array, ``consistent_beliefs`` is a boolean, and
+       the rest are strings.
    * - ``plank_command``
      - empty
      - Path to the plank binary. Empty takes ``$PLANK``, then PATH.
@@ -129,6 +130,12 @@ are strings except where noted:
      - What to do with a branching solution: ``policy``, ``flatten`` or
        ``reject``. The parameters file shipped by ``plansys2_bringup`` sets
        ``policy``.
+   * - ``consistent_beliefs``
+     - ``true``
+     - Refuses any state in which an agent believes a contradiction. An agent
+       that observes an event its beliefs rule out is left with no accessible
+       world, and every goal about what it believes then holds without it
+       believing anything. ``false`` accepts those plans, as plank does.
 
 The solver validates a solution before returning it, and a plan that fails
 validation is not returned at all.
@@ -161,10 +168,10 @@ file, runs a process under the solver timeout, and reads its output back.
          command: "/abs/path/to/epistemic_planner"
          conditional_plan: "policy"
 
-It adds three parameters to the six above: ``command``, the binary, which
+It adds three parameters to the seven above: ``command``, the binary, which
 defaults to ``epistemic_planner`` on the path; ``arguments``, appended
 verbatim; and ``output_dir``, where the task, the plan and the planner's log
-are written. The other six keep their names and meanings, so a parameters file
+are written. The other seven keep their names and meanings, so a parameters file
 moves between the two plugins by changing ``plugin`` alone.
 
 The plan file names actions and event indices only. What a branch is taken on,

eplansys_docs/concepts/epistemic_models.rst

@@ -213,8 +213,9 @@ accepts:
 
 The search records why branches were discarded, not merely how many.
 ``PlannerStats`` separates dead ends, duplicates, updates rejected by the world
-cap, updates whose designated set was emptied by KD45 seriality repair, and
-truly inapplicable actions. Only the last is a property of the domain, and
+cap, updates whose designated set was emptied by KD45 seriality repair,
+updates refused because an agent was left believing a contradiction, and truly
+inapplicable actions. Only the last is a property of the domain, and
 collapsing them makes a failed run unreadable.
 
 Selection policy

plansys2_aletheia_plan_solver/README.md

@@ -64,6 +64,7 @@ failure mode a separately built planner introduces.
 | `policy_file` | empty | selection-policy JSON overriding the planner's built-in rules |
 | `action_mapping` | empty | JSON map from grounded names to PlanSys2 action expressions |
 | `conditional_plan` | `flatten` | `policy`, `flatten` or `reject` |
+| `consistent_beliefs` | `true` | passes `--consistent-beliefs`, refusing any state in which an agent believes a contradiction |
 
 The last six are the in-process plugin's parameters under the same names, so a
 parameters file moves between the two plugins by changing `plugin:` alone.

plansys2_aletheia_plan_solver/include/plansys2_aletheia_plan_solver/aletheia_plan_solver.hpp

@@ -156,6 +156,7 @@ class AletheiaPlanSolver : public PlanSolverBase
     std::string & error) const;
 
   std::string parameter(const std::string & name) const;
+  bool consistent_beliefs() const;
 
   std::string command_parameter_name_;
   std::string arguments_parameter_name_;
@@ -166,6 +167,7 @@ class AletheiaPlanSolver : public PlanSolverBase
   std::string policy_file_parameter_name_;
   std::string action_mapping_parameter_name_;
   std::string conditional_parameter_name_;
+  std::string consistent_beliefs_parameter_name_;
 };
 
 }  // namespace plansys2

plansys2_aletheia_plan_solver/src/plansys2_aletheia_plan_solver/aletheia_plan_solver.cpp

@@ -235,6 +235,7 @@ void AletheiaPlanSolver::configure(
   policy_file_parameter_name_ = plugin_name + ".policy_file";
   action_mapping_parameter_name_ = plugin_name + ".action_mapping";
   conditional_parameter_name_ = plugin_name + ".conditional_plan";
+  consistent_beliefs_parameter_name_ = plugin_name + ".consistent_beliefs";
 
   const auto declare = [&](const std::string & name, const std::string & def) {
       if (!lc_node_->has_parameter(name)) {
@@ -251,6 +252,18 @@ void AletheiaPlanSolver::configure(
   declare(policy_file_parameter_name_, "");
   declare(action_mapping_parameter_name_, "");   // empty: naming convention
   declare(conditional_parameter_name_, "flatten");
+
+  // On by default, as in plansys2_epistemic_planner: a robot whose beliefs
+  // collapse satisfies every goal about them.
+  if (!lc_node_->has_parameter(consistent_beliefs_parameter_name_)) {
+    lc_node_->declare_parameter<bool>(consistent_beliefs_parameter_name_, true);
+  }
+}
+
+bool AletheiaPlanSolver::consistent_beliefs() const
+{
+  return lc_node_ && lc_node_->has_parameter(consistent_beliefs_parameter_name_) &&
+         lc_node_->get_parameter(consistent_beliefs_parameter_name_).as_bool();
 }
 
 std::string AletheiaPlanSolver::parameter(const std::string & name) const
@@ -369,6 +382,10 @@ std::string AletheiaPlanSolver::build_command(
   // solution rather than being killed mid-write.
   cmd << " --timeout " << static_cast<std::int64_t>(solver_timeout.seconds());
 
+  if (consistent_beliefs()) {
+    cmd << " --consistent-beliefs";
+  }
+
   const auto arguments = parameter(arguments_parameter_name_);
   if (!arguments.empty()) {
     cmd << " " << arguments;
@@ -413,6 +430,7 @@ std::optional<plansys2_msgs::msg::Plan> AletheiaPlanSolver::getPlan(
       task_path->string().c_str(), e.what());
     return std::nullopt;
   }
+  task.consistent_beliefs = consistent_beliefs();
 
   ActionMapping mapping = ActionMapping::conventional();
   const auto mapping_file = parameter(action_mapping_parameter_name_);

plansys2_aletheia_plan_solver/test/unit/fleet_solver_test.cpp

@@ -160,6 +160,36 @@ TEST_F(FleetSolverTest, TheInProcessPluginReturnsTheSamePolicy)
   }
 }
 
+// coin4's shortest plan works because B hears A announce what B believes A
+// cannot know, and is left believing everything, the goal included. With
+// consistent_beliefs on, which is the default, both plugins refuse that and
+// find the plan in which B and C look for themselves; off, both return the
+// short one plank would accept.
+TEST_F(FleetSolverTest, BothPluginsKeepBeliefsConsistentUnlessToldOtherwise)
+{
+  plansys2::EpistemicPlanSolver in_process;
+  in_process.configure(node_, "EPISTEMIC");
+  node_->set_parameter(rclcpp::Parameter("ALETHEIA.task_file", task("coin-in-the-box-4")));
+  node_->set_parameter(rclcpp::Parameter("EPISTEMIC.task_file", task("coin-in-the-box-4")));
+
+  for (const bool consistent : {true, false}) {
+    SCOPED_TRACE(consistent ? "consistent_beliefs on" : "consistent_beliefs off");
+    node_->set_parameter(rclcpp::Parameter("ALETHEIA.consistent_beliefs", consistent));
+    node_->set_parameter(rclcpp::Parameter("EPISTEMIC.consistent_beliefs", consistent));
+
+    const auto through_binary = solver_.getPlan("", "");
+    if (!through_binary) {
+      GTEST_SKIP() << "the epistemic_planner binary is not available";
+    }
+    const auto linked = in_process.getPlan("", "");
+    ASSERT_TRUE(linked.has_value());
+
+    const std::size_t steps = consistent ? 9u : 6u;
+    EXPECT_EQ(through_binary->items.size(), steps);
+    EXPECT_EQ(linked->items.size(), steps);
+  }
+}
+
 // Leave through _exit, so the DDS threads never outlive the process.
 //
 // rclcpp::shutdown() does not finalise the global context; that happens in

plansys2_epistemic_executor/include/plansys2_epistemic_executor/EpistemicStateNode.hpp

@@ -142,6 +142,13 @@ class EpistemicStateNode : public rclcpp_lifecycle::LifecycleNode
   /// state without polling a service on every change.
   void publish_state();
 
+  /// How the tracked model takes an action: repaired on a KD45 task, as it
+  /// always was, and never refused, since what it records has already happened.
+  Seriality tracked_seriality() const
+  {
+    return task_->kd45 ? Seriality::Repair : Seriality::Ignore;
+  }
+
   rclcpp::Service<plansys2_epistemic_msgs::srv::LoadTask>::SharedPtr load_task_service_;
   rclcpp::Service<plansys2_epistemic_msgs::srv::CheckFormula>::SharedPtr check_formula_service_;
   rclcpp::Service<plansys2_epistemic_msgs::srv::ApplyAction>::SharedPtr apply_action_service_;

plansys2_epistemic_executor/src/plansys2_epistemic_executor/EpistemicStateNode.cpp

@@ -762,7 +762,7 @@ void EpistemicStateNode::apply_action_callback(
   }
 
   if (action.is_ontic()) {
-    auto updated = product_update(*state_, action, task_->kd45);
+    auto updated = product_update(*state_, action, tracked_seriality());
     if (!updated) {
       response->success = false;
       response->error =
@@ -775,7 +775,7 @@ void EpistemicStateNode::apply_action_callback(
     response->outcome = "";   // an ontic action has nothing to observe
     applied_outcomes_[request->epistemic_action] = "";
   } else {
-    auto outcomes = product_update_split(*state_, action, task_->kd45);
+    auto outcomes = product_update_split(*state_, action, tracked_seriality());
     if (outcomes.empty()) {
       response->success = false;
       response->error = "the sensing action produced no outcome at all";
@@ -810,7 +810,7 @@ void EpistemicStateNode::apply_action_callback(
 
         std::string gave_up;
         if (target && redesignate_for_event(*state_, *target, gave_up)) {
-          outcomes = product_update_split(*state_, action, task_->kd45);
+          outcomes = product_update_split(*state_, action, tracked_seriality());
           for (std::size_t i = 0; i < outcomes.size(); ++i) {
             if (outcomes[i].first < action.events.size() &&
               action.events[outcomes[i].first].name == request->observed_outcome)

plansys2_epistemic_planner/include/plansys2_epistemic_planner/epistemic_plan_solver.hpp

@@ -171,6 +171,7 @@ class EpistemicPlanSolver : public PlanSolverBase
 
   std::string goal_from_state_parameter_name_;
   std::string initial_from_state_parameter_name_;
+  std::string consistent_beliefs_parameter_name_;
 
   /// The last goal the epistemic state published, as text. Latched by the
   /// subscription rather than fetched, so reading it costs nothing and cannot

plansys2_epistemic_planner/src/epistemic_plan_solver.cpp

@@ -183,6 +183,7 @@ void EpistemicPlanSolver::configure(
   epddl_parameter_names_ = EpddlParameterNames(plugin_name);
   goal_from_state_parameter_name_ = plugin_name + ".goal_from_state";
   initial_from_state_parameter_name_ = plugin_name + ".initial_from_state";
+  consistent_beliefs_parameter_name_ = plugin_name + ".consistent_beliefs";
 
   const auto declare = [&](const std::string & name, const std::string & def) {
       if (!lc_node_->has_parameter(name)) {
@@ -203,6 +204,11 @@ void EpistemicPlanSolver::configure(
   if (!lc_node_->has_parameter(initial_from_state_parameter_name_)) {
     lc_node_->declare_parameter<bool>(initial_from_state_parameter_name_, true);
   }
+  // On by default: a robot whose beliefs collapse satisfies every goal about
+  // them, and a policy credited that way has nothing to execute.
+  if (!lc_node_->has_parameter(consistent_beliefs_parameter_name_)) {
+    lc_node_->declare_parameter<bool>(consistent_beliefs_parameter_name_, true);
+  }
 
   declare_epddl_parameters(lc_node_, epddl_parameter_names_);
 
@@ -423,6 +429,8 @@ std::optional<plansys2_msgs::msg::Plan> EpistemicPlanSolver::getPlan(
       task_opt->symmetry = std::move(symmetry);
     }
   }
+  task_opt->consistent_beliefs =
+    lc_node_->get_parameter(consistent_beliefs_parameter_name_).as_bool();
   const PlanningTask & task = *task_opt;
 
   // Selection policy: explicit parameters win, otherwise the rule table

plansys2_epistemic_planner/test/state_json_test.cpp

@@ -88,7 +88,9 @@ TEST(StateJsonTest, AModelAdvancedByAnActionSurvivesTheRoundTrip)
     if (!action.applicable(task.init)) {
       continue;
     }
-    auto result = product_update(task.init, action, task.kd45);
+    auto result = product_update(
+      task.init, action,
+      task.kd45 ? Seriality::Repair : Seriality::Ignore);
     if (!result) {
       continue;   // capped or pruned; another action will do
     }

plansys2_epistemic_planner/test/tasks/README.md

@@ -16,6 +16,7 @@ tests assert).
 | `muddy-children-2.json` | `muddy-children/out/muddy-children-problem.json` | smallest solvable task; the default for search tests |
 | `muddy-children-3.json` | `muddy-children/out/muddy-children-problem-3.json` | asymmetric variant, used for the determinism check |
 | `coin-in-the-box.json` | `coin-in-the-box/out/problem_1.json` | sensing domain with a `box` (not `Kw`) goal |
+| `coin-in-the-box-4.json` | del-planner `benchmarks/coin4/problem_4.json` | its shortest plan leaves B believing a contradiction; the `consistent_beliefs` test |
 | `active-muddy-child.json` | `Active-Muddy-Child/out/problem_1.json` | 32 initial worlds; the canonical partial-observability case |
 | `coin-in-the-box-multipointed.json` | derived, see below | hand-made branching fixture, kept for the parser tests |