From d8199ed97b50a41393e615fa4dbe2db1570031c5 Mon Sep 17 00:00:00 2001 From: HanielUlises Date: Mon, 28 Sep 2026 09:37:09 -0600 Subject: [PATCH 1/2] Pin del-planner at the merge of its belief check --- dependency_repos.repos | 18 +++++++++--------- .../EpistemicStateNode.hpp | 7 +++++++ .../EpistemicStateNode.cpp | 6 +++--- .../test/state_json_test.cpp | 4 +++- 4 files changed, 22 insertions(+), 13 deletions(-) diff --git a/dependency_repos.repos b/dependency_repos.repos index bc52fc43..ad5c3cb1 100644 --- a/dependency_repos.repos +++ b/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 /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 /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 /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 diff --git a/plansys2_epistemic_executor/include/plansys2_epistemic_executor/EpistemicStateNode.hpp b/plansys2_epistemic_executor/include/plansys2_epistemic_executor/EpistemicStateNode.hpp index c754fa24..3db17813 100644 --- a/plansys2_epistemic_executor/include/plansys2_epistemic_executor/EpistemicStateNode.hpp +++ b/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::SharedPtr load_task_service_; rclcpp::Service::SharedPtr check_formula_service_; rclcpp::Service::SharedPtr apply_action_service_; diff --git a/plansys2_epistemic_executor/src/plansys2_epistemic_executor/EpistemicStateNode.cpp b/plansys2_epistemic_executor/src/plansys2_epistemic_executor/EpistemicStateNode.cpp index 9ad31065..95b25706 100644 --- a/plansys2_epistemic_executor/src/plansys2_epistemic_executor/EpistemicStateNode.cpp +++ b/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) diff --git a/plansys2_epistemic_planner/test/state_json_test.cpp b/plansys2_epistemic_planner/test/state_json_test.cpp index af5fc64c..2bf171ee 100644 --- a/plansys2_epistemic_planner/test/state_json_test.cpp +++ b/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 } From 3e3c32d0c672424aa47728750e724c7d4905af18 Mon Sep 17 00:00:00 2001 From: HanielUlises Date: Mon, 28 Sep 2026 09:37:09 -0600 Subject: [PATCH 2/2] Refuse plans that rest on a belief in a contradiction --- eplansys_docs/concepts/architecture.rst | 13 +- eplansys_docs/concepts/epistemic_models.rst | 5 +- plansys2_aletheia_plan_solver/README.md | 1 + .../aletheia_plan_solver.hpp | 2 + .../aletheia_plan_solver.cpp | 18 + .../test/unit/fleet_solver_test.cpp | 30 + .../epistemic_plan_solver.hpp | 1 + .../src/epistemic_plan_solver.cpp | 8 + .../test/tasks/README.md | 1 + .../test/tasks/coin-in-the-box-4.json | 2483 +++++++++++++++++ 10 files changed, 2557 insertions(+), 5 deletions(-) create mode 100644 plansys2_epistemic_planner/test/tasks/coin-in-the-box-4.json diff --git a/eplansys_docs/concepts/architecture.rst b/eplansys_docs/concepts/architecture.rst index 12f12020..f364b510 100644 --- a/eplansys_docs/concepts/architecture.rst +++ b/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, diff --git a/eplansys_docs/concepts/epistemic_models.rst b/eplansys_docs/concepts/epistemic_models.rst index b0963086..f45d7181 100644 --- a/eplansys_docs/concepts/epistemic_models.rst +++ b/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 diff --git a/plansys2_aletheia_plan_solver/README.md b/plansys2_aletheia_plan_solver/README.md index 001e6cae..2fa03247 100644 --- a/plansys2_aletheia_plan_solver/README.md +++ b/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. diff --git a/plansys2_aletheia_plan_solver/include/plansys2_aletheia_plan_solver/aletheia_plan_solver.hpp b/plansys2_aletheia_plan_solver/include/plansys2_aletheia_plan_solver/aletheia_plan_solver.hpp index a8bba4b8..68a03c0f 100644 --- a/plansys2_aletheia_plan_solver/include/plansys2_aletheia_plan_solver/aletheia_plan_solver.hpp +++ b/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 diff --git a/plansys2_aletheia_plan_solver/src/plansys2_aletheia_plan_solver/aletheia_plan_solver.cpp b/plansys2_aletheia_plan_solver/src/plansys2_aletheia_plan_solver/aletheia_plan_solver.cpp index d668acc7..6586b1ab 100644 --- a/plansys2_aletheia_plan_solver/src/plansys2_aletheia_plan_solver/aletheia_plan_solver.cpp +++ b/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(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(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 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_); diff --git a/plansys2_aletheia_plan_solver/test/unit/fleet_solver_test.cpp b/plansys2_aletheia_plan_solver/test/unit/fleet_solver_test.cpp index 893f04ff..9639ecf0 100644 --- a/plansys2_aletheia_plan_solver/test/unit/fleet_solver_test.cpp +++ b/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 diff --git a/plansys2_epistemic_planner/include/plansys2_epistemic_planner/epistemic_plan_solver.hpp b/plansys2_epistemic_planner/include/plansys2_epistemic_planner/epistemic_plan_solver.hpp index e26e35a9..c274c159 100644 --- a/plansys2_epistemic_planner/include/plansys2_epistemic_planner/epistemic_plan_solver.hpp +++ b/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 diff --git a/plansys2_epistemic_planner/src/epistemic_plan_solver.cpp b/plansys2_epistemic_planner/src/epistemic_plan_solver.cpp index d23f777a..0df9cc3f 100644 --- a/plansys2_epistemic_planner/src/epistemic_plan_solver.cpp +++ b/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(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(consistent_beliefs_parameter_name_, true); + } declare_epddl_parameters(lc_node_, epddl_parameter_names_); @@ -423,6 +429,8 @@ std::optional 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 diff --git a/plansys2_epistemic_planner/test/tasks/README.md b/plansys2_epistemic_planner/test/tasks/README.md index fa1ecaf5..8fd79390 100644 --- a/plansys2_epistemic_planner/test/tasks/README.md +++ b/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 | diff --git a/plansys2_epistemic_planner/test/tasks/coin-in-the-box-4.json b/plansys2_epistemic_planner/test/tasks/coin-in-the-box-4.json new file mode 100644 index 00000000..08ed7e27 --- /dev/null +++ b/plansys2_epistemic_planner/test/tasks/coin-in-the-box-4.json @@ -0,0 +1,2483 @@ +{ + "planning-task-info": { + "problem": "cb-4", + "domain": "coin-in-the-box", + "libraries": [ + "intermediate" + ], + "requirements": [ + ":common-knowledge", + ":disjunctive-goals", + ":disjunctive-list-formulas", + ":disjunctive-preconditions", + ":equality", + ":events-conditions", + ":finitary-S5-theories", + ":group-modalities", + ":knowing-whether", + ":list-comprehensions", + ":lists", + ":modal-goals", + ":modal-preconditions", + ":multi-pointed-models", + ":negative-goals", + ":negative-list-formulas", + ":negative-preconditions", + ":ontic-actions", + ":partial-observability", + ":static-common-knowledge", + ":universal-preconditions" + ], + "agents-number": 3, + "atoms-number": 8, + "facts-number": 0, + "actions-number": 21, + "initial-worlds-number": 2, + "goal-modal-depth": 2, + "goal-size": 11 + }, + "language": { + "atoms": [ + "has-key_A", + "has-key_B", + "has-key_C", + "looking_A", + "looking_B", + "looking_C", + "opened", + "tails" + ], + "agents": [ + "A", + "B", + "C" + ] + }, + "facts": [], + "initial-state": { + "worlds": [ + "w0", + "w1" + ], + "relations": { + "A": { + "w0": [ + "w0", + "w1" + ], + "w1": [ + "w0", + "w1" + ] + }, + "B": { + "w0": [ + "w0", + "w1" + ], + "w1": [ + "w0", + "w1" + ] + }, + "C": { + "w0": [ + "w0", + "w1" + ], + "w1": [ + "w0", + "w1" + ] + } + }, + "labels": { + "w0": [ + "has-key_A", + "looking_A" + ], + "w1": [ + "has-key_A", + "looking_A", + "tails" + ] + }, + "designated": [ + "w1" + ] + }, + "actions": { + "open_A": { + "action-type": "private-ontic", + "events": [ + "e-open", + "nil" + ], + "relations": { + "Fully": { + "e-open": [ + "e-open" + ], + "nil": [ + "nil" + ] + }, + "Oblivious": { + "e-open": [ + "nil" + ], + "nil": [ + "nil" + ] + } + }, + "designated": [ + "e-open" + ], + "preconditions": { + "e-open": { + "formula": { + "connective": "and", + "formulas": [ + { + "connective": "not", + "formula": "opened" + }, + "looking_A", + "has-key_A" + ] + } + }, + "nil": { + "formula": "true" + } + }, + "effects": { + "e-open": { + "opened": { + "formula": "true" + } + }, + "nil": null + }, + "observability-conditions": { + "A": { + "Fully": { + "formula": "true" + } + }, + "B": { + "Fully": { + "formula": "looking_B" + }, + "Oblivious": { + "formula": { + "connective": "not", + "formula": "looking_B" + } + } + }, + "C": { + "Fully": { + "formula": "looking_C" + }, + "Oblivious": { + "formula": { + "connective": "not", + "formula": "looking_C" + } + } + } + } + }, + "open_B": { + "action-type": "private-ontic", + "events": [ + "e-open", + "nil" + ], + "relations": { + "Fully": { + "e-open": [ + "e-open" + ], + "nil": [ + "nil" + ] + }, + "Oblivious": { + "e-open": [ + "nil" + ], + "nil": [ + "nil" + ] + } + }, + "designated": [ + "e-open" + ], + "preconditions": { + "e-open": { + "formula": { + "connective": "and", + "formulas": [ + { + "connective": "not", + "formula": "opened" + }, + "looking_B", + "has-key_B" + ] + } + }, + "nil": { + "formula": "true" + } + }, + "effects": { + "e-open": { + "opened": { + "formula": "true" + } + }, + "nil": null + }, + "observability-conditions": { + "A": { + "Fully": { + "formula": "looking_A" + }, + "Oblivious": { + "formula": { + "connective": "not", + "formula": "looking_A" + } + } + }, + "B": { + "Fully": { + "formula": "true" + } + }, + "C": { + "Fully": { + "formula": "looking_C" + }, + "Oblivious": { + "formula": { + "connective": "not", + "formula": "looking_C" + } + } + } + } + }, + "open_C": { + "action-type": "private-ontic", + "events": [ + "e-open", + "nil" + ], + "relations": { + "Fully": { + "e-open": [ + "e-open" + ], + "nil": [ + "nil" + ] + }, + "Oblivious": { + "e-open": [ + "nil" + ], + "nil": [ + "nil" + ] + } + }, + "designated": [ + "e-open" + ], + "preconditions": { + "e-open": { + "formula": { + "connective": "and", + "formulas": [ + { + "connective": "not", + "formula": "opened" + }, + "looking_C", + "has-key_C" + ] + } + }, + "nil": { + "formula": "true" + } + }, + "effects": { + "e-open": { + "opened": { + "formula": "true" + } + }, + "nil": null + }, + "observability-conditions": { + "A": { + "Fully": { + "formula": "looking_A" + }, + "Oblivious": { + "formula": { + "connective": "not", + "formula": "looking_A" + } + } + }, + "B": { + "Fully": { + "formula": "looking_B" + }, + "Oblivious": { + "formula": { + "connective": "not", + "formula": "looking_B" + } + } + }, + "C": { + "Fully": { + "formula": "true" + } + } + } + }, + "signal_A_B": { + "action-type": "private-ontic", + "events": [ + "e-signal", + "nil" + ], + "relations": { + "Fully": { + "e-signal": [ + "e-signal" + ], + "nil": [ + "nil" + ] + }, + "Oblivious": { + "e-signal": [ + "nil" + ], + "nil": [ + "nil" + ] + } + }, + "designated": [ + "e-signal" + ], + "preconditions": { + "e-signal": { + "formula": { + "connective": "and", + "formulas": [ + "looking_A", + { + "connective": "not", + "formula": "looking_B" + }, + { + "modality-name": "box", + "modality-index": [ + "A", + "B" + ], + "formula": { + "connective": "and", + "formulas": [ + "looking_A", + { + "connective": "not", + "formula": "looking_B" + } + ] + } + } + ] + } + }, + "nil": { + "formula": "true" + } + }, + "effects": { + "e-signal": { + "looking_B": { + "formula": "true" + } + }, + "nil": null + }, + "observability-conditions": { + "A": { + "Fully": { + "formula": "true" + } + }, + "B": { + "Fully": { + "formula": "true" + } + }, + "C": { + "Oblivious": { + "formula": "true" + } + } + } + }, + "signal_A_C": { + "action-type": "private-ontic", + "events": [ + "e-signal", + "nil" + ], + "relations": { + "Fully": { + "e-signal": [ + "e-signal" + ], + "nil": [ + "nil" + ] + }, + "Oblivious": { + "e-signal": [ + "nil" + ], + "nil": [ + "nil" + ] + } + }, + "designated": [ + "e-signal" + ], + "preconditions": { + "e-signal": { + "formula": { + "connective": "and", + "formulas": [ + "looking_A", + { + "connective": "not", + "formula": "looking_C" + }, + { + "modality-name": "box", + "modality-index": [ + "A", + "C" + ], + "formula": { + "connective": "and", + "formulas": [ + "looking_A", + { + "connective": "not", + "formula": "looking_C" + } + ] + } + } + ] + } + }, + "nil": { + "formula": "true" + } + }, + "effects": { + "e-signal": { + "looking_C": { + "formula": "true" + } + }, + "nil": null + }, + "observability-conditions": { + "A": { + "Fully": { + "formula": "true" + } + }, + "B": { + "Oblivious": { + "formula": "true" + } + }, + "C": { + "Fully": { + "formula": "true" + } + } + } + }, + "signal_B_A": { + "action-type": "private-ontic", + "events": [ + "e-signal", + "nil" + ], + "relations": { + "Fully": { + "e-signal": [ + "e-signal" + ], + "nil": [ + "nil" + ] + }, + "Oblivious": { + "e-signal": [ + "nil" + ], + "nil": [ + "nil" + ] + } + }, + "designated": [ + "e-signal" + ], + "preconditions": { + "e-signal": { + "formula": { + "connective": "and", + "formulas": [ + "looking_B", + { + "connective": "not", + "formula": "looking_A" + }, + { + "modality-name": "box", + "modality-index": [ + "B", + "A" + ], + "formula": { + "connective": "and", + "formulas": [ + "looking_B", + { + "connective": "not", + "formula": "looking_A" + } + ] + } + } + ] + } + }, + "nil": { + "formula": "true" + } + }, + "effects": { + "e-signal": { + "looking_A": { + "formula": "true" + } + }, + "nil": null + }, + "observability-conditions": { + "A": { + "Fully": { + "formula": "true" + } + }, + "B": { + "Fully": { + "formula": "true" + } + }, + "C": { + "Oblivious": { + "formula": "true" + } + } + } + }, + "signal_B_C": { + "action-type": "private-ontic", + "events": [ + "e-signal", + "nil" + ], + "relations": { + "Fully": { + "e-signal": [ + "e-signal" + ], + "nil": [ + "nil" + ] + }, + "Oblivious": { + "e-signal": [ + "nil" + ], + "nil": [ + "nil" + ] + } + }, + "designated": [ + "e-signal" + ], + "preconditions": { + "e-signal": { + "formula": { + "connective": "and", + "formulas": [ + "looking_B", + { + "connective": "not", + "formula": "looking_C" + }, + { + "modality-name": "box", + "modality-index": [ + "B", + "C" + ], + "formula": { + "connective": "and", + "formulas": [ + "looking_B", + { + "connective": "not", + "formula": "looking_C" + } + ] + } + } + ] + } + }, + "nil": { + "formula": "true" + } + }, + "effects": { + "e-signal": { + "looking_C": { + "formula": "true" + } + }, + "nil": null + }, + "observability-conditions": { + "A": { + "Oblivious": { + "formula": "true" + } + }, + "B": { + "Fully": { + "formula": "true" + } + }, + "C": { + "Fully": { + "formula": "true" + } + } + } + }, + "signal_C_A": { + "action-type": "private-ontic", + "events": [ + "e-signal", + "nil" + ], + "relations": { + "Fully": { + "e-signal": [ + "e-signal" + ], + "nil": [ + "nil" + ] + }, + "Oblivious": { + "e-signal": [ + "nil" + ], + "nil": [ + "nil" + ] + } + }, + "designated": [ + "e-signal" + ], + "preconditions": { + "e-signal": { + "formula": { + "connective": "and", + "formulas": [ + "looking_C", + { + "connective": "not", + "formula": "looking_A" + }, + { + "modality-name": "box", + "modality-index": [ + "C", + "A" + ], + "formula": { + "connective": "and", + "formulas": [ + "looking_C", + { + "connective": "not", + "formula": "looking_A" + } + ] + } + } + ] + } + }, + "nil": { + "formula": "true" + } + }, + "effects": { + "e-signal": { + "looking_A": { + "formula": "true" + } + }, + "nil": null + }, + "observability-conditions": { + "A": { + "Fully": { + "formula": "true" + } + }, + "B": { + "Oblivious": { + "formula": "true" + } + }, + "C": { + "Fully": { + "formula": "true" + } + } + } + }, + "signal_C_B": { + "action-type": "private-ontic", + "events": [ + "e-signal", + "nil" + ], + "relations": { + "Fully": { + "e-signal": [ + "e-signal" + ], + "nil": [ + "nil" + ] + }, + "Oblivious": { + "e-signal": [ + "nil" + ], + "nil": [ + "nil" + ] + } + }, + "designated": [ + "e-signal" + ], + "preconditions": { + "e-signal": { + "formula": { + "connective": "and", + "formulas": [ + "looking_C", + { + "connective": "not", + "formula": "looking_B" + }, + { + "modality-name": "box", + "modality-index": [ + "C", + "B" + ], + "formula": { + "connective": "and", + "formulas": [ + "looking_C", + { + "connective": "not", + "formula": "looking_B" + } + ] + } + } + ] + } + }, + "nil": { + "formula": "true" + } + }, + "effects": { + "e-signal": { + "looking_B": { + "formula": "true" + } + }, + "nil": null + }, + "observability-conditions": { + "A": { + "Oblivious": { + "formula": "true" + } + }, + "B": { + "Fully": { + "formula": "true" + } + }, + "C": { + "Fully": { + "formula": "true" + } + } + } + }, + "distract_A_B": { + "action-type": "private-ontic", + "events": [ + "e-distract", + "nil" + ], + "relations": { + "Fully": { + "e-distract": [ + "e-distract" + ], + "nil": [ + "nil" + ] + }, + "Oblivious": { + "e-distract": [ + "nil" + ], + "nil": [ + "nil" + ] + } + }, + "designated": [ + "e-distract" + ], + "preconditions": { + "e-distract": { + "formula": { + "connective": "and", + "formulas": [ + "looking_A", + "looking_B", + { + "modality-name": "box", + "modality-index": [ + "A", + "B" + ], + "formula": { + "connective": "and", + "formulas": [ + "looking_A", + "looking_B" + ] + } + } + ] + } + }, + "nil": { + "formula": "true" + } + }, + "effects": { + "e-distract": { + "looking_B": { + "formula": "false" + } + }, + "nil": null + }, + "observability-conditions": { + "A": { + "Fully": { + "formula": "true" + } + }, + "B": { + "Fully": { + "formula": "true" + } + }, + "C": { + "Oblivious": { + "formula": "true" + } + } + } + }, + "distract_A_C": { + "action-type": "private-ontic", + "events": [ + "e-distract", + "nil" + ], + "relations": { + "Fully": { + "e-distract": [ + "e-distract" + ], + "nil": [ + "nil" + ] + }, + "Oblivious": { + "e-distract": [ + "nil" + ], + "nil": [ + "nil" + ] + } + }, + "designated": [ + "e-distract" + ], + "preconditions": { + "e-distract": { + "formula": { + "connective": "and", + "formulas": [ + "looking_A", + "looking_C", + { + "modality-name": "box", + "modality-index": [ + "A", + "C" + ], + "formula": { + "connective": "and", + "formulas": [ + "looking_A", + "looking_C" + ] + } + } + ] + } + }, + "nil": { + "formula": "true" + } + }, + "effects": { + "e-distract": { + "looking_C": { + "formula": "false" + } + }, + "nil": null + }, + "observability-conditions": { + "A": { + "Fully": { + "formula": "true" + } + }, + "B": { + "Oblivious": { + "formula": "true" + } + }, + "C": { + "Fully": { + "formula": "true" + } + } + } + }, + "distract_B_A": { + "action-type": "private-ontic", + "events": [ + "e-distract", + "nil" + ], + "relations": { + "Fully": { + "e-distract": [ + "e-distract" + ], + "nil": [ + "nil" + ] + }, + "Oblivious": { + "e-distract": [ + "nil" + ], + "nil": [ + "nil" + ] + } + }, + "designated": [ + "e-distract" + ], + "preconditions": { + "e-distract": { + "formula": { + "connective": "and", + "formulas": [ + "looking_B", + "looking_A", + { + "modality-name": "box", + "modality-index": [ + "B", + "A" + ], + "formula": { + "connective": "and", + "formulas": [ + "looking_B", + "looking_A" + ] + } + } + ] + } + }, + "nil": { + "formula": "true" + } + }, + "effects": { + "e-distract": { + "looking_A": { + "formula": "false" + } + }, + "nil": null + }, + "observability-conditions": { + "A": { + "Fully": { + "formula": "true" + } + }, + "B": { + "Fully": { + "formula": "true" + } + }, + "C": { + "Oblivious": { + "formula": "true" + } + } + } + }, + "distract_B_C": { + "action-type": "private-ontic", + "events": [ + "e-distract", + "nil" + ], + "relations": { + "Fully": { + "e-distract": [ + "e-distract" + ], + "nil": [ + "nil" + ] + }, + "Oblivious": { + "e-distract": [ + "nil" + ], + "nil": [ + "nil" + ] + } + }, + "designated": [ + "e-distract" + ], + "preconditions": { + "e-distract": { + "formula": { + "connective": "and", + "formulas": [ + "looking_B", + "looking_C", + { + "modality-name": "box", + "modality-index": [ + "B", + "C" + ], + "formula": { + "connective": "and", + "formulas": [ + "looking_B", + "looking_C" + ] + } + } + ] + } + }, + "nil": { + "formula": "true" + } + }, + "effects": { + "e-distract": { + "looking_C": { + "formula": "false" + } + }, + "nil": null + }, + "observability-conditions": { + "A": { + "Oblivious": { + "formula": "true" + } + }, + "B": { + "Fully": { + "formula": "true" + } + }, + "C": { + "Fully": { + "formula": "true" + } + } + } + }, + "distract_C_A": { + "action-type": "private-ontic", + "events": [ + "e-distract", + "nil" + ], + "relations": { + "Fully": { + "e-distract": [ + "e-distract" + ], + "nil": [ + "nil" + ] + }, + "Oblivious": { + "e-distract": [ + "nil" + ], + "nil": [ + "nil" + ] + } + }, + "designated": [ + "e-distract" + ], + "preconditions": { + "e-distract": { + "formula": { + "connective": "and", + "formulas": [ + "looking_C", + "looking_A", + { + "modality-name": "box", + "modality-index": [ + "C", + "A" + ], + "formula": { + "connective": "and", + "formulas": [ + "looking_C", + "looking_A" + ] + } + } + ] + } + }, + "nil": { + "formula": "true" + } + }, + "effects": { + "e-distract": { + "looking_A": { + "formula": "false" + } + }, + "nil": null + }, + "observability-conditions": { + "A": { + "Fully": { + "formula": "true" + } + }, + "B": { + "Oblivious": { + "formula": "true" + } + }, + "C": { + "Fully": { + "formula": "true" + } + } + } + }, + "distract_C_B": { + "action-type": "private-ontic", + "events": [ + "e-distract", + "nil" + ], + "relations": { + "Fully": { + "e-distract": [ + "e-distract" + ], + "nil": [ + "nil" + ] + }, + "Oblivious": { + "e-distract": [ + "nil" + ], + "nil": [ + "nil" + ] + } + }, + "designated": [ + "e-distract" + ], + "preconditions": { + "e-distract": { + "formula": { + "connective": "and", + "formulas": [ + "looking_C", + "looking_B", + { + "modality-name": "box", + "modality-index": [ + "C", + "B" + ], + "formula": { + "connective": "and", + "formulas": [ + "looking_C", + "looking_B" + ] + } + } + ] + } + }, + "nil": { + "formula": "true" + } + }, + "effects": { + "e-distract": { + "looking_B": { + "formula": "false" + } + }, + "nil": null + }, + "observability-conditions": { + "A": { + "Oblivious": { + "formula": "true" + } + }, + "B": { + "Fully": { + "formula": "true" + } + }, + "C": { + "Fully": { + "formula": "true" + } + } + } + }, + "peek_A": { + "action-type": "quasi-private-sensing", + "events": [ + "e-peek-pos", + "e-peek-neg", + "nil" + ], + "relations": { + "Fully": { + "e-peek-pos": [ + "e-peek-pos" + ], + "e-peek-neg": [ + "e-peek-neg" + ], + "nil": [ + "nil" + ] + }, + "Partially": { + "e-peek-pos": [ + "e-peek-pos", + "e-peek-neg" + ], + "e-peek-neg": [ + "e-peek-pos", + "e-peek-neg" + ], + "nil": [ + "nil" + ] + }, + "Oblivious": { + "e-peek-pos": [ + "nil" + ], + "e-peek-neg": [ + "nil" + ], + "nil": [ + "nil" + ] + } + }, + "designated": [ + "e-peek-pos", + "e-peek-neg" + ], + "preconditions": { + "e-peek-pos": { + "formula": { + "connective": "and", + "formulas": [ + { + "connective": "and", + "formulas": [ + { + "connective": "imply", + "formulas": [ + "looking_A", + { + "modality-name": "box", + "modality-index": [ + "A" + ], + "formula": { + "connective": "and", + "formulas": [ + "opened", + "looking_A" + ] + } + } + ] + }, + { + "connective": "imply", + "formulas": [ + "looking_B", + { + "modality-name": "box", + "modality-index": [ + "B" + ], + "formula": { + "connective": "and", + "formulas": [ + "opened", + "looking_A" + ] + } + } + ] + }, + { + "connective": "imply", + "formulas": [ + "looking_C", + { + "modality-name": "box", + "modality-index": [ + "C" + ], + "formula": { + "connective": "and", + "formulas": [ + "opened", + "looking_A" + ] + } + } + ] + } + ] + }, + "tails" + ] + } + }, + "e-peek-neg": { + "formula": { + "connective": "and", + "formulas": [ + { + "connective": "and", + "formulas": [ + { + "connective": "imply", + "formulas": [ + "looking_A", + { + "modality-name": "box", + "modality-index": [ + "A" + ], + "formula": { + "connective": "and", + "formulas": [ + "opened", + "looking_A" + ] + } + } + ] + }, + { + "connective": "imply", + "formulas": [ + "looking_B", + { + "modality-name": "box", + "modality-index": [ + "B" + ], + "formula": { + "connective": "and", + "formulas": [ + "opened", + "looking_A" + ] + } + } + ] + }, + { + "connective": "imply", + "formulas": [ + "looking_C", + { + "modality-name": "box", + "modality-index": [ + "C" + ], + "formula": { + "connective": "and", + "formulas": [ + "opened", + "looking_A" + ] + } + } + ] + } + ] + }, + { + "connective": "not", + "formula": "tails" + } + ] + } + }, + "nil": { + "formula": "true" + } + }, + "effects": { + "e-peek-pos": null, + "e-peek-neg": null, + "nil": null + }, + "observability-conditions": { + "A": { + "Fully": { + "formula": "true" + } + }, + "B": { + "Partially": { + "formula": "looking_B" + }, + "Oblivious": { + "formula": { + "connective": "not", + "formula": "looking_B" + } + } + }, + "C": { + "Partially": { + "formula": "looking_C" + }, + "Oblivious": { + "formula": { + "connective": "not", + "formula": "looking_C" + } + } + } + } + }, + "peek_B": { + "action-type": "quasi-private-sensing", + "events": [ + "e-peek-pos", + "e-peek-neg", + "nil" + ], + "relations": { + "Fully": { + "e-peek-pos": [ + "e-peek-pos" + ], + "e-peek-neg": [ + "e-peek-neg" + ], + "nil": [ + "nil" + ] + }, + "Partially": { + "e-peek-pos": [ + "e-peek-pos", + "e-peek-neg" + ], + "e-peek-neg": [ + "e-peek-pos", + "e-peek-neg" + ], + "nil": [ + "nil" + ] + }, + "Oblivious": { + "e-peek-pos": [ + "nil" + ], + "e-peek-neg": [ + "nil" + ], + "nil": [ + "nil" + ] + } + }, + "designated": [ + "e-peek-pos", + "e-peek-neg" + ], + "preconditions": { + "e-peek-pos": { + "formula": { + "connective": "and", + "formulas": [ + { + "connective": "and", + "formulas": [ + { + "connective": "imply", + "formulas": [ + "looking_A", + { + "modality-name": "box", + "modality-index": [ + "A" + ], + "formula": { + "connective": "and", + "formulas": [ + "opened", + "looking_B" + ] + } + } + ] + }, + { + "connective": "imply", + "formulas": [ + "looking_B", + { + "modality-name": "box", + "modality-index": [ + "B" + ], + "formula": { + "connective": "and", + "formulas": [ + "opened", + "looking_B" + ] + } + } + ] + }, + { + "connective": "imply", + "formulas": [ + "looking_C", + { + "modality-name": "box", + "modality-index": [ + "C" + ], + "formula": { + "connective": "and", + "formulas": [ + "opened", + "looking_B" + ] + } + } + ] + } + ] + }, + "tails" + ] + } + }, + "e-peek-neg": { + "formula": { + "connective": "and", + "formulas": [ + { + "connective": "and", + "formulas": [ + { + "connective": "imply", + "formulas": [ + "looking_A", + { + "modality-name": "box", + "modality-index": [ + "A" + ], + "formula": { + "connective": "and", + "formulas": [ + "opened", + "looking_B" + ] + } + } + ] + }, + { + "connective": "imply", + "formulas": [ + "looking_B", + { + "modality-name": "box", + "modality-index": [ + "B" + ], + "formula": { + "connective": "and", + "formulas": [ + "opened", + "looking_B" + ] + } + } + ] + }, + { + "connective": "imply", + "formulas": [ + "looking_C", + { + "modality-name": "box", + "modality-index": [ + "C" + ], + "formula": { + "connective": "and", + "formulas": [ + "opened", + "looking_B" + ] + } + } + ] + } + ] + }, + { + "connective": "not", + "formula": "tails" + } + ] + } + }, + "nil": { + "formula": "true" + } + }, + "effects": { + "e-peek-pos": null, + "e-peek-neg": null, + "nil": null + }, + "observability-conditions": { + "A": { + "Partially": { + "formula": "looking_A" + }, + "Oblivious": { + "formula": { + "connective": "not", + "formula": "looking_A" + } + } + }, + "B": { + "Fully": { + "formula": "true" + } + }, + "C": { + "Partially": { + "formula": "looking_C" + }, + "Oblivious": { + "formula": { + "connective": "not", + "formula": "looking_C" + } + } + } + } + }, + "peek_C": { + "action-type": "quasi-private-sensing", + "events": [ + "e-peek-pos", + "e-peek-neg", + "nil" + ], + "relations": { + "Fully": { + "e-peek-pos": [ + "e-peek-pos" + ], + "e-peek-neg": [ + "e-peek-neg" + ], + "nil": [ + "nil" + ] + }, + "Partially": { + "e-peek-pos": [ + "e-peek-pos", + "e-peek-neg" + ], + "e-peek-neg": [ + "e-peek-pos", + "e-peek-neg" + ], + "nil": [ + "nil" + ] + }, + "Oblivious": { + "e-peek-pos": [ + "nil" + ], + "e-peek-neg": [ + "nil" + ], + "nil": [ + "nil" + ] + } + }, + "designated": [ + "e-peek-pos", + "e-peek-neg" + ], + "preconditions": { + "e-peek-pos": { + "formula": { + "connective": "and", + "formulas": [ + { + "connective": "and", + "formulas": [ + { + "connective": "imply", + "formulas": [ + "looking_A", + { + "modality-name": "box", + "modality-index": [ + "A" + ], + "formula": { + "connective": "and", + "formulas": [ + "opened", + "looking_C" + ] + } + } + ] + }, + { + "connective": "imply", + "formulas": [ + "looking_B", + { + "modality-name": "box", + "modality-index": [ + "B" + ], + "formula": { + "connective": "and", + "formulas": [ + "opened", + "looking_C" + ] + } + } + ] + }, + { + "connective": "imply", + "formulas": [ + "looking_C", + { + "modality-name": "box", + "modality-index": [ + "C" + ], + "formula": { + "connective": "and", + "formulas": [ + "opened", + "looking_C" + ] + } + } + ] + } + ] + }, + "tails" + ] + } + }, + "e-peek-neg": { + "formula": { + "connective": "and", + "formulas": [ + { + "connective": "and", + "formulas": [ + { + "connective": "imply", + "formulas": [ + "looking_A", + { + "modality-name": "box", + "modality-index": [ + "A" + ], + "formula": { + "connective": "and", + "formulas": [ + "opened", + "looking_C" + ] + } + } + ] + }, + { + "connective": "imply", + "formulas": [ + "looking_B", + { + "modality-name": "box", + "modality-index": [ + "B" + ], + "formula": { + "connective": "and", + "formulas": [ + "opened", + "looking_C" + ] + } + } + ] + }, + { + "connective": "imply", + "formulas": [ + "looking_C", + { + "modality-name": "box", + "modality-index": [ + "C" + ], + "formula": { + "connective": "and", + "formulas": [ + "opened", + "looking_C" + ] + } + } + ] + } + ] + }, + { + "connective": "not", + "formula": "tails" + } + ] + } + }, + "nil": { + "formula": "true" + } + }, + "effects": { + "e-peek-pos": null, + "e-peek-neg": null, + "nil": null + }, + "observability-conditions": { + "A": { + "Partially": { + "formula": "looking_A" + }, + "Oblivious": { + "formula": { + "connective": "not", + "formula": "looking_A" + } + } + }, + "B": { + "Partially": { + "formula": "looking_B" + }, + "Oblivious": { + "formula": { + "connective": "not", + "formula": "looking_B" + } + } + }, + "C": { + "Fully": { + "formula": "true" + } + } + } + }, + "shout-tails_A": { + "action-type": "private-announcement", + "events": [ + "e-shout-tails", + "nil" + ], + "relations": { + "Fully": { + "e-shout-tails": [ + "e-shout-tails" + ], + "nil": [ + "nil" + ] + }, + "Oblivious": { + "e-shout-tails": [ + "nil" + ], + "nil": [ + "nil" + ] + } + }, + "designated": [ + "e-shout-tails" + ], + "preconditions": { + "e-shout-tails": { + "formula": { + "connective": "and", + "formulas": [ + { + "modality-name": "box", + "modality-index": [ + "A" + ], + "formula": "tails" + }, + { + "connective": "and", + "formulas": [ + { + "connective": "imply", + "formulas": [ + "looking_A", + { + "modality-name": "box", + "modality-index": [ + "A" + ], + "formula": "looking_A" + } + ] + }, + { + "connective": "imply", + "formulas": [ + "looking_B", + { + "modality-name": "box", + "modality-index": [ + "B" + ], + "formula": "looking_A" + } + ] + }, + { + "connective": "imply", + "formulas": [ + "looking_C", + { + "modality-name": "box", + "modality-index": [ + "C" + ], + "formula": "looking_A" + } + ] + } + ] + }, + "looking_A" + ] + } + }, + "nil": { + "formula": "true" + } + }, + "effects": { + "e-shout-tails": null, + "nil": null + }, + "observability-conditions": { + "A": { + "Fully": { + "formula": "true" + } + }, + "B": { + "Fully": { + "formula": "looking_B" + }, + "Oblivious": { + "formula": { + "connective": "not", + "formula": "looking_B" + } + } + }, + "C": { + "Fully": { + "formula": "looking_C" + }, + "Oblivious": { + "formula": { + "connective": "not", + "formula": "looking_C" + } + } + } + } + }, + "shout-tails_B": { + "action-type": "private-announcement", + "events": [ + "e-shout-tails", + "nil" + ], + "relations": { + "Fully": { + "e-shout-tails": [ + "e-shout-tails" + ], + "nil": [ + "nil" + ] + }, + "Oblivious": { + "e-shout-tails": [ + "nil" + ], + "nil": [ + "nil" + ] + } + }, + "designated": [ + "e-shout-tails" + ], + "preconditions": { + "e-shout-tails": { + "formula": { + "connective": "and", + "formulas": [ + { + "modality-name": "box", + "modality-index": [ + "B" + ], + "formula": "tails" + }, + { + "connective": "and", + "formulas": [ + { + "connective": "imply", + "formulas": [ + "looking_A", + { + "modality-name": "box", + "modality-index": [ + "A" + ], + "formula": "looking_B" + } + ] + }, + { + "connective": "imply", + "formulas": [ + "looking_B", + { + "modality-name": "box", + "modality-index": [ + "B" + ], + "formula": "looking_B" + } + ] + }, + { + "connective": "imply", + "formulas": [ + "looking_C", + { + "modality-name": "box", + "modality-index": [ + "C" + ], + "formula": "looking_B" + } + ] + } + ] + }, + "looking_B" + ] + } + }, + "nil": { + "formula": "true" + } + }, + "effects": { + "e-shout-tails": null, + "nil": null + }, + "observability-conditions": { + "A": { + "Fully": { + "formula": "looking_A" + }, + "Oblivious": { + "formula": { + "connective": "not", + "formula": "looking_A" + } + } + }, + "B": { + "Fully": { + "formula": "true" + } + }, + "C": { + "Fully": { + "formula": "looking_C" + }, + "Oblivious": { + "formula": { + "connective": "not", + "formula": "looking_C" + } + } + } + } + }, + "shout-tails_C": { + "action-type": "private-announcement", + "events": [ + "e-shout-tails", + "nil" + ], + "relations": { + "Fully": { + "e-shout-tails": [ + "e-shout-tails" + ], + "nil": [ + "nil" + ] + }, + "Oblivious": { + "e-shout-tails": [ + "nil" + ], + "nil": [ + "nil" + ] + } + }, + "designated": [ + "e-shout-tails" + ], + "preconditions": { + "e-shout-tails": { + "formula": { + "connective": "and", + "formulas": [ + { + "modality-name": "box", + "modality-index": [ + "C" + ], + "formula": "tails" + }, + { + "connective": "and", + "formulas": [ + { + "connective": "imply", + "formulas": [ + "looking_A", + { + "modality-name": "box", + "modality-index": [ + "A" + ], + "formula": "looking_C" + } + ] + }, + { + "connective": "imply", + "formulas": [ + "looking_B", + { + "modality-name": "box", + "modality-index": [ + "B" + ], + "formula": "looking_C" + } + ] + }, + { + "connective": "imply", + "formulas": [ + "looking_C", + { + "modality-name": "box", + "modality-index": [ + "C" + ], + "formula": "looking_C" + } + ] + } + ] + }, + "looking_C" + ] + } + }, + "nil": { + "formula": "true" + } + }, + "effects": { + "e-shout-tails": null, + "nil": null + }, + "observability-conditions": { + "A": { + "Fully": { + "formula": "looking_A" + }, + "Oblivious": { + "formula": { + "connective": "not", + "formula": "looking_A" + } + } + }, + "B": { + "Fully": { + "formula": "looking_B" + }, + "Oblivious": { + "formula": { + "connective": "not", + "formula": "looking_B" + } + } + }, + "C": { + "Fully": { + "formula": "true" + } + } + } + } + }, + "goal": { + "formula": { + "connective": "and", + "formulas": [ + { + "modality-name": "box", + "modality-index": [ + "B", + "C" + ], + "formula": "tails" + }, + { + "modality-name": "box", + "modality-index": [ + "B" + ], + "formula": { + "connective": "not", + "formula": { + "modality-name": "Kw.box", + "modality-index": [ + "A" + ], + "formula": "tails" + } + } + }, + { + "modality-name": "diamond", + "modality-index": [ + "A" + ], + "formula": { + "connective": "not", + "formula": { + "modality-name": "Kw.box", + "modality-index": [ + "C" + ], + "formula": "tails" + } + } + } + ] + } + } +}