Multi agent monitor

.gitmodules

@@ -1,6 +1,6 @@
 [submodule "submodules/lydia"]
 	path = submodules/lydia
-	url = https://github.com/whitemech/lydia.git
+	url = https://github.com/GianmarcoDIAG/lydia.git
 [submodule "submodules/slugs"]
 	path = submodules/slugs
 	url = https://github.com/VerifiableRobotics/slugs

.vscode/c_cpp_properties.json

@@ -0,0 +1,17 @@
+{
+    "configurations": [
+        {
+            "name": "Linux",
+            "includePath": [
+                "${workspaceFolder}/**",
+                "${workspaceFolder}/src/synthesis/header"
+            ],
+            "defines": [],
+            "compilerPath": "/usr/bin/gcc",
+            "cStandard": "c17",
+            "cppStandard": "gnu++17",
+            "intelliSenseMode": "linux-gcc-x64"
+        }
+    ],
+    "version": 4
+}

CMakeLists.txt

@@ -3,7 +3,10 @@ project(LydiaSyft)
 
 include(FetchContent)
 
-set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++17")
+set(CMAKE_CXX_STANDARD 17)
+set(CMAKE_CXX_STANDARD_REQUIRED ON)
+set(CMAKE_CXX_EXTENSIONS OFF)
+
 set(CMAKE_EXPORT_COMPILE_COMMANDS ON)
 set(CMAKE_INSTALL_PREFIX /usr/local)
 
@@ -31,7 +34,6 @@ if (NOT DEFINED MONA_USE_STATIC_LIBS)
 endif()
 find_package(mona REQUIRED)
 
-
 if (NOT DEFINED Z3_FETCH)
   set(Z3_FETCH ON)
 endif()
