example: add p05_api_example_ltlf_synthesis_maximally_permissive

docs/api/p05_api_example_ltlf_synthesis_maximally_permissive.md

@@ -0,0 +1,76 @@
+# LTLf Synthesis with Maximally Permissive Strategy {#p05_api_example_ltlf_synthesis_maximally_permissive}
+
+In this example, we will show how to use the LydiaSyft C++ APIs to solve LTLf synthesis with maximally permissive strategies.
+
+The code for this example can be found in `examples/05_ltlf_synthesis_maximally_permissive/ltlf_synthesis.cpp`.
+To build this example, you can run `make ltlf_synthesis_maximally_permissive_example`.
+
+
+```cpp
+#include <filesystem>
+#include <memory>
+#include <string>
+
+#include <lydia/parser/ltlf/driver.hpp>
+
+#include "automata/SymbolicStateDfa.h"
+#include "Player.h"
+#include "VarMgr.h"
+#include "Utils.h"
+#include "Preprocessing.h"
+
+
+int main(int argc, char ** argv) {
+
+    // parse TLSF file
+    std::filesystem::path ROOT_DIRECTORY = __ROOT_DIRECTORY;
+    std::filesystem::path tlsf_file_test = ROOT_DIRECTORY / "examples" / "test1.tlsf";
+    auto driver = std::make_shared<whitemech::lydia::parsers::ltlf::LTLfDriver>();
+    Syft::TLSFArgs args = Syft::parse_tlsf(driver, tlsf_file_test.string());
+    std::cout << "TLSF file parsed: " << tlsf_file_test.string() << std::endl;
+    std::cout << "Starting Player: " << (args.protagonist_player == Syft::Player::Agent? "Agent" : "Environment") << std::endl;
+    std::cout << "Protagonist Player: " << (args.starting_player == Syft::Player::Agent? "Agent" : "Environment") << std::endl;
+    std::cout << "Input variables: ";
+    for (const auto& var : args.partition.input_variables){
+        std::cout << var << ", ";
+    }
+    std::cout << std::endl;
+    std::cout << "Output variables: ";
+    for (const auto& var : args.partition.output_variables){
+        std::cout << var << ", ";
+    }
+    std::cout << std::endl;
+
+    // build variable manager
+    auto var_mgr = Syft::build_var_mgr(args.partition);
+
+    std::cout << "Building DFA of the formula..." << std::endl;
+    Syft::SymbolicStateDfa dfa = Syft::do_dfa_construction(*args.formula, var_mgr);
+
+    std::cout << "Solving the DFA game (with maximally permissive strategies)..." << std::endl;
+    var_mgr->partition_variables(args.partition.input_variables, args.partition.output_variables);
+
+    Syft::LTLfMaxSetSynthesizer synthesizer(dfa, args.starting_player,
+                                            args.protagonist_player, dfa.final_states(),
+                                            var_mgr->cudd_mgr()->bddOne());
+    Syft::MaxSetSynthesisResult result = synthesizer.run();
+    if (result.realizability) {
+        std::cout << "Specification is realizable!" << std::endl;
+        std::cout << "Printing the (maximally permissive) strategy in DOT format..." << std::endl;
+        var_mgr->dump_dot(result.deferring_strategy.Add(), "deferring_strategy.dot");
+        var_mgr->dump_dot(result.nondeferring_strategy.Add(), "nondeferring_strategy.dot");
+    }
+    else {
+        std::cout << "Specification is unrealizable!" << std::endl;
+    }
+
+}
+```
+
+The code is similar to the classical setting, except that:
+
+- the class `Syft::LTLfMaxSetSynthesizer` is used;
+- the result is an instance of the class `Syft::MaxSetSynthesisResult`;
+- we have two strategies: the _deferring_ strategy and the _nondeferring_ strategy
+
+The header file is named `synthesizer/LTLfMaxSetSynthesizer.h`.

docs/p00_api.md

@@ -6,3 +6,4 @@ In this part of the documentation, we show examples of how to use the C++ API of
 - @subpage p02_api_example_dfa_representation
 - @subpage p03_api_example_dfa_creation_and_manipulation
 - @subpage p04_api_example_ltlf_synthesis
