fix: one step unrealizability now depends on first player

whitemech · Jan 21, 2024 · 3bb4532 · 3bb4532
1 parent 5a49170
commit 3bb4532
Show file tree

Hide file tree

Showing 7 changed files with 44 additions and 29 deletions.
diff --git a/src/Main.cpp b/src/Main.cpp
@@ -71,7 +71,7 @@ int main(int argc, char ** argv) {
     if (!maxset) {
 //         abstract single strategy
 //         preprocessing
-        auto one_step_result = preprocessing(*parsed_formula, partition, *var_mgr);
+        auto one_step_result = preprocessing(*parsed_formula, partition, *var_mgr, starting_player);
         bool preprocessing_success = one_step_result.realizability.has_value();
         if (preprocessing_success and one_step_result.realizability.value()) {
             std::cout << Syft::REALIZABLE_STR << std::endl;

diff --git a/src/synthesis/header/OneStepUnrealizability.h b/src/synthesis/header/OneStepUnrealizability.h
@@ -7,6 +7,7 @@
 #include <optional>
 
 #include "InputOutputPartition.h"
+#include "Player.h"
 #include "VarMgr.h"
 
 namespace Syft {
@@ -19,9 +20,10 @@ namespace Syft {
     z3::context& z3_context;
     z3::solver& solver;
     z3::expr result;
+    Syft::Player starting_player;
     // dummy value for 'result' since z3::expr does not have a default constructor
-    explicit SmtOneStepUnrealizabilityVisitor(const InputOutputPartition &partition, const Syft::VarMgr& var_mgr, z3::context& z3_context, z3::solver& solver)
-        : partition{partition}, var_mgr{var_mgr}, z3_context{z3_context}, solver{solver}, result{z3_context.bool_val(true)} {}
+    explicit SmtOneStepUnrealizabilityVisitor(const InputOutputPartition &partition, const Syft::VarMgr& var_mgr, z3::context& z3_context, z3::solver& solver, Syft::Player starting_player)
+        : partition{partition}, var_mgr{var_mgr}, z3_context{z3_context}, solver{solver}, result{z3_context.bool_val(true)}, starting_player{starting_player} {}
     ~SmtOneStepUnrealizabilityVisitor() {}
     void visit(const whitemech::lydia::LTLfTrue &) override;
     void visit(const whitemech::lydia::LTLfFalse &) override;
@@ -39,7 +41,7 @@ namespace Syft {
     z3::expr apply(const whitemech::lydia::LTLfFormula &f);
   };
 
-  bool one_step_unrealizable(const whitemech::lydia::LTLfFormula &f, const InputOutputPartition &partition, const Syft::VarMgr& var_mgr);
+  bool one_step_unrealizable(const whitemech::lydia::LTLfFormula &f, const InputOutputPartition &partition, const Syft::VarMgr& var_mgr, Syft::Player starting_player);
 
 }
 

diff --git a/src/synthesis/header/Preprocessing.h b/src/synthesis/header/Preprocessing.h
@@ -7,7 +7,7 @@
 
 namespace Syft {
 
-  OneStepSynthesisResult preprocessing(const whitemech::lydia::LTLfFormula& formula, const InputOutputPartition &partition, const Syft::VarMgr& var_mgr);
+  OneStepSynthesisResult preprocessing(const whitemech::lydia::LTLfFormula& formula, const InputOutputPartition &partition, const Syft::VarMgr& var_mgr, Syft::Player starting_player);
 }
 
 #endif //PREPROCESSING_HPP
diff --git a/src/synthesis/source/OneStepUnrealizability.cpp b/src/synthesis/source/OneStepUnrealizability.cpp
@@ -76,7 +76,7 @@ namespace Syft {
     }
 
     void SmtOneStepUnrealizabilityVisitor::visit(const whitemech::lydia::LTLfEventually &formula) {
-      result = z3_context.bool_val(true);
+        result = z3_context.bool_val(true);
     }
 
     void SmtOneStepUnrealizabilityVisitor::visit(const whitemech::lydia::LTLfAlways &formula) {
@@ -88,8 +88,32 @@ namespace Syft {
         return result;
     }
 
+    z3::expr quantify_agent_vars_(z3::solver &solver, const InputOutputPartition &partition, z3::expr &result) {
+        // exist an agent move such that for all env moves...
+        z3::expr_vector exist_vars(solver.ctx());
+        if (!partition.output_variables.empty()) {
+            for (const auto &controllable_var: partition.output_variables) {
+                exist_vars.push_back(solver.ctx().bool_const(controllable_var.c_str()));
+            }
+            result = z3::exists(exist_vars, result);
+        }
+        return result;
+    }
+
+    z3::expr quantify_env_vars_(z3::solver &solver, const InputOutputPartition &partition, z3::expr &result) {
+        // for all env moves...
+        z3::expr_vector forall_vars(solver.ctx());
+        if (!partition.input_variables.empty()) {
+            for (const auto &controllable_var: partition.input_variables) {
+                forall_vars.push_back(solver.ctx().bool_const(controllable_var.c_str()));
+            }
+            result = z3::forall(forall_vars, result);
+        }
+        return result;
+    }
+
     bool one_step_unrealizable(const whitemech::lydia::LTLfFormula &f, const InputOutputPartition &partition,
-                               const Syft::VarMgr &var_mgr) {
+                               const Syft::VarMgr &var_mgr, Syft::Player starting_player) {
 
         whitemech::lydia::ltlf_ptr nnf_formula = whitemech::lydia::to_nnf(f);
 
@@ -98,26 +122,15 @@ namespace Syft {
         z3::params p(ctx);
         solver.set(p);
 
-        auto visitor = SmtOneStepUnrealizabilityVisitor{partition, var_mgr, ctx, solver};
+        auto visitor = SmtOneStepUnrealizabilityVisitor{partition, var_mgr, ctx, solver, starting_player};
         auto result = visitor.apply(*nnf_formula);
 
-
-        // for all env moves...
-        z3::expr_vector forall_vars(ctx);
-        if (!partition.input_variables.empty()) {
-            for (const auto &controllable_var: partition.input_variables) {
-                forall_vars.push_back(ctx.bool_const(controllable_var.c_str()));
-            }
-            result = z3::forall(forall_vars, result);
-        }
-
-        // exist an agent move such that for all env moves...
-        z3::expr_vector exist_vars(ctx);
-        if (!partition.output_variables.empty()) {
-            for (const auto &controllable_var: partition.output_variables) {
-                exist_vars.push_back(ctx.bool_const(controllable_var.c_str()));
-            }
-            result = z3::exists(exist_vars, result);
+        if (starting_player == Player::Environment) {
+            result = quantify_agent_vars_(solver, partition, result);
+            result = quantify_env_vars_(solver, partition, result);
+        } else {
+            result = quantify_env_vars_(solver, partition, result);
+            result = quantify_agent_vars_(solver, partition, result);
         }
 
         solver.reset();

diff --git a/src/synthesis/source/Preprocessing.cpp b/src/synthesis/source/Preprocessing.cpp
@@ -6,7 +6,7 @@
 
 namespace Syft {
 
-  OneStepSynthesisResult preprocessing(const whitemech::lydia::LTLfFormula& formula, const InputOutputPartition &partition, const Syft::VarMgr& var_mgr) {
+  OneStepSynthesisResult preprocessing(const whitemech::lydia::LTLfFormula& formula, const InputOutputPartition &partition, const Syft::VarMgr& var_mgr, Syft::Player starting_player) {
     Syft::OneStepSynthesisResult result;
 
     // one-step realizability check
@@ -18,7 +18,7 @@ namespace Syft {
     }
 
     // one-step unrealizability check
-    bool one_step_unrealizability_check_result = one_step_unrealizable(formula, partition, var_mgr);
+    bool one_step_unrealizability_check_result = one_step_unrealizable(formula, partition, var_mgr, starting_player);
     if (one_step_unrealizability_check_result) {
       result.realizability = false;
       return result;

diff --git a/test/test_one_step_unrealizability_check.cpp b/test/test_one_step_unrealizability_check.cpp
@@ -10,7 +10,7 @@ bool get_one_step_unrealizability(const std::string& formula, const std::vector<
     auto partition = Syft::InputOutputPartition::construct_from_input(input_variables, output_variables);
     var_mgr.create_named_variables(partition.input_variables);
     var_mgr.create_named_variables(partition.output_variables);
-    return Syft::one_step_unrealizable(*parsed_formula, partition, var_mgr);
+    return Syft::one_step_unrealizable(*parsed_formula, partition, var_mgr, Syft::Player::Agent);
 }
 
 

diff --git a/test/utils.cpp b/test/utils.cpp
@@ -38,7 +38,7 @@ namespace Test{
         var_mgr->create_named_variables(partition.input_variables);
         var_mgr->create_named_variables(partition.output_variables);
 
-        auto one_step_result = Syft::preprocessing(*formula, partition, *var_mgr);
+        auto one_step_result = Syft::preprocessing(*formula, partition, *var_mgr, Player::Agent);
         bool preprocessing_success = one_step_result.realizability.has_value();
         if (preprocessing_success and one_step_result.realizability.value()){
           return true;