Add CLI subcommands

README.md

@@ -1,6 +1,8 @@
-###Compilation Instructions using CMake
+# LydiaSyft: A Compositional Symbolic Synthesis Framework for LTLf Specification
 
-=== System-wide dependencies ===
+## Compilation Instructions using CMake
+
+### System-wide dependencies
 
 We assume the software will be built on a Ubuntu 22.04 machine.
 
@@ -18,7 +20,7 @@ sudo apt install -y \
 ```
 
 
-==== Install CUDD ====
+### Install CUDD
 
 0.1 Make sure CUDD is installed. CUDD can be found at: 
 
@@ -36,22 +38,22 @@ sudo apt install -y \
         autoreconf -i
 
 
-==== Install FLEX, BISON ====
+### Install FLEX, BISON
 
 0.3 Install flex and bison:
 
     sudo apt-get install flex bison
 
 
-==== Install LYDIA ====
+### Install LYDIA
 
     cd submodules
     cd lydia
 
 Follow the instructions to complete the installation of lydia.
 
 
-==== Install Z3 ====
+### Install Z3
 
 By default, the CMake configuration will fetch z3 automatically from the GitHub repository.
 In order to disable this behaviour, you can configure the project by setting -DZ3_FETCH=OFF.
@@ -67,7 +69,7 @@ cp bin/libz3.a /usr/local/lib
 cp include/*.h /usr/local/include
 ```
 
-=== Graphviz ===
+### Graphviz
 
 For the graphical features (automata and strategy visualization), graphviz need to be installed:
 
@@ -76,7 +78,7 @@ sudo apt install graphviz libgraphviz-dev
 ```
 
 
-==== Build LYDIASYFT ====
+## Build LYDIASYFT
 
 1. Make build folder so your directory is not flooded with build files:
 
@@ -98,12 +100,62 @@ sudo apt install graphviz libgraphviz-dev
    ```
 
 
-==== Run LYDIASYFT ====
+## Run LYDIASYFT
+
+Usage:
+```
+LydiaSyft: A compositional synthesizer for Linear Temporal Logic on finite traces (LTLf)
+Usage: ./cmake-build-debug/bin/LydiaSyft [OPTIONS] SUBCOMMAND
+
+Options:
+  -h,--help                   Print this help message and exit
+  --help-all                  Expand all help
+  -p,--print-strategy         Print out the synthesized strategy (default: false)
+  -t,--print-times            Print out running times of each step (default: false)
+
+Subcommands:
+  synthesis                   solve a classical LTLf synthesis problem
+  maxset                      solve LTLf synthesis with maximally permissive strategies
+  fairness                    solve LTLf synthesis with fairness assumptions
+  stability                   solve LTLf synthesis with stability assumptions
+  gr1                         Solve LTLf synthesis with GR(1) conditions
+```
 
-1. Reach executable file LydiaSyft
+To see the options of each subcommand, run:
+
+```
+LydiaSyft [SUBCOMMAND] --help
+```
 
-   ```cd bin```
+Examples (run commands from the root directory of the project):
 
-2. Run example:
-   ```./Lydiasyft -f ../../example/test.tlsf```
+- Classical synthesis:
 
+```
+./build/bin/LydiaSyft synthesis -f example/test.tlsf   # UNREALIZABLE
+./build/bin/LydiaSyft synthesis -f example/test1.tlsf  # REALIZABLE
+```
+
+- Maxset synthesis:
+
+```
+./build/bin/LydiaSyft maxset -f example/test.tlsf
+```
+
+- Fairness synthesis:
+
+```
+./build/bin/LydiaSyft .fairness -f example/fair_stable_test.tlsf -a example/fair_stable_test_assumption.txt  # REALIZABLE
+```
+
+- Stability synthesis:
+
+```
+./build/bin/LydiaSyft stability -f example/fair_stable_counter_test.tlsf -a example/fair_stable_test_assumption.txt  # REALIZABLE
+```
+
+- GR(1) synthesis:
+
+```
+./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
+```

src/CMakeLists.txt

@@ -2,8 +2,8 @@ add_subdirectory(utils)
 add_subdirectory(parser)
 add_subdirectory(synthesis)
 
-include_directories(${UTILS_INCLUDE_PATH} ${PARSER_INCLUDE_PATH} ${SYNTHESIS_INCLUDE_PATH} ${EXT_INCLUDE_PATH})
-add_executable(LydiaSyft Main.cpp)
+include_directories(cli ${UTILS_INCLUDE_PATH} ${PARSER_INCLUDE_PATH} ${SYNTHESIS_INCLUDE_PATH} ${EXT_INCLUDE_PATH})
+add_executable(LydiaSyft Main.cpp cli/base.cpp cli/fairness.cpp cli/gr1.cpp cli/maxset.cpp cli/stability.cpp cli/synthesis.cpp)
 
 target_link_libraries(LydiaSyft ${PARSER_LIB_NAME} ${SYNTHESIS_LIB_NAME} ${UTILS_LIB_NAME} ${LYDIA_LIBRARIES})