# HPL Runtime Verification
This project provides tools from which you can build and manage runtime monitors based on [HPL properties](https://github.com/git-afsantos/hpl-specs/).
- [Installation](#installation)
- [Usage](#usage)
- [GitHub Features](#github-features)
- [Tooling](#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.
```bash
# 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:
```python
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:
```bash
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.
```py
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](https://github.com/marketplace/actions/release-drafter). 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:
```bash
pre-commit install
```
To run type checking:
```bash
tox -e typecheck
```
To run linting tools:
```bash
tox -e lint
```
To run automatic formatting:
```bash
tox -e format
```
To run tests:
```bash
tox
```
To build the package:
```bash
tox -e build
```
To build the package (with `build`):
```bash
python -m build
```
To clean the previous build files:
```bash
tox -e clean
```
To test package publication (publish to *Test PyPI*):
```bash
tox -e publish
```
To publish the package to PyPI:
```bash
tox -e publish -- --repository pypi
```
To install an editable version:
```bash
pip install -e .
```
Raw data
{
"_id": null,
"home_page": "https://github.com/git-afsantos/hpl-rv",
"name": "hpl-rv",
"maintainer": "",
"docs_url": null,
"requires_python": ">=3.8, <4",
"maintainer_email": "",
"keywords": "runtime verification,runtime monitoring,code generation",
"author": "Andr\u00e9 Santos",
"author_email": "haros.framework@gmail.com",
"download_url": "https://files.pythonhosted.org/packages/19/4f/c97226223ad2b6e46147ccaeaba62e845a5a167137b727957cc7ea9f5d6b/hpl-rv-1.2.0.tar.gz",
"platform": null,
"description": "# HPL Runtime Verification\n\nThis project provides tools from which you can build and manage runtime monitors based on [HPL properties](https://github.com/git-afsantos/hpl-specs/).\n\n- [Installation](#installation)\n- [Usage](#usage)\n- [GitHub Features](#github-features)\n- [Tooling](#tooling)\n\n## Installation\n\nInstall this package with\n\n```\npip install hpl-rv\n```\n\n## Usage\n\n### Code Generation\n\nThis package provides a command line interface from which you can generate runtime monitors with a simple command.\n\n```bash\n# generating monitors from a specification file\nhpl-rv gen -f my_spec.hpl\n# generating monitors directly from properties\nhpl-rv gen \"globally: no /a\"\n# redirecting the output to a file\nhpl-rv gen -o ./code.py \"globally: some /b within 100ms\"\n```\n\nWhen used as a library, you can generate Python code for a runtime monitor class with a few simple steps.\nFor example:\n\n```python\nfrom hplrv.gen import lib_from_properties\nhpl_properties = ['globally: no (/a or /b)']\ncode: str = lib_from_properties(hpl_properties)\nprint(code)\n```\n\n### Monitoring Dashboard\n\nThis package also includes a web-based dashboard that enables live feedback from runtime monitors in a human-friendly format.\n\n\n\nTo execute the web server for this dashboard, run the `gui` command:\n\n```bash\nhpl-rv gui --host \"127.0.0.1\" --port 8080\n```\n\nThen, open the dashboard client with a web browser (e.g., on `http://localhost:8080`).\n\nThrough the dashboard, you can connect to runtime monitors to get live feedback.\nTo enable this feature, though, your runtime monitors should first start the feedback server.\n\nFor example, for code generated with `lib_from_properties()`, the main script where these monitors are included should follow roughly the following guidelines.\n\n```py\nfrom threading import Thread\nfrom .generated_monitors import HplMonitorManager\n\nman = HplMonitorManager()\nman.live_server.host = '127.0.0.1'\nman.live_server.port = 4242\nthread: Thread = man.live_server.start_thread()\nnow: float = 0.0\nman.launch(now)\ntry:\n # sleep or feed messages to the monitors; example:\n while True:\n sleep(1.0)\n now += 1.0\n man.on_timer(now)\nexcept KeyboardInterrupt:\n pass\nman.shutdown(now)\nthread.join(10.0)\n```\n\nThe call to `live_server.start_thread()` is what enables the dashboard to get live feedback.\n\n## GitHub Features\n\nThe `.github` directory comes with a number of files to configure certain GitHub features.\n\n- Various Issue templates can be found under `ISSUE_TEMPLATE`.\n- A Pull Request template can be found at `PULL_REQUEST_TEMPLATE.md`.\n- Automatically mark issues as stale after a period of inactivity. The configuration file can be found at `.stale.yml`.\n- Keep package dependencies up to date with Dependabot. The configuration file can be found at `dependabot.yml`.\n- Keep Release Drafts automatically up to date with Pull Requests, using the [Release Drafter GitHub Action](https://github.com/marketplace/actions/release-drafter). The configuration file can be found at `release-drafter.yml` and the workflow at `workflows/release-drafter.yml`.\n- Automatic package building and publishing when pushing a new version tag to `main`. The workflow can be found at `workflows/publish-package.yml`.\n\n## Tooling\n\nThis package sets up various `tox` environments for static checks, testing, building and publishing.\nIt is also configured with `pre-commit` hooks to perform static checks and automatic formatting.\n\nIf you do not use `tox`, you can build the package with `build` and install a development version with `pip`.\n\nAssume `cd` into the repository's root.\n\nTo install the `pre-commit` hooks:\n\n```bash\npre-commit install\n```\n\nTo run type checking:\n\n```bash\ntox -e typecheck\n```\n\nTo run linting tools:\n\n```bash\ntox -e lint\n```\n\nTo run automatic formatting:\n\n```bash\ntox -e format\n```\n\nTo run tests:\n\n```bash\ntox\n```\n\nTo build the package:\n\n```bash\ntox -e build\n```\n\nTo build the package (with `build`):\n\n```bash\npython -m build\n```\n\nTo clean the previous build files:\n\n```bash\ntox -e clean\n```\n\nTo test package publication (publish to *Test PyPI*):\n\n```bash\ntox -e publish\n```\n\nTo publish the package to PyPI:\n\n```bash\ntox -e publish -- --repository pypi\n```\n\nTo install an editable version:\n\n```bash\npip install -e .\n```\n",
"bugtrack_url": null,
"license": "MIT",
"summary": "Tools to enable Runtime Verification from HPL properties",
"version": "1.2.0",
"project_urls": {
"Homepage": "https://github.com/git-afsantos/hpl-rv",
"Source": "https://github.com/git-afsantos/hpl-rv/",
"Tracker": "https://github.com/git-afsantos/hpl-rv/issues"
},
"split_keywords": [
"runtime verification",
"runtime monitoring",
"code generation"
],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "ada982e800297937e1a04cf726e03f1918355a1074e1daf335fd089f10d13b8f",
"md5": "22888866c557d96d882d08f94d467a23",
"sha256": "eece5241972059660f0d7a7ffa6d17c1e63000bd294e8c0e73351c606ca53b4e"
},
"downloads": -1,
"filename": "hpl_rv-1.2.0-py3-none-any.whl",
"has_sig": false,
"md5_digest": "22888866c557d96d882d08f94d467a23",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.8, <4",
"size": 53933,
"upload_time": "2023-11-06T15:29:49",
"upload_time_iso_8601": "2023-11-06T15:29:49.379482Z",
"url": "https://files.pythonhosted.org/packages/ad/a9/82e800297937e1a04cf726e03f1918355a1074e1daf335fd089f10d13b8f/hpl_rv-1.2.0-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "194fc97226223ad2b6e46147ccaeaba62e845a5a167137b727957cc7ea9f5d6b",
"md5": "d543d7d69e5497fa794cee07604f9101",
"sha256": "1b243684d35d079fc2b61f9825d8e5e98159a2d6e5a0bef108c7e9a41c2d9754"
},
"downloads": -1,
"filename": "hpl-rv-1.2.0.tar.gz",
"has_sig": false,
"md5_digest": "d543d7d69e5497fa794cee07604f9101",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.8, <4",
"size": 217958,
"upload_time": "2023-11-06T15:29:52",
"upload_time_iso_8601": "2023-11-06T15:29:52.523131Z",
"url": "https://files.pythonhosted.org/packages/19/4f/c97226223ad2b6e46147ccaeaba62e845a5a167137b727957cc7ea9f5d6b/hpl-rv-1.2.0.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2023-11-06 15:29:52",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "git-afsantos",
"github_project": "hpl-rv",
"travis_ci": false,
"coveralls": false,
"github_actions": true,
"tox": true,
"lcname": "hpl-rv"
}
JSON
