# PyDejaVu
[](https://opensource.org/license/apache-2-0)
`PyDejaVu` is a Python library that wraps the original [DejaVu](https://github.com/havelund/dejavu/tree/master) binary,
providing a bridge between Python and the
Scala-based (and JVM-based) DejaVu runtime verification tool. It is a powerful tool designed for two-phase
Runtime Verification (RV) processing, similar to the [Tp-DejaVu](https://github.com/moraneus/TP-DejaVu) tool,
combining the flexibility and expressiveness of
Python with the rigorous, declarative monitoring capabilities of
the DejaVu tool.
#### Two-Phase Runtime Verification
`PyDejaVu` operates in two distinct phases:
1. **Operational Runtime Verification (Phase 1):**
- This phase is implemented in Python, allowing for any Pythonic operations on the events.
You can perform arithmetic, string manipulations, and Boolean logic, and leverage
Python's extensive data structures and objects for storing data and making complex calculations.
This flexibility enables `PyDejaVu` to handle a wide range of operational tasks during runtime,
offering users the ability to customize how events are processed and analyzed.
2. **Declarative Monitoring (Phase 2):**
- The second phase is declarative and leverages the DejaVu tool to perform monitoring against a first-order
past time temporal logic specification. This phase ensures that the runtime behavior conforms to the formal properties
defined in the specification. By integrating with DejaVu, `PyDejaVu` provides a robust framework for verifying
that the system adheres to specified safety properties, making it suitable for applications requiring
high levels of assurance.
## PyDejaVu Installation
`PyDejaVu` is a Unix-compatible tool designed for cross-platform use, initially developed on macOS
and tested on both macOS and Ubuntu Linux distributions.
While specifically tested on these two platforms, `PyDejaVu` may potentially work on other Unix-like
systems as well, though this would require further testing to confirm.
It's important to note that as a Unix-based tool, `PyDejaVu` is not natively compatible with
Windows and may require additional setup and modifications, to run on Windows machines.
Here we suggest three methods of installation:
- [**Pip Installation**](#pip-installation):
For users who need to use `PyDejaVu` without making changes to the codebase, pip offers a quick
and straightforward setup.
This method allows you to focus on using the tool rather than managing its dependencies.
- [**Docker Installation**](#docker-installation):
Docker provides a robust solution for running `PyDejaVu` in an isolated and consistent environment.
This method is ideal for users who prefer not to modify their local system or manage package
installations manually.
With Docker, you don't need to prepare your system for running `PyDejaVu`, as the Docker image comes
pre-packaged with all the necessary Scala and Java dependencies required for `DejaVu`.
- [**Source Code Installation**](#source-code-installation):
Installing the source code is a great option if you need more flexibility and control over the `PyDejaVu` project.
Here are some reasons why you might choose this method:
- **Customization and Modification:** If you plan to modify the code to suit specific requirements or contribute to the project, installing the source code gives you direct access to all the files. This is ideal for developers who want to extend or alter the functionality of `PyDejaVu`.
- **Development and Debugging:** When working on new features or fixing bugs, having the source code installed locally allows you to test changes immediately. This setup is essential for contributors or developers actively working on the `PyDejaVu` project.
- **Learning and Exploration:** If you're interested in understanding how `PyDejaVu` works internally, studying the source code can be very educational. You can explore the implementation details, experiment with changes, and see how different components interact.
### Pip Installation
👉 Before proceeding, ensure your environment is properly configured according to the instructions
in the [environment setup guide](docs/ENVIRONMENT_SETUP.md). This step is crucial for the
successful execution of `PyDejaVu` and helps prevent potential issues arising from an incorrectly
set up environment.
#### Step 1: Create Virtual Environment
Creating a virtual environment is highly recommended when installing `PyDejaVu`.
A virtual environment isolates your project's dependencies from the global Python installation,
preventing package conflicts and making dependency management easier.
Create the Virtual Environment:
```bash
python3 -m venv pydejavu-env
```
This command creates a new directory called pydejavu-env containing the isolated Python environment.
Activate the Virtual Environment:
```bash
source pydejavu-env/bin/activate
```
After activation, your command prompt will change to indicate that you are now using the virtual environment.
👉**Note**: Remember to activate the virtual environment each time you start a new session to
ensure you are using the isolated environment.
#### Step 2: Install PyDejaVu
With the virtual environment activated, install the latest version of `PyDejaVu` from PyPI:
```bash
pip install pydejavu-rv
```
This command will download and install `PyDejaVu` along with all its dependencies into your virtual environment.
To upgrade an existing installation to the latest version:
```bash
pip install --upgrade pydejavu-rv
```
#### Step 3: Verify the Installation
After installation, verify that `PyDejaVu` has been installed correctly:
```bash
pip show pydejavu-rv
```
This command should display details about the `PyDejaVu` package, confirming a
successful installation within your virtual environment.
You should see output similar to:
```bash
Name: PyDejaVu-RV
Version: x.y.z
Summary: PyDejaVu is a Python implementation that wraps the original DejaVu jar file, providing a bridge between Python and the Java-based DejaVu runtime verification tool. This wrapper extends DejaVu's functionality by supporting a 2-phase monitoring approach.
Home-page: https://github.com/moraneus/pydejavu
Author: moraneus
Author-email: moraneus@gmail.com
License: Apache-2.0
Location: /path/to/your/python/site-packages
Requires: psutil, pyjnius, pytest, pytest-forked, pytest-xdist
```
#### Step 4: Operate PyDejaVu
To test the library and explore the capabilities of `PyDejaVu`,
you can download the
[experiments archive](https://raw.githubusercontent.com/moraneus/pydejavu/main/experiments/experiments.zip),
which contains the experiments
used in our paper. This archive includes three folders named `example_1`, `example_2` and `example_3`,
each corresponding to a different experiment. Each example folder contains all the necessary
files to run the experiment.
- Extract the [experiments.zip](https://raw.githubusercontent.com/moraneus/pydejavu/main/experiments/experiments.zip)
file:
```bash
unzip experiments.zip
```
- Change directory to the example folder you wish to run:
```bash
cd example_X
```
Replace `X` with the example number (1 to 3).
- Execute the experiment using the provided bash script. **Make sure you are execute it from the virtual environment**.
```bash
./run_experiment
```
In some cases, if `run_experiment` cannot be run, you need to make it executable using the following command:
```bash
chmod +x run_experiment
```
This script automates the execution of all experiments within the specified `example_X` folder.
It sequentially runs the experiments using different log files to evaluate PyDejaVu's performance
across varying trace sizes (10K, 100K, 500K, and 1M). Upon completion, the results will be saved
in a file named `result-spec-X`.
#### 🛠️ Troubleshooting
If you encounter issues during installation or usage of `PyDejaVu`, consider the following:
- **Python Environment**: Ensure your Python environment is correctly configured and you have
the necessary permissions to install packages.
- **Virtual Environment**: If using a virtual environment, activate it before running
the pip install command:
```bash
source path/to/your/venv/bin/activate
```
- **Dependencies**: If you encounter dependency-related issues, try installing them separately
```bash
pip install psutil pyjnius pytest pytest-forked pytest-xdist
```
- **Version Conflicts**: In case of version conflicts, consider creating a new virtual environment
for a clean installation.
- **System Requirements**: Ensure your system meets the requirements for running Java-based
applications, as `PyDejaVu` relies on a Java runtime.
### Docker Installation
The Docker installation process automatically clones the latest `PyDejaVu` source code inside
the container. Unlike the standard installation method, it does not use the `pip install
pydejavu-rv` command. Instead, it builds and installs `PyDejaVu` directly from the cloned
source code within the Docker environment.
This approach ensures that you are running the most recent version of `PyDejaVu`,
including the latest features and updates that may not yet be available through PyPI.
#### Prerequisites
Ensure Docker is installed. You can download
Docker from [here](https://docs.docker.com/engine/install/).
#### Step 1: Clone the Repository
First, clone the repository to your local machine:
```bash
git clone https://github.com/moraneus/pydejavu.git
cd pydejavu
```
#### Step 2: Build the Docker Image
Ensure the Docker service is running, then build the image:
```bash
docker build -t pydejavu .
```
This command creates a Docker image named "pydejavu" (based on a `Dockerfile` located in the root project folder)
with the following features:
- Ubuntu based environment for running `PyDejaVu`.
- Java and Scala installations.
- Python with Poetry for dependency management.
- `PyDejaVu` and its dependencies.
- Linter and tests run to ensure proper configuration.
You should see output similar to:
```bash
[+] Building 412.7s (17/17) FINISHED
=> [internal] load build definition from Dockerfile 0.0s
=> => transferring dockerfile: 2.32kB 0.0s
=> [internal] load .dockerignore 0.0s
=> => transferring context: 2B 0.0s
=> [internal] load metadata for docker.io/library/python:3.12-slim 2.6s
=> [ 1/13] FROM docker.io/library/python:3.12-slim@sha256:XXXchecksumXXX 57.4s
=> => resolve docker.io/library/python:3.12-slim@sha256:XXXchecksumXXX 0.0s
=> => sha256:XXXchecksumXXX 9.12kB / 9.12kB 0.0s
=> => sha256:XXXchecksumXXX 1.75kB / 1.75kB 0.0s
=> => sha256:XXXchecksumXXX 5.11kB / 5.11kB 0.0s
=> => sha256:XXXchecksumXXX 29.16MB / 29.16MB 6.1s
=> => sha256:XXXchecksumXXX 3.33MB / 3.33MB 0.8s
=> => sha256:XXXchecksumXXX 13.38MB / 13.38MB 57.1s
=> => sha256:XXXchecksumXXX 250B / 250B 1.2s
=> => extracting sha256:XXXchecksumXXX 0.5s
=> => extracting sha256:XXXchecksumXXX 0.1s
=> => extracting sha256:XXXchecksumXXX 0.3s
=> => extracting sha256:XXXchecksumXXX 0.0s
=> [ 2/13] RUN apt-get update && apt-get install -y curl wget gnupg2 software-properties-common unzip zip && rm -rf /var/lib/apt/lists/* 21.8s
=> [ 3/13] RUN wget -O- https://packages.adoptium.net/artifactory/api/gpg/key/public | tee /usr/share/keyrings/adoptium.asc && echo "deb [signed-by=/usr/share/keyrings/adoptium.asc] https:// 179.2s
=> [ 4/13] RUN curl -s "https://get.sdkman.io" | bash && bash -c "source $HOME/.sdkman/bin/sdkman-init.sh && sdk install scala 2.12.18" 14.6s
=> [ 5/13] RUN bash -c "source $HOME/.sdkman/bin/sdkman-init.sh && scalac -version && java -version && python --version" 0.6s
=> [ 6/13] RUN pip install --no-cache-dir "poetry==1.6.1" 18.4s
=> [ 7/13] RUN poetry config virtualenvs.create false 0.5s
=> [ 8/13] RUN pip install flake8 2.5s
=> [ 9/13] RUN git clone https://github.com/moraneus/pydejavu.git /app 20.1s
=> [10/13] WORKDIR /app 0.0s
=> [11/13] RUN poetry install --no-interaction --no-ansi 2.2s
=> [12/13] RUN bash -c "source $HOME/.sdkman/bin/sdkman-init.sh && flake8 . --count --select=E9,F63,F7,F82 --show-source --statistics && flake8 . --count --exit-zero --max-complexity=10 --max-line 0.7s
=> [13/13] RUN bash -c "source $HOME/.sdkman/bin/sdkman-init.sh && pytest --forked" 90.6s
=> exporting to image 1.4s
=> => exporting layers 1.4s
=> => writing image sha256:XXXchecksumXXX 0.0s
=> => naming to docker.io/library/pydejavu
```
#### Step 3: Run the Docker Container
Start an interactive session in the Docker container:
```bash
docker run -it pydejavu
```
This command starts an interactive session inside the Docker container,
where `PyDejaVu` is set up and ready to use.
#### Step 4: Operate PyDejaVu
Inside the Docker container, you can use `PyDejaVu` with no addition configuration. For example:
##### Example: Running a Pre-defined Monitor
```bash
cd /app/examples/pydejavu_monitor
python monitor_for_detecting_suspicious_login_patterns.py
```
##### Example: Using the CLI
```bash
cd /app/examples/cli
python -m pydejavu --bits 20 --stats true --qtl sample.qtl --operational sample.pqtl --trace sample.log
```
##### Example: Experiments
Since we are using the `PyDejaVu` source code inside the Docker container
we have direct access to the experiment folders.
- Change directory to the experiment folder you wish to test:
```bash
cd /app/experiments/example_X
```
Replace `X` with the example number (1 to 3).
- Execute the experiments using the provided bash script:
```bash
bash -i run_experiment
```
This script automates the execution of all experiments within the specified `example_X` folder.
It sequentially runs the experiments using different log files to evaluate PyDejaVu's performance
across varying trace sizes (10K, 100K, 500K, and 1M). Upon completion, the results will be saved
in a file named `result-spec-X`.
#### 🛠️ Troubleshooting
- **Docker Service**: Ensure the Docker service is running before building or running containers.
- **Persistent Storage**: To persist data between container runs and share files between your host
machine and the Docker container, you can use Docker volumes.
This is particularly useful when you have predefined `PyDejaVu` monitor files or other
resources on your local machine that you want to use inside the container without
copying or rewriting them:
```bash
docker run -it -v /path/on/host:/path/in/container pydejavu
```
- **Resource Allocation**: If `PyDejaVu` requires more resources, allocate them using Docker's resource flags:
```bash
docker run -it --cpus 2 --memory 4g pydejavu
```
- **Cached Images**: If the Docker build command completes unusually quickly (within a few seconds),
it's likely using cached images from previous builds. In this case, you may need to
remove the older Docker containers and images associated with your project
(in this case, `pydejavu`) to force a fresh build. Here's how you can do this:
1. Stop and remove existing containers:
```bash
docker stop $(docker ps -a -q --filter ancestor=pydejavu)
docker rm $(docker ps -a -q --filter ancestor=pydejavu)
```
2. Remove associated images:
```bash
docker rmi $(docker images | grep pydejavu | awk '{print $3}')
```
3. Rebuild your Docker image:
```bash
docker build --no-cache -t pydejavu .
```
This process ensures that your next build will create a fresh image
without relying on potentially outdated cached layers.
- **Debugging**: To debug issues, you can start a shell in the container:
```bash
docker run -it pydejavu /bin/bash
```
### Source Code Installation
👉 Before proceeding, ensure your environment is properly configured according to the instructions
in the [environment setup guide](docs/ENVIRONMENT_SETUP.md). This step is crucial for the
successful execution of `PyDejaVu` and helps prevent potential issues arising from an incorrectly
set up environment.
#### Step 1: Clone the Repository
First, clone the repository to your local machine:
```bash
git clone https://github.com/moraneus/pydejavu.git
cd pydejavu
```
#### Step 2: Install Poetry
This project uses [Poetry](https://python-poetry.org/) for managing dependencies and packaging.
Follow these steps to set up your development environment:
1. Create and activate a virtual environment:
```bash
python3 -m venv pydejavu-env
source pydejavu-env/bin/activate
```
2. Install Poetry:
```bash
pip install poetry
```
3. Verify the installation:
```bash
poetry --version
```
If Poetry is correctly installed, you should see the version number.
#### Step 3: Install Project Dependencies
With Poetry installed, you can now install the project dependencies.
Run the following command in the root directory of the project:
```bash
poetry install
```
This will create a `poetry.lock` file and install all necessary dependencies for the project.
#### Step 4: Operate PyDejaVu
After the installation is finished we can use `PyDejaVu` with no addition configuration.
##### Example: Running a Pre-defined Monitor
👉**Note**: Make sure you are in the root directory of `PyDejaVu`.
```bash
cd examples/pydejavu_monitor
python monitor_for_detecting_suspicious_login_patterns.py
```
##### Example: Using the CLI
👉**Note**: Make sure you are in the root directory of `PyDejaVu`.
```bash
cd /app/examples/cli
python -m pydejavu --bits 20 --stats true --qtl sample.qtl --operational sample.pqtl --trace sample.log
```
##### Example: Experiments
Since we are using the `PyDejaVu` source code we have direct access to the experiment folders.
👉**Note**: Make sure you are in the root directory of `PyDejaVu`.
- Change directory to the experiment folder you wish to test:
```bash
cd experiments/example_X
```
Replace `X` with the example number (1 to 3).
- Execute the experiments using the provided bash script:
```bash
./run_experiment
```
This script automates the execution of all experiments within the specified `example_X` folder.
It sequentially runs the experiments using different log files to evaluate PyDejaVu's performance
across varying trace sizes (10K, 100K, 500K, and 1M). Upon completion, the results will be saved
in a file named `result-spec-X`.
#### 🛠️ Troubleshooting
If you encounter issues during installation or while running the project, consider the following:
- Ensure that your Python version meets the minimum requirement.
- Check that Poetry is correctly installed and accessible from your command line.
- Verify that all dependencies are properly installed by running poetry show.
## Usage
In this section, we present a simple usage of the tool divided into two
examples. The first example demonstrates how users can easily operate `DejaVu` directly
from `PyDejaVu`. The second example builds upon the first, showing how to enhance the
expressiveness of your application by leveraging the power of `PyDejaVu`.
By leverages `DejaVu`'s capabilities, `PyDejaVu` involves a few steps before it starts
the evaluation process. First, it analyzes and parses the specification to ensure it
meets the syntax of QTL (Quantified Temporal Logic).
Then, it compiles a Scala-based monitor.
This Scala compilation step may take some time, so don't be alarmed if there is a delay
during this process.
For more advanced usage and explanations, please refer to the [documentation](docs/ADVANCED_USAGE.md).
### Example 1
Consider a simple filesystem mechanism that handles several key events. The filesystem
allows opening a file with the an `open(F, f, m, s)`, carrying as arguments the
folder name `F`, the filename `f` (technically a file id), the access mode `m` (read or write), and the size
`s` which is the maximal number of bytes that can be written. The `close(f)` event
indicates that a file `f` has been closed. The write event `write(f, d)` contains the
filename and the data `d` (a string) being written. Additionally, the system
supports `create(F)` and `delete(F)` events, which represent the creation or deletion
of a folder.
The requirement we are verifying states that if data is written to a file, the
file must have been opened in write mode, not closed since, and must reside in
a folder that has been created and not deleted since.
```python
from pydejavu.core.monitor import Monitor
specification = """
prop example: forall f . forall d .
write(f, d) ->
(exists F . Exists s .
((!close(f) S open(F, f, "w", s)) & (!delete(F) S create(F))))
"""
monitor = Monitor(specification)
events = [
{"name": "create", "args": ["tmp"]},
{"name": "open", "args": ["tmp", "f1", "w", "5"]},
{"name": "write", "args": ["f1", "some text"]},
{"name": "close", "args": ["f1"]},
{"name": "delete", "args": ["tmp"]}
]
for e in events:
monitor.verify(e)
monitor.end()
```
This code snippet demonstrates how to operate `DejaVu` directly
from `PyDejaVu` to perform runtime verification based on a formal specification written in first-order
past time temporal logic.
First, the Monitor class is imported from `pydejavu.core.monitor`,
and the specification, named as `example`, is defined as a multi-line string.
The monitor is then initialized with this specification, setting up the verification environment.
A list of events is created to simulate a sequence of I/O operations: creating a folder (`create`),
opening a file (`open`), writing to it (`write`), closing it (`close`),
and finally deleting the hosting folder (`delete`).
Each event is a dictionary containing the event name and its arguments.
The events are processed in a loop where each event is passed to the `monitor.verify(e)` method.
In this case, where no event handlers are defined, the events are forwarded directly to the declarative phase
for verification against the specification.
After all events are processed, `monitor.end()` is called to finalize the evaluation.
This step is crucial for obtaining statistics results and for the monitor
to release resources appropriately.
#### Example 1 Output
As shown in the following output snippet, this example reports no errors.
```bash
0 errors detected!
==================
Event Counts:
------------------
create : 1
open : 1
delete : 1
close : 1
write : 1
==================
- Garbage collector was not activated
```
### Example 2
```python
from pydejavu.core.monitor import Monitor, event
specification = """
prop example: forall f .
!write(f, "false") & (write(f, "true") ->
(exists F . ((!close(f) S open(F, f, "w")) & (!delete(F) S create(F)))))
"""
monitor = Monitor(specification)
total_sizes: dict[str, int] = {}
@event("open")
def open(F: str, f: str, m: str, s: int):
global total_sizes
if m == "w":
total_sizes[f] = s
return ["open", F, f, m]
@event("close")
def close(f: str):
global total_sizes
del total_sizes[f]
return ["close", f]
@event("write")
def write(f: str, d: str):
global total_sizes
if f not in total_sizes:
total_sizes[f] = 0
data_len = len(d)
ok = total_sizes[f] >= data_len
if ok:
total_sizes[f] -= data_len
return ["write", f, ok]
events = [
{"name": "create", "args": ["tmp"]},
{"name": "open", "args": ["tmp", "f1", "w", "5"]},
{"name": "write", "args": ["f1", "some text"]},
{"name": "close", "args": ["f1"]},
{"name": "delete", "args": ["tmp"]}
]
for e in events:
monitor.verify(e)
monitor.end()
```
This code differs from the previous example by incorporating operational event handlers that
perform real-time computations and state management before events are passed to the
declarative phase for verification. In the earlier code, events were directly forwarded to
the declarative phase without any operational processing.
Here, the `@event` decorator is used to define custom handlers for the `open`, `close`,
and `write` events, enabling the code to maintain and manipulate state during the operational
phase. Generally, the handlers are decorated with the `@event("event_name")` decorator,
linking them to specific events in your specification.
This definition is optional; if no handler is defined for a specific event, `PyDejaVu` will forward the
event directly to DejaVu for evaluation. Without any handler definitions, PyDejaVu functions
the same as `DejaVu` without the operational phase.
A key difference is the introduction of the `total_sizes` dictionary,
which tracks the remaining allowed write sizes for each file.
In the `open` handler, the code checks if the file is opened in write mode `"w"` and
initializes the total allowed size `s` for that file in the `total_sizes` dictionary.
The `write` handler then uses this information to ensure that the length of the data
being written does not exceed the remaining allowed size.
It calculates the length of the data `d`, compares it against the remaining size for the file,
and updates the `total_sizes` accordingly.
If the `write` operation exceeds the allowed size, an `ok` flag is set to `False`,
indicating that the `write` is not permitted.
These operational event handlers allow for immediate enforcement of constraints and
preliminary checks before events are evaluated against the formal specification in
the declarative phase. By performing these computations upfront, the code can prevent
invalid or undesirable events from proceeding further, enhancing efficiency and providing
immediate feedback. This integration of operational logic with declarative specifications
showcases how `PyDejaVu` increases the expressiveness of the system, enabling more complex
and nuanced runtime verification scenarios compared to the previous example where such
operational checks were absent.
#### Example 2 Output
As shown in the following output snippet, this example reports one error because it failed when
attempting to write the `"some text"` string into `f1`, which is limited to 5 characters.
```bash
1 errors detected!
==================
Event Counts:
------------------
create : 1
open : 1
delete : 1
close : 1
write : 1
==================
- Garbage collector was not activated
```
### More Usage Examples
You can find more comprehensive usage examples of monitors in the [examples](https://github.com/moraneus/pydejavu/tree/main/examples/pydejavu_monitor) folder
and the [experiments](https://github.com/moraneus/pydejavu/tree/main/experiments) folder. These folders contain various use cases and demonstrations
of how to effectively use `PyDejaVu` for runtime verification.
## Output Files
After each execution of `PyDejaVu`, several output files are generated and stored in designated folders.
These outputs are crucial for reviewing the results of the verification process and understanding the
internal workings of the tool.
### Logs Folder:
The logs folder will contain the log file from the last execution.
This log file is named with a timestamp to ensure that each run's output is distinct and easy to identify.
### Output Folder:
The `output` folder contains several important files generated during the verification process:
- `ast.dot`: A Graphviz source file used to create an abstract syntax tree (AST) graph for the specification.
This file can be visualized using Graphviz to better understand the structure of the specification.
- `TraceMonitor.jar`: If the specification was compiled into a Java archive, this file will contain the
compiled monitor.
- `TraceMonitor.scala`: If the specification was synthesized into Scala code, this file will be generated.
It represents the synthesized monitor in Scala.
- `resultFile`: This file is primarily used in unit testing to compare the expected errors with
the actual errors encountered. It contains the results of the original `DejaVu` execution,
capturing any errors from the verification process. When an error occurs, the event index is
written to this file. However, be aware that the `resultFile` remains empty if no errors
are detected during verification. To ensure the `resultFile` is created correctly,
make sure to run `monitor.end()` to notify `DejaVu` to close the result file and finalize
the execution.
- `generated_trace.py` (Optional): This file is automatically generated when the user utilizes the CLI options.
In this case, a `PyDejaVu` script is created in the working directory,
tailored to the user's input parameters for runtime verification.
These output files provide a comprehensive overview of each execution, allowing you to analyze and debug the
behavior of your specifications in detail.
```bash
output/
├── ast.dot
├── TraceMonitor.jar
├── TraceMonitor.scala
├── resultFile
└── generated_trace.py (Optional)
```
## Contributors - For `PyDejaVu` (Ordered by last name):
* [Klaus Havelund](http://www.havelund.com), Jet Propulsion Laboratory/NASA, USA
* [Moran Omer](https://github.com/moraneus), Bar Ilan University, Israel
* [Doron Peled](http://u.cs.biu.ac.il/~doronp), Bar Ilan University, Israel
Raw data
{
"_id": null,
"home_page": "https://github.com/moraneus/pydejavu",
"name": "PyDejaVu-RV",
"maintainer": null,
"docs_url": null,
"requires_python": "<4.0,>=3.8",
"maintainer_email": null,
"keywords": "runtime verification, dejavu, monitoring, java bridge",
"author": "moraneus",
"author_email": "moraneus@gmail.com",
"download_url": "https://files.pythonhosted.org/packages/9f/f0/4cad0dccdc37032b253a80845c536ae4a0fd091c583a31650bbb1091b3e9/pydejavu_rv-1.0.0.tar.gz",
"platform": null,
"description": "# PyDejaVu\n\n\n\n[](https://opensource.org/license/apache-2-0)\n\n\n\n`PyDejaVu` is a Python library that wraps the original [DejaVu](https://github.com/havelund/dejavu/tree/master) binary, \nproviding a bridge between Python and the \nScala-based (and JVM-based) DejaVu runtime verification tool. It is a powerful tool designed for two-phase \nRuntime Verification (RV) processing, similar to the [Tp-DejaVu](https://github.com/moraneus/TP-DejaVu) tool, \ncombining the flexibility and expressiveness of \nPython with the rigorous, declarative monitoring capabilities of \nthe DejaVu tool.\n\n#### Two-Phase Runtime Verification\n\n`PyDejaVu` operates in two distinct phases:\n\n1. **Operational Runtime Verification (Phase 1):**\n - This phase is implemented in Python, allowing for any Pythonic operations on the events. \n You can perform arithmetic, string manipulations, and Boolean logic, and leverage \n Python's extensive data structures and objects for storing data and making complex calculations. \n This flexibility enables `PyDejaVu` to handle a wide range of operational tasks during runtime, \n offering users the ability to customize how events are processed and analyzed.\n\n2. **Declarative Monitoring (Phase 2):**\n - The second phase is declarative and leverages the DejaVu tool to perform monitoring against a first-order \n past time temporal logic specification. This phase ensures that the runtime behavior conforms to the formal properties \n defined in the specification. By integrating with DejaVu, `PyDejaVu` provides a robust framework for verifying \n that the system adheres to specified safety properties, making it suitable for applications requiring \n high levels of assurance.\n\n\n## PyDejaVu Installation\n\n`PyDejaVu` is a Unix-compatible tool designed for cross-platform use, initially developed on macOS \nand tested on both macOS and Ubuntu Linux distributions. \nWhile specifically tested on these two platforms, `PyDejaVu` may potentially work on other Unix-like \nsystems as well, though this would require further testing to confirm. \nIt's important to note that as a Unix-based tool, `PyDejaVu` is not natively compatible with \nWindows and may require additional setup and modifications, to run on Windows machines.\n\nHere we suggest three methods of installation:\n- [**Pip Installation**](#pip-installation): \nFor users who need to use `PyDejaVu` without making changes to the codebase, pip offers a quick \nand straightforward setup. \nThis method allows you to focus on using the tool rather than managing its dependencies.\n- [**Docker Installation**](#docker-installation): \nDocker provides a robust solution for running `PyDejaVu` in an isolated and consistent environment. \nThis method is ideal for users who prefer not to modify their local system or manage package \ninstallations manually.\nWith Docker, you don't need to prepare your system for running `PyDejaVu`, as the Docker image comes \npre-packaged with all the necessary Scala and Java dependencies required for `DejaVu`.\n- [**Source Code Installation**](#source-code-installation): \nInstalling the source code is a great option if you need more flexibility and control over the `PyDejaVu` project. \nHere are some reasons why you might choose this method:\n - **Customization and Modification:** If you plan to modify the code to suit specific requirements or contribute to the project, installing the source code gives you direct access to all the files. This is ideal for developers who want to extend or alter the functionality of `PyDejaVu`.\n - **Development and Debugging:** When working on new features or fixing bugs, having the source code installed locally allows you to test changes immediately. This setup is essential for contributors or developers actively working on the `PyDejaVu` project.\n - **Learning and Exploration:** If you're interested in understanding how `PyDejaVu` works internally, studying the source code can be very educational. You can explore the implementation details, experiment with changes, and see how different components interact.\n\n\n### Pip Installation\n\n\ud83d\udc49 Before proceeding, ensure your environment is properly configured according to the instructions \nin the [environment setup guide](docs/ENVIRONMENT_SETUP.md). This step is crucial for the \nsuccessful execution of `PyDejaVu` and helps prevent potential issues arising from an incorrectly \nset up environment.\n\n#### Step 1: Create Virtual Environment\nCreating a virtual environment is highly recommended when installing `PyDejaVu`. \nA virtual environment isolates your project's dependencies from the global Python installation, \npreventing package conflicts and making dependency management easier.\n\nCreate the Virtual Environment:\n```bash\npython3 -m venv pydejavu-env\n```\nThis command creates a new directory called pydejavu-env containing the isolated Python environment.\n\nActivate the Virtual Environment:\n```bash\nsource pydejavu-env/bin/activate\n```\nAfter activation, your command prompt will change to indicate that you are now using the virtual environment.\n\n\ud83d\udc49**Note**: Remember to activate the virtual environment each time you start a new session to \nensure you are using the isolated environment.\n\n#### Step 2: Install PyDejaVu\n\nWith the virtual environment activated, install the latest version of `PyDejaVu` from PyPI:\n```bash\npip install pydejavu-rv\n```\nThis command will download and install `PyDejaVu` along with all its dependencies into your virtual environment.\n\nTo upgrade an existing installation to the latest version:\n```bash\npip install --upgrade pydejavu-rv\n```\n\n#### Step 3: Verify the Installation\nAfter installation, verify that `PyDejaVu` has been installed correctly:\n```bash\npip show pydejavu-rv\n```\nThis command should display details about the `PyDejaVu` package, confirming a \nsuccessful installation within your virtual environment.\nYou should see output similar to:\n```bash\nName: PyDejaVu-RV\nVersion: x.y.z\nSummary: PyDejaVu is a Python implementation that wraps the original DejaVu jar file, providing a bridge between Python and the Java-based DejaVu runtime verification tool. This wrapper extends DejaVu's functionality by supporting a 2-phase monitoring approach.\nHome-page: https://github.com/moraneus/pydejavu\nAuthor: moraneus\nAuthor-email: moraneus@gmail.com\nLicense: Apache-2.0\nLocation: /path/to/your/python/site-packages\nRequires: psutil, pyjnius, pytest, pytest-forked, pytest-xdist\n```\n\n#### Step 4: Operate PyDejaVu\nTo test the library and explore the capabilities of `PyDejaVu`, \nyou can download the \n[experiments archive](https://raw.githubusercontent.com/moraneus/pydejavu/main/experiments/experiments.zip), \nwhich contains the experiments \nused in our paper. This archive includes three folders named `example_1`, `example_2` and `example_3`, \neach corresponding to a different experiment. Each example folder contains all the necessary \nfiles to run the experiment.\n\n- Extract the [experiments.zip](https://raw.githubusercontent.com/moraneus/pydejavu/main/experiments/experiments.zip) \n file:\n ```bash\n unzip experiments.zip\n ```\n- Change directory to the example folder you wish to run:\n ```bash\n cd example_X\n ```\n Replace `X` with the example number (1 to 3).\n\n- Execute the experiment using the provided bash script. **Make sure you are execute it from the virtual environment**.\n ```bash\n ./run_experiment\n ```\n In some cases, if `run_experiment` cannot be run, you need to make it executable using the following command:\n ```bash \n chmod +x run_experiment\n ```\n This script automates the execution of all experiments within the specified `example_X` folder. \n It sequentially runs the experiments using different log files to evaluate PyDejaVu's performance \n across varying trace sizes (10K, 100K, 500K, and 1M). Upon completion, the results will be saved \n in a file named `result-spec-X`.\n\n#### \ud83d\udee0\ufe0f Troubleshooting\nIf you encounter issues during installation or usage of `PyDejaVu`, consider the following:\n - **Python Environment**: Ensure your Python environment is correctly configured and you have \n the necessary permissions to install packages.\n - **Virtual Environment**: If using a virtual environment, activate it before running \n the pip install command:\n ```bash\n source path/to/your/venv/bin/activate\n ```\n - **Dependencies**: If you encounter dependency-related issues, try installing them separately\n ```bash\n pip install psutil pyjnius pytest pytest-forked pytest-xdist\n ```\n - **Version Conflicts**: In case of version conflicts, consider creating a new virtual environment \n for a clean installation.\n - **System Requirements**: Ensure your system meets the requirements for running Java-based \n applications, as `PyDejaVu` relies on a Java runtime.\n\n### Docker Installation\nThe Docker installation process automatically clones the latest `PyDejaVu` source code inside \nthe container. Unlike the standard installation method, it does not use the `pip install \npydejavu-rv` command. Instead, it builds and installs `PyDejaVu` directly from the cloned \nsource code within the Docker environment. \nThis approach ensures that you are running the most recent version of `PyDejaVu`,\nincluding the latest features and updates that may not yet be available through PyPI.\n\n\n#### Prerequisites\nEnsure Docker is installed. You can download \nDocker from [here](https://docs.docker.com/engine/install/).\n\n#### Step 1: Clone the Repository\n\nFirst, clone the repository to your local machine:\n\n```bash\ngit clone https://github.com/moraneus/pydejavu.git\ncd pydejavu\n```\n\n#### Step 2: Build the Docker Image\n\nEnsure the Docker service is running, then build the image:\n\n```bash\ndocker build -t pydejavu .\n```\nThis command creates a Docker image named \"pydejavu\" (based on a `Dockerfile` located in the root project folder)\nwith the following features:\n\n- Ubuntu based environment for running `PyDejaVu`.\n- Java and Scala installations.\n- Python with Poetry for dependency management.\n- `PyDejaVu` and its dependencies.\n- Linter and tests run to ensure proper configuration.\n\nYou should see output similar to:\n```bash\n[+] Building 412.7s (17/17) FINISHED \n => [internal] load build definition from Dockerfile 0.0s\n => => transferring dockerfile: 2.32kB 0.0s\n => [internal] load .dockerignore 0.0s\n => => transferring context: 2B 0.0s\n => [internal] load metadata for docker.io/library/python:3.12-slim 2.6s\n => [ 1/13] FROM docker.io/library/python:3.12-slim@sha256:XXXchecksumXXX 57.4s\n => => resolve docker.io/library/python:3.12-slim@sha256:XXXchecksumXXX 0.0s\n => => sha256:XXXchecksumXXX 9.12kB / 9.12kB 0.0s\n => => sha256:XXXchecksumXXX 1.75kB / 1.75kB 0.0s\n => => sha256:XXXchecksumXXX 5.11kB / 5.11kB 0.0s\n => => sha256:XXXchecksumXXX 29.16MB / 29.16MB 6.1s\n => => sha256:XXXchecksumXXX 3.33MB / 3.33MB 0.8s\n => => sha256:XXXchecksumXXX 13.38MB / 13.38MB 57.1s\n => => sha256:XXXchecksumXXX 250B / 250B 1.2s\n => => extracting sha256:XXXchecksumXXX 0.5s\n => => extracting sha256:XXXchecksumXXX 0.1s\n => => extracting sha256:XXXchecksumXXX 0.3s\n => => extracting sha256:XXXchecksumXXX 0.0s\n => [ 2/13] RUN apt-get update && apt-get install -y curl wget gnupg2 software-properties-common unzip zip && rm -rf /var/lib/apt/lists/* 21.8s\n => [ 3/13] RUN wget -O- https://packages.adoptium.net/artifactory/api/gpg/key/public | tee /usr/share/keyrings/adoptium.asc && echo \"deb [signed-by=/usr/share/keyrings/adoptium.asc] https:// 179.2s\n => [ 4/13] RUN curl -s \"https://get.sdkman.io\" | bash && bash -c \"source $HOME/.sdkman/bin/sdkman-init.sh && sdk install scala 2.12.18\" 14.6s \n => [ 5/13] RUN bash -c \"source $HOME/.sdkman/bin/sdkman-init.sh && scalac -version && java -version && python --version\" 0.6s \n => [ 6/13] RUN pip install --no-cache-dir \"poetry==1.6.1\" 18.4s \n => [ 7/13] RUN poetry config virtualenvs.create false 0.5s \n => [ 8/13] RUN pip install flake8 2.5s \n => [ 9/13] RUN git clone https://github.com/moraneus/pydejavu.git /app 20.1s \n => [10/13] WORKDIR /app 0.0s \n => [11/13] RUN poetry install --no-interaction --no-ansi 2.2s \n => [12/13] RUN bash -c \"source $HOME/.sdkman/bin/sdkman-init.sh && flake8 . --count --select=E9,F63,F7,F82 --show-source --statistics && flake8 . --count --exit-zero --max-complexity=10 --max-line 0.7s \n => [13/13] RUN bash -c \"source $HOME/.sdkman/bin/sdkman-init.sh && pytest --forked\" 90.6s \n => exporting to image 1.4s \n => => exporting layers 1.4s \n => => writing image sha256:XXXchecksumXXX 0.0s \n => => naming to docker.io/library/pydejavu \n```\n\n#### Step 3: Run the Docker Container\nStart an interactive session in the Docker container:\n```bash\ndocker run -it pydejavu\n```\nThis command starts an interactive session inside the Docker container, \nwhere `PyDejaVu` is set up and ready to use.\n\n#### Step 4: Operate PyDejaVu\nInside the Docker container, you can use `PyDejaVu` with no addition configuration. For example:\n\n##### Example: Running a Pre-defined Monitor\n```bash\ncd /app/examples/pydejavu_monitor\npython monitor_for_detecting_suspicious_login_patterns.py\n```\n\n##### Example: Using the CLI\n```bash\ncd /app/examples/cli\npython -m pydejavu --bits 20 --stats true --qtl sample.qtl --operational sample.pqtl --trace sample.log\n```\n\n##### Example: Experiments\nSince we are using the `PyDejaVu` source code inside the Docker container \nwe have direct access to the experiment folders.\n\n- Change directory to the experiment folder you wish to test:\n ```bash\n cd /app/experiments/example_X\n ```\n Replace `X` with the example number (1 to 3).\n\n- Execute the experiments using the provided bash script:\n ```bash\n bash -i run_experiment\n ```\nThis script automates the execution of all experiments within the specified `example_X` folder. \nIt sequentially runs the experiments using different log files to evaluate PyDejaVu's performance \nacross varying trace sizes (10K, 100K, 500K, and 1M). Upon completion, the results will be saved \nin a file named `result-spec-X`.\n\n#### \ud83d\udee0\ufe0f Troubleshooting\n\n- **Docker Service**: Ensure the Docker service is running before building or running containers.\n- **Persistent Storage**: To persist data between container runs and share files between your host\n machine and the Docker container, you can use Docker volumes. \n This is particularly useful when you have predefined `PyDejaVu` monitor files or other \n resources on your local machine that you want to use inside the container without \n copying or rewriting them:\n ```bash\n docker run -it -v /path/on/host:/path/in/container pydejavu\n ```\n- **Resource Allocation**: If `PyDejaVu` requires more resources, allocate them using Docker's resource flags:\n ```bash\n docker run -it --cpus 2 --memory 4g pydejavu\n ```\n- **Cached Images**: If the Docker build command completes unusually quickly (within a few seconds), \n it's likely using cached images from previous builds. In this case, you may need to \n remove the older Docker containers and images associated with your project \n (in this case, `pydejavu`) to force a fresh build. Here's how you can do this:\n 1. Stop and remove existing containers:\n ```bash\n docker stop $(docker ps -a -q --filter ancestor=pydejavu)\n docker rm $(docker ps -a -q --filter ancestor=pydejavu)\n ```\n 2. Remove associated images:\n ```bash\n docker rmi $(docker images | grep pydejavu | awk '{print $3}')\n ```\n 3. Rebuild your Docker image:\n ```bash\n docker build --no-cache -t pydejavu .\n ```\n This process ensures that your next build will create a fresh image \n without relying on potentially outdated cached layers.\n\n- **Debugging**: To debug issues, you can start a shell in the container:\n ```bash\n docker run -it pydejavu /bin/bash\n ```\n\n### Source Code Installation\n\n\ud83d\udc49 Before proceeding, ensure your environment is properly configured according to the instructions \nin the [environment setup guide](docs/ENVIRONMENT_SETUP.md). This step is crucial for the \nsuccessful execution of `PyDejaVu` and helps prevent potential issues arising from an incorrectly \nset up environment.\n\n#### Step 1: Clone the Repository\n\nFirst, clone the repository to your local machine:\n\n```bash\ngit clone https://github.com/moraneus/pydejavu.git\ncd pydejavu\n```\n\n#### Step 2: Install Poetry\nThis project uses [Poetry](https://python-poetry.org/) for managing dependencies and packaging. \nFollow these steps to set up your development environment:\n\n1. Create and activate a virtual environment:\n ```bash\n python3 -m venv pydejavu-env\n source pydejavu-env/bin/activate\n ```\n2. Install Poetry:\n ```bash\n pip install poetry\n ```\n3. Verify the installation:\n ```bash\n poetry --version\n ```\n If Poetry is correctly installed, you should see the version number.\n\n#### Step 3: Install Project Dependencies\nWith Poetry installed, you can now install the project dependencies.\nRun the following command in the root directory of the project:\n```bash\npoetry install\n```\nThis will create a `poetry.lock` file and install all necessary dependencies for the project.\n\n#### Step 4: Operate PyDejaVu\nAfter the installation is finished we can use `PyDejaVu` with no addition configuration.\n\n##### Example: Running a Pre-defined Monitor\n\ud83d\udc49**Note**: Make sure you are in the root directory of `PyDejaVu`.\n```bash\ncd examples/pydejavu_monitor\npython monitor_for_detecting_suspicious_login_patterns.py\n```\n\n##### Example: Using the CLI\n\ud83d\udc49**Note**: Make sure you are in the root directory of `PyDejaVu`.\n```bash\ncd /app/examples/cli\npython -m pydejavu --bits 20 --stats true --qtl sample.qtl --operational sample.pqtl --trace sample.log\n```\n\n##### Example: Experiments\nSince we are using the `PyDejaVu` source code we have direct access to the experiment folders.\n\n\ud83d\udc49**Note**: Make sure you are in the root directory of `PyDejaVu`.\n- Change directory to the experiment folder you wish to test:\n ```bash\n cd experiments/example_X\n ```\n Replace `X` with the example number (1 to 3).\n\n- Execute the experiments using the provided bash script:\n ```bash\n ./run_experiment\n ```\nThis script automates the execution of all experiments within the specified `example_X` folder. \nIt sequentially runs the experiments using different log files to evaluate PyDejaVu's performance \nacross varying trace sizes (10K, 100K, 500K, and 1M). Upon completion, the results will be saved \nin a file named `result-spec-X`.\n\n\n#### \ud83d\udee0\ufe0f Troubleshooting\nIf you encounter issues during installation or while running the project, consider the following:\n\n - Ensure that your Python version meets the minimum requirement.\n - Check that Poetry is correctly installed and accessible from your command line. \n - Verify that all dependencies are properly installed by running poetry show.\n\n## Usage\n\nIn this section, we present a simple usage of the tool divided into two \nexamples. The first example demonstrates how users can easily operate `DejaVu` directly \nfrom `PyDejaVu`. The second example builds upon the first, showing how to enhance the \nexpressiveness of your application by leveraging the power of `PyDejaVu`. \nBy leverages `DejaVu`'s capabilities, `PyDejaVu` involves a few steps before it starts \nthe evaluation process. First, it analyzes and parses the specification to ensure it \nmeets the syntax of QTL (Quantified Temporal Logic). \nThen, it compiles a Scala-based monitor. \nThis Scala compilation step may take some time, so don't be alarmed if there is a delay \nduring this process.\nFor more advanced usage and explanations, please refer to the [documentation](docs/ADVANCED_USAGE.md).\n\n\n### Example 1\nConsider a simple filesystem mechanism that handles several key events. The filesystem\nallows opening a file with the an `open(F, f, m, s)`, carrying as arguments the\nfolder name `F`, the filename `f` (technically a file id), the access mode `m` (read or write), and the size\n`s` which is the maximal number of bytes that can be written. The `close(f)` event\nindicates that a file `f` has been closed. The write event `write(f, d)` contains the\nfilename and the data `d` (a string) being written. Additionally, the system\nsupports `create(F)` and `delete(F)` events, which represent the creation or deletion\nof a folder.\nThe requirement we are verifying states that if data is written to a file, the\nfile must have been opened in write mode, not closed since, and must reside in\na folder that has been created and not deleted since.\n\n```python\nfrom pydejavu.core.monitor import Monitor\n\nspecification = \"\"\"\nprop example: forall f . forall d . \n write(f, d) ->\n (exists F . Exists s . \n ((!close(f) S open(F, f, \"w\", s)) & (!delete(F) S create(F))))\n\"\"\"\n\nmonitor = Monitor(specification)\n\nevents = [ \n {\"name\": \"create\", \"args\": [\"tmp\"]}, \n {\"name\": \"open\", \"args\": [\"tmp\", \"f1\", \"w\", \"5\"]},\n {\"name\": \"write\", \"args\": [\"f1\", \"some text\"]},\n {\"name\": \"close\", \"args\": [\"f1\"]},\n {\"name\": \"delete\", \"args\": [\"tmp\"]}\n]\n\nfor e in events:\n monitor.verify(e)\nmonitor.end()\n```\n\nThis code snippet demonstrates how to operate `DejaVu` directly \nfrom `PyDejaVu` to perform runtime verification based on a formal specification written in first-order \npast time temporal logic.\nFirst, the Monitor class is imported from `pydejavu.core.monitor`,\nand the specification, named as `example`, is defined as a multi-line string. \nThe monitor is then initialized with this specification, setting up the verification environment.\nA list of events is created to simulate a sequence of I/O operations: creating a folder (`create`), \nopening a file (`open`), writing to it (`write`), closing it (`close`), \nand finally deleting the hosting folder (`delete`). \nEach event is a dictionary containing the event name and its arguments.\nThe events are processed in a loop where each event is passed to the `monitor.verify(e)` method. \nIn this case, where no event handlers are defined, the events are forwarded directly to the declarative phase \nfor verification against the specification. \nAfter all events are processed, `monitor.end()` is called to finalize the evaluation.\nThis step is crucial for obtaining statistics results and for the monitor \nto release resources appropriately.\n\n#### Example 1 Output\nAs shown in the following output snippet, this example reports no errors.\n\n```bash\n0 errors detected!\n\n==================\n Event Counts:\n------------------\n create : 1\n open : 1\n delete : 1\n close : 1\n write : 1\n==================\n\n- Garbage collector was not activated\n```\n\n\n### Example 2\n\n```python\nfrom pydejavu.core.monitor import Monitor, event\n\nspecification = \"\"\"\nprop example: forall f . \n !write(f, \"false\") & (write(f, \"true\") ->\n (exists F . ((!close(f) S open(F, f, \"w\")) & (!delete(F) S create(F)))))\n\"\"\"\nmonitor = Monitor(specification)\ntotal_sizes: dict[str, int] = {}\n\n@event(\"open\")\ndef open(F: str, f: str, m: str, s: int):\n global total_sizes\n if m == \"w\":\n total_sizes[f] = s\n return [\"open\", F, f, m]\n\n@event(\"close\")\ndef close(f: str):\n global total_sizes\n del total_sizes[f]\n return [\"close\", f]\n\n@event(\"write\")\ndef write(f: str, d: str):\n global total_sizes\n if f not in total_sizes:\n total_sizes[f] = 0\n data_len = len(d)\n ok = total_sizes[f] >= data_len\n if ok:\n total_sizes[f] -= data_len\n return [\"write\", f, ok]\n\nevents = [ \n {\"name\": \"create\", \"args\": [\"tmp\"]}, \n {\"name\": \"open\", \"args\": [\"tmp\", \"f1\", \"w\", \"5\"]},\n {\"name\": \"write\", \"args\": [\"f1\", \"some text\"]},\n {\"name\": \"close\", \"args\": [\"f1\"]},\n {\"name\": \"delete\", \"args\": [\"tmp\"]}\n]\n\nfor e in events:\n monitor.verify(e)\nmonitor.end()\n```\n\nThis code differs from the previous example by incorporating operational event handlers that \nperform real-time computations and state management before events are passed to the \ndeclarative phase for verification. In the earlier code, events were directly forwarded to \nthe declarative phase without any operational processing. \nHere, the `@event` decorator is used to define custom handlers for the `open`, `close`,\nand `write` events, enabling the code to maintain and manipulate state during the operational \nphase. Generally, the handlers are decorated with the `@event(\"event_name\")` decorator, \nlinking them to specific events in your specification.\nThis definition is optional; if no handler is defined for a specific event, `PyDejaVu` will forward the \nevent directly to DejaVu for evaluation. Without any handler definitions, PyDejaVu functions \nthe same as `DejaVu` without the operational phase.\n\nA key difference is the introduction of the `total_sizes` dictionary, \nwhich tracks the remaining allowed write sizes for each file. \nIn the `open` handler, the code checks if the file is opened in write mode `\"w\"` and \ninitializes the total allowed size `s` for that file in the `total_sizes` dictionary. \nThe `write` handler then uses this information to ensure that the length of the data \nbeing written does not exceed the remaining allowed size. \nIt calculates the length of the data `d`, compares it against the remaining size for the file, \nand updates the `total_sizes` accordingly. \nIf the `write` operation exceeds the allowed size, an `ok` flag is set to `False`, \nindicating that the `write` is not permitted.\n\nThese operational event handlers allow for immediate enforcement of constraints and \npreliminary checks before events are evaluated against the formal specification in \nthe declarative phase. By performing these computations upfront, the code can prevent \ninvalid or undesirable events from proceeding further, enhancing efficiency and providing \nimmediate feedback. This integration of operational logic with declarative specifications \nshowcases how `PyDejaVu` increases the expressiveness of the system, enabling more complex \nand nuanced runtime verification scenarios compared to the previous example where such \noperational checks were absent.\n\n#### Example 2 Output\nAs shown in the following output snippet, this example reports one error because it failed when\nattempting to write the `\"some text\"` string into `f1`, which is limited to 5 characters.\n\n```bash\n1 errors detected!\n\n==================\n Event Counts:\n------------------\n create : 1\n open : 1\n delete : 1\n close : 1\n write : 1\n==================\n\n- Garbage collector was not activated\n```\n\n### More Usage Examples\nYou can find more comprehensive usage examples of monitors in the [examples](https://github.com/moraneus/pydejavu/tree/main/examples/pydejavu_monitor) folder \nand the [experiments](https://github.com/moraneus/pydejavu/tree/main/experiments) folder. These folders contain various use cases and demonstrations \nof how to effectively use `PyDejaVu` for runtime verification.\n\n\n## Output Files\nAfter each execution of `PyDejaVu`, several output files are generated and stored in designated folders. \nThese outputs are crucial for reviewing the results of the verification process and understanding the \ninternal workings of the tool.\n\n### Logs Folder:\n\nThe logs folder will contain the log file from the last execution. \nThis log file is named with a timestamp to ensure that each run's output is distinct and easy to identify.\n\n### Output Folder:\n\nThe `output` folder contains several important files generated during the verification process:\n- `ast.dot`: A Graphviz source file used to create an abstract syntax tree (AST) graph for the specification. \nThis file can be visualized using Graphviz to better understand the structure of the specification.\n- `TraceMonitor.jar`: If the specification was compiled into a Java archive, this file will contain the \ncompiled monitor.\n- `TraceMonitor.scala`: If the specification was synthesized into Scala code, this file will be generated. \nIt represents the synthesized monitor in Scala.\n- `resultFile`: This file is primarily used in unit testing to compare the expected errors with \nthe actual errors encountered. It contains the results of the original `DejaVu` execution, \ncapturing any errors from the verification process. When an error occurs, the event index is \nwritten to this file. However, be aware that the `resultFile` remains empty if no errors \nare detected during verification. To ensure the `resultFile` is created correctly, \nmake sure to run `monitor.end()` to notify `DejaVu` to close the result file and finalize \nthe execution.\n- `generated_trace.py` (Optional): This file is automatically generated when the user utilizes the CLI options. \nIn this case, a `PyDejaVu` script is created in the working directory, \ntailored to the user's input parameters for runtime verification.\n\nThese output files provide a comprehensive overview of each execution, allowing you to analyze and debug the \nbehavior of your specifications in detail.\n\n```bash\noutput/\n\u251c\u2500\u2500 ast.dot\n\u251c\u2500\u2500 TraceMonitor.jar\n\u251c\u2500\u2500 TraceMonitor.scala\n\u251c\u2500\u2500 resultFile\n\u2514\u2500\u2500 generated_trace.py (Optional)\n```\n\n## Contributors - For `PyDejaVu` (Ordered by last name):\n* [Klaus Havelund](http://www.havelund.com), Jet Propulsion Laboratory/NASA, USA\n* [Moran Omer](https://github.com/moraneus), Bar Ilan University, Israel\n* [Doron Peled](http://u.cs.biu.ac.il/~doronp), Bar Ilan University, Israel\n\n\n",
"bugtrack_url": null,
"license": "Apache-2.0",
"summary": "PyDejaVu is a Python implementation that wraps the original DejaVu jar file, providing a bridge between Python and the Java-based DejaVu runtime verification tool. This wrapper extends DejaVu's functionality by supporting a 2-phase monitoring approach.",
"version": "1.0.0",
"project_urls": {
"Bug Tracker": "https://github.com/moraneus/pydejavu/issues",
"Documentation": "https://github.com/moraneus/pydejavu/blob/main/README.md",
"Homepage": "https://github.com/moraneus/pydejavu",
"Repository": "https://github.com/moraneus/pydejavu"
},
"split_keywords": [
"runtime verification",
" dejavu",
" monitoring",
" java bridge"
],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "31d7b840ff1da84bf747a462a06bf6915a3b203f07b5ac9042fa9642ea0817a6",
"md5": "fddd2e83923e0f991687a5f0bfc03bed",
"sha256": "2f873337dee84413fe55dfa111d0e1ceeb827d9d57e193918018c26c7aae934e"
},
"downloads": -1,
"filename": "pydejavu_rv-1.0.0-py3-none-any.whl",
"has_sig": false,
"md5_digest": "fddd2e83923e0f991687a5f0bfc03bed",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": "<4.0,>=3.8",
"size": 11897104,
"upload_time": "2024-09-27T13:29:15",
"upload_time_iso_8601": "2024-09-27T13:29:15.255316Z",
"url": "https://files.pythonhosted.org/packages/31/d7/b840ff1da84bf747a462a06bf6915a3b203f07b5ac9042fa9642ea0817a6/pydejavu_rv-1.0.0-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "9ff04cad0dccdc37032b253a80845c536ae4a0fd091c583a31650bbb1091b3e9",
"md5": "768a354f30d8e0384a1a285f2660eb6f",
"sha256": "59d1afc413aa1b3611a6ed82115bb210abdf29047c0b5083e12330ab4efbbfec"
},
"downloads": -1,
"filename": "pydejavu_rv-1.0.0.tar.gz",
"has_sig": false,
"md5_digest": "768a354f30d8e0384a1a285f2660eb6f",
"packagetype": "sdist",
"python_version": "source",
"requires_python": "<4.0,>=3.8",
"size": 11899742,
"upload_time": "2024-09-27T13:29:32",
"upload_time_iso_8601": "2024-09-27T13:29:32.071249Z",
"url": "https://files.pythonhosted.org/packages/9f/f0/4cad0dccdc37032b253a80845c536ae4a0fd091c583a31650bbb1091b3e9/pydejavu_rv-1.0.0.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2024-09-27 13:29:32",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "moraneus",
"github_project": "pydejavu",
"travis_ci": false,
"coveralls": false,
"github_actions": true,
"lcname": "pydejavu-rv"
}
JSON