@@ -85,14 +87,14 @@ set(EXT_INCLUDE_PATH ${LYDIA_INCLUDE_DIR} ${LYDIA_THIRD_PARTY_INCLUDE_PATH} ${CU
 
 message(STATUS EXT_LIBRARIES_PATH ${EXT_LIBRARIES_PATH})
 
-enable_testing()
+# enable_testing()
 
 add_subdirectory(src)
 
-if (LYDIASYFT_ENABLE_TESTS)
-  add_subdirectory(test)
-endif()
+#if (LYDIASYFT_ENABLE_TESTS)
+   add_subdirectory(test)
+# endif()
 
-if (LYDIASYFT_ENABLE_EXAMPLES)
+# if (LYDIASYFT_ENABLE_EXAMPLES)
   add_subdirectory(examples)
-endif()
+# endif()

examples/01_quickstart/quickstart.cpp

@@ -1,57 +1,98 @@
+#include <iostream>
+#include <string>
+#include "Parser.h"
+#include "VarMgr.h"
 #include <memory>
 #include <sstream>
 #include <string>
 #include <vector>
-
+#include <filesystem>
+#include "lydia/mona_ext/mona_ext_base.hpp"
 #include <lydia/parser/ltlf/driver.hpp>
-
 #include "automata/ExplicitStateDfa.h"
 #include "automata/ExplicitStateDfaAdd.h"
 #include "automata/SymbolicStateDfa.h"
 #include "game/InputOutputPartition.h"
 #include "Player.h"
-#include "VarMgr.h"
 #include "synthesizer/LTLfSynthesizer.h"
 
 
 int main(int argc, char ** argv) {
-
-    // define the formula and the input/output variables
-    std::string formula_str = "F(a | b)";
-    std::vector<std::string> input_vars{"a"};
-    std::vector<std::string> output_vars{"b"};
+    std::string partition_file = "/examples/01_quickstart/test_vars.part";
+    std::cout << "Open file: " << partition_file << std::endl;
 
-    // parse the formula
-    auto driver = std::make_shared<whitemech::lydia::parsers::ltlf::LTLfDriver>();
-    std::stringstream formula_stream(formula_str);
-    driver->parse(formula_stream);
-    whitemech::lydia::ltlf_ptr formula = driver->get_result();
+
+    Syft::InputOutputPartition partition = Syft::InputOutputPartition::read_from_file(partition_file);
 
-    // initialize the variables
-    Syft::InputOutputPartition partition = Syft::InputOutputPartition::construct_from_input(input_vars, output_vars);
-    std::shared_ptr<Syft::VarMgr> var_mgr = std::make_shared<Syft::VarMgr>();
-    var_mgr->create_named_variables(partition.input_variables);
-    var_mgr->create_named_variables(partition.output_variables);
+    auto input = partition.input_variables;
+    auto agents = partition.agent_variables;
+
+    std::vector<std::string> formulas = {
+        "F(x & a)",      // Agent 0
+        "G(y -> b)",     // Agent 1
+        "F(a & b & c)"   // Agent 2
+    };
+    std::cout << "Input variables found: " << input.size() << std::endl;
+    std::cout << "Number of agents found: " << agents.size() << std::endl; 
+    std::cout << "Agent formulas found: " << formulas.size() << std::endl;
 
-    // build the explicit-state DFA
-    Syft::ExplicitStateDfa explicit_dfa = Syft::ExplicitStateDfa::dfa_of_formula(*formula);
-    Syft::ExplicitStateDfaAdd explicit_dfa_add = Syft::ExplicitStateDfaAdd::from_dfa_mona(var_mgr, explicit_dfa);
+    std::cout << "Input variables: " << std::endl;  
+    for (const auto& var : input) {
+        std::cout << var << std::endl;
+    }
+    for (std::size_t i = 0; i < agents.size(); ++i) {
+        std::cout << "Agent " << i << " variables: " << std::endl;
+        for (const auto& var : agents[i]) {
+            std::cout << var << std::endl;
+        }
+        std::cout << "Agent " << i << " formula: " << formulas[i] << std::endl;
+    }
+
+    //set up VarMgr
+    std::shared_ptr<Syft::VarMgr> var_mgr = std::make_shared<Syft::VarMgr>();
+    var_mgr->create_named_variables(input);
+    for (const auto& agent_vars : agents) {
+        var_mgr->create_named_variables(agent_vars);
+    }
+    var_mgr->partition_variables(input, agents);
 
-    // build the symbolic-state DFA from the explicit-state DFA
-    Syft::SymbolicStateDfa symbolic_dfa = Syft::SymbolicStateDfa::from_explicit(
-            std::move(explicit_dfa_add));
+    //Directory for showing results
+    std::string out_dir = "dfa_outputs";
+    std::filesystem::remove_all(out_dir);
+    std::filesystem::create_directories(out_dir);
 
+    auto driver = std::make_shared<whitemech::lydia::parsers::ltlf::LTLfDriver>();
 
-    // do synthesis
-    var_mgr->partition_variables(partition.input_variables, partition.output_variables);
-    Syft::Player starting_player = Syft::Player::Agent;
-    Syft::Player protagonist_player = Syft::Player::Agent;
-    Syft::LTLfSynthesizer synthesizer(symbolic_dfa, starting_player,
-                                        protagonist_player, symbolic_dfa.final_states(),
-                                        var_mgr->cudd_mgr()->bddOne());
-    Syft::SynthesisResult result = synthesizer.run();
+    for (size_t i = 0; i < formulas.size(); ++i){
+        std::string name = (i == 0) ? " main_agent" : " peer" + std::to_string(i);
+        std::string prefix= out_dir + "/" + name;
+        std::cout << "Generating DFA for" << name << " with formula: " << formulas[i] << std::endl;
+        std::stringstream formula_stream(formulas[i]);
+        driver->parse(formula_stream);
+        auto ltlf_ptr = driver->get_result();
+
+        //Explicit DFA
+        auto ltlf_formula = std::dynamic_pointer_cast<const whitemech::lydia::LTLfFormula>(ltlf_ptr);
+        Syft::ExplicitStateDfa dfa = Syft::ExplicitStateDfa::dfa_of_formula(*ltlf_formula);
+        dfa.export_dfa(prefix + ".mona");
+        whitemech::lydia::print_mona_dfa(
+            dfa.dfa_,
+            prefix,
+            dfa.get_nb_variables()
+        );
+
+        //Explicit DFA
+        Syft::ExplicitStateDfaAdd explicit_dfa_add = Syft::ExplicitStateDfaAdd::from_dfa_mona(var_mgr, dfa);
+        explicit_dfa_add.dump_dot(prefix + "_add.dot");
 
+        //Symbolic DFA
+        Syft::SymbolicStateDfa symbolic_dfa = Syft::SymbolicStateDfa::from_explicit(std::move(explicit_dfa_add));
+        symbolic_dfa.dump_dot(prefix + "_symbolic.dot");
+
+
+    }
+    std::cout << "\nCompleted" << std::endl;
 
-    std::cout << (result.realizability? "" : "NOT ") << "REALIZABLE" << std::endl;
     return 0;
+
 }

examples/01_quickstart/quickstartB.cpp

@@ -0,0 +1,87 @@
+#include <memory>
+#include <sstream>
+#include <string>
+#include <vector>
+#include <filesystem>
+
+#include <lydia/parser/ltlf/driver.hpp>
+
+#include "automata/ExplicitStateDfa.h"
+#include "automata/ExplicitStateDfaAdd.h"
+#include "automata/SymbolicStateDfa.h"
+#include "game/InputOutputPartition.h"
+#include "Player.h"
+#include "VarMgr.h"
+#include "synthesizer/LTLfSynthesizer.h"
+
+int main(int argc, char ** argv) {
+
+    // Define formulas
+    std::vector<std::string> formula_strs = {
+        "F(a & b)", "G(c)", "F(d | e)", "G(f)", "F(g & h)", "G(i)"
+    };
+
+    std::vector<std::string> input_vars = {"a", "b"};
+    std::vector<std::vector<std::string>> agent_vars = {
+        {"c"}, {"d", "e"}, {"f"}, {"g", "h"}, {"i"}
+    };
+
+    // Parse the formulas
+    std::vector<whitemech::lydia::ltlf_ptr> formulas;
+    auto driver = std::make_shared<whitemech::lydia::parsers::ltlf::LTLfDriver>();
+    for (const auto& formula_str : formula_strs) {
+        std::stringstream formula_stream(formula_str);
+        driver->parse(formula_stream);
+        formulas.push_back(std::dynamic_pointer_cast<const whitemech::lydia::LTLfFormula>(driver->get_result()));
+    }
+
+    // Initialize partition and variables
+    Syft::InputOutputPartition partition = Syft::InputOutputPartition::construct_from_input(input_vars, agent_vars);
+    std::shared_ptr<Syft::VarMgr> var_mgr = std::make_shared<Syft::VarMgr>();
+
+    std::vector<std::string> all_named_vars = partition.input_variables;
+    for (const auto& ag : partition.agent_variables) {
+        all_named_vars.insert(all_named_vars.end(), ag.begin(), ag.end());
+    }
+    var_mgr->create_named_variables(all_named_vars);
+
+    for (std::size_t i = 0; i < partition.agent_variables.size(); ++i) {
+        var_mgr->create_agent_variables(i, partition.agent_variables[i]);
+    }
+    var_mgr->partition_variables(partition.input_variables, partition.agent_variables);
+
+    std::string output_dir = "quickstart_outputs";
+    std::filesystem::remove_all(output_dir);
+    std::filesystem::create_directories(output_dir);
+
+
+    // Build and Save DFAs
+    for (size_t i = 0; i < formulas.size(); ++i) {
+        std::string base_name;
+        if (i == 0) {
+            base_name = "environment";
+        } else if (i == 1) {
+            base_name = "main_agent";
+        } else {
+            base_name = "peer_agent_" + std::to_string(i - 1);
+        }
+
+        // build the explicit-state DFA
+        Syft::ExplicitStateDfa explicit_dfa = Syft::ExplicitStateDfa::dfa_of_formula(*formulas[i]);
+        Syft::ExplicitStateDfaAdd explicit_dfa_add = Syft::ExplicitStateDfaAdd::from_dfa_mona(var_mgr, explicit_dfa);
+
+        explicit_dfa.export_dfa(output_dir + "/" + base_name + ".mona");
+        explicit_dfa_add.dump_dot(output_dir + "/" + base_name + "_explicit.dot");
+
+        // build the symbolic-state DFA from the explicit-state DFA
+        Syft::SymbolicStateDfa symbolic_dfa = Syft::SymbolicStateDfa::from_explicit(std::move(explicit_dfa_add));
+
+
+        std::string symbolic_dot_path = output_dir + "/" + base_name + "_symbolic.dot";
+        symbolic_dfa.dump_dot(symbolic_dot_path);
+
+        //std::cout << "Saved symbolic DFA for " << base_name << " to " << symbolic_dot_path << std::endl;
+    }
+
+    return 0;
+}

examples/01_quickstart/quickstartO.cpp

@@ -0,0 +1,105 @@
+#include <memory>
+#include <sstream>
+#include <string>
+#include <vector>
+#include <filesystem>
+
+#include <lydia/parser/ltlf/driver.hpp>
+
+#include "automata/ExplicitStateDfa.h"
+#include "automata/ExplicitStateDfaAdd.h"
+#include "automata/SymbolicStateDfa.h"
+#include "game/InputOutputPartition.h"
+#include "Player.h"
+#include "VarMgr.h"
+#include "synthesizer/LTLfSynthesizer.h"
+
+
+int main(int argc, char ** argv) {
+
+    // Define formulas: one for environment, one for main agent, and for peer agents
+    std::vector<std::string> formula_strs = {
+        "F(a & b)",          // Environment formula
+        "G(c)",              // Main agent formula
+        "F(d | e)",          // Peer agent 1 formula
+        "G(f)",              // Peer agent 2 formula
+        "F(g & h)",          // Peer agent 3 formula
+        "G(i)"               // Peer agent 4 formula
+    };
+
+    // Define variables: inputs and agents (vector of vectors)
+    std::vector<std::string> input_vars = {"a", "b"};
+    std::vector<std::vector<std::string>> agent_vars = {
+        {"c"},        // Main agent (index 0)
+        {"d", "e"},   // Peer agent 1 (index 1)
+        {"f"},        // Peer agent 2 (index 2)
+        {"g", "h"},   // Peer agent 3 (index 3)
+        {"i"}         // Peer agent 4 (index 4)
+    };
+
+    // parse the formula
+    std::vector<whitemech::lydia::ltlf_ptr> formulas;
+    auto driver = std::make_shared<whitemech::lydia::parsers::ltlf::LTLfDriver>();
+    for (const auto& formula_str : formula_strs) {
+        std::stringstream formula_stream(formula_str);
+        driver->parse(formula_stream);
+        formulas.push_back(std::dynamic_pointer_cast<const whitemech::lydia::LTLfFormula>(driver->get_result()));
+    }
+
+    // Initialize partition and variables
+    Syft::InputOutputPartition partition = Syft::InputOutputPartition::construct_from_input(input_vars, agent_vars);
+    std::shared_ptr<Syft::VarMgr> var_mgr = std::make_shared<Syft::VarMgr>();
+
+    // Create all named variables
+    std::vector<std::string> all_named_vars = partition.input_variables;
+    for (const auto& ag : partition.agent_variables) {
+        all_named_vars.insert(all_named_vars.end(), ag.begin(), ag.end());
+    }
+    var_mgr->create_named_variables(all_named_vars);
+
+    for (std::size_t i = 0; i < partition.agent_variables.size(); ++i) {
+        var_mgr->create_agent_variables(i, partition.agent_variables[i]);
+    }
+    var_mgr->partition_variables(partition.input_variables, partition.agent_variables);
+
+    std::string output_dir = "quickstart_outputs";
+    std::filesystem::remove_all(output_dir);
+    std::filesystem::create_directories(output_dir);
+
+    // Build DFAs for each agent
+    std::vector<Syft::ExplicitStateDfaAdd> explicit_dfas_add;
+    std::vector<Syft::SymbolicStateDfa> symbolic_dfas;
+    for (size_t i = 0; i < formulas.size(); ++i) {
+        Syft::ExplicitStateDfa explicit_dfa = Syft::ExplicitStateDfa::dfa_of_formula(*formulas[i]);
+        Syft::ExplicitStateDfaAdd explicit_dfa_add = Syft::ExplicitStateDfaAdd::from_dfa_mona(var_mgr, explicit_dfa);
+        std::cout << "DFA " << i << " (agent " << i << "): " << explicit_dfa_add.state_count() << " states" << std::endl;
+
+        std::string mona_file = output_dir + "/agent_" + std::to_string(i) + ".mona";
+        //std::cout << "Exporting DFA " << i << " to " << mona_file << std::endl;
+        explicit_dfa.export_dfa(mona_file);
+
+        explicit_dfas_add.push_back(explicit_dfa_add);
+
+        // Build symbolic DFA
+        Syft::SymbolicStateDfa symbolic_dfa = Syft::SymbolicStateDfa::from_explicit(std::move(explicit_dfa_add));
+        symbolic_dfas.push_back(symbolic_dfa);
+    }
+
+    // Check if everything worked
+    std::cout << "Multi-agent DFA construction successful! All modifications work." << std::endl;
+
+
+
+    // do synthesis
+    //var_mgr->partition_variables(partition.input_variables, partition.output_variables);
+    //Syft::Player starting_player = Syft::Player::Agent;
+    //Syft::Player protagonist_player = Syft::Player::Agent;
+    //Syft::LTLfSynthesizer synthesizer(symbolic_dfa, starting_player,
+    //                                    protagonist_player, symbolic_dfa.final_states(),
+    //                                    var_mgr->cudd_mgr()->bddOne());
+    //Syft::SynthesisResult result = synthesizer.run();
+
+
+    //std::cout << (result.realizability? "" : "NOT ") << "REALIZABLE" << std::endl;
+    return 0;
+}