Refactoring and finishing touches (#59)

* Unify the inference session title in UI.

* Unify naming of the inference session on the backend.

* Add propagating var id change into properties.

* Add note regarding web-based docs.

* Refactoring + documenting main TypeScript components.

* Fix issue in network sampling.

* Add new version of the example sketch.

* Update installation instruction.

* Update older todos.

* Add initial version of the manual.

* Instructions, refactoring, selenium tests.

* Update manual.

* Reorganize data folder, add additional data files.

* Add instructions for tauri on linux.

* Add tutorial video.

* Update project structure description.

README.md

@@ -9,7 +9,21 @@ Sketchbook presents a way to design all these components and more.
 
 Once you finish designing your sketch, you can run the state-of-the-art synthesis algorithms and symbolically compute all BNs consistent with your requirements. You can then sample individual BNs, or export the results for further analysis with libraries like [AEON.py](https://pypi.org/project/biodivine-aeon/).
 
-### Citation
+#### Manual and tutorial
+
+In the provided `manual.pdf`, we discuss the details regarding
+- installation,
+- editing BN sketches in Sketchbook,
+- running BN inference in Sketchbook,
+- format and syntax used.
+
+We also provide an introduction to Sketchbook using a short video tutorial that you can find as `tutorial.mp4`.
+This tutorial covers basics on how to edit an sketch and run the inference.
+For more details and explanations, see the manual.
+
+The installation is also summarized below, with an additional development guide.
+
+#### Citation
 
 If you used Sketchbook for some academic work, we'd be very happy if you could cite it using the following publication:
 
@@ -33,12 +47,17 @@ Alternatively, if you want to build the tool locally, the instructions are provi
 
 The following instructions describe the local installation of the application and relevant frameworks. We recommend using the pre-built binaries described in the previous section.
 
-For a summary of all technologies and detailed project structure, see `project-docs/ARCHITECTURE.md`. The directory `project-docs` also contains other documents relevant to the design/development.
+For a summary of all technologies and detailed project structure, see `project-docs/architecture.md`. The directory `project-docs` also contains other documents relevant to the design/development.
+
+We also provide web-based Rust documentation (including internal modules), currently hosted on [these GitHub pages](https://ondrej33.github.io/biodivine_sketchbook/). Instructions to generate Rust documentation locally are given below.
+
 
 ### Installation of dependencies
 
 First, make sure you have Rust and NPM installed. For Rust, we recommend following the instructions on [rustlang.org](https://www.rust-lang.org/learn/get-started). For instructions on NPM and Node installation, feel free to check [their website](https://docs.npmjs.com/downloading-and-installing-node-js-and-npm).
 
+On some Linux distributions, additional packages might be needed for developing with Tauri. We recommend checking the [setup instructions by Tauri](https://v1.tauri.app/v1/guides/getting-started/prerequisites/).
+
 We have tested the app using the following versions:
 - npm 10.9.0 
 - node 22.11.0
@@ -48,10 +67,9 @@ Then, after cloning the repository, run `npm install` to download all JS/TS depe
 
 ### Building the app
 
-To build a release version of the app, run `npm run build`. Note that the first build can take a few minutes as the application backend needs to be compiled. Subsequent builds should be a lot faster. 
-To properly build the full installation file for the app, you can also use `cargo tauri build`. It will create an installation bundle at `src-tauri/target/release/bundle`.
+To build a release version of the app, run `npm run tauri build`. It will create an installation bundle at `src-tauri/target/release/bundle/` (the exact path will be displayed at the end of the command's standard output). Note that the first build can take a few minutes as the application backend needs to be compiled. Subsequent builds should be a lot faster. 
 
-To start the application in debug mode, run `npm run tauri dev`. Note that upon startup, the application window can be unresponsive for a few seconds when using development mode. This is because the whole application is running in debug mode without any optimizations. This startup delay should be substantially reduced when using the release binaries produced by `npm run build`.
+To start the application in debug mode, run `npm run tauri dev`. Note that upon startup, the application window can be unresponsive for a few seconds when using development mode. This is because the whole application is running in debug mode without any optimizations. This startup delay should be substantially reduced when using the release binaries produced by `npm run tauri build`.
 
 ### Static analysis, tests, documentation
 
@@ -75,15 +93,20 @@ cargo doc --no-deps --document-private-items
 ```
 
 #### End-to-end tests
-We also utilize an end-to-end Selenium-based testing framework. Note that these tests require additional dependencies, and they are limited for Linux and Windows (due to MacOS issues with WebDriver). 
+We also utilize an end-to-end Selenium-based testing framework. Note that these tests require additional dependencies, and they are limited for Linux and Windows (due to MacOS issues with WebDriver). You should also update the test configs based on your system.
+
+You can follow this [detailed tutorial](https://jonaskruckenberg.github.io/tauri-docs-wip/development/testing.html) for setup. In short, you should install `tauri-driver` (with `cargo install tauri-driver`), and then you will need either `WebKitWebDriver` on Linux or `Microsoft Edge Driver` on Windows (make sure that you have updated Microsoft Edge too). The mocha test runner can be installed with `npm install mocha chai selenium-webdriver`. You might need to update the configuration at the top of the testing script `test/test.js`, mainly the path to your Sketchbook binary and to your webdriver.
 
-You can follow this [detailed tutorial](https://jonaskruckenberg.github.io/tauri-docs-wip/development/testing.html) for setup. In short, you should install `tauri-driver` (with `cargo install tauri-driver`), and then you will need either `WebKitWebDriver` on Linux or `Microsoft Edge Driver` on Windows (make sure that you have updated Microsoft Edge too). The mocha test runner can be installed with `npm install mocha chai selenium-webdriver`. 
-To run the tests, first build the app with `cargo tauri build` and then use `npx mocha` (you might need a longer timeout, like `npx mocha --timeout 20000`). 
+To run the tests, first build the app with `cargo tauri build` and then use `npx mocha` (you might need a longer timeout, like `npx mocha --timeout 20000`).
 The framework was tested on Windows with `Microsoft Edge WebDriver` version `130.0.2849.89`.
 However, note that we found the testing framework a bit unstable when the testing machine is overloaded with other tasks. Sometimes, the tests do not go through due to internal WebDriver issues, and we are investigating this.
 
-### Benchmarks
+## Benchmarks and data
 
 The benchmark models, results, and more details are in `data/benchmarks`. 
 There is also a README with further instructions, you can follow it.
 Tldr, to run the performance benchmarks, you can use python and execute them all with `python3 run_performance_eval.py`.
+
+Sketches and datasets relevant to cases studies on biological models and real datasets are in `data/real_cases`. There is also a README with further details.
+
+An example sketch used to introduce the framework is in `data/small_example`. Sketch is available in AEON and JSON format. We also provide results of the inference and the resulting sampled BN candidate.

data/load-results-aeon-py.py

@@ -3,7 +3,7 @@
 import zipfile
 
 # Path to the zip archive with results
-zip_file_path = Path("real_cases/results-tlgl.zip")
+zip_file_path = Path("real_cases/tlgl/results.zip")
 
 # Filenames inside the zip archive
 bn_filename = "derived_model.aeon"

data/readme.md

@@ -0,0 +1,7 @@
+This folder contains various models, benchmarks, and datasets. The structure is following:
+
+- `benchmarks` | Multiple sketches used for performance evaluation. Also contains expected output and metadata. Check `benchmarks/readme.md` for more details.
+- `real_cases` | Sketches and datasets relevant to cases studies on biological models and real datasets. Check `real_cases/readme.md` for more details.
+- `small_example` | An example sketch used to introduce the framework. Sketch is available in AEON and JSON format. We also provide results of the inference and the resulting sampled BN candidate.
+- `test_data` | Sketches and datasets for testing purposes. Used to test importing and inference.
+- `load-results-aeon-py.py` | Python script illustrating how to load a results archive exported by Sketchbook and load it into `aeon-py` library. You need to install python and biodivine_aeon library first (`https://pypi.org/project/biodivine-aeon/`). Script is just for illustration, so the path is fixed.

data/real_cases/readme.md

@@ -1,15 +1,17 @@
-A real case studies collected and adapted to BN sketches framework:
+A real case studies collected and adapted to BN sketches framework. The Arabidopsis is discussed in the Sketchbook thesis, while TLGL in our original theoretical paper. 
 
-1) Apoptosis case study:
+1) Arabidopsis sketch:
     - background: This model and expected attractor data is taken from [this paper](https://doi.org/10.3389/fgene.2018.00039) about the BN inference tool Griffin. Originally, the model was developed by La Rota et al. in [this paper](https://doi.org/10.1105/tpc.111.092619).
     - model: We use the fully unspecified model directly as is.
     - properties: We use two fixed-point properties adapted from the Griffin paper.
     - candidates after static: 4761711360
     - candidates after all: 439296
 
-2) TLGL case study:
+2) TLGL sketch:
     - background: The original model was developed by Saadatpour et al. in [this paper](https://doi.org/10.1371/journal.pcbi.1002267). It is a reduced version of the model developed by Zhang et al. in [this article](https://doi.org/10.1073/pnas.0806447105). The experimental attractor data comes [this work](https://doi.org/10.1371/journal.pcbi.1002267) as well.
     - model: We use a partially specified version of the reduced model, only assuming that Apoptosis must inactivate all variables.
     - properties: We use a fixed-point property for a "healthy attractor" (cell death) and a complex attractor property for a "diseased attractor", based on provided data regarding the T-LGL state.
     - candidates after static: 1296
-    - candidates after all: 486
+    - candidates after all: 486
+
+For both cases, we present the constructed sketch (in AEON and JSON format) and inference results produced by Sketchbook as a zip archive. There can be also additional datasets or other relevant model files.

data/small_example/previous-version/resulting-BN.aeon

@@ -0,0 +1,8 @@
+v_3 -| v_1
+v_1 -?? v_2
+v_2 -? v_3
+v_1 -> v_3
+v_3 -?? v_3
+$v_1: !v_3
+$v_2: v_1
+$v_3: ((v_1 & (!v_2 | v_3)) | (!v_1 & v_3))

data/small_example/resulting-BN.aeon

@@ -1,8 +1,11 @@
-v_3 -| v_1
-v_1 -?? v_2
-v_2 -? v_3
-v_1 -> v_3
-v_3 -?? v_3
-$v_1: !v_3
-$v_2: v_1
-$v_3: ((v_1 & (!v_2 | v_3)) | (!v_1 & v_3))
+#position:C:196.222646417978,222.1758650941348
+$C:(B & C) | (!A & B)
+B -> C
+A -| C
+C ->? C
+#position:A:24.815603034996407,225.86087672588792
+$A:C
+C -?? A
+#position:B:102.24128185543081,79.45256430306468
+$B:A
+A -> B

data/small_example/small_example_sketch.aeon

@@ -0,0 +1,26 @@
+C -?? A
+B -> C
+A -| C
+C ->? C
+A -> B
+$A: g(C)
+$B: A
+$C: B & h(A, C)
+#position:B:102.24128,79.45257
+#position:C:196.22264,222.17586
+#position:A:24.815603,225.86087
+#!dataset:d1:#`{"name":"dataset 1","id":"d1","annotation":"Example steady-state dataset with two attractor observations.","observations":[{"id":"o1","name":"observation 1","annotation":"","dataset":"d1","values":"111"},{"id":"o2","name":"observation 2","annotation":"","dataset":"d1","values":"000"}],"variables":["A","B","C"]}`#
+#!dynamic_property:dynamic_1:#`{"id":"dynamic_1","name":"Exists state reaching two attractors","annotation":"","variant":"GenericDynProp","formula":"\\exists {a}: \\exists {b}: \\exists {c}: ( \\jump{c}: ( EF {a} & EF {b} & ( \\jump {a}: AG EF {a} ) & ( \\jump {b}: ( AG EF {b} & ~EF {a} ) ) ) )         "}`#
+#!dynamic_property:dynamic_2:#`{"id":"dynamic_2","name":"Observations of dataset d1 are in attractors","annotation":"","variant":"HasAttractor","dataset":"d1","observation":null}`#
+#!function:g:#`{"id":"g","name":"g","annotation":"","arguments":[["Unknown","Unknown"]],"expression":""}`#
+#!function:h:#`{"id":"h","name":"h","annotation":"","arguments":[["Unknown","Unknown"],["Unknown","Unknown"]],"expression":""}`#
+#!static_property:essentiality_A_B:#`{"id":"essentiality_A_B","name":"Regulation essentiality property","annotation":"","variant":"RegulationEssential","input":"A","target":"B","value":"True","context":null}`#
+#!static_property:essentiality_A_C:#`{"id":"essentiality_A_C","name":"Regulation essentiality property","annotation":"","variant":"RegulationEssential","input":"A","target":"C","value":"True","context":null}`#
+#!static_property:essentiality_B_C:#`{"id":"essentiality_B_C","name":"Regulation essentiality property","annotation":"","variant":"RegulationEssential","input":"B","target":"C","value":"True","context":null}`#
+#!static_property:monotonicity_A_B:#`{"id":"monotonicity_A_B","name":"Regulation monotonicity property","annotation":"","variant":"RegulationMonotonic","input":"A","target":"B","value":"Activation","context":null}`#
+#!static_property:monotonicity_A_C:#`{"id":"monotonicity_A_C","name":"Regulation monotonicity property","annotation":"","variant":"RegulationMonotonic","input":"A","target":"C","value":"Inhibition","context":null}`#
+#!static_property:monotonicity_B_C:#`{"id":"monotonicity_B_C","name":"Regulation monotonicity property","annotation":"","variant":"RegulationMonotonic","input":"B","target":"C","value":"Activation","context":null}`#
+#!static_property:monotonicity_C_C:#`{"id":"monotonicity_C_C","name":"Regulation monotonicity property","annotation":"","variant":"RegulationMonotonic","input":"C","target":"C","value":"Activation","context":null}`#
+#!variable:A:#`{"id":"A","name":"A","annotation":"","update_fn":"g(C)"}`#
+#!variable:B:#`{"id":"B","name":"B","annotation":"","update_fn":"A"}`#
+#!variable:C:#`{"id":"C","name":"C","annotation":"","update_fn":"B & h(A, C)"}`#