ltlparse provides a language specification for defining temporal expressions which act on timed data, from either a simulation or a real-time system. During execution of either, ltlparse will verify the truthiness of the user-specified formulas.
Timed data is (currently) sourced from a set of user-specified comma-separated-value files, which are written to by external programs, and watched/read by ltlparse.
In the configuration file, each formula defined has an associated csv path, allowing for different formulas to work on data from different sources. Nonetheless, multiple formulas may take data from the same csv file.
The intended use-case of ltlparse is real-time evaluation of temporal formulas for error and safety-checking, especially for robotic systems.
This brings us to the following roadmap:
To maximize usability, the arithmetic syntax is an infix representation similar to that used C/C++. Here we define all of the operators included in the syntax, in order of increasing execution priority.
| Priority | Ops | Arity | Description |
|---|---|---|---|
| 1 | || | 2 | Logical OR |
| 2 | ^^ | 2 | Logical XOR |
| 3 | && | 2 | Logical AND |
| 4 | == | 2 | Equals |
| 4 | != | 2 | Not-equals |
| 5 | < | 2 | Less-than |
| 5 | <= | 2 | Less-than-or-equal |
| 5 | > | 2 | Greater-than |
| 5 | >= | 2 | Greater-than-or-equal |
| 6 | + | 2 | Add |
| 6 | - | 2 | Subtract |
| 7 | * | 2 | Multiply |
| 7 | / | 2 | Divide |
| 7 | % | 2 | Modulo (Remainder) |
| 8 | ^ | 2 | Power |
| 9 | ! | 1 | Logical NOT |
| 10 | N: | 1 | Next 1 |
| 10 | A: | 1 | Always 2 |
| 10 | E: | 1 | Eventually 3 |
| 10 | U: | 2 | Until 4 |
| 10 | R: | 2 | Release 5 |
_
| Unbounded LTL Operators | Description |
|---|---|
| N: (x) | x must have held in the previous time instance. |
| A: (x) | x must have held in all previous time instances, as well as the current instance. |
| E: (x) | x must hold in any of the previous time instances, or the current instance. |
| (x) U: (y) | x must have held at least until y became true, which must have held during any point, including now. |
| (x) R: (y) | y had to have held until and including the first instance where x held; if x never holds, y must always hold. |
FAQs
Verify ROS states using LTL expressions
The npm package ltlparse receives a total of 1 weekly downloads. As such, ltlparse popularity was classified as not popular.
We found that ltlparse demonstrated a not healthy version release cadence and project activity because the last version was released a year ago. It has 1 open source maintainer collaborating on the project.
Did you know?
Socket for GitHub automatically highlights issues in each pull request and monitors the health of all your open source dependencies. Discover the contents of your packages and block harmful activity before you install or update your dependencies.
Security News
Create React App is officially deprecated due to React 19 issues and lack of maintenance—developers should switch to Vite or other modern alternatives.
Security News
Oracle seeks to dismiss fraud claims in the JavaScript trademark dispute, delaying the case and avoiding questions about its right to the name.
Security News
The Linux Foundation is warning open source developers that compliance with global sanctions is mandatory, highlighting legal risks and restrictions on contributions.
