Merge branch 'master' of https://github.com/zwang271/2022-Iowa-State-…

…REU-Temporal-Logic-

Documentation/BENCHMARKREADME.md

@@ -12,33 +12,33 @@ We ran all of our experiments on a computer with the following hardware specific
 All of these experiments could be run on a standard laptop in a reasonable time frame. Please allow additional runtime.
 
 1. WEST BENCHMARKING EXPERIMENTS: 
-In these experiments we measure the time it takes to compute the truth tables of formulas with different complexities (input formula length) and their output lengths. The generated random MLTL formulas and their measured complexities are provided in the input/output files for each experiment below. Please take care to not overwrite the provided output files.
+In these experiments we measure the time it takes to compute the truth tables of formulas with different complexities (input formula length) and their output lengths. The generated random MLTL formulas and their measured complexities are provided in the input/output files for each experiment below. Please take care to not overwrite the provided input/output files.
   - From the WEST tool root directory, `cd ./MLTL_reg/MLTL/`
   - Run the script `make benchmark_west`
   - Then run `./benchmark_west`
 
   - Subset 1: 2 Iterations (Depth), 5 Prop vars, Delta (Max interval length) = 10, Interval Max = 10
-	- Input: `random_mltl1.txt` in `./MLTL_reg/MLTL/complexity_graph`; use the option `n` to generate formulas;
+	- Input: `n` to formula generation; `./complexity_graph/random_mltl1.txt` for formula file;
 	`NUM_PROP_VARS = 5`
-	- Output: `complexities1.txt` in `./MLTL_reg/MLTL/complexity_graph`
+	- Output: `./complexity_graph/complexities1.txt`
 	- Runtime: approximately 3 minutes
 
   - Subset 2: 1 Iterations (Depth), 10 Prop vars, Delta (Max interval length) = 20, Interval Max = 20
-	- Input: `random_mltl2.txt` in `./MLTL_reg/MLTL/complexity_graph`; use the option `n` to generate formulas;
+	- Input: `n` to formula generation; `./complexity_graph/random_mltl2.txt` for formula file;
 	`NUM_PROP_VARS = 10`
-	- Output: `complexities2.txt` in `./MLTL_reg/MLTL/complexity_graph`
+	- Output: `./complexity_graph/complexities2.txt`
 	- Runtime: less than a second
 
   - Subset 3: 2 Iterations (Depth), 10 Prop vars, Delta (Max interval length) = 5, Interval Max = 10
-	- Input: `random_mltl3.txt` in `./MLTL_reg/MLTL/complexity_graph`; put `n` to generate formulas;
+	- Input: `n` to formula generation; `./complexity_graph/random_mltl3.txt` for formula file;
 	`NUM_PROP_VARS = 10`
-	- Output: `complexities3.txt` in `./MLTL_reg/MLTL/complexity_graph`
+	- Output: `./complexity_graph/complexities3.txt`
 	- Runtime: Approximately 1 minute
 
   - Subset 4: 1 Iterations (Depth), 5 Prop vars, Delta (Max interval length) = 10, Interval Max = 10
-	- Input: `random_mltl4.txt` in `./MLTL_reg/MLTL/complexity_graph`; `n` to generate formulas;
+	- Input: `n` to formula generation; `./complexity_graph/random_mltl4.txt` for formula file;
 	`NUM_PROP_VARS = 5`
-	- Output: `complexities4.txt` in `./MLTL_reg/MLTL/complexity_graph`
+	- Output: `./complexity_graph/complexities4.txt`
 	- Runtime: less than a second
 
   We generated the random MLTL formulas in the random_mltl files using by inputting `y` to generate

Documentation/GUIREADME.md

@@ -7,9 +7,10 @@ Our recursive algorithm is based on the regular expressions of MLTL operators an
 
 ## Additional Requirements
 - Posix environment (Linux, MacOS, Etc.)
-- Python3 (version 3.6 or greater)
-- C99 std compiler (gcc was the one used, others will likely work as well)
+- Python3 (version 3.6 or greater) with modules `dd`, `lark`, and `PtQt5`, which are all available through `pip`.
+- C99 std compiler (gcc was the one used, others will likely work as well.)
 - Make
+When running it on Linux, it may also require to install `qt5dxcb-plugin`, which is available from the `apt` library.
 
 ## Usage