Merge pull request #33 from whitemech/docs-synthesis

Fixed synthesizers that skip the variable paritition

.gitmodules

@@ -4,3 +4,6 @@
 [submodule "submodules/slugs"]
 	path = submodules/slugs
 	url = https://github.com/VerifiableRobotics/slugs
+[submodule "submodules/doxygen-awesome-css"]
+	path = submodules/doxygen-awesome-css
+	url = https://github.com/jothepro/doxygen-awesome-css.git

README.md

@@ -47,11 +47,9 @@ sudo apt install -y \
 
 ### Install LYDIA
 
-    cd submodules
-    cd lydia
-
-Follow the instructions to complete the installation of lydia.
+The tool requires the installation of Lydia, which will be triggered by the CMake configuration.
 
+However, if you want to install Lydia manually, you can co into `submodules/lydia` and follow the installation instructions in the `README.md`.
 
 ### Install Z3
 
@@ -82,27 +80,36 @@ sudo apt install graphviz libgraphviz-dev
 
 1. Make build folder so your directory is not flooded with build files:
 
-    ```mkdir build && cd build```
+```
+mkdir build && cd build
+```
 
 3. Run CMake to generate the makefile:
 
-    ```cmake -DCMAKE_BUILD_TYPE=Release ..```
+```
+cmake -DCMAKE_BUILD_TYPE=Release ..
+```
 
 4. Compile using the generated makefile:
 
-    ```make -j$(nproc --ignore=1) LydiaSyft```
+```
+make -j$(nproc --ignore=1) LydiaSyft
+```
+
+4.1. For solving LTLf synthesis with GR(1) conditions, please install `slugs` following submodules/slugs/README.md
 
 5. Compile and Run tests:
 
-    ```
-    make -j$(nproc --ignore=1) tests
-    ./bin/tests
-   ```
+```
+make -j$(nproc --ignore=1) tests
+./bin/tests
+```
 
 
 ## Run LYDIASYFT
 
 Usage:
+
 ```
 LydiaSyft: A compositional synthesizer for Linear Temporal Logic on finite traces (LTLf)
 Usage: ./cmake-build-debug/bin/LydiaSyft [OPTIONS] SUBCOMMAND
@@ -139,13 +146,13 @@ Examples (run commands from the root directory of the project):
 - Maxset synthesis:
 
 ```
-./build/bin/LydiaSyft maxset -f example/test.tlsf
+./build/bin/LydiaSyft maxset -f example/test1.tlsf
 ```
 
 - Fairness synthesis:
 
 ```
-./build/bin/LydiaSyft .fairness -f example/fair_stable_test.tlsf -a example/fair_stable_test_assumption.txt  # REALIZABLE
+./build/bin/LydiaSyft fairness -f example/fair_stable_test.tlsf -a example/fair_stable_test_assumption.txt  # REALIZABLE
 ```
 
 - Stability synthesis:
@@ -155,7 +162,20 @@ Examples (run commands from the root directory of the project):
 ```
 
 - GR(1) synthesis:
+```
+./build/bin/LydiaSyft gr1 -f example/GR1benchmarks/finding_nemo_agn_goal.tlsf -g example/GR1benchmarks/finding_nemo_env_gr1.txt -e example/GR1benchmarks/finding_nemo_env_safety.ltlf -a example/GR1benchmarks/finding_nemo_agn_safety.ltlf --slugs-path ./submodules/slugs/
+```
+
+## Documentation
+
+The documentation is built using Doxygen. First, install `doxygen`:
+
+```
+sudo apt install doxygen
+```
+
+Then:
 
 ```
-./cmake-build-debug/bin/LydiaSyft gr1 -f example/GR1benchmarks/finding_nemo_agn_goal.tlsf -g example/GR1benchmarks/finding_nemo_env_gr1.txt -e example/GR1benchmarks/finding_nemo_env_safety.ltlf -a example/GR1benchmarks/finding_nemo_agn_safety.ltlf --slugs-path ./submodules/slugs/src/slugs
+doxygen Doxyfile
 ```

scripts/deploy-docs.sh

