|
1 | | -# Temporal Logic Parser |
| 1 | +> *This artifact extends the open-source tlparser tool [^tlparser] by adding capabilities for the automatic analysis of natural-language specifications and for supporting their quality evaluation. The codebase was obtained by cloning the upstream repository and augmenting it with these features.* |
2 | 2 |
|
3 | | -[](https://github.com/RomanBoegli/tlparser/releases) |
4 | | -[](https://github.com/RomanBoegli/tlparser/actions/workflows/test.yml) |
5 | | -[](https://github.com/RomanBoegli/tlparser/blob/main/LICENSE) |
6 | | -[](https://doi.org/10.5281/zenodo.14764479) |
| 3 | +- Direct link to Edge/IoT dataset: [Dataset.xlsx](./data/Edge_IoT/Dataset.xlsx) |
| 4 | + |
| 5 | +</br> |
| 6 | +</br> |
| 7 | + |
| 8 | +# Temporal Logic Parser (Extended) |
7 | 9 |
|
8 | 10 | The Temporal Logic Parser or `tlparser` takes something like this as input: |
9 | 11 |
|
@@ -199,115 +201,6 @@ source venv/bin/activate |
199 | 201 | # venv\Scripts\activate |
200 | 202 | ``` |
201 | 203 |
|
202 | | -## Extended Statistics |
203 | | - |
204 | | -For automaton-level insight, enable the optional Spot[^spot-citation] integration which will allow you to harvest extended statistics. |
205 | | -Spot is not bundled with `tlparser`, so install the CLI tools (`ltl2tgba`, `ltlfilt`, `autfilt`) beforehand. |
206 | | -You can find installation instructions on [Spot's webpage](https://spot.lre.epita.fr/). |
207 | | -Homebrew users can also install it using the `brew install spot` command. |
208 | | - |
209 | | -With Spot on your `PATH`, add `--extended` to the `digest` or `evaluate` command: |
210 | | - |
211 | | -```bash |
212 | | -tlparser digest ./data/spacewire.json --extended |
213 | | -``` |
214 | | - |
215 | | -Extended digests may also produce a companion `<filename>_errors.md` summarising formulas Spot could not analyse. |
216 | | -You can experiment interactively as well: |
217 | | - |
218 | | -```bash |
219 | | -tlparser evaluate "G (req --> F ack)" --extended |
220 | | -``` |
221 | | - |
222 | | -Sample output: |
223 | | - |
224 | | -```json |
225 | | -{ |
226 | | - "agg": { |
227 | | - "aps": 2, |
228 | | - "cops": 0, |
229 | | - "lops": 1, |
230 | | - "tops": 2 |
231 | | - }, |
232 | | - "ap": [ |
233 | | - "ack", |
234 | | - "req" |
235 | | - ], |
236 | | - "asth": 3, |
237 | | - "cops": { |
238 | | - "eq": 0, |
239 | | - "geq": 0, |
240 | | - "gt": 0, |
241 | | - "leq": 0, |
242 | | - "lt": 0, |
243 | | - "neq": 0 |
244 | | - }, |
245 | | - "entropy": { |
246 | | - "lops": 1.0, |
247 | | - "lops_tops": 1.584962500721156, |
248 | | - "tops": 0.0 |
249 | | - }, |
250 | | - "formula_parsable": "G (req --> F ack)", |
251 | | - "formula_parsed": "G((req --> F(ack)))", |
252 | | - "formula_raw": "G (req --> F ack)", |
253 | | - "lops": { |
254 | | - "and": 0, |
255 | | - "impl": 1, |
256 | | - "not": 0, |
257 | | - "or": 0 |
258 | | - }, |
259 | | - "req_len": null, |
260 | | - "req_sentence_count": null, |
261 | | - "req_word_count": null, |
262 | | - "tops": { |
263 | | - "A": 0, |
264 | | - "E": 0, |
265 | | - "F": 1, |
266 | | - "G": 1, |
267 | | - "R": 0, |
268 | | - "U": 0, |
269 | | - "X": 0 |
270 | | - }, |
271 | | - "z_extended": { |
272 | | - "buchi_analysis": { |
273 | | - "acceptance_sets": 1, |
274 | | - "analysis_source": "ltl2tgba_stats", |
275 | | - "is_complete": true, |
276 | | - "is_deterministic": true, |
277 | | - "is_stutter_invariant": true, |
278 | | - "state_count": 2, |
279 | | - "transition_count": 8 |
280 | | - }, |
281 | | - "deterministic_attempt": { |
282 | | - "automaton_analysis": { |
283 | | - "acceptance_sets": 1, |
284 | | - "analysis_source": "ltl2tgba_stats", |
285 | | - "is_complete": true, |
286 | | - "is_deterministic": true, |
287 | | - "is_stutter_invariant": true, |
288 | | - "state_count": 2, |
289 | | - "transition_count": 8 |
290 | | - }, |
291 | | - "success": true |
292 | | - }, |
293 | | - "formula": "G (req --> F ack)", |
294 | | - "is_stutter_invariant_formula": true, |
295 | | - "manna_pnueli_class": "recurrence reactivity", |
296 | | - "spot_formula": "G (req -> F ack)", |
297 | | - "syntactic_safety": false, |
298 | | - "tgba_analysis": { |
299 | | - "acceptance_sets": 1, |
300 | | - "analysis_source": "ltl2tgba_stats", |
301 | | - "is_complete": true, |
302 | | - "is_deterministic": true, |
303 | | - "is_stutter_invariant": true, |
304 | | - "state_count": 2, |
305 | | - "transition_count": 8 |
306 | | - } |
307 | | - } |
308 | | -} |
309 | | -``` |
310 | | - |
311 | 204 | </br> |
312 | 205 |
|
313 | | -[^spot-citation]: Alexandre Duret-Lutz et al., “[From Spot 2.0 to Spot 2.10: What’s new?](https://doi.org/10.1007/978-3-031-13188-2_9)”, Proc. CAV 2022, LNCS 13372, pp. 174–187, Haifa, Israel, Aug. 2022. |
| 206 | +> [^tlparser] Bögli, R., Rohani, A., Studer, T., Tsigkanos, C., & Kehrer, T. tlparser [Computer software]. <https://github.com/SEG-UNIBE/tlparser> |
0 commit comments