+- @subpage p05_api_example_ltlf_synthesis_maximally_permissive

examples/05_ltlf_synthesis_maximally_permissive/CMakeLists.txt

@@ -0,0 +1,4 @@
+add_executable(ltlf_synthesis_maximally_permissive_example ltlf_synthesis_maximally_permissive.cpp)
+
+target_include_directories(ltlf_synthesis_maximally_permissive_example PRIVATE  ${UTILS_INCLUDE_PATH} ${PARSER_INCLUDE_PATH} ${SYNTHESIS_INCLUDE_PATH} ${EXT_INCLUDE_PATH})
+target_link_libraries(ltlf_synthesis_maximally_permissive_example ${PARSER_LIB_NAME} ${SYNTHESIS_LIB_NAME} ${UTILS_LIB_NAME} ${LYDIA_LIBRARIES})

examples/05_ltlf_synthesis_maximally_permissive/ltlf_synthesis_maximally_permissive.cpp

@@ -0,0 +1,59 @@
+#include <filesystem>
+#include <memory>
+#include <string>
+
+#include <lydia/parser/ltlf/driver.hpp>
+
+#include "automata/SymbolicStateDfa.h"
+#include "Player.h"
+#include "VarMgr.h"
+#include "Utils.h"
+#include "Preprocessing.h"
+
+
+int main(int argc, char ** argv) {
+
+    // parse TLSF file
+    std::filesystem::path ROOT_DIRECTORY = __ROOT_DIRECTORY;
+    std::filesystem::path tlsf_file_test = ROOT_DIRECTORY / "examples" / "test1.tlsf";
+    auto driver = std::make_shared<whitemech::lydia::parsers::ltlf::LTLfDriver>();
+    Syft::TLSFArgs args = Syft::parse_tlsf(driver, tlsf_file_test.string());
+    std::cout << "TLSF file parsed: " << tlsf_file_test.string() << std::endl;
+    std::cout << "Starting Player: " << (args.protagonist_player == Syft::Player::Agent? "Agent" : "Environment") << std::endl;
+    std::cout << "Protagonist Player: " << (args.starting_player == Syft::Player::Agent? "Agent" : "Environment") << std::endl;
+    std::cout << "Input variables: ";
+    for (const auto& var : args.partition.input_variables){
+        std::cout << var << ", ";
+    }
+    std::cout << std::endl;
+    std::cout << "Output variables: ";
+    for (const auto& var : args.partition.output_variables){
+        std::cout << var << ", ";
+    }
+    std::cout << std::endl;
+
+    // build variable manager
+    auto var_mgr = Syft::build_var_mgr(args.partition);
+
+    std::cout << "Building DFA of the formula..." << std::endl;
+    Syft::SymbolicStateDfa dfa = Syft::do_dfa_construction(*args.formula, var_mgr);
+
+    std::cout << "Solving the DFA game (with maximally permissive strategies)..." << std::endl;
+    var_mgr->partition_variables(args.partition.input_variables, args.partition.output_variables);
+
+    Syft::LTLfMaxSetSynthesizer synthesizer(dfa, args.starting_player,
+                                            args.protagonist_player, dfa.final_states(),
+                                            var_mgr->cudd_mgr()->bddOne());
+    Syft::MaxSetSynthesisResult result = synthesizer.run();
+    if (result.realizability) {
+        std::cout << "Specification is realizable!" << std::endl;
+        std::cout << "Printing the (maximally permissive) strategy in DOT format..." << std::endl;
+        var_mgr->dump_dot(result.deferring_strategy.Add(), "deferring_strategy.dot");
+        var_mgr->dump_dot(result.nondeferring_strategy.Add(), "nondeferring_strategy.dot");
+    }
+    else {
+        std::cout << "Specification is unrealizable!" << std::endl;
+    }
+
+
+}

examples/CMakeLists.txt

@@ -3,3 +3,4 @@ add_subdirectory(01_quickstart)
 add_subdirectory(02_dfa_representation)
 add_subdirectory(03_dfa_creation_and_manipulation)
 add_subdirectory(04_ltlf_synthesis)
+add_subdirectory(05_ltlf_synthesis_maximally_permissive)