@@ -0,0 +1,42 @@
+#!/usr/bin/env bash
+
+set -x # un-comment to see what's going on when you run the script
+
+GITHUB_REPONAME="whitemech/LydiaSyft"
+
+# Create a temporary directory and store its name in a variable.
+TEMPD=$(mktemp -d)
+
+# Exit if the temp directory wasn't created successfully.
+if [ ! -e "$TEMPD" ]; then
+    >&2 echo "Failed to create temp directory"
+    exit 1
+fi
+
+# generate documentation
+doxygen Doxyfile
+
+# copy generated HTML documentation in the temporary folder
+cp -r ./docs/html/* "$TEMPD"
+
+# move to temporary directory
+CURDIR=$(pwd)
+cd $TEMPD
+
+# set up Git in temporary directory
+git init
+git checkout -b gh-pages
+git add .
+git commit -m "Deploy documentation"
+
+git remote add origin "[email protected]:${GITHUB_REPONAME}.git"
+
+# Push files
+git push origin gh-pages --force
+
+# return to previous directory
+cd $CURDIR
+
+# Make sure the temp directory gets removed on script exit.
+trap "exit 1"           HUP INT PIPE QUIT TERM
+trap 'rm -rf "$TEMPD"'  EXIT

src/cli/base.cpp

@@ -100,8 +100,8 @@ namespace Syft {
     }
 
     SymbolicStateDfa do_dfa_construction(const whitemech::lydia::LTLfFormula &formula, const std::shared_ptr<Syft::VarMgr> &var_mgr) {
-        ExplicitStateDfaMona explicit_dfa_mona = ExplicitStateDfaMona::dfa_of_formula(formula);
-        ExplicitStateDfa explicit_dfa = ExplicitStateDfa::from_dfa_mona(var_mgr, explicit_dfa_mona);
+        ExplicitStateDfa explicit_dfa_mona = ExplicitStateDfa::dfa_of_formula(formula);
+        ExplicitStateDfaAdd explicit_dfa = ExplicitStateDfaAdd::from_dfa_mona(var_mgr, explicit_dfa_mona);
         SymbolicStateDfa symbolic_dfa = SymbolicStateDfa::from_explicit(explicit_dfa);
         return symbolic_dfa;
     }

src/cli/fairness.cpp

@@ -12,7 +12,7 @@
 #include "Stopwatch.h"
 
 #include "../parser/Parser.h"
-#include "ExplicitStateDfaMona.h"
+#include "ExplicitStateDfa.h"
 #include "ReachabilitySynthesizer.h"
 #include "ReachabilityMaxSetSynthesizer.h"
 #include "InputOutputPartition.h"
@@ -42,6 +42,7 @@ namespace Syft {
     }
 
     void FairnessRunner::do_fairness_synthesis_(const SymbolicStateDfa &symbolic_dfa) const {
+        var_mgr_->partition_variables(args_.partition.input_variables, args_.partition.output_variables);
         Syft::FairReachabilitySynthesizer synthesizer(symbolic_dfa, args_.starting_player,
                                                       args_.protagonist_player, symbolic_dfa.final_states(),
                                                       var_mgr_->cudd_mgr()->bddOne(), assumption_filename_);

src/cli/gr1.cpp

@@ -8,7 +8,7 @@
 
 #include "Stopwatch.h"
 
-#include "ExplicitStateDfaMona.h"
+#include "ExplicitStateDfa.h"
 #include "ReachabilityMaxSetSynthesizer.h"
 #include "InputOutputPartition.h"
 #include "Preprocessing.h"
@@ -48,6 +48,7 @@ namespace Syft {
 
     void GR1Runner::do_gr1_synthesis_(const SymbolicStateDfa& agent_safety_dfa, const SymbolicStateDfa& env_safety_dfa, const SymbolicStateDfa& agent_goal_dfa) const {
         Syft::GR1 gr1 = Syft::GR1::read_from_gr1_file(var_mgr_, gr1_file_);
+        var_mgr_->partition_variables(args_.partition.input_variables, args_.partition.output_variables);
         Syft::GR1ReachabilitySynthesizer synthesizer(var_mgr_, gr1, env_safety_dfa,
                                                      agent_goal_dfa, agent_safety_dfa, path_to_slugs_, "problem");
         Syft::SynthesisResult result = synthesizer.run();

src/cli/stability.cpp

@@ -12,7 +12,7 @@
 #include "Stopwatch.h"
 
 #include "../parser/Parser.h"
-#include "ExplicitStateDfaMona.h"
+#include "ExplicitStateDfa.h"
 #include "ReachabilitySynthesizer.h"
 #include "ReachabilityMaxSetSynthesizer.h"
 #include "InputOutputPartition.h"
@@ -42,6 +42,7 @@ namespace Syft {
     }
 
     void StabilityRunner::do_stability_synthesis_(const Syft::SymbolicStateDfa &symbolic_dfa) {
+        var_mgr_->partition_variables(args_.partition.input_variables, args_.partition.output_variables);
         Syft::StableReachabilitySynthesizer synthesizer(symbolic_dfa, args_.starting_player,
                                                         args_.protagonist_player, symbolic_dfa.final_states(),
                                                         var_mgr_->cudd_mgr()->bddOne(), assumption_filename_);