Last updated:
0 purchases
hplrv 1.2.0
HPL Runtime Verification
This project provides tools from which you can build and manage runtime monitors based on HPL properties.
Installation
Usage
GitHub Features
Tooling
Installation
Install this package with
pip install hpl-rv
Usage
Code Generation
This package provides a command line interface from which you can generate runtime monitors with a simple command.
# generating monitors from a specification file
hpl-rv gen -f my_spec.hpl
# generating monitors directly from properties
hpl-rv gen "globally: no /a"
# redirecting the output to a file
hpl-rv gen -o ./code.py "globally: some /b within 100ms"
When used as a library, you can generate Python code for a runtime monitor class with a few simple steps.
For example:
from hplrv.gen import lib_from_properties
hpl_properties = ['globally: no (/a or /b)']
code: str = lib_from_properties(hpl_properties)
print(code)
Monitoring Dashboard
This package also includes a web-based dashboard that enables live feedback from runtime monitors in a human-friendly format.
To execute the web server for this dashboard, run the gui command:
hpl-rv gui --host "127.0.0.1" --port 8080
Then, open the dashboard client with a web browser (e.g., on http://localhost:8080).
Through the dashboard, you can connect to runtime monitors to get live feedback.
To enable this feature, though, your runtime monitors should first start the feedback server.
For example, for code generated with lib_from_properties(), the main script where these monitors are included should follow roughly the following guidelines.
from threading import Thread
from .generated_monitors import HplMonitorManager
man = HplMonitorManager()
man.live_server.host = '127.0.0.1'
man.live_server.port = 4242
thread: Thread = man.live_server.start_thread()
now: float = 0.0
man.launch(now)
try:
# sleep or feed messages to the monitors; example:
while True:
sleep(1.0)
now += 1.0
man.on_timer(now)
except KeyboardInterrupt:
pass
man.shutdown(now)
thread.join(10.0)
The call to live_server.start_thread() is what enables the dashboard to get live feedback.
GitHub Features
The .github directory comes with a number of files to configure certain GitHub features.
Various Issue templates can be found under ISSUE_TEMPLATE.
A Pull Request template can be found at PULL_REQUEST_TEMPLATE.md.
Automatically mark issues as stale after a period of inactivity. The configuration file can be found at .stale.yml.
Keep package dependencies up to date with Dependabot. The configuration file can be found at dependabot.yml.
Keep Release Drafts automatically up to date with Pull Requests, using the Release Drafter GitHub Action. The configuration file can be found at release-drafter.yml and the workflow at workflows/release-drafter.yml.
Automatic package building and publishing when pushing a new version tag to main. The workflow can be found at workflows/publish-package.yml.
Tooling
This package sets up various tox environments for static checks, testing, building and publishing.
It is also configured with pre-commit hooks to perform static checks and automatic formatting.
If you do not use tox, you can build the package with build and install a development version with pip.
Assume cd into the repository's root.
To install the pre-commit hooks:
pre-commit install
To run type checking:
tox -e typecheck
To run linting tools:
tox -e lint
To run automatic formatting:
tox -e format
To run tests:
tox
To build the package:
tox -e build
To build the package (with build):
python -m build
To clean the previous build files:
tox -e clean
To test package publication (publish to Test PyPI):
tox -e publish
To publish the package to PyPI:
tox -e publish -- --repository pypi
To install an editable version:
pip install -e .
For personal and professional use. You cannot resell or redistribute these repositories in their original state.
There are no reviews.