stability synthesizer, passed tests

example/fair_counter_unrea_test.tlsf → example/fair_stable_counter_unrea_test.tlsf

@@ -2,7 +2,7 @@ INFO {
   TITLE:       "Fair-LTLf-test"
   DESCRIPTION: "Fair-LTLf-test example"
   SEMANTICS:   Finite,Moore
-  TARGET:      Moore
+  TARGET:      Mealy
 }
 
 MAIN {

src/synthesis/header/StableReachabilitySynthesizer.h

@@ -0,0 +1,59 @@
+//
+// Created by shuzhu on 21/01/24.
+//
+
+#ifndef LYDIASYFT_STABLEREACHABILITYSYNTHESIZER_H
+#define LYDIASYFT_STABLEREACHABILITYSYNTHESIZER_H
+
+#include "DfaGameSynthesizer.h"
+
+namespace Syft {
+
+/**
+ * \brief A single-strategy-synthesizer for a Buchi-reachability game given as a symbolic-state DFA.
+ */
+    class StableReachabilitySynthesizer : public DfaGameSynthesizer {
+    private:
+
+        CUDD::BDD goal_states_;
+        CUDD::BDD state_space_;
+
+
+        //fair
+        CUDD::BDD assumption_;
+
+    protected:
+        CUDD::BDD load_CNF(const std::string& filename) const;
+
+    public:
+
+        /**
+         * \brief Construct a single-strategy-synthesizer for the given Buchi-reachability game.
+         *
+         * \param spec A symbolic-state DFA representing the Buchi-reachability game.
+         * \param starting_player The player that moves first each turn.
+         * \param goal_states The set of states that the agent must reach to win.
+         */
+        StableReachabilitySynthesizer(SymbolicStateDfa spec, Player starting_player, Player protagonist_player,
+                                    CUDD::BDD goal_states, CUDD::BDD state_space,
+                                    std::string& assumption_filename);
+
+
+
+        /**
+         * \brief Solves the coBuchi-reachability game.
+         *
+         * \return The result consists of
+         * realizability
+         * a set of agent winning states
+         * a transducer representing a winning strategy or nullptr if the game is unrealizable.
+         */
+        virtual SynthesisResult run() const final;
+
+        std::unique_ptr<Transducer> AbstractSingleStrategy(SynthesisResult result) const;
+
+    };
+
+}
+
+#endif //LYDIASYFT_STABLEREACHABILITYSYNTHESIZER_H

src/synthesis/source/StableReachabilitySynthesizer.cpp

@@ -0,0 +1,160 @@
+//
+// Created by shuzhu on 21/01/24.
+//
+
+
+#include "StableReachabilitySynthesizer.h"
+#include "string_utilities.h"
+
+#include <fstream>
+#include <cassert>
+
+namespace Syft {
+
+    StableReachabilitySynthesizer::StableReachabilitySynthesizer(SymbolicStateDfa spec,
+                                                             Player starting_player, Player protagonist_player,
+                                                             CUDD::BDD goal_states,
+                                                             CUDD::BDD state_space,
+                                                             std::string& assumption_filename)
+            : DfaGameSynthesizer(spec, starting_player, protagonist_player)
+            , goal_states_(goal_states), state_space_(state_space)
+    {
+        assumption_ = load_CNF(assumption_filename);
+    }
+
+
+    SynthesisResult StableReachabilitySynthesizer::run() const {
+        SynthesisResult result;
+        CUDD::BDD winning_states = state_space_;
+        CUDD::BDD winning_moves = winning_states;
+        int c = 0;
+        int inner_c = 0;
+
+        while (true) {
+//            var_mgr_->dump_dot(winning_states.Add(), "winning_states_"+ std::to_string(c)+".dot");
+//            var_mgr_->dump_dot(winning_moves.Add(), "winning_moves_"+ std::to_string(c)+".dot");
+            CUDD::BDD new_winning_states, new_winning_moves;
+            // inner least fixpoint
+            CUDD::BDD inner_winning_states = state_space_ & goal_states_;
+            CUDD::BDD inner_winning_moves = inner_winning_states;
+
+            while (true) {
+//                var_mgr_->dump_dot(inner_winning_states.Add(), "inner_winning_states_"+ std::to_string(c)+".dot");
+//                var_mgr_->dump_dot(inner_winning_moves.Add(), "inner_winning_moves_"+ std::to_string(c)+".dot");
+                CUDD::BDD new_inner_winning_states, new_inner_winning_moves;
+
+                CUDD::BDD transitions_to_winning_states_or_goal =
+                        (winning_states | goal_states_).VectorCompose(transition_vector_);
+//                    var_mgr_->dump_dot(transitions_to_winning_states_or_goal.Add(), "transitions_to_winning_states_or_goal.dot");
+                CUDD::BDD transitions_to_inner_winning_states_or_goal =
+                        (inner_winning_states | goal_states_).VectorCompose(transition_vector_);
+//                    var_mgr_->dump_dot(transitions_to_inner_winning_states_or_goal.Add(), "transitions_to_inner_winning_states_or_goal.dot");
+//                    var_mgr_->dump_dot(assumption_.Add(), "assumption.dot");
+                CUDD::BDD assumption_constrained_transitions = ((!assumption_ | transitions_to_inner_winning_states_or_goal)) * transitions_to_winning_states_or_goal;
+//                    var_mgr_->dump_dot(assumption_constrained_transitions.Add(), "assumption_constrained_transitions.dot");
+                if (starting_player_ == Player::Agent) {
+                    // Quantify all variables that the outputs don't depend on
+                    CUDD::BDD quantified_X_transitions_to_inner_winning_states = quantify_independent_variables_->apply(assumption_constrained_transitions);
+                    new_inner_winning_moves = inner_winning_moves | quantified_X_transitions_to_inner_winning_states;
+
+                    new_inner_winning_states = project_into_states(new_inner_winning_moves);
+                } else {
+                    CUDD::BDD transitions_to_inner_winning_states = quantify_independent_variables_->apply(assumption_constrained_transitions);
+//                        var_mgr_->dump_dot((quantify_independent_variables_->apply(assumption_constrained_transitions)).Add(), "quantified_assumption_constrained_transitions.dot");
+                    CUDD::BDD new_collected_inner_winning_states = project_into_states(transitions_to_inner_winning_states);
+                    new_inner_winning_states = inner_winning_states | new_collected_inner_winning_states;
+//                        var_mgr_->dump_dot(new_inner_winning_states.Add(), "states.dot");
+                    new_inner_winning_moves = inner_winning_moves | ((!inner_winning_states) & new_collected_inner_winning_states & transitions_to_inner_winning_states);
+
+                }
+
+                if (new_inner_winning_states == inner_winning_states) {
+                    if (starting_player_ == Player::Agent) {
+//                        CUDD::BDD transitions_to_winning_states = preimage(inner_winning_states);
+//                        CUDD::BDD quantified_X_transitions_to_inner_winning_states = quantify_independent_variables_->apply(transitions_to_winning_states);
+//                        new_inner_winning_moves = inner_winning_moves & quantified_X_transitions_to_inner_winning_states;
+                        new_winning_moves = winning_moves & inner_winning_moves;
+                        new_winning_states = winning_states & inner_winning_states;
+                    } else {
+                        CUDD::BDD transitions_to_winning_states = preimage(inner_winning_states);
+                        new_winning_states = winning_states & inner_winning_states;
+                        new_winning_moves = winning_moves & transitions_to_winning_states;
+                    }
+                    break;
+                }
+
+                inner_winning_moves = new_inner_winning_moves;
+                inner_winning_states = new_inner_winning_states;
+                inner_c++;
+            }
+
+
+            if (includes_initial_state(new_winning_states)) {
+                result.realizability = true;
+                result.winning_states = new_winning_states;
+                result.winning_moves = new_winning_moves;
+                result.transducer = nullptr;
+                return result;
+
+            } else if (new_winning_states == winning_states) {
+                result.realizability = false;
+                result.winning_states = new_winning_states;
+                result.winning_moves = new_winning_moves;
+                result.transducer = nullptr;
+                return result;
+            }
+
+            winning_moves = new_winning_moves;
+            winning_states = new_winning_states;
+            c++;
+        }
+
+    }
+
+    std::unique_ptr<Transducer> StableReachabilitySynthesizer::AbstractSingleStrategy(SynthesisResult result) const {
+        std::unordered_map<int, CUDD::BDD> strategy = synthesize_strategy(
+                result.winning_moves);
+
+        auto transducer = std::make_unique<Transducer>(
+                var_mgr_, initial_vector_, strategy, spec_.transition_function(),
+                starting_player_);
+        return transducer;
+    }
+
+    CUDD::BDD StableReachabilitySynthesizer::load_CNF(const std::string& filename) const{
+        std::ifstream f(filename.c_str());
+        CUDD::BDD assumption = var_mgr_->cudd_mgr()->bddOne();
+        std::vector<std::string> clause_line;
+        std::string line;
+        while(getline(f, line)) {
+            CUDD::BDD clause = var_mgr_->cudd_mgr()->bddZero();
+            std::set<std::string> clause_set;
+            std::set<std::string> neg_clause_set;
+
+            if (f.is_open()) {
+                clause_line = split(line, " ");
+
+                for (int i = 0; i < clause_line.size(); i++){
+                    std::string c = clause_line[i];
+                    CUDD::BDD literal_bdd;
+                    if(c[0] == '!'){
+                        std::string var_name = c.substr(1, c.length()-1);
+                        literal_bdd = !(var_mgr_->name_to_variable(var_name));
+                    }
+                    else{
+                        literal_bdd = var_mgr_->name_to_variable(c);
+                    }
+                    clause = clause + literal_bdd;
+                }
+            }
+            if(clause != var_mgr_->cudd_mgr()->bddZero()){
+                assumption = assumption * clause;
+            }
+
+        }
+        f.close();
+        return assumption;
+
+    }
+
+}

test/test_fair_synthesis.cpp

@@ -14,7 +14,7 @@
 
 TEST_CASE("Fair Synthesis test", "[fair synthesis]") {
     Syft::Parser parser;
-    parser = Syft::Parser::read_from_file(Syft::Test::SYFCO_LOCATION, Syft::Test::FAIRSYNTHESIS_TEST_TLSF);
+    parser = Syft::Parser::read_from_file(Syft::Test::SYFCO_LOCATION, Syft::Test::FAIRSTABLESYNTHESIS_TEST_TLSF);
 
     bool sys_first = parser.get_sys_first();
 
@@ -52,7 +52,7 @@ TEST_CASE("Fair Synthesis test", "[fair synthesis]") {
 
     Syft::FairReachabilitySynthesizer synthesizer(symbolic_dfa, starting_player,
                                                   protagonist_player, symbolic_dfa.final_states(),
-                                                  var_mgr->cudd_mgr()->bddOne(), Syft::Test::FAIRSYNTHESIS_TEST_ASSUMPTION);
+                                                  var_mgr->cudd_mgr()->bddOne(), Syft::Test::FAIRSTABLESYNTHESIS_TEST_ASSUMPTION);
     Syft::SynthesisResult result = synthesizer.run();
 
     bool expected = true;
@@ -61,7 +61,7 @@ TEST_CASE("Fair Synthesis test", "[fair synthesis]") {
 
 TEST_CASE("Fair Synthesis unrealizability test", "[fair synthesis]") {
     Syft::Parser parser;
-    parser = Syft::Parser::read_from_file(Syft::Test::SYFCO_LOCATION, Syft::Test::FAIRSYNTHESIS_UNREA_TEST_TLSF);
+    parser = Syft::Parser::read_from_file(Syft::Test::SYFCO_LOCATION, Syft::Test::FAIRSTABLESYNTHESIS_UNREA_TEST_TLSF);
 
     bool sys_first = parser.get_sys_first();
 
@@ -99,7 +99,7 @@ TEST_CASE("Fair Synthesis unrealizability test", "[fair synthesis]") {
 
     Syft::FairReachabilitySynthesizer synthesizer(symbolic_dfa, starting_player,
                                                   protagonist_player, symbolic_dfa.final_states(),
-                                                  var_mgr->cudd_mgr()->bddOne(), Syft::Test::FAIRSYNTHESIS_TEST_ASSUMPTION);
+                                                  var_mgr->cudd_mgr()->bddOne(), Syft::Test::FAIRSTABLESYNTHESIS_TEST_ASSUMPTION);
     Syft::SynthesisResult result = synthesizer.run();
 
     bool expected = false;
@@ -108,7 +108,7 @@ TEST_CASE("Fair Synthesis unrealizability test", "[fair synthesis]") {
 
 TEST_CASE("Fair Synthesis of realizable counter_1", "[fair synthesis]") {
     Syft::Parser parser;
-    parser = Syft::Parser::read_from_file(Syft::Test::SYFCO_LOCATION, Syft::Test::FAIRSYNTHESIS_COUNTER_TEST_TLSF);
+    parser = Syft::Parser::read_from_file(Syft::Test::SYFCO_LOCATION, Syft::Test::FAIRSTABLESYNTHESIS_COUNTER_TEST_TLSF);
 
     bool sys_first = parser.get_sys_first();
 
@@ -144,7 +144,7 @@ TEST_CASE("Fair Synthesis of realizable counter_1", "[fair synthesis]") {
 
     Syft::FairReachabilitySynthesizer synthesizer(symbolic_dfa, starting_player,
                                               protagonist_player, symbolic_dfa.final_states(),
-                                              var_mgr->cudd_mgr()->bddOne(), Syft::Test::FAIRSYNTHESIS_TEST_ASSUMPTION);
+                                              var_mgr->cudd_mgr()->bddOne(), Syft::Test::FAIRSTABLESYNTHESIS_TEST_ASSUMPTION);
     Syft::SynthesisResult result = synthesizer.run();
 
     bool expected = true;
@@ -153,7 +153,7 @@ TEST_CASE("Fair Synthesis of realizable counter_1", "[fair synthesis]") {
 
 TEST_CASE("Fair Synthesis of unrealizable counter_1", "[fair synthesis]") {
     Syft::Parser parser;
-    parser = Syft::Parser::read_from_file(Syft::Test::SYFCO_LOCATION, Syft::Test::FAIRSYNTHESIS_COUNTER_UNREA_TEST_TLSF);
+    parser = Syft::Parser::read_from_file(Syft::Test::SYFCO_LOCATION, Syft::Test::FAIRSTABLESYNTHESIS_COUNTER_UNREA_TEST_TLSF);
 
     bool sys_first = parser.get_sys_first();
 
@@ -191,7 +191,7 @@ TEST_CASE("Fair Synthesis of unrealizable counter_1", "[fair synthesis]") {
 
     Syft::FairReachabilitySynthesizer synthesizer(symbolic_dfa, starting_player,
                                                   protagonist_player, symbolic_dfa.final_states(),
-                                                  var_mgr->cudd_mgr()->bddOne(), Syft::Test::FAIRSYNTHESIS_TEST_ASSUMPTION);
+                                                  var_mgr->cudd_mgr()->bddOne(), Syft::Test::FAIRSTABLESYNTHESIS_TEST_ASSUMPTION);
     Syft::SynthesisResult result = synthesizer.run();
 
     bool expected = false;